6 ms·

Frama-C: Modular Analysis of C Programs

103 points by johlo 6y ago

Yoric 6y ago
A few years ago, I learnt of one of the surprising constraints for Frama-C: it may only depend on code that could be patched by the maintainers of Frama-C. That's because Frama-C is meant to be used on highly critical infrastructures (think nuclear plants) even in highly difficult times (think world war).
- flohofwoe 6y ago
  That's a good guideline for selecting external dependencies in general, also for "non-critical infrastructure" software. A slightly more relaxed version of that guideline would be: "never use dependencies that you don't feel comfortable creating or maintaining yourself".
- rwmj 6y ago
  Isn't that "all of open source" or do they mean something quite narrow by "could be patched by the maintainers of Frama-C"?
  - snazz 6y ago
    It seems like they mean that the Frama-C maintainers only use (and vendor) dependencies that they are comfortable maintaining themselves.
  - Yoric 6y ago
    The latter. And that includes the choice of a compiler.
- jacquesm 6y ago
  I have the exact same mentality when it comes to projects that I intend to operate for a longer time than just throwaway try-outs. If I can't understand what's going on under the hood then I'll be happy to pass. This is a limitation, of course. But at least it keeps me on a path where I don't bite off more than I can chew. Experience has led me to believe that any dependency you have is sooner or later going to turn into a either a liability or an obligation, this makes it much easier for me to see dependencies as costs rather than just as advantages. The number of dependencies for my current project is four, and each of those (vexflow, tone.js, lovefield, jquery) I'm in principle prepared to maintain myself. Even so, all of them have already proven to be here for the longer term. Ditto for tooling.
the-smug-one 6y ago
Warning! Lots of disjointed thoughts below. I've used Frama-C ACSL+WP and it was incredibly painful to use to prove basically anything. For me the main issue was that Frama-C can say 3 things about your specs: Yes, No, and Don't know. That means I have no idea where to start to debug my proof, especially as I'm already convinced that my proof works! This is inherent to computing weakest pre-condition AFAIK. I had to provide my own loop invariants, which is also a pain :-). C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course. I haven't used the other plugins, perhaps there are better ones! Type systems can be quite nice with regards to error messages, especially as the programmer themselves essentially derive their own granularity with regards to the domain and the proofs of the domain. But yes, we all have examples of absolutely terrible type system error messages. The paradigm of making comments have semantic meaning in some other language is also terrible. I'd rather have a superset of the core language with syntactic extensions for proofs. The build system can pull out the core language source code for me. Finally: I think that abstract interpretation of a low-level compilation target combined with a proof-carrying compiler is the way to go. The compiler has proofs of a bunch of stuff regarding the code already, carry them down into the assembly level please! There's some work in abstract interpretation of WebAssembly, and I think that could be a great platform for formal verification. Sorry for the barfing :-). Hopefully there're thoughts here to react to and reply to me about!
- unwind 6y ago
  This: C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course. sounds really interesting, do you remember some concrete example? Not saying you're wrong or anything, just curious of what kind of code is hard to analyze like this.
  - rwmj 6y ago
    I was wondering about this too. If I was going to guess I would say it could be stuff that applies to any language that uses fixed width machine types, and not only C. For example, this is not true: ∀a: a+1 > a if the type of 'a' is 32 bit int. Similarly negate(a) ≠ -a for some numbers.
quelsolaar 6y ago
We should be spending a lot less time inventing new languages and spending a lot more time working on tools for existing languages. If we did, all languages would be better, and the languages we did design would be designed to make it easy to make tools that help us use them.
- MaxBarraclough 6y ago
  It's not that we have to choose one of those two options. Work is still being done on static-analysis tools for C. To speak of Frama-C specifically, it isn't competing with new languages like Zig and Nim, it's competing with rival tools like [0], and with SPARK Ada. Formal reasoning about code is, for now, a niche reserved for critical-systems development. That kind of work tends to use tried-and-true languages with tried-and-true tooling: C, C++, Ada, and occasionally even Java. > the languages we did design would be designed to make it easy to make tools that help us use them. This is already a factor in language design. It's one of the reasons C-style preprocessors are now unfashionable. [0] http://www.eschertech.com/products/ http://www.eschertech.com/products/
  - doonesbury 6y ago
    Agree
