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

ABOUT THE PROJECT:

OUR TEAM:

Norman Sadeh

ABOUT THE PROJECT:

OUR TEAM:

Garth Gibson

Our ability to design appropriate information security mechanisms and sound security policies depends on our understanding of how end-users actually behave. To improve this understanding, we will establish a large panel of end-users whose complete online behavior will be captured, monitored, and analyzed over an extended period of time. Establishing such a panel will require the design of sound measurement methodologies, while paying particular attention to the protection of end-users' confidential information. Once established, our panel will offer an unprecedented window on real-time, real-life security and privacy behavior "in the wild." The panel will combine tracking, experimental, and survey data, and will provide a foundation on which sound models of both user and attacker behavior can rest. These models will lead to the scientific design of intervention policies and technical countermeasures against security threats. In other words, in addition to academic research, this research will also lead to actionable recommendations for policy makers and firms.

An important emerging trend in the engineering of complex software-based systems is the ability to incorporate self-adaptive capabilities. Such systems typically include a set of monitoring mechanisms that allow a control layer to observe the running behavior of a target system and its environment, and then repair the system when problems are detected. Substantial results in applying these concepts have emerged over the past decade, addressing quality dimensions such as reliability, performance, and database optimization.  In particular, at Carnegie Mellon we have shown how architectural models, updated at runtime, can form the basis for effective and scalable problem detection and correction. However, to-date relatively little research has been done to apply these techniques to support detection of security-related problems and identification of remedial actions. In this project we propose to develop scientific foundations, as well as practical tools and techniques, to support self-securing systems, focusing specifically on questions of scalable assurance.

OUR QUALIFICATIONS:

Prof. David Garlan and Dr. Bradley Schmerl have been working in the area of architecture-based self-adaptation for over a decade. They have developed both foundations and tools – specifically, a platform called “Rainbow” – that are considered seminal work in this area of architecture-based adaptation. Ivan Ruchkin is a Ph.D. candidate working under the direction of Prof. Garlan in the area of formal modeling of dynamic changes in systems from an architectural perspective. His work will support assurances that operations that change a system at run-time are sound, and do not violate the properties and rules defined by the architecture.

OUR TEAM:

PI: Prof. David Garlan (Faculty),

Staff: Dr. Bradley Schmerl (Research Faculty)

Students: Ivan Ruchkin (Ph.D. Student), new student to be recruited.