Formal methods

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.

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.

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.

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.

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.