Inria teams up with the ANSSI on the Coq software program

Certification plays a pivotal role in the digital products and services sector. By guaranteeing a certain level of protection and security for users, in addition to meeting regulatory and contractual obligations, certification gives the suppliers of goods and services who opt for it a competitive advantage.

The capacity of a given product or service to withstand an attack, of any nature, is tested by an evaluation based on the analysis of its compliance and its vulnerability.

In France, there are currently two types of certification: first-level security certification (CSPN), in which a product's capacity to withstand attacks of moderate severity can be evaluated in quite a short period of time, and Common Criteria certification (CC), an internationally-recognised standard in which product security is rated on a scale of seven levels. The higher the desired security level, the more stringent the requirements for proof and the more thorough the evaluation.

However, the certification sector has run into a stumbling block: the lack of standardisation across evaluation schemes worldwide. Multiple security certification systems are currently in operation which, although they follow an international standard, vary from one country to another.

The ANSSI, France’s National Cybersecurity Agency, set about finding a solution to this problem. As one of the world’s leading issuers of CC certifications, the ANSSI decided to join forces with Inria to draft a document outlining guidelines and rules to be followed for formal analyses with Coq.

Objectives: to present Coq as a benchmark-setting formal method tool and to raise awareness of the requirements for using other tools. In a wider sense, the aim was also to bring French interpretations to the attention of international certification specialists, who may then decide to adopt the same approach.

“The Common Criteria dictate that, from a certain security level upwards, the security of the functional specification of the product being evaluated must be formally proved. In practice, this raises the question of what it means ‘to be formally proved’ and what tools and methods can be used to establish such proof. Developers are free to choose whichever tools suit them, but it is up to evaluators to assess whether or not the ‘quality’ of the solution used is’sufficient’”, explains Thomas Letan, an expert in formal methods for security use at the ANSSI Software Security Laboratory.

As Coq was deemed to be suitable for Common Criteria evaluations, a working document was drafted for the solution, which should help to ensure that developers use the program in the right way. “For Common Criteria, the use of formal methods is recommended for higher certification levels. The goal for this partnership was to prevent users from developing a false sense of security by using Coq incorrectly”, explains Yves Bertot, Senior Researcher at Inria.

France is at the cutting edge of certification activities, and intends to stay there. By providing reliable tools for certification and producing guidelines to ensure that they are properly used, this partnership between the ANSSI and Inria is consistent with this aim. But it goes further.

This partnership has also enabled the ANSSI to obtain quick and insightful feedback from Inria teams on the rules that it advocates: “We made changes to some of our requirements based on feedback we received from Yves Bertot, Maxime Dénès and Vincent Laporte”, explains Thomas Letan.

Meanwhile, the Inria researchers who were involved in this project were able to shed further light on the challenges for Coq concerning security evaluations, in addition to boosting their visibility: “Our goal is to ensure that research results are exploited by industry, and to improve the adoption and use of Coq. The fact that the ANSSI recognises Coq’s relevance to Common Criteria applications and publishes dedicated instructions will help us to achieve this aim”, explains Yves Bertot

This project is part of a partnership launched several years ago between the ANSSI and Inria, with the goal of consolidating the sharing of expertise in order to further research and innovation.