JCRE Project

Team:

• Alessandro Coglio (PI)
• Stephen Fitzpatrick
• Limei Gilham
• Cordell Green
• Christoph Kreitz
• James McDonald
• Douglas Smith
• Stephen Westfold

Kestrel developed, in Specware, a complete formal specification of an embedded smart card operating system: the Java Card Runtime Environment (JCRE). The formal specification includes the Java Card Virtual Machine (which executes bytecodes), the Java Card API library (which includes cryptographic algorithms, transaction management, and other features), and the related GlobalPlatform standard (which includes card and application lifecycle management, as well as several security protocols). Kestrel discharged thousands of consistency proofs of the formal specification, using Specware’s connection to the Isabelle/HOL theorem prover.

Based on the formal specification, Kestrel developed a high-assurance simulator of the JCRE using Specware, to act as a reference implementation. Kestrel also developed, in C, a PC desktop simulator, and an implementation for a commercial USB token. The C implementations have passed thousands of tests, including many from the NIST cryptographic verification program. The specification, simulator, and C implementations are being used and evaluated by the DoD. Kestrel plans to re-develop the C implementations via provably correct refinements from the formal specification.

Kestrel has also formally specified MILS (= Multiple Independent Levels of Security) and MLS (Multi-Level Security) information flow policies for a simplified version of the JCRE, formally specified run-time monitors to enforce those policies, and formally proved that the monitors correctly enforce the policies. The specified run-time monitors have been refined to code using Specware. Kestrel plans to extend this work to the full JCRE.