5 ms·

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

62 points by vmorgulis 11y ago

vmorgulis 11y ago
Tutorial: http://frama-c.com/download/acsl-tutorial.pdf http://frama-c.com/download/acsl-tutorial.pdf
- emikulic 11y ago
  Or, if you like the web: http://frama-c.com/acsl_tutorial_index.html http://frama-c.com/acsl_tutorial_index.html
deleted 11y ago
[deleted]
kensai 11y ago
Could this be considered a more elaborate Valgrind?
- munin 11y ago
  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
- regehr 11y ago
  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.
hellofunk 11y ago
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.
- pjmlp 11y ago
  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.
  - hellofunk 11y ago
    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?
    - pjmlp 11y ago
      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.
- fmarch 11y ago
  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_17 http://link.springer.com/chapter/10.1007/978-3-662-46081-8_1...
- CyberDildonics 11y ago
  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.
ekr 11y ago
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?
JoachimSchipper 11y ago
So, any experience reports? I can recommend https://www.imperialviolet.org/2014/09/07/provers.html 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 http://blog.regehr.org/archives/1261, or the actual report at http://trust-in-soft.com/polarSSL_demo.pdf 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.")

62 points by vmorgulis 11y ago

vmorgulis 11y ago

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

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

deleted 11y ago

[deleted]

kensai 11y ago

Could this be considered a more elaborate Valgrind?

munin 11y ago
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
regehr 11y ago
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.

hellofunk 11y ago

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.

pjmlp 11y ago
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.
- hellofunk 11y ago
  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?
  - pjmlp 11y ago
    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.
fmarch 11y ago
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_17 http://link.springer.com/chapter/10.1007/978-3-662-46081-8_1...
CyberDildonics 11y ago
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.

ekr 11y ago

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?

JoachimSchipper 11y ago

So, any experience reports? I can recommend https://www.imperialviolet.org/2014/09/07/provers.html 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 http://blog.regehr.org/archives/1261, or the actual report at http://trust-in-soft.com/polarSSL_demo.pdf 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.")