ABOUT THE PROJECT:

Making sound security decisions when designing, operating, and maintaining a complex enterprise-scope system is a challenging task. Quantitative security metrics have the potential to provide valuable insight on system security and to aid in security decisions. To produce model-based quantitative security metrics, we developed the ADversary VIew Security Evaluation (ADVISE) method and implemented it in the prototype tool Möbius-SE (Möbius Security Edition), which is suitable for use by security modeling experts. Our goal in this project is to extend the ADVISE method and tool to explicitly account for the behavior of human users as part of the system. While cyber security models traditionally model the behavior of the attacker, they usually do not explicitly account for the behavior of the users of a system, and how that use can create or eliminate system vulnerabilities.

Increasingly, accumulated cyber security data indicate that system users can play an important role in the creation or elimination of cyber security vulnerabilities. Thus, there is a need for cyber security analysis tools that take into account the actions and decisions of human users. 

We are 1) developing a Möbius-SE-compatible, process-oriented modeling formalism for modeling how human users interact with systems, using the concept of a human decision point to explicitly represent decisions that affect the security of a system; 2) implementing the formalism as an atomic model editor in Möbius-SE that generates models that can interact with other Möbius-SE models, e.g., models of the systems itself and the attacker; and 3) demonstrating the use of the implemented tool in a variety of government- and industry-motivated case studies, as suggested by our sponsor and industry partners (HP and GE).

OUR TEAM:

William H. Sanders, David M. Nicol, Jim Blythe (University of Southern California), and Sean W. Smith (Dartmouth College)

ABOUT THE PROJECT:

This project is developing a common logical framework that will account for two principal sources of trust in software: digital signatures and explicit proof. The framework will allow us to rigorously specify, enforce, and analyze security policies that rely on multiple modes and sources of trust. Based on earlier work by the PI and collaborators, the framework is being cast as a modal type theory that comes equipped with a notation for programs and proofs. We will exploit this relationship to guarantee composability (since types govern interfaces between code) and usability from the programmer's point of view (since type checking is effective during software development). The project will proceed in two phases: framework design and metatheoretic study in the first phase, and a testbed implementation in the second phase. A possible third phase may study usability from the end user's point of view.

OUR TEAM:

Frank Pfenning (CSD, CMU) and Elsa L. Gunter

ABOUT THE PROJECT:

In this project, we are formulating a formal science of securing packet forwarding in computer networks. In particular, we are developing a formal algebra of the network's data plane (packet-forwarding) operations. Our approach represents the network’s forwarding behavior and state in the form of Boolean satisfiability (SAT) clauses. Our framework enables rigorous analysis and study of the way that networks forward packets, including the ability to check correctness invariants against a specific network deployment (e.g., reachability, service quality, classification level), providing metrics that capture the degree of packet-forwarding security, and enabling the derivation of theorems about how to build networks with strong security properties on packet-forwarding behavior. We are bridging the gap between theory and practice by developing a system to directly read SAT clauses from network deployments and are building upon existing SAT solver technologies to perform automated reasoning. To speed progress, we are building upon our earlier work on using satisfiability checking for testing network reachability.

OUR TEAM:

Brighten Godfrey and Matthew Caesar

ABOUT THE PROJECT:

This project falls within the areas of control theory and game & decision theory, and aims at addressing some foundational issues. It builds on a platform of ongoing research on strategic decision‐making that accommodates elements of security, robustness, learning, and adversarial intrusion, using control‐ and game‐theoretic frameworks.

OUR TEAM:

Tamer Basar

ABOUT THE PROJECT:

Starting from the premise that cyber attacks have quantifiable objectives, our long-term goal is to develop computational tools that quickly recover the objective associated with any given attack by observing its effects. Knowledge of this objective is critical to threat assessment. It allows us to understand the scope of an attack, to predict how the attack will proceed, and to respond in a systematic and targeted way. Our approach to recovering this objective is based on a new method for solving the problem of "inverse optimal control." Much of our recent work has focused on establishing the theoretical foundations for this method of solution. In this project we are exploring its application to threat assessment.

OUR TEAM:

Timothy W. Bretl

ABOUT THE PROJECT:

The criticality of the information protection and assurance (IPA) problem has understandably sparked rich intellectual and material investment into finding a solution. Several efforts have centered on understanding, identifying, tolerating, and patching security vulnerabilities at different levels of the electronic system stack for various security attack models. Most of these approaches tend to fall into the "sand-boxing" category, whereby unusual events are sequestered until their potential impacts are identified. Such efforts tend to be directed at well-known threats, and thus require that all existing techniques be revisited as newer attack models emerge.

