This talk presents the key points of a complete formalization of a
Java Card platform using the Coq proof assistant. The work was
developed by Trusted Logic SA for SchlumbergerSema in the framework
of the FORMAVIE project. The formalization covers a formal security
policy model, and the functional specification and high level design
of an off-card bytecode verifier, a package transmission protocol, a
linker and an embedded interpreter. As far as we know, it is the
completest model of Java Card that presently exists. It covers all the
structures contained in the cap format, a collection of well-formed
conditions on such structure, all Java Card bytecodes, the basic API,
native method invocation, etc. After a brief description of the model,
a proof of the security architecture of a Java Card platform is
introduced. This proof, also carried out in Coq, simplifies the proof
of applet isolation properties based on the Java Card firewall. The
talk is closed by some statistics about the Coq models and an
evaluation of Coq.