Trustworthy Systems

Program verification in the presence of cached address translation

Authors

Hira Taqdees Syeda and Gerwin Klein

DATA61

UNSW Sydney

Abstract

Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables and translation lookaside buffers (TLBs). Controlling the TLB correctly is a fundamental security property — yet all large-scale formal OS verification projects leave the TLB as an assumption. We present a logic for reasoning about low- level programs in the presence of TLB address translation. We extract invariants and necessary conditions for correct TLB operation that mirror the informal reasoning of OS engineers. 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.

BibTeX Entry

  @inproceedings{Syeda_Klein_18,
    address          = {Oxford, UK},
    author           = {Syeda, Hira Taqdees and Klein, Gerwin},
    booktitle        = {International Conference on Interactive Theorem Proving},
    date             = {2018-7-20},
    doi              = {https://doi.org/10.1007/978-3-319-94821-8\_32},
    month            = jul,
    pages            = {542-559},
    paperurl         = {https://trustworthy.systems/publications/full_text/Syeda_Klein_18.pdf},
    publisher        = {Lecture Notes in Computer Science},
    title            = {Program Verification in the Presence of Cached Address Translation},
    volume           = {10895},
    year             = {2018}
  }

Download