carrying code (PCC) approach^{1, 19} does not attempt to estab-
lish semantic preservation between a source program and
some compiled code. Instead, PCC focuses on the genera-
tion of independently checkable evidence that the compiled
∀S, C, Comp(S) = OK (C) ⇒ S ≈ C ( 6) code C satisfies a behavioral specification Spec such as type
and memory safety. PCC makes use of a certifying compiler,
In other words, a verified compiler either reports an error or which is a function CComp that either fails or returns both
producescodethatsatisfiesthedesiredcorrectnessproperty. a compiled code C and a proof π of the property C Spec.
Notice that a compiler that always fails (Comp(S) = Error The proof π, also called a certificate, can be checked inde-
for all S) is indeed verified, although useless. Whether the pendently by the code user; there is no need to trust the code
compiler succeeds to compile the source programs of inter- producer, nor to formally verify the compiler itself. The only
est is not a correctness issue, but a quality of implementa- part of the infrastructure that needs to be trusted is the cli-
tion issue, which is addressed by nonformal methods such ent-side checker: the program that checks whether π entails
as testing. The important feature, from a formal verification the property C Spec.
standpoint, is that the compiler never silently produces As in the case of translation validation, it suffices to for-
incorrectcode. mally verify the client-side checker to obtain guarantees
Verifying a compiler in the sense of definition ( 6) amounts as strong as those obtained from compiler verification of
to applying program proof technology to the compiler property ( 4). Symmetrically, a certifying compiler can be
sources, using one of the properties defined in Section 2. 1 constructed, at least theoretically, from a verified compiler,
as the high-level specification of the compiler. provided that the verification was conducted in a logic that
Translation Validation with Verified Validators. In the follows the “propositions as types, proofs as programs” par-
translation validation approach^{20, 22} the compiler does not adigm. The construction is detailed in Leroy. ^{11, section 2}
need to be verified. Instead, the compiler is complemented
by a validator: a boolean-valued function Validate(S, C) that
verifies the property S ≈ C a posteriori. If Comp(S) = OK(C)
and Validate(S, C) = true, the compiled code C is deemed
trustworthy. Validation can be performed in several ways,
ranging from symbolic interpretation and static analysis of

S and C to the generation of verification conditions followed by model checking or automatic theorem proving. The property S ≈ C being undecidable in general, validators are necessarily incomplete and should reply false if they cannot establish S ≈ C.

Translation validation generates additional confidence in the correctness of the compiled code, but by itself does not provide formal guarantees as strong as those provided by a verified compiler: the validator could itself be incorrect. To rule out this possibility, we say that a validator Validate is verified if it is accompanied with a formal proof of the following property:

etc.), but also if it exceeds the capacities of the compiler. A compiler Comp is said to be verified if it is accompanied with a formal proof of the following property:

2. 3. Composition of compilation passes

Compilers are naturally decomposed into several passes that communicate through intermediate languages. It is fortunate that verified compilers can also be decomposed in this manner. Consider two verified compilers Comp and Comp 12 from languages L to L and L to L , respectively. Assume 12 23

that the semantic preservation property ≈ is transitive. (This is true for properties ( 1) to ( 5) of Section 2. 1.) Consider the error-propagating composition of Comp and Comp :

12

Comp(S) = match Comp (S) with

1

| Error → Error

| OK (I) → Comp (I)

2

It is trivial to show that this function is a verified compiler from L to L .

13

∀S, C, Validate(S, C) = true ⇒ S ≈ C

2. 4. summary

( 7) The conclusions of this discussion are simple and define the methodology we have followed to verify the CompCert compiler back-end. First, provided the target language of the compiler has deterministic semantics, an appropriate specification for the correctness proof of the compiler is the combination of definitions ( 3) and ( 6):

The combination of a verified validator Validate with an unverified compiler Comp does provide formal guarantees as strong as those provided by a verified compiler. Indeed, consider the following function:

 

Comp′(S) = match Comp (S) with | Error → Error

| OK (C) → if Validate (S, C) then OK(C) else Error

This function is a verified compiler in the sense of definition ( 6). Verification of a translation validator is therefore an attractive alternative to the verification of a compiler, provided the validator is smaller and simpler than the compiler.

Proof-Carrying Code and Certifying Compilers. The proof-

∀S, C, B ∉ Wrong, Comp(S) = OK(C) ∧ S ⇓ B ⇒ C ⇓ B

Second, a verified compiler can be structured as a composition of compilation passes, following common practice. However, all intermediate languages must be given appropriate formal semantics.

Finally, for each pass, we have a choice between proving the code that implements this pass or performing the transformation via untrusted code, then verifying its results using a verified validator. The latter approach can reduce the amount of code that needs to be verified.