Email Gateway (Aug 18 2022 at 10:50): Email Gateway (Aug 18 2022 at 10:50):From: NGUYEN Quang-Huy <quang-huy.nguyen@gemalto.com>
Dear colleagues,
We are proud to announce that we have just successfully completed a
Common Criteria (CC) evaluation on a Java Card based commercial product.
This evaluation will lead to the world's first CC certificate of a Java
product involving EAL7 components.
The specific feature of the evaluation is that all the CC requirements
on the development of the product (the ADV class) have been fulfilled at
their highest level thanks to the use of a formal tool (the Coq proof
assistant). In other words, for the ADV class, we have obtained the
highest assurance level (EAL7).
This evaluation has been done following the French scheme (DCSSI) while
taking into account the new requirements on the use of Formal Methods,
in particular, the application notes AIS34 and AIS39 (*) issued by the
BSI(**).
From a more technical point of view, the formal models and proofs
developed in this work ensure the safe execution of any
bytecode-verified applet on the product.
We will warmly welcome all your questions and/or remarks on this work.
===============================
Formal Methods group
Gemalto Technology & Innovation
(*) AIS34: Evaluation Methodology for CC Assurance Classes for EAL5+
AIS39: Guideline for the Development and Evaluation of formal
security
policy models in the scope of ITSEC and Common Criteria
(**) The Certification Body of the German Federal Office for Information
Security
Last updated: May 03 2024 at 08:18 UTC