Security Reasoning for Distributed Systems with Uncertainty (CMU/Cornell Collaborative Proposal) - October 2014

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)

HARD PROBLEM(S) ADDRESSED
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 will be helpful in designing and analyzing security polices for complicated systems.

PUBLICATIONS
Khalil Ghorbal, Jean-Baptiste Jeannin, Erik W. 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.

ACCOMPLISHMENT HIGHLIGHTS

Studied approximation procedures and error bounds for a class of linear complementarity problems (LCPs). Complementarity problems unify problems from many different domains including convex optimization, machine learning, game theory, and planning.

LCPs can find Nash equilibria in sequential and simultaneous two-player games with multiple rounds of interaction and uncertainty. LCPs can also find optimal policies of MDPs (Markov Decision Processes).
Our new approximation techniques and bounds are based on learning theory such as Rademacher complexity and Fourier basis representations.