The models and proofs in this repository requires (UCLID5)[https://github.com/uclid-org/uclid] to build and run. They can either be run directly or via the Makefiles found in the subdirectories.
Common/contains common UCLID5 code across the models and proofsTrustedAbstractPlatform/modulescontains the TAP modelsTrustedAbstractPlatform/proofscontains the proofs of Secure Remote Execution
If you use TAP and UCLID5 in your work, please cite the following:
Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas Devadas, and Sanjit A. Seshia. A Formal Foundation for Secure Remote Execution of Enclaves. [PDF] In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17). Association for Computing Machinery, New York, NY, USA, 2435–2450. 2017.
Sanjit A. Seshia and Pramod Subramanyan. UCLID5: Integrating Modeling, Verification, Synthesis and Learning. [HTML] Proceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018), Beijing, China. October 2018.