Frama-C: Modular Analysis of C Programs

Re:Frama-C: Modular Analysis of C Programs by the-smug-one on Tuesday October 06, 2020 @08:18AM (#24696902)

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!

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by unwind on Tuesday October 06, 2020 @08:43AM (#24697077)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by rwmj on Tuesday October 06, 2020 @08:46AM (#24697105)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by ritter2a on Tuesday October 06, 2020 @09:15AM (#24697324)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by Jtsummers on Tuesday October 06, 2020 @11:07AM (#24698432)

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)

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by tom_mellior on Tuesday October 06, 2020 @12:46PM (#24699799)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by mcguire on Tuesday October 06, 2020 @12:17PM (#24699373)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by steerablesafe on Tuesday October 06, 2020 @09:12AM (#24697301)

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

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by aidenn0 on Tuesday October 06, 2020 @12:20PM (#24699417)

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)

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by dvfjsdhgfv on Tuesday October 06, 2020 @01:39PM (#24700397)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by unwind on Tuesday October 06, 2020 @09:18AM (#24697342)

Right, that makes total sense yes. Thanks.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by Chris2048 on Tuesday October 06, 2020 @11:07AM (#24698431)

could you add some modifier?

"iff a =/= MAXINT"

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by doonesbury on Tuesday October 06, 2020 @08:52AM (#24697144)

>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

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by creata on Tuesday October 06, 2020 @10:18AM (#24697866)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by Jtsummers on Tuesday October 06, 2020 @11:20AM (#24698607)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by im3w1l on Tuesday October 06, 2020 @12:01PM (#24699161)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by Jtsummers on Tuesday October 06, 2020 @12:14PM (#24699334)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by mcguire on Tuesday October 06, 2020 @12:26PM (#24699533)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by the-smug-one on Tuesday October 06, 2020 @11:36AM (#24698830)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by KsassPeuk on Wednesday October 07, 2020 @03:03AM (#24705958)

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

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by doonesbury on Tuesday October 06, 2020 @11:11AM (#24698484)

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.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by creata on Tuesday October 06, 2020 @11:25AM (#24698689)

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?

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by creata on Tuesday October 06, 2020 @10:35AM (#24698063)

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

[ Parent | on HN ]