A new technical paper titled “A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level” was this year’s first place winner of Intel’s Hardware Security Academic Award program. The approach utilizes UPEC (Unique Program Execution Checking) to identify functional design bugs causing confidentiality violations, covering both the processor and its peripherals.
“In this paper, researchers demonstrate how Unique Program Executing (UPEC) methodology can be used to reason about confidentiality properties of a system-on-chip (SoC). UPEC methodology employs an efficient, induction-based formulation for information flow tracking. While the original UPEC methodology was formulated for micro-architectural side-channel detection for CPUs, this work is demonstrating how to generalize and scale that methodology for confidentiality properties for SoCs. Their formulation works directly on Register Transfer Language (RTL) and has been integrated in one commercial tool backend, thus yielding a first-of-its-kind, practically viable Pre-Si security verification technique, ” according to Intel’s award writeup.
Find the technical paper here and the Intel writeup here. Published November 2021.
J. Müller, M. R. Fadiheh, A. L. D. Antón, T. Eisenbarth, D. Stoffel and W. Kunz, “A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level,” 2021 58th ACM/IEEE Design Automation Conference (DAC), 2021, pp. 991-996, doi: 10.1109/DAC18074.2021.9586248.
Leave a Reply