Formal Verification of Security-Properties on RISC-V Processors

Hardware Security and trustworthiness are becoming ever more important, especially for security-critical applications like autonomous driving and service robots. With the increase in distribution of RISC-V processors, security issues in them arise. Security vulnerabilities and design flaws in processors can be exploited by attackers, e.g. by running software exploiting the vulnerabilities. This can lead to drastic consequences like damaging whole system functionality and even human lives can be endangered. Hence, it is very important to verify compliance of processors with the design specification and microarchitecture intent to harden the hardware against malicious attacks. Detection and removal of design bugs results in improved processor security. Therefore, we formally verified the security-critical functionality of our own commercial RISC-V processor using model checking based formal verification with the formal verification tool Jasper. For this, we determined and implemented a comprehensive list of properties for security-critical functionality, derived from RISC-V

Christian Appold works as a Research Engineer in the field of Microprocessor R&D at automotive supplier DENSO in Munich. He studied Computer Science and did his PhD at University of Würzburg. Afterwards he worked for companies like ARM or Dialog Semiconductor (now Renesas) on formal formal verification of hardware.