The Coq mailing list

[Chan Ngo <chan.ngo2203 AT gmail.com>]

Thanks Adam and Andrew for the information.

—

Chan

On Jan 4, 2016, at 5:07 PM, Andrew Appel <appel AT CS.Princeton.EDU> wrote:

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,

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.