Definition of a certified program

Question

I see a couple of different research groups, and at least one book, that talk about using Coq for designing certified programs. Is there are consensus on what the definition of certified program is? From what I can tell, all it really means is that the program was proved total and type correct. Now, the program's type may be something really exotic such as a list with a proof that it's nonempty, sorted, with all elements >= 5, etc. However, ultimately, is a certified program just one that Coq shows is total and type safe, where all the interesting questions boil down to what was included in the final type?

---

Edit 1

Based on wjedynak's answer, I had a look at Xavier Leroy's paper "Formal Verification of a Realistic Compiler", which is linked in the answers below. I think this contains some good information, but I think the more informative information in this sequence of research can be found in the paper Mechanized Semantics for the Clight Subset of the C Language by Sandrine Blazy and Xavier Leroy. This is the language that the "Formal Verification" paper adds optimizations to. In it, Blazy and Leroy present the syntax and semantics of the Clight language and then discuss the validation of these semantics in section 5. In section 5, there's a list of different strategies used for validating the compiler, which in some sense provides an overview of different strategies for creating a certified program. These are:

1. Manual reviews
2. Proving properties of the semantics
3. Verified translations
4. Testing executable semantics
5. Equivalence with alternate semantics

In any case, there are probably points that could be added and I'd certainly like to hear about more.

Going back to my original question of what the definition is of a certified program, it's still a little unclear to me. Wjedynak sort of provides an answer, but really the work by Leroy involved creating a compiler in Coq and then, in some sense, certifying it. In theory, it makes it possible to now prove things about the C programs since we can now go C->Coq->proof. In that sense, it seems like there's this work flow where we could

1. Write a program in X language
2. Form of a model of the program from step 1 in Coq or some other proof assistant tool. This could involve creating a model of the programming language in Coq or it could involve creating a model of the program directly (i.e. rewriting the program itself in Coq).
3. Prove some property about the model. Maybe it's a proof about the values. Maybe it's the proof of the equivalence of statements (stuff like 3=1+2 or f(x,y)=f(y,x), whatever.)
4. Then, based on these proofs, call the original program certified.

Alternatively, we could create a specification of a program in a proof assistant tool and then prove properties about the specification, but not the program itself.

In any case, I'm still interested in hearing alternative definitions if anyone has them.

Answer 1

I agree that the notion seems vague, but in my understanding a certified program is a program equipped/together with the proof of correctness. Now, by using rich and expressive type signatures you can make it so there is no need for a separate proof, but this is often only a matter of convenience. The real issue is what do we mean by correctness: this a matter of specification. You can take a look at e.g. Xavier Leroy. Formal verification of a realistic compiler.

Answer 2

First note that the phrase "certified" has a slightly French bias: elsewhere the expression "verified" or "proven" is often used.

In any case it is important to ask what that actually means. X. Leroy and CompCert is a very good starting point: it is a big project about C compiler verification, and Leroy is always keen to explain to his audience why verification matters. Especially when talking to people from "certification agencies" who usually mean testing, not proving.

Another big verification project is L4.verified which uses Isabelle/HOL. This part of the exposition explains a bit what is actually stated and proven, and what are the consequences. Unfortunately, the actual proof is top secret, so it cannot be checked publicly.

Answer 3

A certified program is a program that is paired with a proof that the program satisfies its specification, i.e., a certificate. The key is that there exists a proof object that can be checked independently of the tool that produced the proof.

A verified program has undergone verification, which in this context may typically mean that its specification has been formalized and proven correct in a system like Coq, but the proof is not necessarily certified by an external tool.

This distinction is well attested in the scientific literature and is not specific to Francophones. Xavier Leroy describes it very clearly in Section 2.2 of A formally verified compiler back-end.

Answer 4

My understanding is that "certified" in this sense is, as Makarius pointed out, an English word chosen by Francophones where native speakers might instead have used "formally verified". Coq was developed in France, and has many Francophone developers and users.

As to what "formal verification" means, Wikipedia notes (license: CC BY-SA 3.0) that it:

is the act of proving ... the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

(I realise you would like a much more precise definition than this. I hope to update this answer in future, if I find one.)

Wikipedia especially notes the difference between verification and validation:

• Validation: "Are we trying to make the right thing?", i.e., is the product specified to the user's actual needs?
• Verification: "Have we made what we were trying to make?", i.e., does the product conform to the specifications?

The landmark paper seL4: Formal Verification of an OS Kernel (Klein, et al., 2009) corroborates this interpretation:

A cynic might say that an implementation proof only shows that the implementation has precisely the same bugs that the specification contains. This is true: the proof does not guarantee that the specification describes the behaviour the user expects. The difference [in a verified approach compared to a non-verified one] is the degree of abstraction and the absence of whole classes of bugs.

Which classes of bugs are those? The Agda tutorial gives some idea:

• no runtime errors (inevitable errors like I/O errors are handled; others are excluded by design).
• no non-productive infinite loops.

Answer 5

It may means free of runtime error (numeric overflow, invalid references …), which is already good compared to most developed software, while still weak. The other meaning is proved to be correct according to a domain formalization; that is, it does not only have to be formally free of runtime errors, it also has to be proved to do what it's expected to do (which must have been precisely defined).