Colloquium - Specifying and Verifying Compilation of Secure C to Tagged Hardware
Nov 12, 2021
04:00 PM - 05:00 PM
The C language's lack of type and memory safety continues to be a major source of exploitable vulnerabilities in critical software systems. In recent years, there has been increasing interest in using hardware to help mitigate C's safety problems. In one promising approach, called PIPE, the processor is modified to attach metadata tags to the values flowing through memory and registers and to perform per-instruction monitoring to ensure that values are used correctly. Tagging and monitoring are software-configurable, allowing PIPE to enforce both basic language-level safety and higher-level security properties such as information flow control or compartmentalization in support of least privilege.
But to be confident that this approach provides the source-level security properties that we want, we must be certain that the PIPE-enhanced machine-level code is generated correctly. In this talk, I will describe work being done at Portland State to use formal specification and mechanized compiler verification to approach this goal. In particular, I will focus on how several different notions of stack and control-flow safety can be specified and verifiably enforced.
This is joint work with Sean Anderson and CHR Chhak.
Andrew Tolmach is Professor of Computer Science at Portland State University. His research interests are in functional programming languages, verification, compilers, tools, and applications, with a focus on high-assurance software environments. He teaches courses in programming languages, compilers, semantics, and theorem proving.
Passcode: 583807; Video-off please during talk.
[Click on image below ? for talk recording]
Individuals with disabilities are encouraged to attend all University of Iowa–sponsored events. If you are a person with a disability who requires a reasonable accommodation in order to participate in this program, please contact in advance at