16 ms·

CompCert – A formally verified C compiler

185 points by cjg 8y ago

fuklief 8y ago
Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ?
- jjrh 8y ago
  https://www.absint.com/ https://www.absint.com/ is the company that sells licenses/support and they advertise: > For two decades now, Airbus France has been using our tools in the development of safety-critical avionics software for several airplane types, including the flight control software of the A380, the world’s largest passenger aircraft. https://www.absint.com/success.htm https://www.absint.com/success.htm More customers listed here.
  - jng 8y ago
    I have no idea about this specific case, but this kind of claim can be very misleading, while remaining true. Maybe they used the tooling once for an offline script of some sort, and that is all.
    - fmap 8y ago
      It's not misleading in this case. It's used in practice. You have to understand that CompCert's main competition in this space was an ancient version of GCC without any optimizations. This is mostly an issue of certification. CompCert got the same certification and is already a great improvement just by virtue of having a register allocator...
      - jng 8y ago
        Good to know, thanks for explaining. A register allocator! :)
  - throwaway0qw234 8y ago
    >> Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ? I've heard Xavier Leroy say a year or two ago that Airbus was still evaluating CompCert and was thinking of using it in production for the aircraft generation after the next one, or something like that. And that CompCert sales have been very slow in general. But here is a paper about an actual industrial user: https://hal.inria.fr/hal-01643290 https://hal.inria.fr/hal-01643290 > https://www.absint.com/success.htm https://www.absint.com/success.htm More customers listed here. AbsInt has been selling timing analysis tools for decades, and Airbus and the other customers are probably almost exclusively customers for those tools. That doesn't mean that those customers also buy CompCert. It seems like they don't.
jacquesm 8y ago
How does a project like this deal with the bootstrap problem?
- fmap 8y ago
  There's a separate project that solves this problem (CertiCoq https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/). It's making progress, but these things take time. :)
- syrak 8y ago
  It does not.
- dranov 8y ago
  CompCert doesn't do this, but CakeML, a verified compiler for a variant of ML bootstraps itself in the logic: > A unique feature of the CakeML compiler is that it is bootstrapped “in the logic” – essentially, an application of the compiler function with the compiler’s source implementation as argument is evaluated via logical inference. This bootstrapping method produces a machine code implementation of the compiler and also proves a theorem stating functional correctness of that machine code. Bootstrapping removes the need to trust an unverified code generation process. By contrast, CompCert first relies on Coq’s extraction mechanism to produce OCaml, and then relies on the OCaml compiler to produce machine code. For details, see section 11 "Compiler Bootstrapping" in http://www.cs.cmu.edu/~yongkiat/files/cakeml-jfp.pdf http://www.cs.cmu.edu/~yongkiat/files/cakeml-jfp.pdf
  - sansnomme 8y ago
    Does this guard against trusting trust attacks?
    - dranov 8y ago
      I might be mistaken, but my understanding is that it does not. You still need to trust the implementation of the logic. But if you don't trust that, you wouldn't trust the compiler correctness proof anyway, so bootstrapping in the logic does give a benefit.
als0 8y ago
One of the really nice outcomes of this approach is that it allows you to use different optimisation levels. Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation.
- monocasa 8y ago
  > Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation. sel4 verfies the binary against the specification, and lets you use optimization. Once you've extracted the flow graphs from the binary, following the optimizations isn't difficult.
  - sanxiyn 8y ago
    Yes, AutoCorres works, but it is somewhat user hostile, even for these tools, or compared to CompCert. CompCert looks and feels like a compiler, AutoCorres isn't. https://github.com/seL4/l4v/tree/master/tools/autocorres https://github.com/seL4/l4v/tree/master/tools/autocorres
m4r35n357 8y ago
See limitations in the docs.
ttul 8y ago
So when you implement a buffer overflow in your C program, you can be assured it will overflow in the manner specified.
- thekingofh 8y ago
  And that specified manner is 'Undefined'. Exactly to spec!
- pslam 8y ago
  It's just one part of the tooling, and doesn't solve program-correctness on its own. A formally verified toolchain is only really useful for projects which have pervasive mitigations against these kinds of errors. In other words, if you have a code base which has been verified to a high standard, you would also want a toolchain verified to a high standard. In an ideal world you'd have a formally verified toolchain for a language without as many deficiencies as C, but here we are.
  - pjmlp 8y ago
    Yep, where all C compilers would be Frama-C compliant, integrated into the CI/CD, and all OSes would be targeting CPUs with memory tagging like Solaris on SPARC ADI, but oh well.
- tom_mellior 8y ago
  That's both funny and true, but note that the same CompCert semantics is also the basis of a verified static analysis tool that can be used to prove the absence of such errors in C programs: http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/ If you have a program that runs successfully through both the analyzer and the compiler, you can have quite a bit of confidence in the result.
