5 ms·

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 actu

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. https://frama-c.com/ https://frama-c.com/

joe_guy 5y ago
Thank you for the write up. I'll be reading up on this more. Do you know if it models the target arch, too? Like, can it account for different architectures having different instruction reordering rules?
- dandotway 5y ago
  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.
  - KsassPeuk 5y ago
    > 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.
    - dandotway 5y ago
      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.
- edwcross 5y ago
  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 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.
pcwalton 5y ago
> 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.
- andrewjl 5y ago
  > 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.
  - charcircuit 5y ago
    >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.
    - perl4ever 5y ago
      It doesn't seem plausible to me that an organization that refuses to create reliable components will create reliable systems out of the components.
perl4ever 5y ago
If it's so tedious, maybe someone can come up with a more unified language that accomplishes the same thing?
- dandotway 5y ago
  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.
  - perl4ever 5y ago
    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.
- johnisgood 5y ago
  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.
  - perl4ever 5y ago
    There's a lot of interesting stuff out there about the Ariane 5 failure, whose guidance system apparently was in Ada.
    - johnisgood 5y ago
      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. We already discussed it here: https://news.ycombinator.com/item?id=20931242 https://news.ycombinator.com/item?id=20931242 (and probably elsewhere, too). [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.
kobebrookskC3 5y ago
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?
- dandotway 5y ago
  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, https://frama-c.com/html/tutorials.html https://frama-c.com/html/tutorials.html Has a link to the ACSL-by-example PDF which gives examples of creating in C various C++ STL inspired data structures and routines: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... 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.
  - kobebrookskC3 5y ago
    these are relatively small, relatively self-contained algorithms and data structures though, right? not a "big" piece of software.
    - dandotway 5y ago
rurban 5y ago
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.
- dandotway 5y ago
  > You test all possible values 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.
  - rurban 5y ago
    CBMC does formal verification on symbolic values and its ranges, just as Frama-C. Just in a well-known language, C. There is no brute force search. If so it would be impractical. The industry is using CBMC, not Frama-C.
    - dandotway 5y ago
      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. : ) [1] http://www.cprover.org/cprover-manual/cbmc/tutorial/ http://www.cprover.org/cprover-manual/cbmc/tutorial/

joe_guy 5y ago

Thank you for the write up. I'll be reading up on this more. Do you know if it models the target arch, too? Like, can it account for different architectures having different instruction reordering rules?

dandotway 5y ago
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.
- KsassPeuk 5y ago
  > 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.
  - dandotway 5y ago
    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.
edwcross 5y ago
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 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.

pcwalton 5y ago

> 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.

andrewjl 5y ago
> 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.
- charcircuit 5y ago
  >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.
  - perl4ever 5y ago
    It doesn't seem plausible to me that an organization that refuses to create reliable components will create reliable systems out of the components.

perl4ever 5y ago

If it's so tedious, maybe someone can come up with a more unified language that accomplishes the same thing?

dandotway 5y ago
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.
- perl4ever 5y ago
  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.
johnisgood 5y ago
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.
- perl4ever 5y ago
  There's a lot of interesting stuff out there about the Ariane 5 failure, whose guidance system apparently was in Ada.
  - johnisgood 5y ago
    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. We already discussed it here: https://news.ycombinator.com/item?id=20931242 https://news.ycombinator.com/item?id=20931242 (and probably elsewhere, too). [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.

kobebrookskC3 5y ago

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?

dandotway 5y ago
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, https://frama-c.com/html/tutorials.html https://frama-c.com/html/tutorials.html Has a link to the ACSL-by-example PDF which gives examples of creating in C various C++ STL inspired data structures and routines: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... 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.
- kobebrookskC3 5y ago
  these are relatively small, relatively self-contained algorithms and data structures though, right? not a "big" piece of software.
  - dandotway 5y ago

rurban 5y ago

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.

dandotway 5y ago
> You test all possible values 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.
- rurban 5y ago
  CBMC does formal verification on symbolic values and its ranges, just as Frama-C. Just in a well-known language, C. There is no brute force search. If so it would be impractical. The industry is using CBMC, not Frama-C.
  - dandotway 5y ago
    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. : ) [1] http://www.cprover.org/cprover-manual/cbmc/tutorial/ http://www.cprover.org/cprover-manual/cbmc/tutorial/