Frama-C: Function Contracts and Static Analysis for the C Language | Hacker News Reader

Frama-C: Function Contracts and Static Analysis for the C Language

frama-c.com

62 pointsvmorgulis14 comments

I think the era of focus on static analysis tools has begun. I think all languages are moving in this direction. We have the new C++ Core Guidelines which will eventually be compiler-enforced, there is Rust with its program-proving compiler, and there are these neat tools for C, and no doubt more will flourish in coming years. It is going to be interesting to see where it all goes.

The sad thing is that lint was created in 1979, already when C unsafety was clear.

However in the early days, only C was being ported outside UNIX (parts of it actually) and lint became something that only the ultimate versions (to use a more modern expression) had.

There was also the issue of false positives.

So very few bothered buying it.

I wonder also if that possibility of unsafety just doesn't matter much to a lot of people. After all, lisps have been around forever and even today JS and Clojure are popular when the possibility of doing unsafe things is extremely easy in a language where there are no type checks. So perhaps many developers just don't worry so much about compiler checks and instead enjoy the flexibility of "weak" or "no" typing, at the possible expense of safety. And maybe all of that is gradually changing. I really really love Clojure, but find static typing very useful; but also, it's great to throw it away when you feel confident enough to do so, and perhaps a lot of developers just like this, shall I call it "cowboy", style?

All languages allow unsafe things,if you think in terms of logic errors.

But C's unsafety leads to memory corruption as well, even for very skilled developers.

Only matched by programming in straight Assembly.

Yes that was the expression we used in 90's.

There is an interesting paper on external sound static analysis tools (verification tools like SMT and SAT solvers) in Frama-C to increase effectiveness of optimizations and generating better, in terms of performance and not just correctness, code.

http://link.springer.com/chapter/10.1007/978-3-662-46081-8_1...

You could think of types being a form of static analysis. B originally had no types. I think static analysis integrated into languages can progress as people realize there are things that they really don't want to be able to do 90% of the time.

Tutorial: http://frama-c.com/download/acsl-tutorial.pdf

Or, if you like the web: http://frama-c.com/acsl_tutorial_index.html

I wonder how it stacks up against Microsoft's SAL annotations. So far I've only used SAL annotation, with the compiler's /Analyze flag, but the amount of checking done is limited, and the system itself is far from perfect, sometimes pointing to logical errors that are clearly not there. However it is still very useful.

Maybe Frama-C is better?

Could this be considered a more elaborate Valgrind?

Frama-C can be used in "interpreter mode" where it acts like a checking C interpreter. It then catches a superset of the bugs that would be caught by Valgrind / ASan / UBSan. On the other hand it is slower and harder to use than those tools.

no, this is static and compile time while valgrind is dynamic and run time. also, the rules for the failing states for valgrind are specified ad hoc in tool code while properties of programs checked by frama-c are user extensible via the specification language

So, any experience reports?

I can recommend https://www.imperialviolet.org/2014/09/07/provers.html.

Personally, I tried to prove that a fairly simple program I had written a few years prior was free of undefined behavior. Frama-C was tantalizingly capable - it was easy to tell Frama-C what I wanted to prove, and it managed to propagate possible values and control flow through the program pretty accurately, even with minimal assistance. Although I disliked the absence of a usable text-mode integration (vim?), the GUI presented the results clearly. The Frama-C manuals were extensive, mostly up-to-date, and managed to explain even complicated concepts in a pretty clear way. (Fair warning: although I have zero background in formal methods, I have quite a lot of mathematical training and like language lawyering.)

Unfortunately, Frama-C did not grok malloc() at the time. My program consisted of I/O into malloc()'ed buffers plus some processing. Teaching Frama-C about malloc() was clearly beyond my skill. Worse, I really wanted to prove that my program output was some suitably processed form of its input data, and I didn't look forward to trying to model read()/write() - so I stopped the experiment, and planned to revisit Frama-C in a couple years.

Actual experts can apparently get much better results: Frama-C was used to prove that chunks of PolarSSL were free of certain undefined behavior (http://blog.regehr.org/archives/1261, or the actual report at http://trust-in-soft.com/polarSSL_demo.pdf). This is a limited result: huge chunks of code are out-of-bounds. Also, "PolarSSL is memory-safe" is very far from "PolarSSL is a secure SSL library". Still, I'm impressed.

I did not see a good way to integrate Frama-C in our development process. From reading and talking to some people, I am left with the distinct impression that keeping proofs up-to-date in living software is not a solved problem. Frama-C does allow you to annotate code with assertions (which, I expect, can act as hints to the provers). However, the workflow still seems to be oriented around Frama-C's interactive mode, which is very powerful but doesn't yield artifacts that can easily be reused. Also, mastering Frama-C is hard - it's not something that you can just expect a software developer to pick up.

(In contrast, the Coverity static analysis tool uses unsound analysis and can't guarantee anything. However, colleagues report that it does a decent job at finding some bugs with a low false-positive rate, especially after you add a few annotations. Coverity offers ongoing scans to open-source projects; unfortunately, Coverity's scan servers appear to be backlogged at the moment. "Not a need-to-have, but something we could consider buying.")

I use Frama-C without the GUI. The annotations do take some effort, but once you get it, it's very intuitive. Start with adding assertions, for example checking that array indices don't go out of bound. Then start with simple function specifications, and improve on them over time.

I wouldn't use it everywhere, but in small, important functions, it's well worth it.

Here's the classic example of reading into a buffer: https://github.com/eliteraspberries/ttyprompt/blob/master/ge... From those few annotations, Frama-C is able to determine that there are no buffer overflows there.

Reply on news.ycombinator.com