Frama-C allows writing formally verified bug-free C. It is certainly tedious though; you essentially have to write two versions of every function: (1.) the actual C code for the function; (2.) a declarative formal specification of what the function does in ACSL (ANSI C Specification Language), stating all relevant pre-conditions that must be met prior to calling the function, and all relevant post-conditions that hold after the function runs. Then you have to add annotations to computation steps in the function code proving it causes the post-conditions to hold if the pre-conditions hold.
Nevertheless, it is extremely powerful because it can prove the correctness of arbitrary heap manipulation algorithms (lists, trees, graphs). You can formally prove complicated C pointer manipulations are correct that cannot be expressed in 'safe Rust'. There is also the CompCert formally verified C compiler.
I've also studied Ada/Spark's formal verification abilities and C is way ahead here. C is also way ahead of C++ because C has far fewer complicated semantic rules that need to be formalized before they can be analyzed. Even parsing C++ is an enormous task.
In the coming decades as the automation and ease-of-use of formal verification tools improves, I think C may well end up being the best choice for security-critical and correctness-critical systems programming. With current tools it is already ahead of Ada, C++, and Rust.
> In the coming decades as the automation and ease-of-use of formal verification tools improves, I think C may well end up being the best choice for security-critical and correctness-critical systems programming. With current tools it is already ahead of Ada, C++, and Rust.
The problem is that in practice when people reach for C, they reach for stb_image.h, not formal verification packages that are expensive and used for approximately no software in mainstream use outside of fields like avionics. The economics of formal verification just don't work for mainstream software. Organizations are simply not willing to multiply their development costs by 10x or 100x.
> Organizations are simply not willing to multiply their development costs by 10x or 100x.
I think this is a valid point today. Will it remain so in the future?
If say liabilities for bugs in critical software shift or if natsec regulations require software that touch infra like: water, power, telecom, and mass transit to be verified like avionics software is. IMO both are likely 2-3 decades out.
Either or both of these happening will expand demand for more hardened platform-level code.
The thing is software is made to compete for new monopolies rather than to perform functions reliably. There's so much funding for monopoly-rent-seeking that this dominates and characterizes the field. Correctness just isn't that important for that.
Over time, perhaps the available monopolies will dry up, a few megafirms will buy up everything that can collect rents, and the only software left to write will be practical.
>If say liabilities for bugs in critical software shift or if natsec regulations require software that touch infra like: water, power, telecom, and mass transit to be verified like avionics software is. IMO both are likely 2-3 decades out.
This can be mitigated by designing robust systems that are robust to flaws of its components. There is an understanding that bugs or corruption way happen and the system should able to tollerate it and fix itself or alert people that something is wrong or needs to be addressed.
It's cheaper to be able to handle your program crashing every once and a while than to try and earliest 100% of all crashes from your program. It's possible to deal with situation where you know you are never going to be 100% bug free.
Frama-C doesn't need to know anything about the target arch. It guarantees no undefined / implementation defined behavior on all architectures. You have to prove your code does not cause overflow/underflow (or accounts for it) if you add two integers or cast a uint32_t to an int32_t, etc. Very tedious, but it can and is being done.
CompCert, the formally verified C compiler, is a separate thing from Frama-C, but currently supports x86, ARM, RISC-V, and PowerPC. (CompCert is actually mostly programmed in OCaml and the Coq/Gallina proof assistant.) CompCert guarantees that a correct ISO C program (no undefined or implementation defined behavior) is translated into an assembler program with the same semantics, i.e. an assembler program that computes the same results as the C source program. So CompCert for each supported architecture needs a formal semantics for any CPU instructions it generates. CompCert is an optimizing compiler and the optimizer accounts for the delay between when an instruction is issued and when the result is ready, accounts for pipelining and all that if that is what you are asking.
But to write verified C programs you don't need to worry about instruction re-ordering happening lower down changing the meaning of your program and all that. That's a deeper layer of the onion, and, as Bjarne Stroustrup said, each time you peel a layer of the onion you cry more.
> Frama-C doesn't need to know anything about the target arch.
In fact, it needs some knowledge, but this knowledge can be configured for the project under analysis. This is the reason why the Frama-C kernel provides the `-machdep` option ;) .
Then depending on your code, you might need to add particular knowledge according to your target platform. For example validity of some hardware memory location, etc.
For my use cases thus far, the usual C portability pitfalls haven't applied: whether char is signed or unsigned, the range of 'int', little vs. big endian, etc.
Frama-C works at the C semantic level, without knowledge about processor instruction-level details (expect for some extended assembly syntax, and a few details here and there). If you are talking about unspecified sequences of C statements, then Frama-C can warn about some situations, as mentioned in the user manual (https://www.frama-c.com/download/frama-c-user-manual.pdf):
option -unspecified-access may be used to check when the evaluation of an expression depends on the order in which its sub-expressions are evaluated. For instance, this occurs with the following piece of code.
int i, j, *p;
i = 1;
p = &i;
j = i++ + (*p)++;
In this code, it is unclear in which order the elements of the right-hand side of the last assignment are evaluated. Indeed, the variable j can get any value as i and p are aliased.
In some cases, knowing the architecture is essential to get information such as the width of integer types. Ideally, one would like a completely system-independent, portable analysis, but this is extremely hard in C. For instance, the ISO C11 standard, in section 5.2.4.1 Translation limits, states that The implementation shall be able to translate and execute at least one program that contains at least one instance of every one of the following limits [...] 4095 characters in a string literal (after concatenation), 65535 bytes in an object, [...]. It also states that INT_MAX may be, for instance, as low as 32767. So, for a truly portable analysis, one would have to warn whenever any of these limits are reached, leading to an analysis useless except for some toy examples.
I'd rather use CBMC symbolic verification. Only one C code, also it's contracts, no ACSL needed.
The verifiers targets the whole range of the symbolic input. No need for expensive unit-testing over a single input value or random input values. You test all possible values. It's fast and practical.
Which is not feasible if there are, say 2^128 or more possible values. CBMC is a model checker, which is very useful for many problems that can be brute-forced but not the same thing as the correct-by-construction approach of Frama-C style formal methods, which deductively verifies that code works on all possible cases, even all conceivable edge cases, without having to exhaustively test all cases.
I just went through the CBMC tutorial[1] to make sure I'm not crazy. Yes, CBMC is a bounded model checker, as I thought.
CBMC can also be used for programs with unbounded loops. In this
case, CBMC is used for bug hunting only; CBMC does not attempt to
find all bugs.
Frama-C is about eliminating ALL bugs, you are allowed to prove your "unbounded" loop algorithm actually terminates, and terminates with the correct solution, if you are willing to learn to use the manual proof assistant. CBMC can check for an extremely important class of errors, but it doesn't let you prove, say, your traveling salesman solver always returns a shortest trip T through the graph G, or that the graph coloring register allocator for your C compiler always correctly colors the graph, something that is actually done for the CompCert formally verified C compiler (using the Coq/Gallina proof assistant, which can be used with Frama-C).
However, having now gone through the CBMC manual, it appears to be much faster and easier to use for my own limited purposes than Frama-C. I don't need a sledgehammer to swat flies. I also like that the installation procedure on my machine was simply,
$ sudo apt install cbmc
So I plan to give cprover a shot now, thanks for the heads up. : )
And if cancer kills millions every year and successful treatments are expensive and tedious, maybe someone can come up with a cure to cancer that is not expensive and not tedious. It's a hard problem to solve, but a lot of smart people are working on that problem, too.
Solving cancer is a fundamentally new thing that nobody knows how to do yet and probably can't be done by one person.
Taking an ugly language that evolved in parts and synthesizing it into something elegant is something that not everybody can do, but it only takes one talented person, and it's been done before. Craft rather than invention.
We have Ada/SPARK already. SPARK is a subset of Ada that allows you to formally verify your code, e.g. to prove the absence of runtime errors, memory leaks, and so forth.
Not too interesting; they disabled the checks[1]. Lot of stuff have happened since then to Ada and SPARK. The Ada they used is quite different to the Ada we have today. SPARK 2014 is a complete re-design of the language, too. Plus, you are responding to a comment specifically talking about Ada/SPARK (SPARK specifically), so not sure how Ariane 5 is relevant.
[1] Today those checks may not even be needed to begin with due to SPARK. GNATprove may have given them "predicate check might fail" or something like that. Read the AdaCore Blog for more.
I've used SPARK with GNAT Studio, I've used Frama-C, and I'm also experimenting with CBMC. Frama-C is way more powerful than SPARK, but also consequently has a much deeper learning curve.
For example, singly-linked lists and trees are supported whereas
doubly-linked lists are not.
With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.
However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.
AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:
Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:
do you know if anyone has used frama-c to verify properties as "deep" as those done by seL4, like functional correctness and integrity, rather than a "shallower" property like memory safety or absence of crashes?
Yes, Frama-C uses a plugin architecture, and there are plugins to verify all kinds of things, including functional correctness. The Frama-C tutorials page,
Also, it is less effort to write bug-free code in OCaml than C. The Coq/Gallina proof assistant even has an OCaml-extraction (and also Haskell-extraction) feature where you extract runnable code from a formally verified algorithm in the Gallina specification language. (It's generally easier to proof theorems about code in the theorem prover itself, go figure.) Most of these C verification tools are written in OCaml, not C, with varying levels of assistance from Coq/Gallina.
The main reason the functional languages make it easier is because you generally execute side-effect free functions on data structures to give them the mathematical property you want. For example, you execute a lexicographical sort function on a list of strings and then the strings in the list all satisfy the mathematical property of a total ordering. You don't have to do any reasoning about the "in-between state" where pointers under the hood are being manipulated, and you don't have to add pre-conditions and post-conditions about the global environment if the code is side effect free and does not access non-local memory.
"Big" software is mostly not difficult algorithms, but writing boilerplate glue code that connects the inputs and outputs of algorithms/functions that are usually written by someone else. Frama-C can definitely verify the boilerplate for "big" software, this is actually easier than verifying data structures and algorithms, which requires knowing the key property to get the prover to see that the algorithm always makes progress toward a solution. Once you have the contracts set up for calling a function, Frama-C will enforce that the contract is always met.
The CompCert verified C compiler is "big" software, but not actually written in C, rather OCaml and Coq/Gallina.
Yes, a compiler written in C could be verified with Frama-C, but "verifying in Frama-C" for something that hard (i.e. has many proof steps that cannot be automated) really means verifying in a proof assistant that can interact with Frama-C that understands ACSL, and Coq is usually used. And indeed, the loop invariants you mention usually cannot be automatically proved and must be proved manually, which is why there is such a learning curve to Frama-C. I first started using Frama-C without having used Coq/Gallina/OCaml, and I began to learn them simply because I hit a roadblock with Frama-C where I couldn't really progress without a deeper understanding for why automatic proving fails when it fails, why the error messages when automatic proving fails often aren't terribly helpful, what the current limits of automatic proving are, how the automatic proving actually works under the hood, etc.
Coq has been used to formally verify a large body of classical mathematics. Coq can 'understand' what a prime number is and can be used to prove that there are infinitely many primes, can prove that sqrt(2) is irrational, etc. Coq can prove a recursive solver for the Towers of Hanoi actually solves the problem, etc. And thus Coq can prove a C program to solve the Towers of Hanoi correctly solves the problem, because Coq can reason about C programs.
I've been slowly working through the Software Foundations series on using Coq/Gallina:
Another poster mentioned CBMC which I just started playing with. It is much less powerful than Frama-C, there isn't the ACSL specification capability and theorem proving, but it is much more automatic and much faster to get started with. For many cases if I just want to verify that a certain C file frees all its mallocs, doesn't have out-of-bounds accesses, and that all obviously bounded loops terminate, CBMC is much easier. Also, like Frama-C, it converts C functions into "goto programs" (removes the syntactic sugar of 'for' and 'while' loops to obtain a more pure Control-Flow-Graph (CFG)) for certain forms of analysis, and when I first encountered this in Frama-C there was no explanation why, whereas the manual for CBMC actually has an excellent gentle introduction:
If you want to allocate a Meow pointer to a Bark pointer that's your decision. It won't work to your satisfaction, but there's nothing preventing you from doing it. That's why we have programmers. Those people who have the intelligence and skills and know the limitations of a language.
Just like a gun doesn't care if it's pointing at your foot when you pull the trigger, most (all??) programming languages will let you do something stupid if you insist on doing so.
> Just like a gun doesn't care if it's pointing at your foot when you pull the trigger, most (all??) programming languages will let you do something stupid if you insist on doing so.
Well, right, but that's the exact reason why we have stuff like safety switches on guns. While it's your own prerogative if you truly wish to blow your foot off, accidentally injury is something we generally care about preventing. It's not even a question of if kernels written in C have severe memory corruption issues, it's a matter of how many. Many companies have simply given up on trying to find them all and are instead pouring hundreds of millions into making exploitation hard (see: ARM's Pointer Authentication, which is 100% useless unless you expect to encounter memory corruption). While I love C and think it's a great language, "don't shoot your damn foot off, duh" is just something that doesn't work in practice.
Nevertheless, it is extremely powerful because it can prove the correctness of arbitrary heap manipulation algorithms (lists, trees, graphs). You can formally prove complicated C pointer manipulations are correct that cannot be expressed in 'safe Rust'. There is also the CompCert formally verified C compiler.
I've also studied Ada/Spark's formal verification abilities and C is way ahead here. C is also way ahead of C++ because C has far fewer complicated semantic rules that need to be formalized before they can be analyzed. Even parsing C++ is an enormous task.
In the coming decades as the automation and ease-of-use of formal verification tools improves, I think C may well end up being the best choice for security-critical and correctness-critical systems programming. With current tools it is already ahead of Ada, C++, and Rust.
https://frama-c.com/