@Maxime Dénès You had an interesting lecture on Common Criteria at CPP. Have there been any followup on these plans?
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 (:
@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???
Is Coq the only proof assistant for which such an ANSSI document exists?
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 "!".
?
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
@Gaëtan Gilbert I was not aware of this command, no, thanks for sharing
@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
this is something that we could eventually consider
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.
@Pierre-Marie Pédrot tac in terms made it in the spec (see last page).
my whole life won't be enough to redeem me for the one time I introduced tactic-in-terms...
I think you mean "ltac1-in-terms" ;-)
@Bas Spitters Sorry, it's only now that I see our original message!
Thanks @Thomas Letan for answering :)
Last updated: Jun 10 2023 at 06:31 UTC