Securing a Compiler Transformation

Compiler transformations can be correct and yet be insecure. One example is the commonly applied optimization that removes dead (i.e., useless) store instructions, which can introduce new leaks of sensitive information. It is shown that determining a posteriori whether this transformation introduces a new leak is difficult: it is PSPACE-hard for finite-state programs, and undecidable in general. In contrast, checking correctness is in polynomial time. The alternative is to build security into the transformation; a polynomial-time algorithm for secure dead store elimination is presented and proved correct. Furthermore, a general proof technique for secure transformation is developed, and it is used to show that many compiler optimizations are indeed secure. The technique allows implementations of transformations to be tested for security at compile time. However, not all transformations are secure; in particular, it is shown that the important static single assignment optimization can introduce an information leak.