Security Issues in Hardware/Firmware interaction – Can a formal analysis of (just) the hardware help?
Johannes Müller, Technical University Kaiserslautern, DE
Abstract
This talk describes a formal approach to verify hardware security based on hardware property checking at the register-transfer level (RTL). The approach is based on checking uniqueness of program execution with respect to confidential information. It is therefore called Unique Program Execution Checking (UPEC). UPEC can be used to systematically detect all vulnerabilities to microarchitectural side channels as well as to explicit functional leakages. We summarize results obtained for several open-source RISC-V processors, including Rocketchip and Boom. We then report on our current research activities extending UPEC to detecting security issues in the functionality of hardware/firmware interaction. We present preliminary results for this class of security vulnerabilities at the example of Pulpissimo and sketch future research directions.
