The seemingly endless stream of previously unknown microarchitectural attacks and security flaws in hardware systems is driving the need for more efficient and comprehensive verification techniques. Unique Program Execution Checking (UPEC) is a formal verification methodology that can be used to verify a wide variety of security requirements for hardware at the Register Transfer Level (RTL). With its white-box nature and reusable verification IP, UPEC complements the open-source ecosystem provided by RISC-V. We demonstrate the efficacy of UPEC through a set of selected case studies, covering different threat models and ranging from small RISC-V processors to entire Systems-on-Chips (SoCs). Details and slides [1].
The video is played on YouTube if you click on the image below.
[2]