Isadora: automated information-flow property generation for hardware security verification

Isadora is a specification mining tool for creating information-flow properties for hardware. Isadora combines hardware information-flow tracking and specification mining to produce properties that are suitable for the hardware security validation and support a better understanding of the hardware’s security posture. Isadora is fully automated; the user provides only a hardware specification and a testbench—they do not need to supply a threat model or security requirements. Isadora is evaluated on a RISC-V processor, an SoC access control mechanism, and the OpenTitan hardware root of trust. Isadora generates security properties that align with Common Weakness Enumerations (CWEs) and with properties written manually by security experts.