Sketching Secure Hardware

Hardware security-related attacks are growing in number and their severity. Spectre, Meltdown, Foreshadow, Fallout, ZombieLoad, and Starbleed are just a few of the many recent attacks that exploit hardware vulnerabilities. While vulnerabilities are seemingly easy to find, designing secure hardware is challenging (to say the least) and there are limited tools to aid this process.

Armita Ardeshiricham’s PhD thesis made pioneering and fundamental contributions in detecting, localizing, and repairing hardware vulnerabilities. Her thesis developed verification tools that quickly finds vulnerabilities that previous work could not. And it laid the foundation for automated debugging of those flaws.

Her early work focused on developing powerful information flow tracking (IFT) tools that that work at the register transfer level. She extended this work in a fundamentally important manner by formulating IFT logic that detects timing based flows. And she pioneered the idea of sketching for hardware security. The culmination of her PhD research is the VeriSketch framework.

VeriSketch is the first design framework that uses sketching to automatically synthesize secure and functionally-complete hardware design. VeriSketch frees hardware designers from specifying exact cycle-by-cycle behaviors and excruciating bit-level details that often lead to security vulnerabilities. Instead, the designer provides a sketch of the circuit alongside a set of functional and security properties. VeriSketch uses program synthesis techniques to automatically generate a fully-specified design which satisfies these properties. VeriSketch leverages hardware IFT to enable definition and verification of security specifications, which allows for the analysis of a wide variety of security properties related to confidentiality, integrity, and availability.

Armita’s PhD research will undoubtedly have a lasting impact on our group’s hardware security efforts and has laid out a research agenda for the next few years (and likely beyond). Based on her work, we have started projects on error localization (with Prof. Yanjing Li at Univ. of Chicago) and automated property generation (with Prof. Cynthia Sturton at Univ. of North Carolina) that was recently funded by the Semiconductor Research Corporation. Her work was fundamental in developing system on chip access control monitors in collaboration with Leidos and Sant’Anna School of Advanced Studies in Pisa. She will certainly be missed!

Dr. Ardeshiricham currently works at Apple doing things that she can tell no one about (as is typically with Apple). But I’m certain that future Apple devices will be much more secure with her overseeing the verification process.

A very long overdue post and congrats again!

-Ryan

Ryan’s acknowledgment — acting as Mel Gibson to Armita’s Jim Caviezel during her PhD career.