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

Johannes Muller, Mohammad Rahmani Fadiheh, Anna Lena Duque Anton, Thomas Eisenbarth, Dominik Stoffel, Wolfgang Kunz


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.

Original languageEnglish
Title of host publication2021 58th ACM/IEEE Design Automation Conference (DAC)
Publication date05.12.2021
Publication statusPublished - 05.12.2021


Dive into the research topics of 'A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level'. Together they form a unique fingerprint.

Cite this