Paper Info
Title
BesFS: Mechanized Proof of an Iago-Safe Filesystem for Enclaves.
Abstract
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. However, the OS can compromise the integrity of the applications via the system call interface by tampering the return values. This class of attacks (commonly referred to as Iago attacks) have been shown to be powerful enough to execute arbitrary logic in enclave programs. To this end, we present BesFS -- a formal and provably Iago-safe API specification for the filesystem subset of the POSIX interface. We prove 118 lemmas and 2 key theorems in 3676 lines of CoQ proof scripts, which directly proves safety properties of BesFS implementation. BesFS API is expressive enough to support 17 real applications we test, and this principled approach eliminates several bugs. BesFS integrates into existing SGX-enabled applications with minimal impact to TCB (less than 750 LOC), and it can serve as concrete test oracle for other hand-coded Iago-safety checks.
Year
Venue
Field
2018
arXiv: Cryptography and Security
Iago,Trusted Computing,Computer security,Computer science,Oracle,System call,POSIX,Operating system,Scripting language
DocType
Volume
Citations 
Journal
abs/1807.00477
0
PageRank 
References 
Authors
0.34
0
6
Name
Order
Citations
PageRank
Shweta Shinde11739.15
Shengyi Wang200.34
Pinghai Yuan391.86
Aquinas Hobor424317.42
Abhik Roychoudhury52449122.18
Prateek Saxena6191597.73