Additional Materials for CCS 2015 submission

This companion document contains the soundness proof for Moat's type system.

sgx.bpl contains Boogie models of all SGX instructions used in Moat's proofs.

theorem1.bpl contains Boogie proof of Theorem 1.