Getting compilers right: a reliable foundation for secure software
microsoft.com
microsoft.com
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!)
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/...
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...
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.
- 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.
Arguably a JS VM written in C++ may be vulnerable until the compiler is proven not to be.
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.
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.
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.
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.