The Coq mailing list

[Claude Marché <Claude.Marche AT inria.fr>]

Let me add my 2 cents:

* I completely agree that the specification language needs advanced
mathematics features for expressive power. This is why when I
participated to the design of ACSL, I insisted on having unbounded
mathematical integers, and real numbers in the base logic, and having
the opportunity to import existing theories e.g. from Coq. For example,
this how we proceed to prove complex functional properties of
floating-point programs. Here are a few links if one is interested :
http://hal.inria.fr/hal-00649240/en/
http://hal.inria.fr/hal-00777605/en/
http://hal.inria.fr/hal-00967124/en/

* The point on having a certified tool chain from annotated C code to
proof obligations was precisely the subject of Herms' thesis. Let me
give the link again:
http://tel.archives-ouvertes.fr/tel-00789543

- Claude


Le 04/01/2016 17:07, Andrew Appel a écrit :
> I agree with Adam's point about soundness, but I think AT LEAST as important
> is the specification language.  VST gives the full power of Coq to
> specify the
> partial-correctness properties of your program.    That is, the program
> logic
> is higher-order separation logic, embedded within Coq; it allows proving
> the relation of your C program to full functional or relational specs in
> CiC.
> This is important when the reasoning in your application domain involves 
> mathematics for which you want the expressive power of a general-purpose
> higher-order logic.  An example of that is shown here:
> 
> Verified Correctness and Security of OpenSSL HMAC
> <http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf>,
> by Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel.
> In /24th USENIX Security Symposium,/August 2015.
> 
> The C-to-Gallina proof is done in VST (Verifiable C), and the
> Gallina-to-mathematical-crypto-properties
> is done in Adam Petcher's Foundational Cryptography Framework; since
> both VST and FCF are
> embedded in Coq, there are no specification gaps between them.
> 
> -- Andrew Appel
> ------------------------------------------------------------------------
> 
>     *From: *"Adam Chlipala" 
> <adamc AT csail.mit.edu>
>     *To: 
> *coq-club AT inria.fr
>     *Sent: *Monday, January 4, 2016 10:29:13 AM
>     *Subject: *Re: [Coq-Club] VST release 1.6
> 
>     On 01/04/2016 10:21 AM, Chan Ngo wrote:
>     >> On Jan 4, 2016, at 4:03 PM, Adam Chlipala 
> <adamc AT csail.mit.edu>
>     wrote:
>     >>
>     >> On 01/04/2016 04:23 AM, Chan Ngo wrote:
>     >>>> On Jan 4, 2016, at 9:55 AM, Claude Marché
>     
> <Claude.Marche AT inria.fr>
>  wrote:
>     >>>>
>     >>>> So, in short:
>     >>>>
>     >>>> VST: specification language = Coq, back-end prover = Coq
>     >>>> Frama-C/Why3: specification language = ACSL, back-end provers =
>     SMT solvers
>     >>>>
>     >>>> VST provides a much higher level of trust than the latter,
>     thanks to the
>     >>>> use of CompCert. There was an attempt to design a Frama-C deductive
>     >>>> verification plugin of Frama-C through CompCert (PhD thesis of
>     Paolo
>     >>>> Hemrs, https://tel.archives-ouvertes.fr/tel-00789543) but it
>     did not
>     >>>> make its way to a robust, distributed plug-in.
>     >>>>
>     >>> I think that if we can certify the automated provers used in
>     that tools, we can obtain the same formal level of trust as
>     providing by VST. It is the same as some additional parts of the
>     CompCert compiler which use translation validation approach (produce
>     a validator), meaning that if we certify the validator formally then
>     the result validated compiler is the same level of trust as the
>     formal verified compiler.
>     >> I'm afraid that description is rather far from accurate, if by
>     "automated provers" you mean "SMT solvers."  Frama-C has much
>     trusted code having to do with the C language and associated
>     verification methodologies.  All of that code would need to be
>     certified/certifying, too, not just the SMT solvers.  Compared to
>     proof witnesses from SMT solvers, which are relatively
>     well-understood today, it's not as obvious how to use
>     proof-generating translations to handle the semantics of C or the
>     application of a verification methodology.
>     > Yes, thanks for reminding that. Somehow I assumed that the
>     correctness of the tool’s development (i.e., Frama-C). Since I want
>     to emphasize the use of external libs. Consider a deductive
>     verification proof from VST and the proof from tools like Why3,
>     Frama-C for a same specification, how we can say that these two
>     proofs are the same level of trust? I would like to say if the can
>     prove the correctness of the later tools development (including the
>     tool itself and the external libs), we can guarantee the same level
>     of trust, please correct me if it is not so (As the example of the
>     validator in complier validation does so according  the claims in
>     some work of Leroy in CompCert project)..
> 
>     Well, there are some subtleties.  The approximate answer is that, yes,
>     with proofs of correctness for all the Frama-C tools, you would reach
>     the same level of trust as VST.  However, it would be important that
>     all
>     the proofs are implemented in Coq, in a way that allows them to be
>     linked together within Coq in the usual way.
> 
>     It would be a huge job to make Frama-C and its deductive plugin
>     certified or certifying.  Quite likely it would require implementation
>     changes to both.  That is, I'd be willing to bet money that both
>     Frama-C
>     and its deductive plugin have significant soundness bugs today, just
>     because it's hard to be bug-free without formal certification.
> 

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |