AutoSmart Project


Kestrel has built AutoSmart (= automatic generator of smart card applets), an automatic generator of Java Card applets from higher-level specifications written in SmartSlang (= smart card specification language), a domain-specific language for smart card applications. SmartSlang features high-level constructs that capture smart card concepts in a clear and concise way. Besides generating Java Card code, AutoSmart also performs various analyses on the SmartSlang specification, including an information flow analysis that points out potential security problems in the specification (such as leaking information about a secret or private key). Furthermore, AutoSmart automatically generates a human-readable English report in the format needed for FIPS 140-2 certification.

Kestrel has also started extending AutoSmart to produce a machine-checkable proof of the correctness of the output Java Card code with respect to the input SmartSlang specification. The proof and the input specification can be viewed as a certificate accompanying the output code.