Reasoning about Paging Data Structure Walks on x86-64 Machines

Shilpi Goel
ACL2 Seminar
March 3, 2015

Verification of x86 system code, like kernel routines that manage
physical memory resources, must be done at the level of physical
address space.  Memory management via paging is always enabled in
Intel's 64-bit mode, and 64-bit code can not directly access physical
memory.  Therefore, reasoning at the level of physical memory requires
reasoning about the address translations performed by the paging
mechanism that uses hierarchical data structures.  This greatly
complicates proofs of theorems like memory read-over-write that are
otherwise simple in the context of linear address space.

In this talk, I will present my ongoing effort to reason about "walks"
(or traversals) of the paging data structures.  I will briefly
describe some aspects of these data structures that make reasoning
challenging.  I will also list some key theorems about the paging
walks that need to be proved before embarking on system code
verification.