Security Reasoning for Distributed Systems with Uncertainty (CMU/Cornell Collaborative Proposal) - January 2015

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): Andre Platzer
Co-PI(s):
Researchers: Dexter Kozen (Cornell)

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)
This refers to Hard Problems, released November 2012.

Scalability & composability and resilient architecture.

We are interested in answering the question "Is my system sufficiently robust to both stochastic failures and deliberate attack"? Our methods consist of techniques that will be helpful in analyzing and synthesizing security polices for complicated systems.

Our perspective on security is data-driven. Our goal is to help build tools to manage existing hardware and software by providing new capabilities based on machine learning. As an example, our methods will allow the construction of decision support tools that can both detect anomalies and suggest (or automatically run) corrective actions in the face of anomalous events.

The principle challenge for our view of security is ensuring that we can handle the reams of data that systems generate, while being able to provide a fine-grained analysis. Methods that are not able achieve both of these goals will not be useful--either providing insufficiently accurate security advice or bombarding human operators with too many false positives. Further priorities include making sure that our methods cannot be easily defeated or manipulated by adversaries who are aware that they are facing a learning algorithm.

2) PUBLICATIONS
* Khalil Ghorbal, Jean-Baptiste Jeannin, Erik P. Zawadzki, Andre Platzer, Geoffrey J. Gordon, and Peter Capell. Hybrid theorem proving of aerospace systems: Applications and challenges. Journal of Aerospace Information Systems. 2014

This paper addresses the formal verification of an aerospace controller set in a noisy environment. While this domain does not involve security, this paper also involves trying to certify probabilistic behavior in complicated learned system. Many of the same techniques are applicable.

3) KEY HIGHLIGHTS

How can we reason about security in underspecified and uncertain environments? This project focuses on scalable optimization and proof techniques for both analyzing and synthesizing security policies. Methods focus on approximate reasoning that maintains rigorous bounds on answer quality.