Sean Anderson

A security policy definition framework for the C programming language that uses a tag-based runtime monitor embedded in formal C language semantics. This project forms the core of my PhD thesis. I developed the semantics by extending those of CompCert C, modified the accompanying C interpreter, and proved the soundness and completeness of the interpreter. I have also used this framework to define and verify the correctness of a compartmentalization policy.

How can we know when the stack is protected from attack? Numerous protection mechanisms promise stack safety, but there had been no rigorous, formal definition until I formalized this one. This theory-oriented project was published at Computer Security Foundations in 2023. It was a joint work with four co-authors. I came up with the key concepts of formalism and was the primary driver of the work, and implemented randomized property-based testing (a form of fuzzing) to show that a specific secure hardware mechanism could successfully enforce stack safety.

HyperEnclave is a page-table-based trusted execution environment (TEE) written in Rust. As a CertiK research and development intern, I played a central role in verifying the isolation of enclaves within the system. I formalized the top-level theorem in Coq and sketched the overall proof structure. At the time, Rust had no published formal semantics, and I was responsible for writing the language model that we used to prove correctness. I also led a group of four interns in the proofs of functional correctness for pieces of Rust code, also using Coq. In the process, I became deeply familiar with Ltac metaprogramming, as I kept track of my team's friction points and wrote about Ltac tactics to help smooth the proof process. This work was eventually published in ASPLOS '24.