5 ms·

It exists. It's called CompCert. https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert It's free for non-commercial use. I've used it for seve

It exists. It's called CompCert. https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert It's free for non-commercial use. I've used it for several months now to build things like Tor. I haven't noticed any disadvantage compared to GCC or Clang.

bpicolo 11y ago
> the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code that suggests to me you could still hit C's undefined behaviors. It's only guaranteeing the semantic equivalence between source and output
ufo 11y ago
I don't think compcert avoids undefined behavior pitfalls. Its more of a way to protect yourself from compiler bugs.
- scott_s 11y ago
  Agreed - I read through their website, and I saw no mention of eliminating undefined behavior.
- nickpsecurity 11y ago
  It's a verified subset of the C standard rather than all behaviors of all compilers. There's some semantics and work covering a lot of that already that just needs to be integrated into CompCert or static analyzers. Likewise, there's static analyzers that already cover it too but not formally verified. Here's an example of investigating that with Compcert: http://robbertkrebbers.nl/research/articles/compcert_formalin.pdf http://robbertkrebbers.nl/research/articles/compcert_formali... Here's a semantics that looks for flaws and undefined behavior: https://www.ideals.illinois.edu/bitstream/handle/2142/34297/Ellison_Charles.pdf?sequence=1 https://www.ideals.illinois.edu/bitstream/handle/2142/34297/...
nickpsecurity 11y ago
You beat me to it. Unlike the other commenters, I see that you're describing it as a robust, predictable start to what Bernstein describes. Undefined behavior and other problems can be caught by extensions to the compiler or via static analysis tools like an Astree Analyzer knockoff. The fact that they'll be written in Ocaml (or SML) will make them more reliable. A good choice and what I've promoted here so far. Additionally, the clean passes are easier to bootstrap for those that fear subversion of their compiler. Can use whatever you want on whatever machine to implement it. So long as code matches spec, the output should be the same. That implementation compiles the other compilers, verifiers, whatever. You might also enjoy that people have already extended CompCert work and others for developments that push in the Boring, Safe/Secure, C compiler direction. Here's some: CakeML - Compile CompCert, etc with this https://cakeml.org/ https://cakeml.org/ Verasco - verified, CompCert-based, static analyzer for C http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/ Verification of LLVM transformations later work (eg Softbound or Code-pointer Integrity clone) http://repository.upenn.edu/dissertations/AAI3592852/ http://repository.upenn.edu/dissertations/AAI3592852/ Extension of CompCert for verified, WCET analysis https://hal.inria.fr/hal-01087194 https://hal.inria.fr/hal-01087194 So, lots of good stuff being done by a subset that focus on right design methods with the right tools. And they're getting incredible results. Surprise! :)

bpicolo 11y ago

> the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code that suggests to me you could still hit C's undefined behaviors. It's only guaranteeing the semantic equivalence between source and output

ufo 11y ago

I don't think compcert avoids undefined behavior pitfalls. Its more of a way to protect yourself from compiler bugs.

scott_s 11y ago
Agreed - I read through their website, and I saw no mention of eliminating undefined behavior.
nickpsecurity 11y ago
It's a verified subset of the C standard rather than all behaviors of all compilers. There's some semantics and work covering a lot of that already that just needs to be integrated into CompCert or static analyzers. Likewise, there's static analyzers that already cover it too but not formally verified. Here's an example of investigating that with Compcert: http://robbertkrebbers.nl/research/articles/compcert_formalin.pdf http://robbertkrebbers.nl/research/articles/compcert_formali... Here's a semantics that looks for flaws and undefined behavior: https://www.ideals.illinois.edu/bitstream/handle/2142/34297/Ellison_Charles.pdf?sequence=1 https://www.ideals.illinois.edu/bitstream/handle/2142/34297/...

nickpsecurity 11y ago

You beat me to it. Unlike the other commenters, I see that you're describing it as a robust, predictable start to what Bernstein describes. Undefined behavior and other problems can be caught by extensions to the compiler or via static analysis tools like an Astree Analyzer knockoff. The fact that they'll be written in Ocaml (or SML) will make them more reliable. A good choice and what I've promoted here so far. Additionally, the clean passes are easier to bootstrap for those that fear subversion of their compiler. Can use whatever you want on whatever machine to implement it. So long as code matches spec, the output should be the same. That implementation compiles the other compilers, verifiers, whatever. You might also enjoy that people have already extended CompCert work and others for developments that push in the Boring, Safe/Secure, C compiler direction. Here's some: CakeML - Compile CompCert, etc with this https://cakeml.org/ https://cakeml.org/ Verasco - verified, CompCert-based, static analyzer for C http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/ Verification of LLVM transformations later work (eg Softbound or Code-pointer Integrity clone) http://repository.upenn.edu/dissertations/AAI3592852/ http://repository.upenn.edu/dissertations/AAI3592852/ Extension of CompCert for verified, WCET analysis https://hal.inria.fr/hal-01087194 https://hal.inria.fr/hal-01087194 So, lots of good stuff being done by a subset that focus on right design methods with the right tools. And they're getting incredible results. Surprise! :)