Projects – Completed

Security concept: Key on Blue puzzle pieces background, 3d render

A Hypothesis Testing Framework for Network Security
P. Brighten Godfrey, Matthew Caesar, David Nicol, William Sanders, and Dong (Kevin) Jin

This project develops a scientific approach to testing hypotheses about network security when those tests must consider layers of complex interacting policies within the network stack. The work is motivated by observation that the infrastructure of large networks is hideously complex, and so is vulnerable to various attacks on services and data. Coping with these vulnerabilities consumes significant human management time, just trying to understand the network’s behavior. Unfortunately, even very simple behaviors – such as whether it is possible for any packet (however unusual) to flow between two devises – are difficult for operators to test, and synthesizing these low-level behaviors into a high-level quantitative understanding of network security has been beyond reach.

We propose to develop the analysis methodology needed to support scientific reasoning about the security of networks, with a particular focus on information and data flow security. The core of this vision is Network Hypothesis Testing Methodology (NetHTM), a set of techniques for performing and integrating security analyses applied at different network layers, in different ways, to pose and rigorously answer quantitative hypotheses about the end-to-end security of a network.

Anonymous Messaging
Pramod Viwananth and Carl Gunter

Anonymity is a basic right and a core aspect of Internet. Recently, there has been tremendous interest in anonymity and privacy in social networks, motivated by the natural desire to share one’s opinions without the fear of judgment or personal reprisal (by parents, authorities, and the public). We propose to study the fundamental questions associated with building such a semi-distributed, anonymous messaging platform, which aims to keep anonymous the identity of the source who initially posted a message as well as the identity of the relays who approved and propagated the message.

Classification of Cyber-Physical System Adversaries
Sayan Mitra and Geir Dullerud

Classification and understanding of attacks is the first step towards developing principled design technologies for resilient cyberphysical systems. Building up on the existing hybrid system and stochastic process theories, the project classifies a broad range of attacks on monolithic and distributed CPS which encompass traditional attacks on computing infrastructure as well as attacks that exploit the dynamical and network characteristics. There are two sides to the proposed classification: First, it provides algorithms for detecting classes of attacks that can be detected with reasonable resources. Second, it provides lower bound result characterizing classes of attacks that cannot be detected and yet can destabilize the system. At the theoretical level, the outcomes from this project will provide new techniques for reasoning about adversaries in switched and hybrid systems which combine indistinguishability-based arguments from distributed computing and control theory. In summary, this project develops the foundations of a security science for hybrid systems where physics-based processes play principal roles alongside those of computation and communication.

Data-Driven Model-Based Decision-Making
William Sanders, Masooda Bashir, David Nicol, and Aad Van Moorsel

The goal of this project is to develop quantitative, scientifically grounded, decision-making methodologies to guide information security investments in private or public organizations, combining human and technological concerns, to demonstrate their use in two or more real-life case studies, prototype tools and demonstrate their proof of concept on those case studies. It is our hypothesis that quantitative security models, augmented by collected data, can be used to make credible business decisions about the use of particular security technologies to protect an organization’s infrastructure. The key output of this research will be a data-driven, model-based methodology for security investment decision-making, with associated software tool support, and a validation of the usefulness of the tool in a realistic setting. The main scientific contributions will be new abstractions for modeling human behavior, and techniques and tools for optimization of the associated data collection strategy.

This project is a collaboration between the University of Illinois at Urbana-Champaign and Newcastle University.

Data Driven Security Models and Analysis
Ravishankar Iyer, Zbigniew Kalbarczyk, and Adam Slagell

This project develops a science of deriving from data certain models and metrics suitable for recognizing, mitigating, and containing attacks with a network. Our approach uses production scale data; our initial study of 2005-2012 security incidents at NCSA motivates methods for discovering relationships and time sequences of events in vast amounts of log data, research from which we’ve gained insight and basis for monitoring, and analyzing secure systems. The challenge is to capture and identify attackers’ actions from the measurements, develop predictive models of attacker behavior before and during an attack, and thus develop a framework within which to reason about attacks, independently of the vulnerability exploited or the adopted attack pattern. Our project looks at models and metrics driving (1) cross-layer monitoring and detection, (2) attack containment, and (3) situational awareness.

Developing Security Science from Measurements
Ravishankar Iyer and Zbigniew Kalbarczyk

This project aims to define foundational data-driven methodologies and related science to identify the basis for continuous and dynamic monitoring and placing of detectors, making it possible to enable adaptive approaches to mitigation and containment of the spread of attacks. This will be achieved in the presence of changes in the underlying infrastructure as well as growing sophistication of attackers.

End-to-End Analysis of Side Channels
Nikita Borisov

This project explored a framework for characterizing side channels that is based on 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 give 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 the adversary.

Mathematical Foundations and Analysis Techniques for Protocol Indistinguishability
José Meseguer

This project proposes to make advances in protocol indistinguishability research by accomplishing the following main research goals:

1.  Develop the mathematical foundations of indistinguishability in the Doleve-Yao model modulo algebraic properties.

2. Develop formal verification techniques to automate proofs of indistinguishability properties.

