I apply formal methods tools to construct, test, and verify secure systems. I am particularly interested in compositional verification and bridging security guarantees across different levels of the software development stack. My recent work focuses on trusted execution environments and cryptographic protocols.
ProInspector: Uncovering Logical Bugs in Protocol Implementations
Zichao Zhang, Limin Jia, and Corina Pasareanu
In In Proceedings of the IEEE European Symposium on Security and Privacy (Euro S&P), Vienna, Austria, July 9-11, 2024., pages 617--632.
[PDF]
Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers
Farzaneh Derakhshan, Zichao Zhang, Amit Vasudevan, and Limin Jia
In Proceedings of the IEEE 36th Computer Security Foundations Symposium (CSF), Dubrovnik, Croatia, July 9-13, 2023., pages 324--339.
[PDF]
[TR]
Learning Assumptions for Verifying Cryptographic Protocols Compositionally
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina Pasareanu.
In Proceedings of the 2021 Formal Aspects of Component Software (FACS),
Virtual Event, October 28-29, 2021. pages 3--23.
[PDF]
Automating Compositional Analysis of Authentication Protocols.
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina Pasareanu.
In Proceedings of the 2020 Formal Methods in Computer Aided Design (FMCAD),
Haifa, Israel, September 21-24, 2020, pages 113--118.
[PDF]
