[SystemSafety] Claims for formal methods

[David MENTRE]

Hello Mr. Jones,

Le 19/02/2014 11:59, Derek M Jones a écrit :
>> Please provide some examples (preferably from peer-reviewed
>> journals) of the "excessive claims" that you are criticising.
>
> There are the articles discussed in links I posted to the original
> thread:
> http://shape-of-code.coding-guidelines.com/2013/03/10/verified-compilers-and-soap-powder-advertising/
>
>
> http://shape-of-code.coding-guidelines.com/2012/05/23/would-you-buy-second-hand-software-from-a-formal-methods-researcher/
>
>
>
> The French group in the above links did some interesting work on
> compiler code generation and I believe they now refer to it as a
> verified compiler backend (which is what it idoes) rather than a
> verified C compiler.

They are doing more than just a C backend and they are progressing
slowly but surely towards parsing the C grammar. For example, you can
have a look at this work:
   http://gallium.inria.fr/blog/verifying-a-parser-for-a-c-compiler/
   http://gallium.inria.fr/blog/verifying-a-parser-for-a-c-compiler-2/

Above work is dated end of 2012. I don't know if it has been integrated
within currently released ComptCert (http://compcert.inria.fr/) or not.

Regarding the points you raised:
> 1.    C source code is not verified directly, it is first translated
> to the formal notations used by the verification system; the software
> that performs this translation is assumed to be correct.

True. But as I said above, they are working on it.

> 2.    The CompCert system may successfully translate programs
> containing undefined behavior. Any proof statements made about such
> programs may not be valid.

Yes. But this is not the issue with the Verified C compiler but with the 
input C program itself. You can use other tools (like Frama-C, Astrée or 
Polyspace) to check your C program has no undefined behaviour.

> 3.    The support tools are assumed to be correct; primarily the Coq
> proof assistant, which is written in OCaml.

Yes. But Coq is designed in such a way (a very small, manually verified 
trusted core and then libraries built upon that core) that the 
possibility to have an issue in Coq is very very low (but not zero, I 
agree).

Regarding OCaml, yes some bugs in the OCaml compiler or run-time could 
theoretically impact Coq. But having such bugs is very remote. And some 
people (Esterel Technologies people for SCADE compiler) have developed a 
simplified OCaml run-time to fulfil DO178B criteria (see "Certified 
Development Tools Implementation in Objective Caml". Pagano, Andrieu, et 
al. PADL 2008, LNCS 4902).

> 4.    The CompCert system makes decisions about implementation
> dependent behaviors and any proofs only apply in the context of these
> decisions.

Yes. As any compiler. At least those decisions are formally documented.

> 5;    The CompCert system makes decisions about unspecified behaviors
> and any proofs only apply in the context of these decisions.

Yes. As any compiler. At least those decisions are formally documented.


As pointed out on the comment of your blog, an independent research 
paper (http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf) has 
shown that ComptCert is a very strong compiler, much stronger that any 
others. Quoting Regehr's paper:
"""
The striking thing about our CompCert results is that the middleend
bugs we found in all other compilers are absent. As of early 2011,
the under-development version of CompCert is the only compiler we
have tested for which Csmith cannot find wrong-code errors. This is
not for lack of trying: we have devoted about six CPU-years to the
task. The apparent unbreakability of CompCert supports a strong
argument that developing compiler optimizations within a proof
framework, where safety checks are explicit and machine-checked,
has tangible benefits for compiler users.
"""

I've read somewhere (sorry, no precise reference), that the parts where 
bugs were found in Regehr's paper have been formalized since then.


Sincerely yours,
D. Mentré