Limin Jia      Dr. Limin Jia
Assistant Research Professor
Electrical and Computer Engineering Department and
Information Networking Institute
Carnegie Mellon University
"Proving systems secure against adversaries"
Thursday, October 16, 4:00 PM
Packard Lab, Room 466

Abstract:  A system can be secure only relative to the specific capabilities of an attacker. One key component of formally analyzing a system's security properties is to model and reason about the adversary. In this talk, I will discuss compositional reasoning principles for analyzing systems' security guarantees. I will present our recent work on applying these techniques to verifying the origin and path authenticity properties of a new secure network protocol that we designed. Our proofs are constructed using an interactive theorem prover, Coq, and thus are fully machine verifiable. In the second part of the talk, I will discuss our work on designing new reasoning principles to analyze more powerful adversaries: ones that can supply code to be executed by trusted system components. Examples of these adversaries include malicious scripts on web pages and untrusted devices and guest OSes on top of a hypervisor.

Bio:   Limin Jia is an Assistant Research Professor at ECE & INI at Carnegie Mellon University. She received her B.E. in Computer Science and Engineering from the University of Science and Technology of China and her Ph.D. in Computer Science from Princeton University. Limin's research focuses on formal aspects of security, and her research interests include language-based security, programming languages, logic, and program verification. She is particularly interested in applying language-based security techniques as well as formal logic to model and verify security properties of software systems.

© 2014-2016 Computer Science and Engineering, P.C. Rossin College of Engineering & Applied Science, Lehigh University, Bethlehem PA 18015.