Compiler Can Undo Your Security Checks

The key problem is that compilation operates on an implicit (compiler writers have this in the back of their heads) notion of correctness which is very roughly “preservation of observable behaviors” where “observable” is sequences of system calls and then return value. That is, the final output of a compiler should never add new sequences of observable behaviors.

Security properties on the other hand are very often about the relationship between these sequences. For example we like to say that an external observer/attacker can’t distinguish internal state by the external observations (confidentiality) which requires that two observable traces given different hidden values don’t have different observations from the same starting observable state.

If you’re an LTS nerd you know this difference as trace properties vs hyper properties. Compilers try to preserve the former but not the latter.

Title should be "Your C compiler can undo your security checks".

The compiler is allowed to transform your code if it can prove that the result would interact with the outside world in exactly the same way as your original code would, right? You can optimize on "I already checked the value of X" if you can prove that nothing could have changed X.

Well, it sounds like a lot of compilers are making unjustified assumptions about what the outside world is allowed to affect or observe. Maybe with the encouragement of specs, maybe not.

Compiler does what I tell it. Not the other way around.