- Retra 8y ago
  I know you're being facetious, but even if your compiler is verifying that your overflows are happening correctly, it is not a stretch to see that it can report that such overflows are occurring at all and what assumptions are causing them.
marinintim 8y ago
Going to great lengths to avoid writing Rust.
- stcredzero 8y ago
  Would the world be a better place if Linux, the BSD kernel behind OS X, and the Windows kernel were all rewritten in Rust? (I don't think it would be dramatically better overnight.)
  - c1yd3i 8y ago
    It would be better overnight. But it would be even better if we had one NT like kernel and a new OS built from scratch with a browser (webkit) based ui.
    - stcredzero 8y ago
      a new OS built from scratch with a browser (webkit) based ui So basically, ChromeOS rewritten in Rust? Why not a Servo based UI?
      - cjmaria 8y ago
        The hard part is the NT-like kernel in Rust, not the web-based UI. ChromeOS uses the linux kernel.
  - sanxiyn 8y ago
    If we could do this by waving a wand without downsides (e.g. all existing maintainers magically acquire Rust knowledge, etc.), yes it would be better. No question. Seriously, people, you can find kernel bugs at will with kernel fuzzers like syzkaller from Google. Look at https://github.com/google/syzkaller/blob/master/docs/found_bugs.md https://github.com/google/syzkaller/blob/master/docs/found_b... and weep.
  - AnimalMuppet 8y ago
    If the Linux kernel writers all instantly knew Rust as well as they know C, then in 10 years they might produce something that is as functional as the Linux kernel currently is. In the process, they would lose everything that they could do over the next ten years to improve the Linux kernel. You could claim that eventually the payoff would pay back the lost 10 years. But "eventually" can be a very long time...
herodotus 8y ago
In 1983, Ken Thompson gave a Turing Award talk in which he shows how to embed a backdoor into a compiler in such a way that it would not be visible, even if you had access to the compiler source. (http://delivery.acm.org/10.1145/1290000/1283940/a1983-thompson.pdf http://delivery.acm.org/10.1145/1290000/1283940/a1983-thomps...) I wonder if the verified compiler could be altered in the same way? (A snippet from the paper so you get the idea: >We compile the modified source with the normal C compiler to produce a bugged binary. We install this binary as the official C compiler. We can now remove the bugs from the source of the compiler and the new binary will reinsert the bugs whenever it is compiled. Of course, the login command will remain bugged with no trace in source anywhere.)
- fulafel 8y ago
  As long as the compiler system is self-bootstrapping. I don't know if this is the case with CompCert C. Probably not becuse of the ML compiler tech involved, which usually doesn't bootstrap on C. But aside from these incidental properties, yes the same thing could be done. (This still leaves a large class of related, less recursively symmetric integrity attacks that could be made without the language fully bootstrapping itself, of course)
  - iaabtpbtpnn 8y ago
    The ML compiler tech is OCaml which is bootstrapped on C. (It wasn't always so, but has been since Caml Light.)
  - nickpsecurity 8y ago
    There's a new extractor that can output C from Coq. There's also multiple compilers for each language you can extract to. My solution was to do diverse compilation where multiple compilers, OS's, and ISA's compiled the compiler. Then you just run it through itself on each one. Use end result that most agree on.
    - unboxed_type 8y ago
      Are you talking about CertiCoq project? It is not ready yet and not clear when will be. [1] https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/
kazinator 8y ago
> Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. Which semantics? The ISO C semantics is rather lacking; "undefined behavior" lurks around every corner. A C compiler that correctly implements all ISO C requirements is a fine thing, and certainly better than one which gets some of that semantics wrong, but doesn't achieve all that much in the big picture. If the verified compiler actually provides extended semantics beyond ISO C that eliminates much of the undefined behavior, such that programmers using this dialect can rely on a safer language, then we're talking.
- chrisseaton 8y ago
  > doesn't achieve all that much in the big picture Bizarre way to talk about award-winning breakthrough research in applying verification to large practical programs.
  - kazinator 8y ago
    Don't mean to say that the technique isn't valuable; just the particular application (verified C compiler) not as much as other potential applications (verified ... almost anything else).
- ychen306 8y ago
  Eliminating undefined behavior from the language is a language design issue orthogonal to the problem CompCert is trying to solve.
  - deleted 8y ago
    [deleted]
- kurtisc 8y ago
  You're describing a problem already solved by MISRA C, etc., for which there are static analysis tools to allow you to ensure programmatically that you're conforming to the standard.
User23 8y ago
Sadly even a proved correct C compiler can produce incorrect behavior in a real system: https://blog.regehr.org/archives/482 https://blog.regehr.org/archives/482

185 points by cjg 8y ago

fuklief 8y ago

Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ?

jjrh 8y ago
https://www.absint.com/ https://www.absint.com/ is the company that sells licenses/support and they advertise: > For two decades now, Airbus France has been using our tools in the development of safety-critical avionics software for several airplane types, including the flight control software of the A380, the world’s largest passenger aircraft. https://www.absint.com/success.htm https://www.absint.com/success.htm More customers listed here.
- jng 8y ago
  I have no idea about this specific case, but this kind of claim can be very misleading, while remaining true. Maybe they used the tooling once for an offline script of some sort, and that is all.
  - fmap 8y ago
    It's not misleading in this case. It's used in practice. You have to understand that CompCert's main competition in this space was an ancient version of GCC without any optimizations. This is mostly an issue of certification. CompCert got the same certification and is already a great improvement just by virtue of having a register allocator...
    - jng 8y ago
      Good to know, thanks for explaining. A register allocator! :)
- throwaway0qw234 8y ago
  >> Does anyone in the industry use it ? Does anyone knows for sure that Airbus uses it ? I've heard Xavier Leroy say a year or two ago that Airbus was still evaluating CompCert and was thinking of using it in production for the aircraft generation after the next one, or something like that. And that CompCert sales have been very slow in general. But here is a paper about an actual industrial user: https://hal.inria.fr/hal-01643290 https://hal.inria.fr/hal-01643290 > https://www.absint.com/success.htm https://www.absint.com/success.htm More customers listed here. AbsInt has been selling timing analysis tools for decades, and Airbus and the other customers are probably almost exclusively customers for those tools. That doesn't mean that those customers also buy CompCert. It seems like they don't.

jacquesm 8y ago

How does a project like this deal with the bootstrap problem?

fmap 8y ago
There's a separate project that solves this problem (CertiCoq https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/). It's making progress, but these things take time. :)
syrak 8y ago
It does not.
dranov 8y ago
CompCert doesn't do this, but CakeML, a verified compiler for a variant of ML bootstraps itself in the logic: > A unique feature of the CakeML compiler is that it is bootstrapped “in the logic” – essentially, an application of the compiler function with the compiler’s source implementation as argument is evaluated via logical inference. This bootstrapping method produces a machine code implementation of the compiler and also proves a theorem stating functional correctness of that machine code. Bootstrapping removes the need to trust an unverified code generation process. By contrast, CompCert first relies on Coq’s extraction mechanism to produce OCaml, and then relies on the OCaml compiler to produce machine code. For details, see section 11 "Compiler Bootstrapping" in http://www.cs.cmu.edu/~yongkiat/files/cakeml-jfp.pdf http://www.cs.cmu.edu/~yongkiat/files/cakeml-jfp.pdf
- sansnomme 8y ago
  Does this guard against trusting trust attacks?
  - dranov 8y ago
    I might be mistaken, but my understanding is that it does not. You still need to trust the implementation of the logic. But if you don't trust that, you wouldn't trust the compiler correctness proof anyway, so bootstrapping in the logic does give a benefit.

als0 8y ago

One of the really nice outcomes of this approach is that it allows you to use different optimisation levels. Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation.

monocasa 8y ago
> Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation. sel4 verfies the binary against the specification, and lets you use optimization. Once you've extracted the flow graphs from the binary, following the optimizations isn't difficult.
- sanxiyn 8y ago
  Yes, AutoCorres works, but it is somewhat user hostile, even for these tools, or compared to CompCert. CompCert looks and feels like a compiler, AutoCorres isn't. https://github.com/seL4/l4v/tree/master/tools/autocorres https://github.com/seL4/l4v/tree/master/tools/autocorres

m4r35n357 8y ago

See limitations in the docs.

ttul 8y ago

So when you implement a buffer overflow in your C program, you can be assured it will overflow in the manner specified.

thekingofh 8y ago
And that specified manner is 'Undefined'. Exactly to spec!
pslam 8y ago
It's just one part of the tooling, and doesn't solve program-correctness on its own. A formally verified toolchain is only really useful for projects which have pervasive mitigations against these kinds of errors. In other words, if you have a code base which has been verified to a high standard, you would also want a toolchain verified to a high standard. In an ideal world you'd have a formally verified toolchain for a language without as many deficiencies as C, but here we are.
- pjmlp 8y ago
  Yep, where all C compilers would be Frama-C compliant, integrated into the CI/CD, and all OSes would be targeting CPUs with memory tagging like Solaris on SPARC ADI, but oh well.
tom_mellior 8y ago
That's both funny and true, but note that the same CompCert semantics is also the basis of a verified static analysis tool that can be used to prove the absence of such errors in C programs: http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/ If you have a program that runs successfully through both the analyzer and the compiler, you can have quite a bit of confidence in the result.
Retra 8y ago
I know you're being facetious, but even if your compiler is verifying that your overflows are happening correctly, it is not a stretch to see that it can report that such overflows are occurring at all and what assumptions are causing them.

marinintim 8y ago

Going to great lengths to avoid writing Rust.

stcredzero 8y ago
Would the world be a better place if Linux, the BSD kernel behind OS X, and the Windows kernel were all rewritten in Rust? (I don't think it would be dramatically better overnight.)
- c1yd3i 8y ago
  It would be better overnight. But it would be even better if we had one NT like kernel and a new OS built from scratch with a browser (webkit) based ui.
  - stcredzero 8y ago
    a new OS built from scratch with a browser (webkit) based ui So basically, ChromeOS rewritten in Rust? Why not a Servo based UI?
    - cjmaria 8y ago
      The hard part is the NT-like kernel in Rust, not the web-based UI. ChromeOS uses the linux kernel.
- sanxiyn 8y ago
  If we could do this by waving a wand without downsides (e.g. all existing maintainers magically acquire Rust knowledge, etc.), yes it would be better. No question. Seriously, people, you can find kernel bugs at will with kernel fuzzers like syzkaller from Google. Look at https://github.com/google/syzkaller/blob/master/docs/found_bugs.md https://github.com/google/syzkaller/blob/master/docs/found_b... and weep.
- AnimalMuppet 8y ago
  If the Linux kernel writers all instantly knew Rust as well as they know C, then in 10 years they might produce something that is as functional as the Linux kernel currently is. In the process, they would lose everything that they could do over the next ten years to improve the Linux kernel. You could claim that eventually the payoff would pay back the lost 10 years. But "eventually" can be a very long time...

herodotus 8y ago

In 1983, Ken Thompson gave a Turing Award talk in which he shows how to embed a backdoor into a compiler in such a way that it would not be visible, even if you had access to the compiler source. (http://delivery.acm.org/10.1145/1290000/1283940/a1983-thompson.pdf http://delivery.acm.org/10.1145/1290000/1283940/a1983-thomps...) I wonder if the verified compiler could be altered in the same way? (A snippet from the paper so you get the idea: >We compile the modified source with the normal C compiler to produce a bugged binary. We install this binary as the official C compiler. We can now remove the bugs from the source of the compiler and the new binary will reinsert the bugs whenever it is compiled. Of course, the login command will remain bugged with no trace in source anywhere.)

fulafel 8y ago
As long as the compiler system is self-bootstrapping. I don't know if this is the case with CompCert C. Probably not becuse of the ML compiler tech involved, which usually doesn't bootstrap on C. But aside from these incidental properties, yes the same thing could be done. (This still leaves a large class of related, less recursively symmetric integrity attacks that could be made without the language fully bootstrapping itself, of course)
- iaabtpbtpnn 8y ago
  The ML compiler tech is OCaml which is bootstrapped on C. (It wasn't always so, but has been since Caml Light.)
- nickpsecurity 8y ago
  There's a new extractor that can output C from Coq. There's also multiple compilers for each language you can extract to. My solution was to do diverse compilation where multiple compilers, OS's, and ISA's compiled the compiler. Then you just run it through itself on each one. Use end result that most agree on.
  - unboxed_type 8y ago
    Are you talking about CertiCoq project? It is not ready yet and not clear when will be. [1] https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/

kazinator 8y ago

> Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. Which semantics? The ISO C semantics is rather lacking; "undefined behavior" lurks around every corner. A C compiler that correctly implements all ISO C requirements is a fine thing, and certainly better than one which gets some of that semantics wrong, but doesn't achieve all that much in the big picture. If the verified compiler actually provides extended semantics beyond ISO C that eliminates much of the undefined behavior, such that programmers using this dialect can rely on a safer language, then we're talking.

chrisseaton 8y ago
> doesn't achieve all that much in the big picture Bizarre way to talk about award-winning breakthrough research in applying verification to large practical programs.
- kazinator 8y ago
  Don't mean to say that the technique isn't valuable; just the particular application (verified C compiler) not as much as other potential applications (verified ... almost anything else).
ychen306 8y ago
Eliminating undefined behavior from the language is a language design issue orthogonal to the problem CompCert is trying to solve.
- deleted 8y ago
  [deleted]
kurtisc 8y ago
You're describing a problem already solved by MISRA C, etc., for which there are static analysis tools to allow you to ensure programmatically that you're conforming to the standard.

User23 8y ago

Sadly even a proved correct C compiler can produce incorrect behavior in a real system: https://blog.regehr.org/archives/482 https://blog.regehr.org/archives/482