The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.