The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Sorry to hijack this thread a little. Since you are mentioning your
very nice paper on OpenSLL, could you comment a bit more on the "HMAC
brawl". As you indicate in sec 3 there is some discussion about
precisely what the security model is, and hence what has been
verified.

Thanks,

Bas

On Mon, 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.