[Kestrel circling]

Home : Current Projects : High-Assurance Java Card Applets
 

Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel

High-Assurance Java Card Applets

Contributors

Current

Past

  • Matthias Anlauff
  • David Cyrluk
  • Jim McDonald
  • Weilyn Pa
  • Yun-Mei Wei
  • Stephen Westfold

Background

Java Card is a version of Java for smart cards. A Java Card applet is a program written in Java Card. A single smart card can contain multiple applets.

Motivation

Smart cards are usually deployed in security-critical domains (e.g. authentication, banking). So, correctness has paramount importance in smart card applications.

Even though Java is relatively high-level, developing Java Card applets requires the programmer to deal with fairly low-level details. This greatly increases the potential for bugs.

Objectives

Our goal is to build tools to synthesize Java Card applets from higher-level specifications, in a way that the generated code is provably correct with respect to the specification. This enables the applet developer to operate in more abstract terms, thus greatly reducing the potential for introducing bugs in the first place. Furthermore, higher-level specifications can be automatically analyzed more effectively than lower-level code, so that problems in the specifications can be identified and corrected, thus contributing to the validation of the specifications.

Results

We have 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.

The current version of SmartSlang can already describe a large class of real-world applets in a fairly high-level way. We are actively extending SmartSlang towards covering all the Java Card 2.2.2 functionality and towards enabling even higher-level descriptions of applet functionality.

We are also 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.

We are developing an applet checker to verify the correctness of a generated applet independently from AutoSmart. The checker takes as inputs a SmartSlang specification, a Java Card program, and a proof (as produced by AutoSmart). The checker checks, by means of a proof checker, that the proof is a valid proof of the correctness of the program with respect to the specification, yielding a yes/no answer. In other words, the applet checker checks the validity of the certificate that accompanies the applet code.

Early versions of the AutoSmart and applet checker architecture and of the code generator back end are described in [1,2,3]. An account of the approach to correctness that we are following in this project is in [4]. More publications will appear shortly.

AutoSmart is being developed on top of Kestrel's Specware.

A Related Project

While the project described in this page aims at high assurance for the applets that run on top of the Java Card Runtime Environment, the project described in this other page aims at high assurance for the Java Card Runtime Environment itself. Together, the two projects aim at high assurance for the whole smart card software.

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
    [PS] [PDF] [BibTeX]
    {Description of an early version of the AutoSmart and applet checker architecture. A slight evolution of that architecture is described in [2,1].}

  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
    [PS] [PDF] [BibTeX]
    {Description of an early version of the AutoSmart and applet checker architecture and of the code generation back end. 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
    [PS] [PDF] [BibTeX]
    {Description of an early version of the AutoSmart and applet checker architecture and of the code generation back end. 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
    October 2005
    [PS] [PDF] [BibTeX]
    {Description of the approach to the generation of correct software that we are following in this project.}

 

 

- Back to Top -


- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -