Phenomena like Stuxnet make apparent to the public what experts knew long ago: security is not an isolated question of securing a single door against lockpicking or securing a single computer against a single hacker trying to gain access via a single network activity. Because the strength of a security system is determined by its weakest link, security is much more holistic and affects more and more elements of a system design. Most systems are not understood properly by simplistic finite-state abstractions like yes/no information about whether a node in a (sufficiently small) finite network has been compromised or not. Stuxnet, for example, is reported to have a sophisticated interaction of control affects, sensor modifications, and even exhibits hidden long-term effects on the physical world by changing the behavior of programmable logic controllers (PLCs). Moreover, security-relevant systems of today are more often than not characterized by distributed setups, both in the system and in the attack. The security analyst, furthermore, faces uncertainties that aggregate to paralytic “zero” knowledge—unless he takes a probabilistic view and quantitatively relates the relative likelihoods of symptoms and explanations via partial observations and incomplete prior knowledge. The scale and complexity of any affected system, however, makes the analysis hard. But, more crucially, it is becoming infeasible to scale between systems to craft and tune a new security analysis over and over again for each new particular application scenario.

Research

We propose to address the scale problem in security analysis by developing  representation and reasoning techniques that support higher level structure and that enable the security community to factor out common core reasoning principles from the particular elements, rules, and data facts that are specific to the application at hand. This principle, separation of reasoning engine and problem specification, has been pursued with great success in satisfiability modulo theories (SMT) solving. Probabilistic reasoning is powerful for many specific domains, but does not have any full-fledged extensions to the level of scalable higher-level representations that are truly first-order. Based on our preliminary results, we propose to develop first-order probabilistic programs and study how they can represent security analysis questions for systems with both distributed aspects and quantitative uncertainty. We propose to study instance-based methods for reasoning about first-order probabilistic programs. Instance-based methods enjoy a good trade-off between generality and efficiency. They can leverage classical advances in probabilistic reasoning for finite-dimensional representations and lift them to the full expressive and descriptive power of first-order representations. With this approach, we achieve inter-system scaling by decoupling the generics from the specifics and we hope to improve intra-system scaling by being able to combine more powerful reasoning techniques from classically disjoint domains.

Relevance

This project is of relevance to the security community, since, if successful, it would provide more general and more flexible off-the-shelve solutions that can be used to address security analysis questions for particular systems. To simplify the design of problem-specific computer-aided security analysis procedures, this project addresses a separation of the problem description from the reasoning techniques about them. At the same time, it increases representational and computational power to scale to systems with uncertainty and distributed effects.

Impact

This project has the potential to help solve security analysis questions that scale to distributed systems and the presence of uncertainty. Both aspects are central in security challenges like Stuxnet. Because each security analysis question is different, it is more economically feasible to assemble particular security analyses from suitable reasoning components. This project addresses one such component with a good trade-off between generality and efficiency.

OUR TEAM:

The project team includes Andre Platzer who is an assistant professor in the computer science department at Carnegie Mellon University. He is an expert in verification and analysis of hybrid, distributed, and stochastic dynamic systems, including cyber-physical systems. The team further includes Erik P. Zawadzki, who is a fourth year graduate student in the computer science department at Carnegie Mellon University and is developing reasoning techniques for first-order MILPs and fast propositional solvers for probabilistic model counting.

 

Compositional security is a recognized central scientific challenge for trustworthy computing. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired end-to-end security property: an adversary may exploit complex interactions between components to compromise security. Such attacks have shown up in the wild in many different settings, including web browsers and infrastructure, network protocols and infrastructure, and application and systems software. While there has been progress on understanding secure composition in some settings, such as information flow control for non-interference-style properties, cryptographic protocols, and certain classes of software systems, a number of important scientific questions pertaining to secure composition remain open. The broad goal of this project is to improve our scientific understanding of secure composition.

This project will focus on the following research directions:

Compositional Reasoning Principles for Higher-order Code. We propose to develop sound secure composition principles for trusted systems that interact with adversaries who have the capability to supply executable code to and modify code of the trusted system. We will build on prior work by Datta and collaborators on sound composition principles for trusted systems that interact with adversaries that can supply data (but not code) to tackle this problem. Theoretical Categorization of Compositionality. We will generalize from the insights acquired during the development of compositional reasoning principles and prior technical work in the computer security community on challenges in composing certain specific classes of security policies to arrive at semantic characterizations of classes of security policies that are and are not amenable to a compositional analysis. We plan to start from the security policy algebra in the prior work by Pincus and Wing, and expand the theory to larger classes of policy compositions.

Correspondence Between High-level Policies and Low-level Properties. We will develop a technical connection—a correspondence theorem—between high-level security policies (expressed either in the policy algebra or a logic) and lower level security properties expressed in our program logic. This result will connect our two lines of work and might also be useful in explaining failures of security policy composition in terms of failures of environmental assumptions.  Case Studies. We will conduct a compositional analysis of a class of systems that combine trusted computing technology and memory protection mechanisms to provide strong security guarantees against powerful adversaries. We will also revisit the real-world examples in the Pincus- Wing paper using the new formalism.

Secure software depends upon the ability of software developers to respond to security risks early in the software development process.  Despite a wealth of security requirements, often called security controls, there is a shortfall in the adoption and implementation of these requirements.  This shortfall is due to the extensive expertise and higher level cognitive skillsets required to comprehend, decompose and reassemble security requirements concepts in the context of an emerging system design.  To address this shortfall, we propose to develop two empirical methods: (1) a method to derive security requirements patterns from requirements catalogues using expert knowledge; and (2) a method to empirically evaluate these patterns for their "usability" by novice software developers against a set of common problem descriptions, including the developer's ability to formulate problems, select and instantiate patterns.  The study results will yield a framework for discovering and evaluation security requirements patterns and new scientific knowledge about the limitations of patterns-based approaches when applied by novice software developers.

Hard Problem:

Security requirements are difficult to apply in design and must incorporate system architecture, functional requirements, security policies, regulations, and standards.

OUR TEAM:

PI(s):Travis Breaux, Laurie Williams, Jianwei Niu

Mobile applications are a critical emerging segment of the software industry, and security for web-based mobile applications is of increasing concern.  We hypothesize that many of the most important security vulnerabilities in web-based mobile applications are a consequence of expressing programs at a low level of abstraction, in which important security properties are implicit and only indirectly related to code.  In order to test this hypothesis, we are building a system for expressing web-based mobile applications at a higher level of abstraction, in which security properties are made explicit through expressions of design intent, and in which those properties are more directly related to code.  We will evaluate whether such an approach can reduce or eliminate the most common vulnerabilities of web-based mobile software, while imposing a low or even negative marginal cost on developers.