I am looking forward to working with motivated PhD students.
Spring 2016: Special Topics in Security: Formal Foundations of Secure
Software Security (15-811/18-739M)
Fall 2015: Introduction to Information Security (18-631/14-741)
Fall 2015: Information Security & Privacy (15-421 / 08-731 / 08-761 / 45-885 / 45-985)
Summer 2015: Elements of Browser Security (14-847)
Fall 2014: Introduction to Information Security (18-631/14-741)
Spring 2014: Network Security and Management (18-739/14-817)
I am interested in applying formal techniques to make software systems more secure, either through using language-based techniques to build provably secure software systems, or using formal logic to verify the security properties of (distributed) software systems, or developing formalisms to reason about security and privacy guarantees of software systems in the presence of adversaries.
Monitors and Blame Assignment for Higher-Order Session Types.
Limin Jia, Hannah Gommerstadt, and Frank Pfenning.
In Proceedings of 43rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) , to appear 2016.
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-15-004, 2015. [PDF]
Omar Chowdhury, Deepak Garg, Limin Jia, and Anupam Datta.
In Proceedings of ACM Conference on Computer and Communications Security (CCS) , Nov. 2015. [PDF]
A Logic of Programs with Interface-confined Code.
Limin Jia, Shayak Sen, Deepak Garg, and Anupam Datta.
In Proceedings of 28th IEEE Computer Security Foundations Symposium (CSF), July 2015. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-13-001, 2013 (updated 2015). [PDF]
Automated Verification of Safety Properties of Declarative Networking Programs.
Chen Chen, Lay Kuan Loh, Limin Jia, Wenchao Zhou, and Boon Thau Loo.
In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP), July 2015. [PDF]
Run-time monitoring and formal analysis of information flows in Chromium.
Lujo Bauer, Shaoying Cai, Limin Jia, Tim Passaro, Michael Strouchen, and Yuan Tian.
In Proceedings of the 22nd Annual Network & Distributed System Security Symposium (NDSS), Feburary 2015. [PDF]
Mechanized Network Origin and Path Authenticity Proofs.
Fuyuan Zhang, Limin Jia, Cristina Basescu, Tiffany HyunJin Kim, YihChun Hu, and Adrian Perrig.
In 21st ACM Conference on Computer and Communications Security (CCS), November 2014. [PDF]
Lightweight Source Authentication and Path Validation.
Tiffany Hyun-Jin Kim, Limin Jia, Cristina Basescu, Soo Bum Lee, Yih-Chun Hu, and Adrian Perrig.
In ACM SIGCOMM, August 2014. [PDF]
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.
Omar Chowdhury, Limin Jia, Deepak Garg, and Anupam Datta.
In 26th International Conference on Computer Aided Verification (CAV), July 2014. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-14-005, May 2014. [PDF]
Continuous Tamper-proof Logging Using TPM 2.0.
Arunesh Sinha, Limin Jia, Paul England, and Jacob R. Lorch
In 7th International Conference on Trust & Trustworthy Computing (TRUST), June 2014. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-13-008, July 2013. [PDF]
A Program Logic for Verifying Secure Routing
Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou, and Boon Thau Loo.
In IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE), June 2014. [PDF]
Long version appeared as University of Pennsylvania Technical Report, Feb. 2014. [PDF]
Privacy-Preserving Audit for Broker-Based Health
Se Eun Oh, Ji Young Chun, Limin Jia, Deepak Garg, Carl A. Gunter, and Anupam Datta.
In ACM Conference on Data and Application Security and Privacy (CODASPY), Feb. 2014. [PDF]