Towards formally verified compilation of tag-based policy enforcement. - Chris Chhak; Andrew Tolmach; Sean Noble Anderson (CPP, 2021)

Security Properties for Stack Safety. - Sean Noble Anderson; Leonidas Lampropoulos; Roberto Blanco; Benjamin C. Pierce; Andrew Tolmach (CoRR, 2021)

Formalizing Stack Safety as a Security Property. - Sean Noble Anderson; Roberto Blanco; Leonidas Lampropoulos; Benjamin C. Pierce; Andrew Tolmach (CSF, 2023)

Flexible Runtime Security Enforcement with Tagged C. - Sean Noble Anderson; Allison Naaktgeboren; Andrew Tolmach (RV, 2023)

Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor. - Zhenyang Dai; Shuang Liu; Vilhelm Sjöberg; Xupeng Li; Yu Chen 004; Wenhao Wang 001; Yuekai Jia; Sean Noble Anderson; Laila Elbeheiry; Shubham Sondhi; Yu Zhang; Zhaozhong Ni; et al. (ASPLOS (2), 2024)

Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. - Andrew Tolmach; Chris Chhak; Sean Noble Anderson (ITP, 2024)

Foundational Verification of Smart Contracts through Verified Compilation. - Vilhelm Sjöberg; Kinnari Dave; Daniel Britten; Maria A Schett; Xinyuan Sun; Qinshi Wang; Sean Noble Anderson; Steve Reeves; Zhong Shao 001 (CoRR, 2024)

Pipe-Cleaner: Flexible Fuzzing Using Security Policies. - Allison Naaktgeboren; Sean Noble Anderson; Andrew Tolmach; Greg Sullivan (CoRR, 2024)