Security Reasoning for Distributed Systems with Uncertainty (CMU/Cornell Collaborative Proposal) - April 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 failure 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.
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.
2) PUBLICATIONS
N/A
3) KEY HIGHLIGHTS
This project has made two contributions that will help reasoning about security goals in uncertain systems. First, we described a new problem class called SAT (Zawadzki, Platzer, & Gordon, A Generalization of SAT and #SAT for Robust Policy Evaluation, 2013), which is a quantified generalization of SAT, one of the most important problems in computer science. Our extension includes both counting ( ) and search ( ) quantifiers. We demonstrated that a number of questions about the robustness and reliability of policies can be set up as SAT instances. We also gave a rigorous theoretical characterization of the problem's worst-case complexity. Furthermore, we designed an algorithm that, despite the problem class's formidable worst-case complexity, performed extremely well empirically. The empirical success was due to exploiting a type of structure that seems common in practice.
Our second contribution is ongoing work on a set of approximate optimization techniques. These techniques involve solving an optimization problem within a restricted basis of functions. This technique, called Galerkin approximation, allows problems to be solved rapidly but with some loss in solution quality. We are currently focused on applying these methods to anomaly detection problems, but hope to extend our work to policy synthesis questions shortly. Many anomaly detection and policy synthesis questions can be cast as instances of a general problem called the linear complementarity problem (LCP) (Zawadzki, Gordon, & Platzer, A Projection Algorithm for Strictly Monotone Linear Complementarity Problems, 2013). The LCP subsumes a broad class of optimization problems that include quadratic programming. We have already theoretically investigated this method, implemented a number of solvers based on these techniques, and are currently in the middle of empirical work. We are experimenting using anomaly detection LCP instances based on one-class kernel support vector machines (SVMs). One-class SVMs are used in practice to perform anomaly detection, such as in phishing detection. A second paper on this subject is in preparation.