Generating Correct Initial Page Tables from Formal Hardware Descriptions

Authors

Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe and Daniel Schwyn

Venue

Proceedings of the 11th Workshop on Programming Languages and Operating Systems (PLOS'21)

Links

[ .doi ] [ .pdf ] [ .bib ]

Abstract

Modern hardware platforms are increasingly complex and heterogeneous. System software uses a hodgepodge of different mechanisms and representations to express the memory topology of the target platform. Considerable maintenance effort is required to keep them in sync while often sharing is impossible due to hard-coded values. Incorrect platform-specific values in the hardware initialization sequence can lead to security critical and hard-to-find bugs because of misconfigured translation hardware, inaccessible devices, or the use of bad pointers.

We present a better way for system software to express and initialize memory hardware. We adopt an existing, powerful hardware description language, and efficiently compile it to generate correct initial page tables and memory maps for OS kernels and firmware from a single system description.

We evaluate our system on multiple architectures and platforms, and demonstrate that we can use the generated data structures to successfully initialize translation hardware, devices, memory maps, and allocators enabling easy support of new hardware platforms.

Bibtex

@inproceedings{Achermann:2021:GCIP,
 author = {Achermann, Reto and Cock, David and Haecki, Roni and Hossle, Nora and Humbel, Lukas and Roscoe, Timothy and Schwyn, Daniel},
 booktitle = {Proceedings of the 11th Workshop on Programming Languages and Operating Systems},
 doi = {10.1145/3477113.3487270},
 id = {Achermann:2021:GCIP},
 isbn = {9781450387071},
 location = {Virtual Event, Germany},
 pages = {69–75},
 publisher = {Association for Computing Machinery},
 series = {PLOS'21},
 title = {Generating Correct Initial Page Tables from Formal Hardware Descriptions},
 url = {https://doi.org/10.1145/3477113.3487270},
 year = {2021}
}

Contact

The University of British Columbia
Department of Computer Science
2366 Main Mall
ICICS Building, Office 341
Vancouver, BC V6T 1Z4
Canada

achreto [at] cs.ubc.ca
+1 604 827 2446