UIUC

group_project

Visible to the public Quantitative Security Metrics for Cyber-Human Systems

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.

group_project

Visible to the public Trust from Explicit Evidence: Integrating Digital Signatures and Formal Proofs

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.

group_project

Visible to the public Towards a Science of Securing Network Forwarding

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.

group_project

Visible to the public Toward a Theory of Resilience in Systems: A Game-Theoretic Approach

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

group_project

Visible to the public Theoretical Foundations of Threat Assessment by Inverse Optimal Control

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.

group_project

Visible to the public Secure Platforms via Stochastic Computing

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.

group_project

Visible to the public The Science of Summarizing Systems: Generating Security Properties Using Data Mining and Formal Analysis

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.

group_project

Visible to the public Scalable Methods for Security Against Distributed Attacks

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.

group_project

Visible to the public Quantitative Assessment of Access Control in Complex Distributed Systems

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:

group_project

Visible to the public Protocol Verification: Beyond Reachability Properties

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.