[isabelle] Isabelle Foundation & Certification



Dear all, 

with respect to the debate around the paper by OndÅej KunÄar and Andrei Popescu: A Consistent Foundation for Isabelle/HOL (ITP 2015) 
and the debate it created, I have the following remarks and informations to add:

1) To be not misunderstood: I find this publication helpful and, after the quite nonchalant 
    reactions of key members of the Isabelle Community, strictly speaking necessary.

2) This paper creates outside the Isabelle community more echo than people might think.
    At the moment, I am as part of the EUROMILS project part of the team that attempts
    to get a common criteria (CC EAL5) evaluation for PikeOS through, where the models
    and proofs were done with Isabelle. I can tell that I had a lengthy debate with
    Evaluators and (indirectly) BSI representatives which became aware about this paper.

    And of course, there is the effect of a children's telephone game which distorts the 
    story hopelessly.

3) As part of the project, we wrote early a Recommandations-Whitepaper explaining the importance
    of conservative extensions and trying to define something like a âsafe subsetâ of Isabelle. 
    It is called:

        "Using Isabelle/HOL in Certification Processes: A System Description and Mandatory Recommendations" 

    and is part one of the EUROMILS Deliverable http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf <http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf>,
   (pp. 1 .. 39)
    a paper that is submitted to the ANSI and the BSI as part of the Common Criteria Evaluation of the PikeOS operating system.
    It may be that these Mandatory recommendations were reused in future projects of this kind.

    In this paper, we ruled out the critical consts - defs combination as unsafe, and made sure that we did not use these constructs in
    our entire theories (as well as axioms, etc. Restraining strictly to conservative extension and avoiding obfuscation).

4) I welcome to see more formally proved meta-theory of Isabelleâs specification constructs; the HOL4 community shows at the
    moment impressive progresses in this direction. May be that other open issues could be addressed as well. 


Best regards,

Burkhart


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.