[dranov]

CompCert doesn't do this, but CakeML, a verified compiler for a variant of ML bootstraps itself in the logic:

> A unique feature of the CakeML compiler is that it is bootstrapped “in the logic” – essentially, an application of the compiler function with the compiler’s source implementation as argument is evaluated via logical inference. This bootstrapping method produces a machine code implementation of the compiler and also proves a theorem stating functional correctness of that machine code. Bootstrapping removes the need to trust an unverified code generation process. By contrast, CompCert first relies on Coq’s extraction mechanism to produce OCaml, and then relies on the OCaml compiler to produce machine code.

For details, see section 11 "Compiler Bootstrapping" in http://www.cs.cmu.edu/~yongkiat/files/cakeml-jfp.pdf

[sansnomme]

Does this guard against trusting trust attacks?

[dranov]

I might be mistaken, but my understanding is that it does not. You still need to trust the implementation of the logic. But if you don't trust that, you wouldn't trust the compiler correctness proof anyway, so bootstrapping in the logic does give a benefit.

[sansnomme]

So Coq basically have to be correct and trusted for this to be secure?

[sanxiyn]

Yes, but large part of Coq is designed to be untrusted. Roughly, Coq searches proof and checks found proof. Search part is larger, it can be incorrect, can have bugs, etc. without affecting the proof. Check part is trusted, and is available as a separate binary (coqchk), which consumes proof found by search (coqc).

For CompCert, the more worrying is the correctness of "extraction". This is somewhat technical, you should be able to search if you are curious. CakeML solves extraction problem.

For HOL, Proof Technologies Ltd developed HOL Zero, which is solely dedicated to trustworthiness without bells and whistles. Bells and whistles are absolutely necessary for proof development. The idea is to use HOL Zero at the end, after proof is finished. It's like coqchk idea on steroid. http://proof-technologies.com/holzero/

Summary: CompCert trusts coqchk and extraction. CakeML trusts HOL, hopefully something like HOL Zero can be used in the future.

[smallnamespace]

Note that Godel's Incompleteness Theorems tell us that formal systems with sufficient power cannot 'prove themselves' in some sense, and we see that rather convincingly:

1. Implementations can be wrong, so we want a formal proof system

2. The proof system can be wrong, so we want to apply the proof system to itself

3. But the proof system may be wrong (either in implementation or specification) in a way such that its self-proof is actually invalid

At some point, we want to assert some property (completeness, correctness) of the system as a whole, but whenever we augment the system to allow this, that augmented system's own properties now come into question.

[ChrisLomont]

Logic proving systems need never hit Godel incompleteness. Many systems weaker than Godel are proven consistent within themselves, and are strong enough to verify code.

Godel’s Proofs rely on statement encoding using properties of integers not required for these logic systems.

Presburger Arithmetic, for example, avoids Godel incompleteness, yet provides a decent system for a lot of work.

[cmrx64]

not coq but HOL4 and Poly/ML. there are verified HOL kernels but you’d need to do substantial manual validation of the exported theorems to make sure they didn’t get subverted during proof export.