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.
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.