Hacker News new | ask | show | jobs
by eliteraspberrie 3834 days ago
It exists. It's called 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.
3 comments
nickpsecurity 3834 days 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/

Verasco - verified, CompCert-based, static analyzer for C http://compcert.inria.fr/verasco/

Verification of LLVM transformations later work (eg Softbound or Code-pointer Integrity clone) http://repository.upenn.edu/dissertations/AAI3592852/

Extension of CompCert for verified, WCET analysis 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! :)

link
bpicolo 3834 days 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

link
ufo 3834 days ago
I don't think compcert avoids undefined behavior pitfalls. Its more of a way to protect yourself from compiler bugs.
link
nickpsecurity 3834 days 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_formali...

Here's a semantics that looks for flaws and undefined behavior:

https://www.ideals.illinois.edu/bitstream/handle/2142/34297/...

link
scott_s 3834 days ago
Agreed - I read through their website, and I saw no mention of eliminating undefined behavior.
link