Automated detection of hardware Trojans and vulnerabilities to adversary attacks
The modern world relies on complex electronic systems. Connected autonomous vehicles (CAVs), medical devices, aerospace applications, smartphones, defense systems, nuclear power plants and other critical infrastructure, 5G networks, IoT devices, and cloud computing must all be resilient to adversary attacks that could compromise the safety and privacy of people.
In the past, security engineering has focused on software and system-level issues. However, there is ample evidence that ever more risks and attacks involve hardware. Embedded systems using relatively simple processors are not exempt. Malicious actors may construct misuse-case scenarios, exploiting hardware Trojans and vulnerabilities for nefarious purposes.
Hardware assurance (HwA) is critical to build secure systems from the ground up. OneSpin takes a holistic approach to IC integrity, providing solutions that verify not only functional correctness and safety but also trust and security.
Automated Trustworthiness Assessment
All stages of the IC development process are vulnerable to the insertion of hardware Trojans and malicious logic. The complexity of modern, highly-configurable hardware provides a favorable hiding place for backdoors, time bombs, performance degradation or kill switches. Organizations can no longer ignore the risk of tampering. Manual review of in-house and third-party semiconductor IPs (3PIPs) before SoC integration is costly and insufficient. Functional pre-silicon verification does not address the trust concern.
OneSpin provides solutions that automatically generate trustworthiness assessment data and reports. Auditors with limited hardware knowledge, engineers not familiar with the implementation details of an IP, and trust assurance experts can use these solutions to detect suspicious logic and assess trustworthiness using an objective, efficient approach.
Proof of Trojan Absence
Pre-silicon verification provides confidence in IP functional correctness, thus ensuring that the IP does what it is supposed to do, as specified. Proving Trojan's absence, on the other hand, can only be ensured through rigorous proof that the IP does not do anything else.
OneSpin’s GapFreeVerification™ provides exhaustive proof that an IP RTL model is free from both functional bugs and hidden, malicious functions. The process generates a trusted executable specification. It also detects specification omissions or inconsistencies. Apps, leveraging pre-packaged SystemVerilog assertions (SVAs) as executable specification, are available for critical IPs, such as RISC-V processor cores. For more information, read the paper Complete Formal Verification of RISC V Processor IPs for Trojan-Free Trusted ICs presented at GOMACTech 2019.
OneSpin’s EC-RTL™, EC-ASIC™, and EC-FPGA™ use formal sequential equivalence checking (EC) to compare two design representations. EC proves that design transformations such as synthesis and place-and-route do not introduce accidental or malicious changes.
Adversaries may leverage corner-case hardware bugs and unforeseen misuse-case scenarios to construct attack vectors. Denial-of-service, privilege escalation, side-channels, and other attacks may violate the confidentiality, integrity, or availability of protected assets, a cryptographic key, for example.
Security must become an integral part of IC development, encompassing the entire hardware development lifecycle. Hardware root of trust (HRoT) and other security IPs or features must be rigorously verified. Checking that secure and non-secure hardware regions are properly isolated is also critical.
OneSpin’s Security Solution leverages unique under-the-hood technology that uncovers security-relevant hardware weaknesses and vulnerabilities in complex IPs and SoCs. OneSpin’s technology enables efficient processes that detect – and rigorously demonstrate the absence of – information paths between unauthorized interfaces or transactions and protected assets, micro-architectural and implementation-level side channels, and more.
Automotive Cybersecurity and ISO/SAE 21434
Complex electronic systems connecting cars to other vehicles, the infrastructure, and the cloud (V2X), and performing security- and safety-critical functions, offer many opportunities for physical and remote attacks. Automotive cybersecurity is crucial to ensure safety and protect IPs and data. Car manufactures and their supply chain need a comprehensive, standardized process to develop and maintain secure systems based on secure hardware and software components. The upcoming ISO/SAE 21434 Road vehicles – Cybersecurity engineering standard, which will supersede SAE J3061, promises to address this need.
The ISO/SAE 21434 standard recognizes that security cannot be built on top of existing systems and components, and requires a security-by-design development process. Threat analysis and risk assessment (TARA) is a crucial part of the standard, and an activity that can be automated using dedicated tools that model a system and its security requirements, track dependencies to hardware and software components, and perform a risk assessment. This website from itemis provides a comprehensive overview of the ISO/SAE 21434 standard.
OneSpin provides unique solutions to identify violation of security requirements in automotive ICs and IPs.
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…