A POSIX Filesystem for Enclaves with a Mechanized Safety Proof


New trusted computing primitives such as Intel SGX have shown the feasibility of running user-level applications in enclaves on a commodity trusted processor without trusting a large OS. The OS can compromise the integrity of an enclave by tampering with the system call return values. In fact, it has been shown that a subclass of these attacks called Iago attacks enables arbitrary logic execution in enclave programs. Existing enclave systems have very large TCB and they implement ad-hoc checks at the system call interface which are hard to verify for completeness. To this end, we present BesFS-—the first filesystem interface which provably protects integrity against a completely malicious OS. We prove 167 lemmas and 2 key theorems in 4625 lines of Coq proof scripts, which directly proves safety properties of the BesFS specification. BesFS comprises of 15 APIs with compositional safety and is expressive enough to support real applications. BesFS can serve as a reference implementation for hand-coded API checks.

Before we begin with BesFS

Software Requirements

Tested with The Coq Proof Assistant, version 8.8+alpha

Install The Coq Proof Assistant

Download the code and follow the installation instructions here.

Proof General

Alternatively, you can use Proof General IDE with Emacs to step through the proof.

Get the code

git clone

Build BesFS

make depend

make all


BesFS Team

Shweta Shinde

Shengyi Wang

Pinghai Yuan

Aquinas Hobor

Abhik Roychoudhury

Prateek Saxena


National Research Foundation

This research was partially supported by a grant from the National Research Foundation, Prime Ministers Office, Singapore under its National Cybersecurity R&D Program (TSUNAMi project, No. NRF2014NCR-NCR001-21 ) and administered by the National Cybersecurity R&D Directorate.

National Science Foundation

This material is in part based upon work supported by the National Science Foundation under Grant No. DARPA N66001-15-C-4066 and Center for Long-Term Cybersecurity. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.