CompCert – A formally verified C compiler

So when you implement a buffer overflow in your C program, you can be assured it will overflow in the manner specified.

One of the really nice outcomes of this approach is that it allows you to use different optimisation levels.<p>Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation.

In 1983, Ken Thompson gave a Turing Award talk in which he shows how to embed a backdoor into a compiler in such a way that it would not be visible, even if you had access to the compiler source. (<a href="http:&#x2F;&#x2F;delivery.acm.org&#x2F;10.1145&#x2F;1290000&#x2F;1283940&#x2F;a1983-thompson.pdf" rel="nofollow">http:&#x2F;&#x2F;delivery.acm.org&#x2F;10.1145&#x2F;1290000&#x2F;1283940&#x2F;a1983-thomps...</a>) I wonder if the verified compiler could be altered in the same way? (A snippet from the paper so you get the idea:<p>&gt;We compile the modified source with the normal C compiler to produce a bugged binary. We install this binary as the official C compiler. We can now remove the bugs from the source of the compiler and the new binary will reinsert the bugs whenever it is compiled. Of course, the login command will remain bugged with no trace in source anywhere.)

Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ?

&gt; <i>Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program.</i><p>Which semantics? The ISO C semantics is rather lacking; &quot;undefined behavior&quot; lurks around every corner.<p>A C compiler that correctly implements all ISO C requirements is a fine thing, and certainly better than one which gets some of that semantics wrong, but doesn&#x27;t achieve all that much in the big picture.<p>If the verified compiler actually provides extended semantics beyond ISO C that eliminates much of the undefined behavior, such that programmers using this dialect can rely on a safer language, then we&#x27;re talking.

Sadly even a proved correct C compiler can produce incorrect behavior in a real system: <a href="https:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;482" rel="nofollow">https:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;482</a>

How does a project like this deal with the bootstrap problem?

See limitations in the docs.

Going to great lengths to avoid writing Rust.