- pjmlp 6y ago
  This is already what is happening with static analyzers for C and C++, some of them even getting some Rust like ideas on the analyzers. This is important, because as much as some of us would like to nuke those languages, they aren't going away and plenty of domains are not going to move away from them anyway. However there is only so much that one can improve without changing their semantics. And if you start changing their semantics, then you end up with what is effectively another language, e.g. Checked C.
the_french 6y ago
I'm starting my PhD under the supervision of one of the Frama-C authors, if you have questions I can relay them. In general I've found deductive verification techniques interesting / promising because they free engineers of a lot of required but tedious details you'd have in ITPs. However, I think there's a LOT of room for improvement in terms of ergonomics of proof debugging. For a frequent (for me) problem when debugging invariants is conditionals that break the invariant. if i have some code doing something like while (X) { invariant { forall i. 0 <= i < N .... } if j < i A else B } But it turns out that one of the branches A, B doesn't preserve the invariant well all the provers will tell me is 'can't prove this!' it's up to you to perform the transformations that split the two cases (granted in this example it's trivial) so that you can see that only _one_ branch was failing. I think that there should be transforms that automatically do things like split the range of an interval along relevant points (aka j) to help you figure out which portions are failing. There are tons of other issues related to proof ergonomics that could be improved, the UIs are really stuck in the 90s!
- mcguire 6y ago
  What's the status of handling manual memory management? The last time I looked, that was a huge, gaping hole in both Spark and Frama-C provers.
  - KsassPeuk 6y ago
    It depends on the verification tool you use. Eva (the abstract interpreter) has different ways to model dynamic allocation. It is thus a tradeoff to find between precision and computation time. WP does not have dynamic allocation support. This is an ongoing work, but it will not be available in the next release. Note that there are different ways to model the behavior of dynamic allocation, generally via axiomatic definitions and/or ghosts.
- aidenn0 6y ago
  Is frama-c still limited to single-threaded debugging? I know in the general case a context-switch is the same as "call any function anywhere in your code at any point into it" but it would be nice if it had a way for me to teach it about my expected threading invarients (e.g. prove that these objects never escape the current thread of execution).
mcguire 6y ago
Since you mentioned it, some posts I wrote a while back about Frama-C: Applied Formal Logic: Brute Force String Search https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.... Applied Formal Logic: The bug in Quick Search. https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.... Applied Formal Logic: Correctness of Quick Search. https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic...

103 points by johlo 6y ago

A few years ago, I learnt of one of the surprising constraints for Frama-C: it may only depend on code that could be patched by the maintainers of Frama-C. That's because Frama-C is meant to be used on highly critical infrastructures (think nuclear plants) even in highly difficult times (think world war).

flohofwoe 6y ago
That's a good guideline for selecting external dependencies in general, also for "non-critical infrastructure" software. A slightly more relaxed version of that guideline would be: "never use dependencies that you don't feel comfortable creating or maintaining yourself".
rwmj 6y ago
Isn't that "all of open source" or do they mean something quite narrow by "could be patched by the maintainers of Frama-C"?
- snazz 6y ago
  It seems like they mean that the Frama-C maintainers only use (and vendor) dependencies that they are comfortable maintaining themselves.
- Yoric 6y ago
  The latter. And that includes the choice of a compiler.
jacquesm 6y ago
I have the exact same mentality when it comes to projects that I intend to operate for a longer time than just throwaway try-outs. If I can't understand what's going on under the hood then I'll be happy to pass. This is a limitation, of course. But at least it keeps me on a path where I don't bite off more than I can chew. Experience has led me to believe that any dependency you have is sooner or later going to turn into a either a liability or an obligation, this makes it much easier for me to see dependencies as costs rather than just as advantages. The number of dependencies for my current project is four, and each of those (vexflow, tone.js, lovefield, jquery) I'm in principle prepared to maintain myself. Even so, all of them have already proven to be here for the longer term. Ditto for tooling.

the-smug-one 6y ago

