Certifying An Embedded Remote Method Invocation Protocol

This paper describes an approach to formally prove that an implementation of the Java Card Remote Method Invocation protocol on smart cards fulfills its functional and security specification. For that, we refine the specification in two intermediate formal models: the functional specification and the high level design. These two models are both defined upon an existing complete formal model of the Java Card virtual machine, allowing to formalize all the security requirements. We focus on certifying the Java code portion since the native portion has been handled in a previous work. The correctness is showed to be preserved while composing the native and Java codes. Our refinement scheme has been designed to fulfill the requirements of a high-level Common Criteria security evaluation.