Kestrel developed, in Specware,
a complete formal specification of an embedded
smart card operating system: the Java Card Runtime Environment (JCRE).
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
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.