A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level

We propose a formal verification methodology to detect security-critical bugs in the hardware (HW) and in the hardware/firmware interface of SoCs. Our approach extends Unique Program Execution Checking (UPEC), originally proposed for detecting transient execution side channels, to also detect all functional design bugs that cause confidentiality violations, and to cover not only the processor but also its peripherals. The proposed methodology is particularly effective in capturing security vulnerabilities that are introduced based on cross-modular effects (integration and communication issues) or poorly understood hardware/firmware interaction. Such bugs are known to be hard to detect by previous methods.We demonstrate a compositional approach where vulnerabilities discovered by our method can be used to create restrictions for the software (SW). This supports design fixes not only at the HW but also at the SW level. We present experiments for the Pulpissimo platform (v4.0) where several security-critical bugs were identified (and confirmed), as well as for RocketChip.