Fully Verified JAVA CARD API Reference Implementation

This paper presents a formally verified reference implementation of the JAVA CARD API. This case study has been developed with the KeY verification system. The KeY system allows them to symbolically execute the JAVA source code of the API in the KeY verification environment and, in turn, prove correctness of the implementation w.r.t. formal specification the authors developed along the way. The resulting formal API framework (The Implementation and The Specification) can be used to prove correctness of any JAVA CARD applet code. As a side effect, this case study also serves as a benchmark for the KeY system. It shows that a code base of such size can be feasibly verified, and that KeY indeed covers all of the JAVA CARD language specification.