Komodo: Using verification to disentangle secure-enclave hardware from software

Scaling symbolic evaluation for automated verification of systems code with Serval

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang

27th ACM Symposium on Operating Systems Principles (SOSP) | October 2019

Best paper award, Distinguished artifact award

DOI PDF Author's Version

Komodo: Using verification to disentangle secure-enclave hardware from software

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno

26th ACM Symposium on Operating Systems Principles | October 2017

PDF DOI

Hardware is the new Software

Andrew Baumann

16th Workshop on Hot Topics in Operating Systems | May 2017

PDF DOI

Scaling symbolic evaluation for automated verification of systems code with Serval

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang

27th ACM Symposium on Operating Systems Principles (SOSP) | October 2019

Best paper award, Distinguished artifact award

DOI PDF Author's Version

Komodo: Using verification to disentangle secure-enclave hardware from software

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno

26th ACM Symposium on Operating Systems Principles | October 2017

PDF DOI

Hardware is the new Software

Andrew Baumann

16th Workshop on Hot Topics in Operating Systems | May 2017

PDF DOI

Scaling symbolic evaluation for automated verification of systems code with Serval

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang

27th ACM Symposium on Operating Systems Principles (SOSP) | October 2019

Best paper award, Distinguished artifact award

DOI PDF Author's Version

Komodo: Using verification to disentangle secure-enclave hardware from software

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno

26th ACM Symposium on Operating Systems Principles | October 2017

PDF DOI

Hardware is the new Software

Andrew Baumann

16th Workshop on Hot Topics in Operating Systems | May 2017

PDF DOI