UC Santa Cruz

Since the advent of the modern microprocessor, the pursuit of better performance has led to increased design complexity. This increased complexity manifests due to adopting several design concepts like branch prediction, speculative execution, Out-of-Order execution, and their respective implementation choices. When implementing these design concepts in hardware, it is necessary to store information about the execution state of the processor in some form. By design, multiple processes can run on the same hardware. This leads to the execution state of any given process being influenced by one or more other processes. This creates massive security vulnerabilities through timing side-channel attacks, the most infamous classes belonging to Spectre, MDS, and Foreshadow. These are flaws inherent in the nature of the aforementioned design concepts due to their need to maintain information about the execution state to deliver increased performance. These vulnerabilities are found in most deployed modern processors. Most attempts at fixing or patching them through software incur huge performance penalties and require a hardware redesign to recoup them. This work presents a framework to be deployed during the design and verification of microprocessors that will utilize the timing and side-channel effects of these vulnerabilities to the designers' advantage to prove the existence of such vulnerabilities in designs that have been verified using conventional design methodologies. We demonstrate the incidence of timing and side-channel effects in three RISC-V designs, Ariane, BlackParrot, and BOOM. We also prove the correctness of our framework using the patched version of these designs.