back
19 comments
For C and C++, the cost of proving a compiler correct seems hugely out of proportion to the actual benefit gained from doing so. Most critical security bugs in C++ code are found in code that the compiler had no obligations whatsoever to compile "properly", because they are the result of undefined behavior (use after free, buffer overflows, stray writes, etc.) A perfect, proven-correct C++ compiler would do nothing to protect against any of the famous vulnerabilities you've heard of. Even the famous "null check eliminated by a GCC optimization" Linux kernel bug would be unaffected, as that was a valid optimization per the language definition.

By contrast, I think JavaScript VMs are the target of miscompilation attacks many of orders of magnitude more often than C++ compilers are. They actually have to compile untrusted and hostile code. A miscompilation can be disastrous, and in fact actual browser vulnerabilities have traced back to incorrect JS compilation. So I feel this impressive research might have a more practical impact if applied to JS (or Web Assembly!)

If you look at the actual papers [1, 2] they don't mention security even once. I believe the security angle was just a PR spin added to the blog post.

This is a tool for compiler writers to reason about the correctness of optimizations, and as such I believe it is useful to unlock more and more sophisticated optimization techniques. I agree that this has no impact on secure code.

[1] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf

[2] https://www.microsoft.com/en-us/research/wp-content/uploads/...

Yeah, as a testcase generator that sounds useful to help compiler developers move faster.
One of the cool proofs that comes with sel4 IIRC is that it doesn't invoke undefined behavior. And since it does end to end validation, the proof would fail if the generated binary doesn't perform stuff like null checks when they are specified by the abstract specification written along side the kernel itself.

IMO taking the compiler out of the trusted computing base is the way to go.

> IMO taking the compiler out of the trusted computing base is the way to go.

That is the point of compiler verification after all.

I'm biased here, but I think that another important point is to work out what the specification of a compiler is in the first place. Obviously, we've made a poor job of communicating this for C/C++, since so many people write broken code...

The KCC compiler will crash/stall on a program if it detects undefined behavior. Those willing to accept the penalty or separately verify those structures needing it can still benefit. If they need the performance & won't just do assembly, then they won't use such a tool as you said. That's why formal, equivalence checks for optimizing compilers are important. Need that work finished fast since it might help here.
Undefined behavior isn't something that can be detected. Any addition of signed integers might be undefined behavior. What UB means is the compiler can apply transformations only correct in the range where UB doesn't happen.
I presume that KCC in question is https://github.com/kframework/c-semantics, i.e., a formalization of C programming language in a form suitable for evaluation. It indeed can detect undefined behaviour, though last time I played with it (a few years ago) it was hardly something that you can use on anything but trivial examples. Not to mention that it crashed on various implementation defined behaviours (for example comparing unrelated pointers with <) limiting its usefulness even further.

BTW, both gcc and clang contain runtime checker for easily detectable undefined behaviours like singed overflow you have mentioned. You can enable it with -fsanitize=undefined.

You really think the cost for C and C++ are similar or comparable enough to lump both languages in the same category? Have you looked at or reviewed CompCert C compiler (and a handful of other C compiler projects, as opposed to practically zero such projects for C++ that I know of)?
For both languages, the number of security-relevant issues in the wild caused by undefined behavior far exceeds the number of such issues caused by compiler bugs. Yes, C++ compilers are much harder to write, but the number of actual security problems caused by genuine C++ miscompilations is still a relative drop in the bucket.
Even if I buy what you said, it means the following:

- C compiler correctness verification cost _is not_ out of proportion of its benefits, by virtue of the verification being very doable (and done already multiple times). In other words, low cost, low benefit. (though I seriously doubt your 'low benefit' claim and I think security, and guarding against undefined behavior, is easier to enforce through verified implementations, because it makes modifying compiler behavior more efficient, but let's stick to what you said).

- C++ compiler correctness verification cost _is_ out of proportion (high cost, low benefit)

- JS compiler/interpreter correctness verification cost is not out of proportion of its benefits, by virtue of existing JS implementations being very buggy. (high cost, high benefit).

This still leaves your original comment inconsistent with what you just said.

A good compiler might define its behavior. Just because the spec leaves things undefined doesn't mean the compiler should.

Arguably a JS VM written in C++ may be vulnerable until the compiler is proven not to be.

> A good compiler might define its behavior. Just because the spec leaves things undefined doesn't mean the compiler should.

All indications are that it's not possible to eliminate undefined behavior from C and C++ without significantly regressing performance.

> Arguably a JS VM written in C++ may be vulnerable until the compiler is proven not to be.

Vulnerabilities in JS engines are enormously more likely to be the result of undefined behavior in C++ than the result of C++ compiler miscompilations. As I said, eliminating miscompilations in LLVM/clang does nothing to address the problems of C++ UB.

Defining undefined behavior is very different from eliminating it. Every time a compiler compiles code that could potentially invoke UB, it defines what the UB means in that context.

If you make the specific way the compiler handles certain cases of UB part of the spec (e.g. overflow wraps around, who cares about sign-magnitude anyway?), then programmers using that compiler can rely on these specifics to write code that does something sensible even when UB is invoked.

The compiled code is also a lot slower. https://www.cis.upenn.edu/acg/softbound/
Only if you want to define the undefined behavior to be safe. If you define out-of-bounds writes to lead to memory corruption, your compiled code doesn't get any slower.

My point is that you can write your compiler spec to make explicit how exactly various kinds of UB are actually implemented, which then allows you to program to that spec and know that e.g. your overflowing bounds check is not completely eliminated from the program, but instead compiled into the machine instructions you had in mind.

If a compiler is verified to conform to such a specification, unintended changes in handling UB will be very obvious, since the spec will have to be changed to make the verification go through.

> If you define out-of-bounds writes to lead to memory corruption, your compiled code doesn't get any slower.

Yes, it does, because some optimizations now become invalid. For example, a compiler would no longer allowed to delete a provably out-of-bounds write. This happens all the time.

I don't think there's a lot of practical value in changing the definition of some kinds of undefined behavior to "memory corruption" (however defined) in the first place.

It only seems like a small problem because these compilers have been bug-free so far. The bugs you mention only affect certain applications. A buggy C++ compiler would affect almost every application ever created. JavaScript VMs are written in C++. This argument seems kinda like "no we don't need a tsunami warning system because no tsunami has hit us yet".
CompCert, CakeML, Simpl/C, VeLLVM, and SPARK Ada are the related reading for those interested in this sort of thing. The others naturally fit the topic with SPARK being a mature tool for verifying imperative algorithms.