Warning! Lots of disjointed thoughts below. I've used Frama-C ACSL+WP and it was incredibly painful to use to prove basically anything. For me the main issue was that Frama-C can say 3 things about your specs: Yes, No, and Don't know. That means I have no idea where to start to debug my proof, especially as I'm already convinced that my proof works! This is inherent to computing weakest pre-condition AFAIK. I had to provide my own loop invariants, which is also a pain :-). C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course. I haven't used the other plugins, perhaps there are better ones! Type systems can be quite nice with regards to error messages, especially as the programmer themselves essentially derive their own granularity with regards to the domain and the proofs of the domain. But yes, we all have examples of absolutely terrible type system error messages. The paradigm of making comments have semantic meaning in some other language is also terrible. I'd rather have a superset of the core language with syntactic extensions for proofs. The build system can pull out the core language source code for me. Finally: I think that abstract interpretation of a low-level compilation target combined with a proof-carrying compiler is the way to go. The compiler has proofs of a bunch of stuff regarding the code already, carry them down into the assembly level please! There's some work in abstract interpretation of WebAssembly, and I think that could be a great platform for formal verification. Sorry for the barfing :-). Hopefully there're thoughts here to react to and reply to me about!

unwind 6y ago
This: C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course. sounds really interesting, do you remember some concrete example? Not saying you're wrong or anything, just curious of what kind of code is hard to analyze like this.
- rwmj 6y ago
  I was wondering about this too. If I was going to guess I would say it could be stuff that applies to any language that uses fixed width machine types, and not only C. For example, this is not true: ∀a: a+1 > a if the type of 'a' is 32 bit int. Similarly negate(a) ≠ -a for some numbers.

quelsolaar 6y ago

We should be spending a lot less time inventing new languages and spending a lot more time working on tools for existing languages. If we did, all languages would be better, and the languages we did design would be designed to make it easy to make tools that help us use them.

MaxBarraclough 6y ago
It's not that we have to choose one of those two options. Work is still being done on static-analysis tools for C. To speak of Frama-C specifically, it isn't competing with new languages like Zig and Nim, it's competing with rival tools like [0], and with SPARK Ada. Formal reasoning about code is, for now, a niche reserved for critical-systems development. That kind of work tends to use tried-and-true languages with tried-and-true tooling: C, C++, Ada, and occasionally even Java. > the languages we did design would be designed to make it easy to make tools that help us use them. This is already a factor in language design. It's one of the reasons C-style preprocessors are now unfashionable. [0] http://www.eschertech.com/products/ http://www.eschertech.com/products/
- doonesbury 6y ago
  Agree
pjmlp 6y ago
This is already what is happening with static analyzers for C and C++, some of them even getting some Rust like ideas on the analyzers. This is important, because as much as some of us would like to nuke those languages, they aren't going away and plenty of domains are not going to move away from them anyway. However there is only so much that one can improve without changing their semantics. And if you start changing their semantics, then you end up with what is effectively another language, e.g. Checked C.

the_french 6y ago

I'm starting my PhD under the supervision of one of the Frama-C authors, if you have questions I can relay them. In general I've found deductive verification techniques interesting / promising because they free engineers of a lot of required but tedious details you'd have in ITPs. However, I think there's a LOT of room for improvement in terms of ergonomics of proof debugging. For a frequent (for me) problem when debugging invariants is conditionals that break the invariant. if i have some code doing something like while (X) { invariant { forall i. 0 <= i < N .... } if j < i A else B } But it turns out that one of the branches A, B doesn't preserve the invariant well all the provers will tell me is 'can't prove this!' it's up to you to perform the transformations that split the two cases (granted in this example it's trivial) so that you can see that only _one_ branch was failing. I think that there should be transforms that automatically do things like split the range of an interval along relevant points (aka j) to help you figure out which portions are failing. There are tons of other issues related to proof ergonomics that could be improved, the UIs are really stuck in the 90s!

mcguire 6y ago
What's the status of handling manual memory management? The last time I looked, that was a huge, gaping hole in both Spark and Frama-C provers.
- KsassPeuk 6y ago
  It depends on the verification tool you use. Eva (the abstract interpreter) has different ways to model dynamic allocation. It is thus a tradeoff to find between precision and computation time. WP does not have dynamic allocation support. This is an ongoing work, but it will not be available in the next release. Note that there are different ways to model the behavior of dynamic allocation, generally via axiomatic definitions and/or ghosts.
aidenn0 6y ago
Is frama-c still limited to single-threaded debugging? I know in the general case a context-switch is the same as "call any function anywhere in your code at any point into it" but it would be nice if it had a way for me to teach it about my expected threading invarients (e.g. prove that these objects never escape the current thread of execution).

mcguire 6y ago

Since you mentioned it, some posts I wrote a while back about Frama-C: Applied Formal Logic: Brute Force String Search https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.... Applied Formal Logic: The bug in Quick Search. https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.... Applied Formal Logic: Correctness of Quick Search. https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic...