logoalt Hacker News

johnbendertoday at 4:49 PM0 repliesview on HN

A 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.

Separately there is the problem of “what is observable?” For example, if you include timing in your observable behaviors suddenly the kinds of compiler passes that are able to preserve observations tends to zero rather quickly.