Automated detection of RTL Trojans and hardware vulnerabilities to adversary attacks
Traditional verification focuses only on functional reliability with the goal to eliminate systematic errors (design bugs). Safety-critical applications have demanded functional safety as well, including the ability to handle real-world random errors. Today’s highly interconnected world adds a third requirement to IC integrity: trust and security from adversary attacks. Many IC applications, from autonomous vehicles and financial data servers to defense/aerospace and nuclear power plants, must be protected from such attacks since the consequences could be severe.
A hardware root of trust provides the foundation of any secure and trustworthy system. Vulnerabilities include corner-case functional bugs, undocumented features, debug mode and other marginal use cases, and hidden malicious logic (Trojans). OneSpin’s Trust and Security Solution detects a wide range of Trojans and hardware vulnerabilities. Products are segmented into structural checks, automated formal checks, and property checking, targeting different aspects of security or trust.
Trust Analysis and Verification
A trusted design flow must ensure that no hardware Trojans or other malicious logic is inserted at any point. There are many opportunities for these to be inserted. The original specification might include issues that could lead to design errors or unintended and exploitable features. Problems may creep in during high-level synthesis (HLS) or RTL synthesis, either by deliberate action or tool issues. Integration of third-party IP blocks (3PIPs) presents extra risk since the IC team does not know the details of those designs. Tool bugs or intentional netlist modifications can occur during the place-and-route (P&R process). FPGA designs are especially vulnerable because of the extensive optimizations performed during synthesis/P&R and because changes may be made when generating the bitstream to program the device.
Only formal technologies can provide the absence of unwanted logic. OneSpin’s EC-ASIC™ and EC-FPGA™ use formal equivalence checking to compare two design representations. This not only ensures that transformations of the design do not remove any functionality, but also that hardware Trojans or other malicious logic has not been inserted. EC-FPGA can verify the flow all the way to the bitstream, including transformations performed by synthesis, optimizations, place and route, and bitstream generation.
At the front end of the flow, OneSpin’s unique GapFreeVerification™ provides automatic detection of specification omissions and errors, holes in the verification plan, and unverified RTL functions. Key design features are captured with OneSpin’s Operational SystemVerilog Assertions (SVA), high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way:
- Translate functional requirements in a formal and simulation-executable format
- Capture entire circuit transactions in a concise and elegant way, similar to timing diagrams
- Achieve 100% functional coverage with high-level and easy-to-review assertions
- Adopt a consistent assertion style that is applicable to a wide range of applications and able to deliver optimal performances for both simulators and formal tools
- Cleanly separate implementation-specific supporting verification code from reusable specification-level code
GapFreeVerification enables development of an executable specification in the form of assertions, then proves that this specification has no gaps or inconsistencies and that the specification and RTL are functionally equivalent. The combined result of this approach and equivalence checking beyond the RTL provides a robust trust solution proving that no malicious or unintended functionality has crept in at any stage of the design process.
Security Analysis and Verification
Even in the absence of hardware Trojans or deliberate insertion of logic into a design, adversary attacks can exploit vulnerabilities present in the design itself. Effective hardware security requires innovation beyond traditional functional verification, which focuses on target use cases. Bugs that break these use cases are fixed, but bugs exposed in artificial use cases are often dismissed. Hardware bugs with software workaround may also be acceptable.
This approach is insufficient when security is a concern. Security verification must include a rigorous process to detect all bugs and flaws, establishing precisely what can and cannot happen in the design. A wide range of adversaries, from casual hackers to cyber criminals and foreign intelligence agencies, is always on the lookout for security flaws. Given the interconnected nature of today’s world, if a hardware vulnerability can be exploited, it will be. It’s just a matter of time until an adversary discovers it.
Many of OneSpin’s products have analysis and verification features that are essential for detecting potential security holes in RTL designs. These include a mix of structural checks, automated formal checks, and property checking applications. Together they form the OneSpin Security Solution. Some of the vulnerabilities detected by this solution are shown in the adjacent table.
Security must become an integral part of IC development, encompassing the entire hardware lifecycle of concept, development, and production. Effective security verification requires innovative solutions and industry partnerships. OneSpin’s Security Solution includes a unique and growing portfolio of tools and apps to ensure the absence of vulnerabilities for adversaries to exploit.
OneSpin’s Operational SVA enables formal verification enthusiasts to develop high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way.»Learn more…
The OneSpin 360 Design Verification (DV) product line leverages the most advanced, high-performance formal technology as the basis for a range of verification solutions, from automated design analysis to advanced property checking.»Download the flyer…
OneSpin’s Quantify measures the quality of a formal verification test bench. It provides precise, actionable information on what parts of the design-under-test (DUT) are verified, and it highlights RTL code that could still hide bugs.»Download the data sheet…
OneSpin 360 DV-Verify adds coverage-driven assertion-based verification (ABV) to the DVInspect platform.»Download the data sheet…
Design verification has a lot in common with human hygiene practices. The goal of both activities is to remove all dirt, grime, and bugs through an active process of establishing good hygiene.»Download the white paper…
Fault-tolerant hardware development is no longer a niche and presents new challenges. Many engineers face the daunting task of having to examine countless faulty variants of their design in order to integrate and verify multiple safety mechanisms within complex Systems-on-Chip (SoCs).»Download the white paper…