Skip to main content

TS

Program verification in the presence of cached address translation

Authors

Hira Syeda and Gerwin Klein

DATA61

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,
    publisher        = {Springer's LNCS series},
    doi              = {https://doi.org/10.1007/978-3-319-94821-8\_32},
    booktitle        = {Interactive Theorem Proving, ITP},
    author           = {Syeda, Hira and Klein, Gerwin},
    month            = jul,
    volume           = {10895},
    year             = {2018},
    date             = {2018-7-20},
    title            = {Program Verification in the Presence of Cached Address Translation},
    pages            = {542-559},
    address          = {Oxford, UK}
  }

Download

Served by Apache on Linux on seL4.