Scaling Hardware Security Property Generation

One of the biggest challenges in hardware security verification is developing formal properties that can subsequently be verified by automated tools. This is a difficult and time-consuming task typically assigned to security verification engineers that must manually sort through hundreds of thousands of lines of a hardware description.

Isadora Duncan By Arnold Genthe -, Public Domain,

Our recent article in IEEE Security & Privacy Special Issue on Formal Methods at Scale describes our research on developing Isadora – a tool that automates the property generation process for information-flow properties that are critical to the security of hardware designs. Isadora combines information flow tracking with specification mining to help automate the challenging security verification process. Congrats to the authors: Calvin Deutschbein, Andy Meza, Francesco Restuccia, Ryan Kastner, and Cynthia Sturton.

Olivia Weng Named NSF Graduate Research Fellow

Congratulations to Olivia Weng for being awarded a National Science Foundation Graduate Research Fellowship. The NSF GRF is one of the most prestigious graduate fellowships in the US. The fellowship will fund Liv for the remainder of her PhD allowing her to continue her research on the co-design of efficient, fault-tolerant computer architectures for applications in high-energy physics. One example is the Large Hadron Collider, where physicists need hardware that will process millions of particle collisions per second. Her research will allow their hardware, and the machine learning software that runs on it, to meet these intense computing demands while handing faults that are inherent in such sensors.