Stream: Miscellaneous

Topic: CC EAL7

Bas Spitters (May 29 2020 at 15:41):

@Maxime Dénès You had an interesting lecture on Common Criteria at CPP. Have there been any followup on these plans?

Thomas Letan (Sep 23 2020 at 14:18):

you may be interested in https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.0-en.pdf which is the document _finally_ published (:

Bas Spitters (Sep 23 2020 at 14:35):

@Thomas Letan
Is the distinction between EAL7 and EAL7+ important here?
I understand that there is a common recognition of these standards between some European countries. Can you say more about this?
The requirement on third party libraries is interesting. I imagine, it would be beneficial for Coq if a larger collection of libraries would be accepted. Could one imagine such a thing being done be the community as part of the ongoing refereeing process? E.g. CPP/POPL artifact evaluation would also give a quality stamp???

Bas Spitters (Sep 23 2020 at 14:36):

Is Coq the only proof assistant for which such an ANSSI document exists?

Gaëtan Gilbert (Sep 23 2020 at 14:37):

Developers shall take care to carefully organize their proof scripts
to make them readable and reviewable. In particular, they shall use goal markers (e.g., +,
−, or *).

do they know about Set Default Goal Selector "!".?

Thomas Letan (Sep 23 2020 at 14:40):

Not really, the document addresses the use of Coq in the French scheme, as soon as it is being used, so with ADV_SPM and a formal FSP (in terms of EAL, it means >6). As for the recognition agreements, it’s a mess tbh. I am aware of two RA: CCRAv2 which limits the recognition to EAL2 most of the time, and the SOGIS (European) (agreements) which implies recognition up to EAL7 in certain situations. That being said, this document only applies to the French Scheme, which means you can imagine having a product which does not satisfy this document, but is certified in Netherland or Germany for instance

Thomas Letan (Sep 23 2020 at 14:41):

@Gaëtan Gilbert I was not aware of this command, no, thanks for sharing

Thomas Letan (Sep 23 2020 at 14:42):

@Bas Spitters For your last point, this is tricky, the evaluation lab will ultimately have to look at third party library, but we can indeed imagine having taken part of a refeering process in a prominent academic conference could act as a good reason to trust said library

Thomas Letan (Sep 23 2020 at 14:43):

this is something that we could eventually consider

Bas Spitters (Sep 23 2020 at 14:55):

The document contains a number of useful guidelines, I guess this could be part of inclusion into, say, the coq-platform? Or some subset thereof.

Enrico Tassi (Sep 23 2020 at 15:00):

@Pierre-Marie Pédrot tac in terms made it in the spec (see last page).

Pierre-Marie Pédrot (Sep 23 2020 at 15:14):

my whole life won't be enough to redeem me for the one time I introduced tactic-in-terms...

Enrico Tassi (Sep 23 2020 at 15:35):

I think you mean "ltac1-in-terms" ;-)

Maxime Dénès (Oct 01 2020 at 13:26):

@Bas Spitters Sorry, it's only now that I see our original message!

Maxime Dénès (Oct 01 2020 at 13:27):

Thanks @Thomas Letan for answering :)

Last updated: Dec 05 2023 at 06:01 UTC