Autosmart Project

Team:

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.

Early versions of the AutoSmart architecture are described in [1,2,3]. An account of the approach to correctness that we are following in this project is in [4].

Publications

  1. An Approach to the Generation of High-Assurance Java Card Applets Alessandro Coglio
    2nd NSA Conference on High Confidence Software and Systems, pages 69-77
    March 2002
    [PDF] [BibTeX]
    {Description of an early version of the AutoSmart architecture. A slight evolution of that architecture is described in [2,3].}

  2. Code Generation for High-Assurance Java Card Applets
    Alessandro Coglio
    3rd NSA Conference on High Confidence Software and Systems, pages 85-93
    April 2003
    [PDF] [BibTeX]
    {Description of an early version of the AutoSmart architecture. A slightly more detailed description is in [3]. A slightly earlier version of the architecture is described in [1].}

  3. Toward Automatic Generation of Provably Correct Java Card Applets
    Alessandro Coglio
    5th ECOOP Workshop on Formal Techniques for Java-like Programs
    July 2003
    [PDF] [BibTeX]
    {Description of an early version of the AutoSmart architecture. A slightly less detailed description is in [2]. A slightly earlier version of the architecture is described in [1]. This paper also appears in 4th NSA Conference on High Confidence Software and Systems, April 2004.}

  4. A Constructive Approach To Correctness, Exemplified by a Generator for Certified Java Card Applets
    Alessandro Coglio and Cordell Green
    IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE), number 4171 in Lecture Notes in Computer Science (LNCS), pages 57-63, Springer
    October 2005
    [PDF] [BibTeX]
    {Description of the approach to the generation of correct software that we are following in this project.}