Here is a formal-based solution addressing some of the challenges associated with hardware security verification for processors.
Verifying the security of processors has become an essential step in the design of modern electronic systems. Users want to be sure that their consumer devices can’t be hacked, and that their personal and financial data is safe in the cloud. Effective security verification involves the processor hardware and the many layers of software running atop it.
This article discusses some of the challenges associated with hardware security verification and presents a formal-based methodology to provide a solution. Examples of designs implementing the popular RISC-V instruction set architecture (ISA) demonstrate the power of this approach.
Overview of security verification
Thorough and efficient verification of processors is one of the biggest challenges facing electronics developers. From the moment that processors moved from piles of standard parts to custom chips, functional verification became critical. The cost of re-fabrication to fix missed bugs was daunting, and the prospect of replacing defective devices in the field was terrifying. Sophisticated tools and methodologies were developed for pre-silicon functional verification, with focused teams complementing the chip designers.
As processor chips moved into safety-critical applications, the other shoe dropped: functional safety. Even chips that are 100% correct are at risk of misbehavior due to environmental conditions, alpha particle hits, and silicon aging effects. Lives can be lost if such a failure affects an implanted medical device, weapons system, nuclear power plant, or autonomous vehicle. A whole discipline of safety verification arose to ensure that faults would be detected, and proper responses could be taken, before safety was compromised.
Today, the third shoe is dropping—perhaps a three-legged stool is a better metaphor—with the importance of hardware security. In the context of this discussion, security means that a malicious agent cannot access an electronic system to harvest private data or take control of its operation. Every application that requires functional safety also demands security; clearly product designers must ensure that pacemakers, military devices, and self-driving cars cannot be taken over by someone intent on doing harm.
Many additional applications must also be secure so that secret data is not stolen or modified. The cyber-crime economy is estimated to be at least $1.5 trillion. Of course, banks and other financial institutions must be protected, but valuable personal data exists in countless thousands of systems spread around the world. Identity theft can be costly and personally devastating, even if only a few pieces of personal data can be harvested through a system vulnerability.
Traditionally, security has been considered a software problem, with a focus on such techniques as passwords and privileged modes in operating systems. But widely known vulnerabilities such as Meltdown and Spectre have shown that hardware—the processors themselves—also presents a risk. Rigorous security verification of processors is an urgent need for many applications. Unfortunately, there is no established, comprehensive and consistent security verification methodology for processors.
Assessing security vulnerabilities
There is an established method for assessing vulnerabilities in intellectual property (IP) designs, including processors. The first step is identifying in the register transfer level (RTL) design each asset, which is anything of value or importance that is used, produced, or protected within the IP. To determine from whom these assets must be protected, the next step is identifying the adversaries that might try to compromise these assets and the possible attack surfaces, the set of access points to which threats can be applied.
The final step is determining what must be verified for the assets against which attacks from which adversaries. This includes identifying the ownership of each asset and the confidentiality, integrity, and availability (CIA) objectives for the asset. This process offers a systematic way to tackle the theoretically infinite space of negative actions and consequences and to identify vulnerabilities in the processor design.
The National Institute of Standards and Technology (NIST) brings further order to the process by defining the Common Vulnerability Scoring System (CVSS) to provide a quantitative assessment of the severity of vulnerabilities discovered. As shown in Figure 1, the CVSS v3.1 specification defines three metric groups: Base, Temporal, and Environmental. Only the Base group, representing the intrinsic qualities of a vulnerability that are constant over time and across user environments, needs to be considered for the scope of this article. The CVSS calculator provides the overall score for the vulnerability.
Figure 1 The CVSS specification provides a quantitative assessment of the severity of vulnerabilities. Source: NIST
The argument for formal
Formal techniques have long played an important role in functional verification, and they have become essential in recent years. No simulation testbench and set of tests, or even in-circuit emulation running production code, can guarantee the absence of bugs. There is always the chance that some lurking design error was never triggered or that its impact was never detected. Simulation-based methods are inherently probabilistic; they can only explore a minuscule percentage of possible design behavior.
Formal verification is fundamentally different because of its exhaustive nature. Formal proof of a property guarantees that no possible design behavior can violate the design intent expressed by that property. Therefore, there can be no bugs in the design related to that property.
Specifying a robust set of properties and proving them formally achieves a level of certainty that no other method can possibly provide. Since processors are some of the largest and most complex chip designs, formal verification was applied to their verification well before it became a mainstream technology across the industry.
As noted earlier, functional safety is another area where certainty is essential. Safety standards for many industries and applications mandate that a large percentage of possible faults can be detected and handled properly. Formal safety verification is the only way to mathematically prove that a processor design meets the requirements of the relevant standards such as ISO 26262. Unsurprisingly, formal methods also provide the only mathematically rigorous way to achieve certainty for security verification. Despite the differences across functional correctness, safety, and security, formal verification is a solution common to all three domains.
Formal verification of processor security
The established approach of CVSS classification and the power of formal methods can be combined into a novel methodology for the verification of processor security. The key link is defining the assets of the processor and writing properties that check for any compromise of these assets. These properties can then be formally verified to identify any design bugs and, once these are fixed, they prove the security of the design.
For processors, architecturally visible state elements are the right level of abstraction for the assets. These include:
The arithmetic logic unit (ALU), shifters, decoders, and other processing elements are not considered assets. These are computing elements that enable access to an asset. If they are in the path of a security attack, the net effect will be on the asset, which is where the properties provide checks for compromise.
All the input/output (I/O) interfaces are considered attack surfaces for the processor. Instructions read from memory interfaces, interrupt pins, and debug ports are all valid locations for attacks by adversaries. For the analysis in this article, any instruction that is not a rightful owner of a given asset is automatically considered an adversary. Processor security verification is especially challenging due to the total number of adversaries, the frequency of interchanging ownership of the asset with every clock cycle, and the concurrency of the pipeline, which is a function of the pipeline depth.
Application to RISC-V designs
This methodology can be used on any processor design, but the RISC-V ISA is of particular interest because of its wide adoption throughout the electronics industry. There are many implementations of the ISA available as open-source RTL, providing numerous real-world test cases for any new verification tool or methodology. Figure 2 shows how security for any RISC-V RTL processor design can be verified using the formalISA, a security analyzer that can work with any commercial formal verification tool.
Figure 2 The security analyzer performs formal verification of a RISC-V RTL processor design. Source: Axiomise
The properties specify the legal ways that an asset can be modified, so proof of the property set for the asset guarantees that no unexpected results can occur. Figure 3 shows an example of a property for the Ibex RISC-V design and the standard BEQ (branch if equal) instruction. The ISA specifies that a valid BEQ instruction will compare two registers and, if they are equal, set the PCR value to a new address calculated using an offset included in the instruction. The CVSS metrics have been evaluated and the property is named using a string of abbreviations for the values of these metrics.
Figure 3 The above example shows a security property with CVSS metrics. Source: Axiomise
Determining and listing the security properties to be written defines a verification plan, conceptually similar to a traditional list of simulation tests to be written. As with simulation tests, the results of formal analysis for the security properties can be back-annotated onto the plan to show verification progress.
Figure 4 shows a fragment of the security verification plan for the CV32E40P and zeroriscy RISC-V processors, showing the PCR properties. Formal results have been included in this table, showing that all properties passed (full proof) and no vulnerabilities were found with respect to the processor operations that would be executed through software running on the processor.
Figure 4 A fragment of the security verification plan highlights PCR properties and results for the CV23E40P and zeroriscy cores. Source: Axiomise
Security properties were written and analyzed for other assets for this core beyond the PCR. REG was analyzed for all implemented instructions from the R-type, I-type, and U-type classes as defined by RISC-V. CSR was analyzed for the six CSR instructions, synchronous exceptions, and asynchronous exceptions. DMR was analyzed for STORE instructions. As part of assessing the DMR, it was also established that illegal memory access cannot happen. Additional properties were written and proven to ensure that non-branch/jump instructions increment the PCR as expected.
Examples of bugs found in RISC-V
The methodology has been applied to numerous open-source and proprietary RISC-V implementations, and many security-related bugs have been discovered.
Formal analysis of the property shown in Figure 3 revealed an incorrect behavior in the Ibex core: when executing a BEQ instruction in cycle 5, the PCR value is altered incorrectly in cycle 7 due to an external debug initiated in cycle 6. This would result in the execution of unintended instructions, which may perform unauthorized access or otherwise compromise security.
A serious bug was also found in the CV32E40P core. An unprivileged instruction (STORE) could block access for a privileged instruction (EBREAK), compromising integrity and availability. The high CVSS score of 7.9 shows that this is a significant vulnerability in the design. Figure 5 shows the resulting issue, which is triggered by incoming debug requests only when the finite state machine (FSM) controller is in the DECODE state. The bug will not show up in any other state, making this bug hard to catch with dynamic simulation and likely resulting in a security flaw without formal verification.
Figure 5 The bug in the CV23E40P core is related to instruction privileges. Source: Axiomise
Ideally, if a memory return valid does not arrive, the LOAD or STORE is not expected to work correctly, which isn’t a functional bug. However, when a memory return valid is blocked, and there is an in-flight LOAD/STORE instruction, it should not block (cause a deadlock) the execution of a privileged instruction, especially one linked to an external debug, which is the highest privileged instruction.
Figure 6 and Figure 7 provide two additional examples found by the security analyzer in well-known RISC-V designs.
Figure 6 shows how the PCR is compromised in the WARP-V core. The PCR does not get updated correctly for the JAL instruction. For misaligned jumps, an exception must be raised. The check on byte alignment must happen using the target address, not the target offset. This bug affects multiple variations of this design: 6-stage, 4-stage, and 2-stage. This bug is, however, of moderate severity, compromising the integrity and earning a CVSS score of 5.
Figure 6 This is how the PCR is compromised in the WARP-V core. Source: Axiomise
Figure 7 shows an example of an unintended code causing a security issue in the zeroriscy core that was uncovered by formal verification. This was a particularly troublesome bug, affecting confidentiality, integrity, and availability, with the maximum CVSS score of 10. This is a serious flaw as the regular LOAD instruction cannot work correctly due to a custom modification in the design overriding the normal LOAD instruction’s behavior with a REG-REG load. Although the custom code was left by accident, this could very well have been hacked deliberately in the design. In either case, issues such as these can be caught using the formal approach.
Figure 7 This is how an unintended code causes a security issue in the zeroriscy core. Source: Axiomise
While the unique power for formal verification to provide certainty and proof is clearly valuable, some users might wonder if the exhaustive analysis performed takes too long. Figure 8 should allay any such fears, showing that issues ranging from minor to very dangerous were found in multiple RISC-V processor cores in a matter of seconds.
Figure 8 The verification results also outline time to find issues for RISC-V cores. Source: Axiomise
Formal tools for processor security verification
Verifying processor designs for functional correctness and functional safety has relied on formal tools for some time, and this approach is now extending to security. This article has presented a methodology for processor security verification using formal methods by:
This solution works inter-operably with any formal tool and automatically generates coverage properties reusable in simulation and emulation. The methodology outlined in this paper also provides the rigor needed for processor designs—including RISC-V—used in applications where security is critical.
This article was originally published on EDN.
Ashish Darbari, CEO and founder of Axiomise, has expertise in all aspects of formal methods, including theorem proving, property checking and equivalence checking.