3. Demonstrate the usefulness of such proof techniques on a wide range of protocols, including various kinds of privacy-preserving protocols.

4. Develop substantial case studies which further validate these advances and help in transmitting them to the research community.

Quantitative Assessment of Access Control in Complex Distributed Systems
David Nicol and William Sanders

The technical merit of the proposal is to bring the mathematical science of importance sampling to bear on critical problems in network security. The work is important because the existing tools for validating access control configurations are inadequate for large systems compromised of multiple interacting access control mechanisms. Our work will provide a basis for assessing how well a system meets global policy objectives, and for comparing different configurations to determine which better meets those objectives. In addition, the sampling approach provides  a mathematical basis for assessing the resiliency of a system’s access control mechanisms to intrusions that create connections that bypass its intent. The immediate impact will be an increased “in the field” capability to assess a system’s access control posture and its resilience to intrusion. The long-term impact is in providing a first basis for an engineering science of access control.

Quantitative Security Metrics for Cyber-Human Systems
William Sanders and David Nicol

This project looks at how security metrics that take into account user behavior can be used in the design process. We propose both fundamental work in modeling methodology, formalisms, and solution methods, and practical implementation in software form. When completed, this modeling approach will provide a structured and quantitative means of analyzing cyber security problems whose outcomes are influenced by user, attacker, and system, interactions.  This capability is a key element in creating a true science of security.

Scalable Methods for Security Against Distributed Attacks
Gul Agha

Classical methods for expressing and checking properties do not allow us to express many relevant global security properties. By developing a probabilistic distributed temporal logic, important global properties of systems can be represented, which will enable us to represent distributed attacks and probabilistic reasoning. We propose to develop the logic and efficient, scalable methods for reasoning through decentralized monitoring and adaptive sampling. This will allow confidence that certain types of global security properties ar not violated in systems such as clouds or clusters.

Science of Human Circumvention of Security
Tao Xie, Jim Blythe, Ross Koppel, and Sean Smith

Well-intentioned human users continually circumvent security controls. The pandemic/ubiquitous fact of this circumvention undermines the effectiveness of security designs that implicitly assume circumvention never happens. We seek to develop metrics to enable security engineers and other stakeholders to make meaningful, quantifiable comparisons, decisions, and evaluations of proposed security controls in light of what really happens when these controls are deployed.

This project builds on foundations of human-computer-interface in security and the preliminary research the investigators have been working on already: Blythe, Koppel, and Smith, studying workers’ reasons for and methods of circumvention along with Xie, studying techniques for assisting mobile-app users (who can be enterprise workers) to conduct security controls on apps to be installed on their mobile devices. Research conducted in large enterprise systems increasingly finds that such apps are a major source of malware invasions into those larger systems. Similarly, with the expanded use of BYOD (bring your own device), such dangers are pandemic without security controls and without users’ ability to understand and follow those controls. Security-control circumvention by enterprise workers as mobile app users is reflected by their acceptance to install apps without sufficiently assessing their risk.

Secure Platforms via Stochastic Computing
Naresh Shanbhag and Rakesh Kumar

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 formulated 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 grading of the severity of the infractions. Our work on stochastic computing has been leveraged to provide a foundation for the framework.

Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Sayan Mitra, Geir Dullerud, and Swarat Chaudhuri

Cyber-physical system (CPS) security lapses may lead to catastrophic failure. We are interested in the scientific basis for discovering unique CPS security vulnerabilities to dynamics-aware attacks that alter behaviors of components in ways that lead to instability, unsafe behavior, and ultimately diminished availability. Our project advances this scientific basis through security-metrics-driven design and evaluation of CPS, based on formalization of adversary classes and security metrics. We propose to define metrics, and then develop and study static and dynamic analysis algorithms that provide formal guarantees on them with respect to different adversary classes.

Theoretical Foundations of Threat Assessment by Inverse Optimal Control
Timothy Bretl

Starting from the premise that cyber attacks have quantifiable objectives, our long-term goal was 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 was based on a new method for solving the problem of “inverse optimal control”. Much of our work focused on establishing the theoretical foundations for this method of solution. In this project we explored its application to threat assessment.

Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Tamer Basar

The security and resilience of modern infrastructures require an interdisciplinary research effort to investigate security mechanisms at each layer and develop tools for analyzing an designing complex systems  to achieve inter- and intra-layer resilience. Game-theoretic approaches allow us to adopt a holistic viewpoint towards designing systems of multi-layer interactions. The science of resilience is a critical component of modern system engineering. This project is an attempt in the direction of developing a new general resilient system theory, with potential applications to many emerging complex systems such as those in health care, biomedicine, smart power grid, and transportation systems.

Trust from Explicit Evidence: Integrating Digital Signatures and Formal Proofs
Elsa Gunter

This project proposed to develop a common logical framework that accounts for two principal sources of trust in software:  digital signatures and explicit proof. Such a framework will allow us to rigorously specify, enforce, and analyze security policies that rely on multiple modes and sources of trust. Based on recent work by the PI and collaborators, the framework will be cast as a modal type theory which comes equipped with a notation for programs and proofs. We exploit this relationship to guarantee composability and usability form the programmers point of view.