Formal Reasoning Under Cached Address Translation
Formal Reasoning Under Cached Address Translation
About this item
Full title
Author / Creator
Publisher
Dordrecht: Springer Netherlands
Journal title
Language
English
Formats
Publication information
Publisher
Dordrecht: Springer Netherlands
Subjects
More information
Scope and Contents
Contents
Operating system (OS) kernels achieve isolation between user-level processes using hardware features such as multi-level page tables and translation lookaside buffers (TLBs). The TLB caches address translation, and therefore correctly controlling the TLB is a fundamental security property of OS kernels—yet all large-scale formal OS verification pro...
Alternative Titles
Full title
Formal Reasoning Under Cached Address Translation
Authors, Artists and Contributors
Author / Creator
Identifiers
Primary Identifiers
Record Identifier
TN_cdi_proquest_journals_2427393363
Permalink
https://devfeature-collection.sl.nsw.gov.au/record/TN_cdi_proquest_journals_2427393363
Other Identifiers
ISSN
0168-7433
E-ISSN
1573-0670
DOI
10.1007/s10817-019-09539-7
