Certifying native Java']Java Card API by formal refinement

This paper describes a refinement-based approach to show that a native Java Card API function fulfills its specification. We refine a native function from its informal specification (by Sun) through several intermediate models into a low-level model which is very close to its C implementations. We formally prove the correctness of the refinement steps between two adjacent levels. The low-level model is sufficiently detailed such that its correspondence to the C implementation can be informally checked. This work provides a framework to enforce the security of the native code by formal analysis and can be generalized to verify a complete implementation of the Java Card platform.