Publications

Towards End-to-End Verified Trusted Execution Environments via Verified Interface Confinement and Certified Compilers. Farzaneh Derakhshan, Zichao Zhang, Amit Vasudevan, Limin Jia. IEEE Computer Security Foundations (CSF) Symposium, 2023 (To Appear)

Formal Verification of a Mixed-Trust Synchronization Protocol. Ruben Martins, Michael McCall, Dionisio de Niz, Amit Vasudevan, Björn Andersson, Mark Klein, John P. Lehoczky, Hyoseung Kim. IEEE Real Time Networks and Systems (RTNS), 2021. [pdf]

überSpark: Practical, Provable, End-to-End Guarantees on Commodity Heterogenous Interconnected Computing Platforms. Amit Vasudevan, Petros Maniatis, Ruben Martins. ACM Special Interest Group on Operating Systems (SIGOPS) Operating Systems Review (OSR) Journal, 2020. [pdf]
Towards an Architecture for Trusted Edge IoT Security Gateways. Matt McCormack, Amit Vasudevan, Guyue Liu, Sebastián Echeverría, Kyle O’Meara, Grace A. Lewis, Vyas Sekar. USENIX Workshop on Hot Topics in Edge Computing, HotEdge, 2020. [pdf]

Practical Security Properties on Commodity Platforms: The uber eXtensible Micro-Hypervisor Framework. Amit Vasudevan. Springer Briefs in Computer Science. Springer, ISBN 978-3-030-25048-5, 2019. [pdf]
Mixed-Trust Computing for Real-Time Systems. Dionisio de Niz, Björn Andersson, Mark H. Klein, John P. Lehoczky, Amit Vasudevan, Hyoseung Kim, Gabriel A.Moreno. IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), 2019. [pdf]

Have your PI and Eat it Too: Practical Security on a Low-cost Ubiquitous Computing Platform. Amit Vasudevan, Sagar Chaki. IEEE Euro Symposium on Security and Privacy, 2018. (Best Paper Award) [pdf]

UberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. Amit Vasudevan, Sagar Chaki, Petros Maniatis, Limin Jia, Anupam Datta. USENIX Security Symposium, 2016. [pdf]

Design, Implementation and Verification of an eXtensible and Moduular Hypervisor Framework. Amit Vasudevan, Sagar Chaki, Limin Jia, Jonathan M. McCune, James Newsome, and Anupam Datta. IEEE Symposium on Security and Privacy, May 2013. [pdf]

Parametric Verification of Address Space Separation. Jason Franklin, Sagar Chaki, Anupam Datta, Jonathan M. McCune, Amit Vasudevan. Principles of Security and Trust (POST), 2012. (Best Paper Nomination) [pdf]
Building Verifiable Trusted Path on Commodity x86 Computers. Zongwei Zhou, Virgil Gligor, James Newsome, and Jonathan M. McCune. IEEE Symposium on Security and Privacy (IEEE S&P), 2012. [pdf]
Lockdown: Towards a Safe and Practical Architecture for Security Applications on Commodity Platforms. Amit Vasudevan, Bryan Parno, Ning Qu, Virgil D. Gligor, and Adrian Perrig. Proceedings of the 5th International Conference on Trust and Trustworthy Computing (TRUST), June 2012. [pdf]

TrustVisor: Efficient TCB Reduction and Attestation. Jonathan M. McCune, Yanlin Li, Ning Qu, Zongwei Zhou, Anupam Datta, Virgil Gligor, and Adrian Perrig. IEEE Symposium on Security and Privacy, May 2010. [pdf]