Andrew Ferraiuolo’s paper titled, “Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software” is accepted for publication at SOSP 2017. This is the work that Andrew did with Andrew Baumann, Chris Hawblitzel, and Bryan Parno while he was visiting Microsoft Research as
Our paper, titled “Secure Information Flow Verification with Mutable Dependent Types“, is accepted for publication at this year’s Design Automation Conference (DAC). The paper is authored by Andrew Ferraiuolo, Weizhe Hua, Andrew Myers, and G. Edward Suh, and proposes a new
Our paper on verifying practical security architecture implementations using information flow, titled “Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis”, is accepted for publication at ASPLOS 2017.