An example of something you can formally verify with proofs in Software Development

Question

I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques for formal verification include using type systems, model checking, automated theorem proving, proofs, and doing program derivation. Finally, there is testing, but I wont go into that here.

I have asked several questions regarding these topics:

• What to prove and how to prove it
• What you want to "prove" in algorithms
• High-level requirements for a Proof of "Saving to the Database"
• How to prove a function returns a value
• How proofs can be applied to a simple logging function
• How to prove a side effect in a function
• How to prove $c = a + b$ using Program Verification Techniques
• How to use Hoare Logic to Prove this Assertion
• How to apply Hoare Logic to this function
• How to apply Operational Semantics to this function

The gist of the answers is essentially, you can't apply formal proofs to realistic software applications. This is a bit disappointing to hear, especially when there are projects such as CompCert, the "formally verified" C compiler. My first question is, what exactly they mean (in CompCert) by "formally verified". Wondering which of the following (or something different) this includes:

• Model Checking
• Formal Proofs (e.g. Hoare Logic)
• Type Theory
• Transition Systems
• Operational Semantics / Denotational Semantics

My second question is, what is a realistic application of proofs to formally verify software (i.e. a web application example, not a textbook example). After asking these questions, I am discouraged that there are no applications of formal proofs to practical software development.

At first I thought that using Coq I could somehow write "formal proofs" for my code, and walk away with a sense of confidence that my code was "formally verified". But now I don't know if that has any practical or realistic meaning. That was what I was getting at in How to prove a function returns a value, High-level requirements for a Proof of “Saving to the Database”, and How proofs can be applied to a simple logging function.

Then I imagined that perhaps Operational Semantics or Hoare Logic could help in "formally proving" the behavior of functions. But the gist of the answers was "it's too hard" or "it's impractical". Nevertheless, it seems that CompCert accomplished it (but not sure if they used Hoare Logic, Operational Semantics, or others), or maybe I am missing something. So what my sense is is there is no use in Hoare Logic or Operational Semantics in practical software development. I would like to be proven wrong on that.

I realize that Model Checking is a good candidate for matching a program model with a specification. But the question still remains, how you know that your model is correct in the first place. That is where it seems formal proofs or some other formal verification technique could shine somehow (which is what this question is about). Wondering how in practice you can apply formal proofs to software development. How to verify that your Model Checking model is correct. It seems the only answer is "formal proofs". But then the question is how. How to apply formal proofs to your model to verify it is correct. I've tried asking questions about it but have had no luck.

Answer 1

Look into tools like Frama-C, SPARK, Astrée, etc...

They have their use in very specific cases, notably software verification of small to medium sized embedded safety critical software (e.g. inside aircrafts, per DO-178C, or nuclear power plants, etc...). Such software have a few dozen thousands lines (or perhaps two hundred thousands at most of C or Ada code), but a bug inside them could crash a plane. So the industry is ready (and required by external regulations) to spend a lot of money and efforts on such small critical software. There are also many severe coding rules (e.g. dynamic allocation, recursive functions, dead code are forbidden).

Proving software, even with these tools, is very costly. A typical safety-critical software costs about a hundred or a thousand times more to develop than a usual software (like your phone applet or some Unix command line tool) of equivalent size, because formal methods (but not only them) are involved. The teams developing them should have formal methods experts working together with aircraft software experts. Sometimes, a small routine has to be rewritten and annotated to be processable by code provers.

There are several research projects around such tools and their use. For a recent example look into VESSEDIA (but you could find many others). One of its results might include a simple proof of a small subpart of the Contiki OS. From an outside view, the results are related to simple subsystems of it (e.g. some simply-linked-list module). In practice the proof requires a lot of formal annotations (so the developer has to provide annotations in ACSL about half as long as the simple C code that is specified by these annotations).

The L4 microkernel has also a variant, called seL4, which uses formal methods (the code size which is formally proved is a few dozen thousands of C code). AFAIU that variant (with its proof) is open-source.

