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

ABOUT THE PROJECT:

In security more than in other computing disciplines, professionals depend heavily on rapid analysis of voluminous streams of data gathered by a combination of network-, file-, and system-level monitors. The data are used both to maintain a constant vigil against attacks and compromises on a target system and to improve the monitoring itself. While the focus of the security engineer is on ensuring operational security, it is our experience that the data are a gold mine of information that can be used to develop greater fundamental insight and hence a stronger scientific basis for building, monitoring, and analyzing future secure systems. The challenge lies in being able to extract the underlying models and develop methods and tools that can be the cornerstone of the next generation of disruptive technologies.

This project is taking an important step in addressing that challenge by developing scientific principles and data-driven formalisms that allow construction of dynamic situation-awareness models that are adaptive to system and environment changes (specifically, malicious attacks and accidental errors). Such models will be able (i) to identify and capture attacker actions at the system and network levels, and hence provide a way to reason about the attack independently of the vulnerabilities exploited; and (ii) to assist in reconfiguring the monitoring system (e.g., placing and dynamically configuring the detectors) to adapt detection capabilities to changes in the underlying infrastructure and to the growing sophistication of attackers. In brief, the continuous measurements and the models will form the basis of what we call execution under probation technologies.
 

OUR TEAM:

Ravishankar K. Iyer, Zbigniew Kalbarczyk, and Adam Slagell

ABOUT THE PROJECT:

The scientific objective of this project is to discover statistical models that characterize network resiliency, and develop simulation tools to test whether an existing network is resilient. Our work will show how to place questions of network connectivity resilience on a firm statistical basis, ultimately allowing one to design networks to be more resilient, formally assess the resiliency of existing networks, and formally assess the changes to resiliency achieved as modifications are introduced.

OUR TEAM:

Yuguo Chen

This project is exploring a framework for characterizing side channels that is based on an end-to-end analysis of the side channel process. As in covert channel analysis, we are using information-theoretic tools to identify the potential of a worst-case attack, rather than the success of a given ad hoc approach. However, instead of measuring the capacity of an information channel, which presumes optimal coding and thus overestimates the impact of the side channel, we are measuring the mutual information between the sensitive data and observations available to an adversary.

OUR TEAM:

researcher: Nikita Borisov
 

Cyber-Physical Systems (CPS) are vulnerable to elusive dynamics-aware attacks that subtly change local behaviors in ways that lead to large deviations in global behavior, and to system instability. The broad agenda for this project is to classify attacks on different classes of CPS based on detectability. In particular, we are identifying attacks that are impossible to detect in a given class of CPS (with reasonable resources), and we are developing detection algorithms for those that are possible. The methods developed will primarily be aimed at scenarios in which attackers have some ability to intermittently disrupt either the timing or the quality-of-service of software or communication processes, even though the processes may not have been breached in the traditional sense. Much of the work will also apply to cases where such limited disruptions are introduced physically. Our approach is based on a set of powerful technical tools that draw from and combine ideas from robust control theory, formal methods, and information theory.

OUR TEAM:

Sayan Mitra and Geir Dullerud

ABOUT THE PROJECT:

OUR TEAM:

Frank Pfenning