A Formally Verified Compiler for Programs that Deal with Cached Address Translation

Abstract

Security in modern operating systems ultimately relies on the paging mechanism of the processor, which in turn relies upon the translation lookaside buffer (TLB). One method of showing the correctness of operating systems is formal verification, but previous work has left the correctness of the TLB as an assumption. Later work on the correctness of the TLB and high-level languages respectively leaves a gap. In this report, we investigate how to develop and verify a compiler that preserves the TLB consistency of high-level languages, bridging the gap. We describe the considerations when implementing such a compiler, the roadblocks encountered, and the result. We end with stating the compiler correctness theorem and then discuss the state of the compiler and future work.