This project is formulating a framework for designing secure computing platforms that treat security infractions as computational errors and employ error-resiliency techniques to tolerate them, while simultaneously providing the user with alert levels based on a grading of the severity of the infractions. Our ongoing work on stochastic computing is being leveraged to provide a foundation for the framework.

OUR TEAM:

Naresh Shanbhag and Rakesh Kumar

ABOUT THE PROJECT:

In this project, we are using our invariant generation methodologies for security focused applications, like generation of invariants for a new application from the Android app store. We are investigating the science behind re-engineering a system through iterative invariant generation. We are also studying the connections between the machine-learning model used by the data mining and the finite state machine model of the program that is actually learned. We will generalize the models/abstractions obtained from this study and validate these methods of learning invariants using empirical evidence from a real security application.

OUR TEAM:

Shobha Vasudevan

ABOUT THE PROJECT:

This project is developing methods for resilient, efficient recognition of distributed attacks on clouds, data warehouses, clusters, and other massively parallel systems. Such attacks cannot usually be detected through local monitoring alone. Specifically, we are developing a probabilistic distributed temporal logic for characterizing such attacks and methods of verifying formulas in such a logic. The novel approach of combining probabilistic, distributed, and temporal operators will yield a new representation for system properties. These operators will enable us to express more sophisticated attack patterns, as well as describe a wide variety of local and global properties, ranging from performance to availability.

Using distributed operators localizes the description and supplies the necessary scalability and performance. Probabilistic reasoning adds resilience against the uncertainty inherent in parallel systems. Temporal operators provide for history-awareness and anticipation of future events. The new semantics and associated algorithms we are researching will allow for reasoning about and proving of these properties. We will prototype a compiler that translates formulas into monitoring programs that can instantly be deployed in the network.

OUR TEAM:

Gul Agha

ABOUT THE PROJECT:

Modern networked systems are large and heterogeneous, and employ a variety of access control mechanisms that are the first line of defense against cyber-attack. These mechanisms include, but are not limited to:
 

• router-based dedicated firewalls, such as the Cisco PIX series;
• host-based firewalls, which could be based in software (such as iptables in Linux, or in-built firewalls in the operating system) or hardware (such as specialized NICs);
• operating-system-based mechanisms, such as discretionary access control in Linux or Windows, or more sophisticated mechanisms, such as the mandatory access control in NSA's SELinux and similar functionality provided for Windows by the Cisco Security Agent; and
• middleware-based mechanisms, such as the Java Security Manager, that provide for specification and enforcement of fine-granularity access control policies for Java programs.

This project is addressing the problem of estimating the degree to which the actual security posture given by the configurations of these diverse mechanisms complies with machine-checkable global policy, when (1) the system is too large to admit to an exhaustive analysis, and (2) we consider the possibility of intruders creating connections through compromised hosts set up as stepping stones. The foundational science we are developing consists of application of the statistical method of importance sampling to the problem of statistically estimating metrics that quantify a system’s compliance with global policy, and to the problem of finding the hosts that, if compromised, would have the largest negative impact on accessibility compliance, under our two assumptions. The results of our research will quickly be included in an existing tool we've developed that exhaustively validates compliance. This will transition the technology into practice; furthermore, the insights we gain will have application in other security domains where the challenge is to estimate the number of rare but disastrous states in combinatorially huge state spaces.

OUR TEAM:

David M. Nicol and William H. Sanders

ABOUT THE PROJECT:

This project is investigating the existence of decision procedures for two key properties at the heart of observational equivalence, assuming the protocol's algebraic properties satisfy the finite variant property (FVP), which is satisfied by most cryptographic functions. If time permits, extensions relaxing FVP will be developed. The first such property is deducibility, that is, determining whether an attacker who has seen a sequence of messages can deduce a given message from that sequence. The second is static equivalence, that is, the ability to decide whether two sequences of messages seen by an attacker are equivalent, in the sense that there is nothing that the attacker can distinguish from one of them and not from the other. Static equivalence is key to proving observational equivalence and trace equivalence. The research is trying to develop and prove correct inference systems for these two decision procedures under the FVP assumption or some more general condition.

OUR TEAM:

José Meseguer