Proving Systems Secure Against Adversaries

ECE Seminar: Proving Systems Secure Against Adversaries

Starts at: October 2, 2014 4:00 PM

Ends at: 5:00 PM

Location: Scaife Hall 125

Speaker: Limin Jia

Affiliation: Carnegie Mellon University

Refreshments provided: Yes



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.


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.