Formal methods

group_project

Visible to the public TWC: Medium: Collaborative: Retrofitting Software for Defense-in-Depth

The computer security community has long advocated the concept of building multiple layers of defense to protect a system. Unfortunately, it has been difficult to realize this vision in the practice of software development, and software often ships with inadequate defenses, typically developed in an ad hoc fashion.

group_project

Visible to the public TWC: Medium: Collaborative: Retrofitting Software for Defense-in-Depth

The computer security community has long advocated the concept of building multiple layers of defense to protect a system. Unfortunately, it has been difficult to realize this vision in the practice of software development, and software often ships with inadequate defenses, typically developed in an ad hoc fashion.

group_project

Visible to the public TWC: Medium: Collaborative: Extending Smart-Phone Application Analysis

This research is focused on the creation of new techniques and algorithms to support comprehensive analysis of Android applications. We have developed formally grounded techniques for extracting accurate models of smartphone applications from installation images. The recovery formalization is based on TyDe, a typed meta-representation of Dalvik bytecode (the code structure used by the Android smartphone operating system).

group_project

Visible to the public TWC: Medium: Automating Countermeasures and Security Evaluation Against Software Side-channel Attacks

Side-channel attacks (SCA) have been a realistic threat to various cryptographic implementations that do not feature dedicated protection. While many effective countermeasures have been found and applied manually, they are application-specific and labor intensive. In addition, security evaluation tends to be incomplete, with no guarantee that all the vulnerabilities in the target system have been identified and addressed by such manual countermeasures.

group_project

Visible to the public EAGER: Identifying Security Critical Properties of a Processor

This project focuses on shoring up the security vulnerabilities that exist in computer processors. Just like in software, bugs in hardware present vulnerabilities that can be exploited by determined attackers. Prior work has developed a method whereby the processor monitors itself and sends an alert to software whenever dangerous, anomalous behavior is observed. The question of what constitutes dangerous behavior is an open one, and tackling it is the goal of this research.

group_project

Visible to the public CRII: SaTC: Detecting Security Vulnerabilities in Instruction Set Architectures

The interaction between computer processors -- the hardware at the heart of our computers, tablets, and phones -- and software -- apps, web browsers, and other applications -- is governed by an Instruction Set Architecture (ISA). The ISA is the specification that defines how the processor will respond to commands from the software. It is large and complex, too large for a person to understand and reason about all the interactions between different parts completely. As a result, security vulnerabilities exist in the ISA.

group_project

Visible to the public STARSS: Small: Collaborative: Specification and Verification for Secure Hardware

There is a growing need for techniques to detect security vulnerabilities in hardware and at the hardware-software interface. Such vulnerabilities arise from the use of untrusted supply chains for processors and system-on-chip components and from the scope for malicious agents to subvert a system by exploiting hardware defects arising from design errors, incomplete specifications, or maliciously inserted blocks.

group_project

Visible to the public TWC: Small: Employing Information Theoretic Metrics to Quantify and Enhance the Security of Hardware Designs

Computing devices control much of the world around us. They power smart phones, kitchen appliances, cars, power grids, medical devices, and many of the other objects that we rely upon in our everyday lives. The foundation of these systems is the hardware, which are complex multi-billion transistor chips. Gaining control of the hardware provides unfettered access to every part of the system. This makes it a highly attractive target for attackers.

group_project

Visible to the public  TWC: Medium: Designing Strongly Obfuscated Hardware with Quantifiable Security against Reverse Engineering

Our world has become increasingly reliant on integrated circuits (ICs). Mobile phones are deeply enmeshed in our everyday lives, we drive cars equipped with hundreds of ICs, and have come to depend on the power grid and other cyber physical systems that are controlled by ICs. Not surprisingly, the issue of securing hardware has become increasingly vital. A reverse engineering adversary may, for example, be motivated by extracting intellectual property from a circuit, cloning a design for product piracy, or creating a targeted backdoor for stealing cryptographic keys.