But formal methods don't scale well. It is very unlikely that they would scale -in the next 20 or 30 years- (for present-day programming languages and code) to software as big as the Qt toolkit or the Linux kernel (because formally specifying the intended behavior of Qt or of Linux kernel is practically impossible). For example, C heap allocation is easy to code (that is, a lot of C code uses malloc & free), but difficult to formalize and prove (because current shape analysis techniques don't scale well to large programs). That internal complexity and difficult of formal methods hinders its uses in real-world programs (whose size is growing a lot: a source code editor today is much more complex and bigger than what vi was in the 1980s).

I was part of several research grant submissions mixing more or less formal methods and other approaches (e.g. machine learning techniques on large amount of code, natural language processing techniques), but such funding is hard to get (e.g. there is probably no more any H2020 or FP9 calls dedicated to software engineering before my retirement; the last one was ICT-16 to which I was part of a submission -and waiting (in june 2018) for its evaluation; but only a few percents of submitted proposals get funding). See also this answer to another (but indirectly related) question. BTW, I might be interested in joining some European consortia in 2019 for HPC software tooling using such ideas.

To summarize: There is No silver bullet, so I agree with you:

there is no use in Hoare Logic or Operational Semantics in practical software development

(because even if you have proven your code w.r.t. some explicit formal specifications, there could be - and there still is some - "bugs" or incompleteness in the formal specifications; specifying "correctly" what a real-life software such as a word processor or some web application should do is practically impossible, since you want that specification to be "complete" and cover all the practical cases).

However, notice that recent practical programming languages (e.g. Rust, Ocaml, and also monsters like C++20 or C++17 which became so complex that only a dozen of people understands them fully) have been inspired by formal proof techniques. And academic curiosities like Agda uses even more them. Also, static source code analyzers like clang-analyzer (and even some optimization passes of GCC) use techniques related to formal proofs.

Regarding CompCert, you could download its source code (and proof) and study its code, but you are not allowed to use that source code for non-academic purposes (so CompCert is not free software but its source code is downloadable and you are allowed to study and experiment it. However the resulting binary has license restrictions).

See also this draft report (and the references there).

NB. Seeking partners interested by RefPerSys

Answer 2

Quite a lot of things can and have been formally verified with formal methods.

1. Compilers. We want to prove that a compiler preserves the semantics of its source program. For example, if we write a int x = 3; x++; in C, we mean that. But the compiler might not produce correct assembly and machine code.

   It is known to be difficult to debug compilers, so a bunch of people at INRIA, the French national lab for computer science, led by Xavier Leroy, decided to start from scratch and write a C compiler that is provably correct. Eventually, they produced CompCert, which has since been used commercially by companies like Airbus to compile important software.

   There have also been certified compilers for other languages. One of such exists for ML (CakeML). I would not surprised to find more.

   Note: According to @BasileStarynkevitch, CompCert has been used for purposes related to aviation, but it is not sure if Airbus is using it to compile on-plane software as of June 2018. According to Xavier Leroy (via personal communication to Basile), last year Airbus was still considering this as a possibility. But at least it has been used for something.

2. Operating system kernels. Operating system kernels are also hard to debug, and can be pretty nasty if there's a bug (it stops the entire machine!). If you run into a OS kernel bug on a satellite, it wouldn't be a very good day for you. So, a bunch of researchers in Australia wrote an operational specification for an OS kernel. Then, they developed a kernel according to that specification and proved it free of bugs (e.g., deadlocks, livelocks, overflows...). Of course, the spec is assumed to be correct. That became the seL4 kernel.

   For follow-up on this work, see HACMS (a project which developed a verified drone based on seL4) and CertiKOS (a project which developed a layered, POSIX, concurrent OS kernel).

3. An example closer to us. Part of the control software running on the Paris Metro Line 14 is formally verified using the B-Method. Later, the B-Method was also used on Line 1 when it was automated. The French people really like formal methods!

Of course, most software would be too costly to verify. I doubt anyone would want to fully verify a browser or a word processor, as they don't matter all that much (if they crash, just restart!). But if your software is running on an airplane or a train carrying a hundreds of people and tasked with operating the vehicle, it would be reasonable to want to verify that.

Hoare logic and/or operational semantics per se might not be that useful in software development, but they are important theoretical and/or intellectual foundations of useful verification methods. Therefore, they're still important to have a sound grasp and understanding of those tools. I believe it wouldn't be an exaggeration to state that every software verification expert (or quasi-expert) has a good understanding of Hoare logic and operational semantics!