A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level
TimeWednesday, December 8th3:53pm - 4:04pm PST
Embedded and Cross-Layer Security
DescriptionWe propose a formal verification methodology to detect security-critical bugs in hardware and 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. A compositional approach is developed where vulnerabilities discovered by our method can be used to create restrictions for the software. We present experiments for the Pulpissimo platform where several security-critical bugs were identified (and confirmed), as well as for RocketChip.