Multi-Representational Security Modeling and Analysis

Many security failures arise from unanticipated behaviors that are inadvertently introduced by the designer at various stages of development. A protocol or a design shown to be secure at an abstract level may turn out to be susceptible to attacks when deployed on a concrete platform. Different features of a system, developed independently from one another, may unexpectedly increase the attack surface of the system when brought together. Fundamentally, there exists an inherent tension between abstraction — a key technique in design of any large system — and the complex nature of security attacks, which often involve details across multiple aspects and layers of a system. How do we resolve this tension during construction of secure systems?

In this talk, I will describe a modeling and analysis framework designed to allow developers explore alternative design decisions, and evaluate their potential impact on the security of a system. In this framework, a developer begins with an initial, abstract model of the system, and incrementally elaborates the model into a more concrete one by specifying the underlying representations of various system parts. At each iteration, a verification engine performs an automated analysis to check the system against a desired security property, and discover attacks that exploit details across multiple levels of abstraction. Our framework also contains an extensible library of domain-specific models that can be reused for analysis of multiple systems. I will discuss our experience applying the proposed framework to analyze the security of publicly deployed web systems.
Eunsuk is a postdoctoral researcher working with Prof. Stephane Lafortune at the University of Michigan, and Prof. Stavros Tripakis at the University of California, Berkeley. He completed his PhD in computer science at MIT, and a Bachelor of Software Engineering at the University of Waterloo in Canada. He is interested in software engineering, formal methods, and programming languages, with applications to security and safety-critical systems.