Low-level program verification under cached address translation

Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables. The hardware-implemented translation lookaside buffer (TLB) caches page table walks, and therefore the TLB and its consistency with memory are security critical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified kernels currently leave the TLB as an assumption. They assume correct TLB management because faithfully modeling the hardware details of a TLB would significantly complicate the program logic used to verify the OS code. For instance, a simple memory read operation would now change the state of the program. In this thesis, we present a formal model of the memory management unit (MMU) in the interactive proof assistant Isabelle/HOL for the ARMv7-A architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU using data refinement for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks. Based on the verified abstraction of the MMU model of the ARMv7-A architecture, we present a logic in Isabelle/HOL for reasoning about low-level programs in the presence of cached address translation. We extract invariants and necessary conditions for correct TLB operation that mirror the informal reasoning of OS engineers. We show that our program logic reduces to a standard logic for user-level reasoning, reduces to side-condition checks for kernel-level reasoning, and can handle typical OS kernel tasks such as context switching and page table manipulations. This research removes the unnecessary TLB complexities from program reasoning, and provides a reasoning framework for validating TLB management in OS kernel verification