Frama-C: Modular Analysis of C Programs | Hacker News Reader

Frama-C: Modular Analysis of C Programs

frama-c.com

103 pointsjohlo39 comments

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!

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.

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.

Having written test cases for a similar semantic program analysis tool, I agree: Integer overflow is a very likely cause for such "obviously correct but actually wrong" program invariants. The C semantics can make this problem even worse since signed integer overflow is undefined, leaving the user of such a framework to the mercy of the design decisions of the creators of the framework regarding undefined behavior.

In SPARK/Ada you'd have to constrain the input for something like that or it wouldn't be able to discharge the proof. Suppose you wanted a simple function (which is too simple to write in reality, but for brevity):

  function Increment(A : Integer) return Integer
    with Post => Increment'Result = A + 1;

It would find the counterexample for the situation where A is equal to Integer'Last. So you'd need to add a precondition like:

  function Increment(A : Integer) return Integer
    with Pre => A < Integer'Last,
         Post => Increment'Result = A + 1;

(doing this from memory and not fluent, so syntax may be off but the idea isn't)

You can do that in Frama-C as well. But now this new precondition must be propagated somewhere. For example, if you have some function (syntax from memory as well):

    /*@ ensures \result > a; */
    int increment(int a) {
        return a + 1;
    }

you would change it to:

    /*@ requires a < INT_MAX;
        ensures \result > a; */
    int increment(int a) {
        return a + 1;
    }

But if this function has N call sites, you now have N problems: At every call site you must prove that the precondition holds.

Frama-C has a wp plugin that generates assertions about overflow and underflow, which is one of the best tools it has. It's not spectacular about telling you where the problem is, and wasn't great with floats, though.

Note that it's especially nasty in C, because it's either true or undefined behavior due to signed integer overflow.

Complicating it even more, if "a" is a signed-integer than the compiler will assume that statement holds and optimize accordingly, put your correctness prover would instead need to flag that (or add the caveat that a < INT_MAX)

If I remember correctly, in ANSI C int is guaranteed to have the maximum value of only 65,535 when unsigned, so basically bounds checking is a must. Of course it's even more important for shorter types like char.

Right, that makes total sense yes. Thanks.

could you add some modifier?

"iff a =/= MAXINT"

>I had to provide my own loop invariants, which is also a pain

You either make your spec up as you go along and don't check it as its hidden in the code, or provide it so that static analysis tools and/or things like tla+ can help confirm. There never was any getting around that regardless of language. The code follows from spec which both follow from requirements

The loop invariants aren't part of the spec, they're part of the proof, and the computer's job is to automate as much of the proof as it can. That being said, automatically finding loop invariants is a hard and messy problem, so I can't really blame the Frama-C authors.

The loop invariants that you can detect may not be the loop invariants that they want. Consider:

  for(int i = 0; i < n; i++) {..}

It looks like the invariant should be:

  0 <= i < n

But if they mistyped the loop that would be wrong. You have to explicitly state your invariants. At best, you could detect them and ask for confirmation. And that's for an easy to detect case.

This sounds like an invariant even an optimizing compiler could find, because it's such a common construct. Well... I guess they have an easier job because they can "assume away" signed overflow.

My point was that that may not be the actual invariant. By making your invariants explicit these tools have a better chance of finding real errors since you compare the code against a specification. Deriving a specification just means your code works according to itself.

Presumably, you are doing something other than just incrementing i in the loop, though.

Most of the time with Frama-C, all you have to provide is function pre- and post-conditions and loop invariants.

What programs can do is "loop invariant synthesis" (for people that want to google it), this is still quite tricky to do. There's a reason that humans also find loop invariants tricky.

In fact that would be

``` 0 <= i <= n ```

As the loop reaches this value to terminate. Else, we could not deduce for example that `i = n` at the end of the loop (`0 <= i <= n && !(i < n)`).

Wait - what are you arguing? That Frama or some other code can come up with loop invariants by itself from the code? Even if this is true and doable, it's bad. The question always was: does the code satisfy the spec, not whether we can derive a spec from the code and prove the spec is valid. In the other case - no - it's just what I wrote above.

What? The loop invariants aren't part of the spec! The loop invariants are just an intermediate step in your proof that the preconditions are enough to guarantee that the postconditions will hold.

If I was proving that 0 + 1 + .. n = n(n+1)/2, I wouldn't say that whatever induction step I chose to use was "part of the theorem", would I?

What kind of properties did you use Frama-C to verify?

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!

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

Note that most Frama-C analysis are not debugging tools. Although you can find bugs with them, they mostly focus on proving that there are no bugs, which is slightly different.

There are plugins for multi-thread programs.

One is an experimental plugin called Conc2Seq that I developed during my thesis with a focus on proving properties about small modules with a few functions accessing concurrently some global resources. Note however hat it is very experimental and it is not actively developed anymore, but at least it can be updated or give some ideas on how to write such an analyzer.

The second is a proprietary plugin called MThread (base on the Eva analysis of Frama-C), but it is only available via licensing.

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.

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.

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

Applied Formal Logic: The bug in Quick Search. 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-quic...

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

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.

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

Isn't that "all of open source" or do they mean something quite narrow by "could be patched by the maintainers of Frama-C"?

The latter. And that includes the choice of a compiler.

It seems like they mean that the Frama-C maintainers only use (and vendor) dependencies that they are comfortable maintaining themselves.

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.

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.

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/

Agree

Reply on news.ycombinator.com