Requirements on the Use of Coq in the Context of Common Criteria Evaluations
- Others:
- Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
- Agence nationale de la sécurité des systèmes d'information (ANSSI)
- Proof techniques for security protocols (PESTO) ; Inria Nancy - Grand Est ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM) ; Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Description
Coq is a formal system which provides both a pure, functional programminglanguage with dependent types, and an environment to write machine-checkedproofs.Using Coq, it is possible to model a system, to formalize properties this systemis expected to satisfy, and to prove the correctness of the model with respectto these properties.Coq has already been leveraged for Common Criteria evaluations with formaldevelopments in the context of the French scheme.The present document assumes readers are already familiar with Coq, andintroducesrequirements to write formal developments suitable to take part in CCevaluations.Evaluators are expected to assert that the developers' requirements have beensatisfied during the evaluation process.In addition, this document also introduces requirements specifically forevaluators.
Abstract
Rapport public communiqué par l'ANSSI, émanant de l'ANSSI et d'Inria.
Additional details
- URL
- https://inria.hal.science/hal-04452421
- URN
- urn:oai:HAL:hal-04452421v1
- Origin repository
- UNICA