Obstacles remain, but adoption is growing.
Formal verification is poised to take on an increasingly significant role in automotive security, building upon its already widespread use in safety-critical applications.
Formal has been essential component of automotive semiconductor verification for some time. Even before the advent of ADAS and semi-autonomous vehicles — and functional safety specifications like ISO 26262 and cybersecurity specifications like ISO/SAE 21434 — digital system content in cars was growing fast. Leading automotive IC providers such as Bosch and Infineon have been using formal verification as part of their verification flows for years. In fact, early mainstream formal adoption meshed well with needs of automotive chipmakers, which started with system control ICs.
“Automotive systems consist of networked ECUs connected by a CAN bus,” said Pete Hardee, director of product management at Cadence. “This has introduced many scenarios in which connected systems can interact. And that has presented many driver usability advantages, while also introducing many potential failure modes and attack vulnerabilities for safety-critical systems that must be taken into account.”
Hardee noted that few of these modes are easily covered by verification methods that consider verifying intended functionality. “There are perhaps some failure scenarios the verification engineer can conceive, plus some ‘constrained random’ variants of the resultant tests such as those common in UVM-based verification,” he said. “But failure modes and vulnerabilities manifest themselves in ways often totally unrelated to the known functionality of these systems.”
Formal verification can be used for functional verification of integrated circuits in addition to simulation. The exhaustive nature of formal means it is suitable to finding corner-case bugs that can affect security and safety in automotive applications, said Anders Nordstrom, security application engineer at Tortuga Logic. Formal verification also can be used to prove there are no Trojans embedded in the design.
Sergio Marchese, technical marketing manager at OneSpin, said there are two aspects to consider with formal — the level of confidence that is required and the cost of verification. “When it comes to verification sign-off, simulation and emulation cannot match the quality delivered by formal,” he said. “Automotive chip providers routinely apply formal to key IPs and subsystems to prove the absence of bugs in critical chip functions. As they develop many product derivatives, they can also automate the flow and achieve this quality level while saving effort.”
Formal also works for tasks where simulation is of limited or no value. “Consider the error-correcting functions in memories, for example,” said Marchese. “Creating a testbench and coverage to test all possible combinations is impossible. Even just doing some random testing still requires much more effort than with formal. A similar argument can be made for the verification of configuration registers with built-in redundancies for fault tolerance. Infineon, for example, has demonstrated in various papers and presentations that formal property checking and model-based mutation coverage are far more efficient than simulation.”
In addition, formal verification techniques can increase the level of confidence in the systems’ functional correctness by ensuring, among other things, compliance with protocols and specifications.
“They can also contribute to achieving the higher levels of reliability and security required by the automotive industry,” noted Guillaume Boillet, PMM for VC Formal products at Synopsys. “Formal verification typically works hand-in-hand with the more traditional verification approaches to increase coverage and reduce turnaround time. One such important example is the application of formal techniques to reduce the fault space and perform fault classification, distinguishing safe from dangerous ones by formally checking their controllability and observability in a given design.”
Automotive ICs are among the most complex semiconductors being developed today, making them challenging even for veteran design and verification teams. Making these chips more reliable throughout their projected lifetimes, which may be more than a decade, requires much more focus on eliminating potential problems up front. Simulation, which shows the presence of foreseeable bugs, is limited to what bugs can be conceived of by experts. Formal, in contrast, is conclusive, but with a narrower scope.
“Formal capabilities include clock/reset validation, coverage analysis, logical equivalency, and more,” said Jacob Wiltgen, functional safety solutions manager at Mentor, a Siemens Business. “Ultimately, deploying formal accelerates the automotive lifecycle while simultaneously closing on a primary goal of any safety critical product, zero bugs and zero defects.”
Specifically, the verification techniques needed to discover failure modes so far removed from known functionality are often collectively known as negative testing, and this is fundamentally why formal verification is an attractive technology for safety-critical systems, Hardee said.
“Formal is naturally a ‘negative testing’ method. Rather than the verification engineer having to conceive tests, in formal you capture the desired behavior in the form of an assertion or property. Then the formal tool exercises every possible combination of inputs to break the desired behavior, just like a hardware hacker.”
Verifying interactions
A new area where formal is playing an increasing role involves security, both within and outside the vehicle. That includes vehicle-to-infrastructure (V2I) and vehicle-to-vehicle communication. Formal can be used to detect potential violations of confidentiality and integrity attributes in critical IPs or across the chip fabric.
“The real challenge is to bring this to the next level and support efficient incident response processes and compliance with the upcoming ISO/SAE 21434 standard,” said OneSpin’s Marchese. He noted it is particularly useful for spotting unforseen misuse case scenarios.
Security in automotive is critical because it can impact safety. Unauthorized access to vehicle data and unauthorized control of automotive functions could lead to serious accidents if someone could disable the engine or apply the brakes remotely, according to Tortuga Logic’s Nordstrom. “In this area, security threats originate from either someone having direct access to the automotive system, or someone accessing the automotive system remotely through the V2I or V2V infrastructure. Verifying that the entire automotive system is secure will require multiple verification methods,” he said.
Formal security verification using information flow tracking is effective in verifying data integrity and data leakage issues in ICs. Sensitive data inside a chip cannot be allowed to leak to an outside observer, and an outside agent cannot be allowed to control the setup and behavior of the chip.
“Formal can make sure the interfaces to the circuits are secure, but verifying that several chips or large IP modules can communicate securely without data leakage or data integrity violations may be beyond the scope of formal,” Nordstrom said. “This is more suited to simulation-based information flow tracking technology. Still, formal can address security concerns within the vehicle, from the vehicle to infrastructure, and with other vehicles by making sure the components do not have any security weaknesses. This is an important step, but not sufficient to address the entire automotive system security concern.”
Automotive systems contain multiple processors that run embedded firmware. “This creates many security vulnerabilities in the system,” he said. “Formal may be able to ensure that firmware cannot be overwritten by an unauthorized user. It is also necessary to verify that hardware/software interaction doesn’t create any security vulnerabilities. This verification requires running firmware instructions on a simulation model or in emulation. This is also beyond the scope of formal, and is best verified using information flow tracking technology in simulation or emulation.”
At the same time, vehicular communications systems have been in conceptual and planning stages for years, and are more recently becoming reality, Hardee said. “There’s huge promise for the advantages – including hugely more efficient logistics, management of traffic, as well as significant moves towards vehicle safety and autonomous driving. Whether they’re V2I or V2V, they also bring more considerations for automotive system verification. First, they further increase system complexity with a whole lot more computing power and software involved. Second, they provide remote communication paths for a potential hacker to cause problems. And the differences between V2I and V2V are twofold — how remote, and which systems can be directly communicated with. V2I may increase the chances that a hacker could access a given system and the hack could possibly affect more vehicles, while V2V means a hacker needs to be in close proximity to the target. But a hack could directly access safety-critical ADAS or autonomous vehicle systems controlling braking, acceleration or steering.”
There are numerous videos on YouTube of vehicles being hacked and remotely controlled, and numerous reports about similar occurrences across a range of vehicles. V2I and V2V technologies going live will no doubt increase these instances, in number and perhaps severity.
How can formal verification help?
To the extent that the hacker can make an attack look like a valid communication of some external threat to provoke a vehicle to do something unsafe, there’s little formal can do for the systems at the receiving end, Hardee said. “But only a subset of attacks look like that. In many other attack methods, the hacker gains access via software, but exploits a weakness in the hardware platform to gain access to a system that is the target of the attack.”
The kinds of weaknesses exploited this way include:
Formal verification is proven to be able to harden SoCs for these kinds of attacks by detecting such vulnerabilities.
“Verifying that no unauthenticated access from an internal virus or an external source is possible is a very complex problem for which formal path verification proves to be very effective,” said Synopsys’ Boillet. “Based on the designer’s declaration of the various secure areas, formal techniques can be applied to identify potential data leaks and integrity issues, making sure confidential data is not visible to non-secure areas and cannot be illegally modified.”
Wiltgen noted that formal structural analysis capabilities are ideal in analyzing design connectivity to secure parts of the chip, ensuring no “sneak paths” exist that could compromise security. “This includes path analysis to and from IPs delivering wireless V2I and V2V capabilities. Given the complexity in today’s ICs, past methods such as expert inspection or simulation are inadequate. Similar to how formal augments functional verification, formal’s exhaustive nature identifies security violations in the ‘black space,’ the scenarios and abnormal conditions that aren’t foreseen by humans writing security-based tests.”
FuSa and formal verification
As functional safety verification (FuSa) goes hand-in-hand with security in the automobile, formal verification techniques play a role here, too.
“Formal verification is already in production use in many companies developing chips that need to comply with functional safety standards,” said Marchese. “Let’s consider quantitative FMEDA for ISO 26262, for example. You need to bring evidence that the reported safety metrics are correct and achieve the ASIL targets. In the case of avionics, you may have to prove that all the RTL code maps to specified requirements using elemental analysis, as stated in DO-254. Another application is independent output assessment of synthesis tools with formal equivalence checking for FPGA flows. The alternative — sadly still in use in many projects — is to run slow and hard-to-debug gate-level simulations and avoid advanced synthesis optimizations that could introduce bugs in the netlist. In all these cases, formal verification, whether exposed to the user or running under the hood with other analysis engines, enables very efficient and rigorous solutions.”
Further, the ISO 26262 standard and the Automotive Safety Integrity Level system can impose very high levels of resistance to faults. This is usually achieved via safety mechanisms such as Triple Modular Redundancy (TMR) or dual-core lockstep architectures, which are triggered in the presence of a faulty or corrupted behavior. While those requirements certainly can be verified with structural checks and simulation by injecting stuck-at, bridge, transition, or even transient faults, formal approaches can drastically accelerate diagnostic and coverage closure throughout the fault campaign.
“Indeed, the use of solvers is particularly efficient at identifying if a fault is controllable, in which case it is potentially dangerous, or if it is non-observable, in which case it is safe. The benefits are multiple. Formal engines provide a sense of definiteness and are also very versatile, as they can be applied before of after simulation, while seamlessly interacting with the same fault database,” Synopsys’ Boillet said.
Cadence’s Hardee added that functional safety verification is taken to mean that an overall system will remain dependable and function as intended, even in the event of an unplanned or unexpected occurrence (fault) to avoid unacceptable risk of physical injury or damage.
“Depending on the level of criticality of the system (e.g. levels ASIL A through D are defined in ISO 26262) there might be various design techniques to achieve the level – ranging from no special fault detection circuitry, through fault detection, fault correction, or redundant systems,” Hardee said. “The ability of the system to meet the required safety level usually is verified by introducing faults and measuring their detection and resultant corrective action by the system.”
He agreed that formal verification already plays a big role in functional safety verification as faults can be introduced by formal but usually, fault simulation is more effective for the number of faults that typically need to be checked. Formal verification usually helps with analysis before and after fault simulation.
Before fault simulation, formal analysis is performed on the fault list prior to fault injection in order to reduce the fault set by marking faults as untestable or unobservable per simulation test. This can significantly reduce fault simulation time while improving coverage metrics.
After fault simulation, an FSV app analyzes fault propagation to improve fault classification in order to meet or exceed safety specifications like ISO 26262. The ASIL classifications provide probabilities that must be met depending on whether faults are detected at checker outputs and can propagate to functional outputs. The worst faults are those that can propagate to functional outputs undetected. Formal analysis gives greater certainty that faults can never propagate to functional outputs or are always detected by checkers. Fault simulation alone depends on the quality of the testbench to reach these conclusions.
From safety analysis to safety verification, formal technologies address many challenges in safety-critical workflows, including structural analysis to reduce fault campaign scope, leveraging formal equivalency to perform tool chain assessment, and executing exhaustive fault injection and metric calculation, to name a few.
The exhaustive nature of formal technologies lends itself well to safety critical applications, ensuring products operate correctly and fail safely,” Mentor’s Wiltgen said.
Additionally, Michael Haight, director, Automotive Security, Micros, Security & Software Business Unit at Maxim Integrated asserted that for formal verification, a rule set has to be defined. “Who defines the rules? If they are publicly accessible standards, it seems attackers can see how devices are tested and therefore may exploit some weaknesses in the system by doing something not tested. Safety, on the other hand, is not vulnerable to hackers and the intent is to prove the standard is met. Therefore perhaps formal verification is a better fit for safety than security.”
Formal adoption
While the adoption of formal solutions is accelerating with improvements in ease of use and with tighter integration with the broader verification platform, further enhancements also are being made to provide an end-to-end solution that spans across RF, analog, power management, and MCUs/CPUs, Boillet said.
In order to deliver the highest value to designers, this is accomplished by ensuring all the components have a common understanding of safety techniques such as TMR and unified databases. Unified solutions that use various technologies such as simulation, formal, emulation and analog mixed-signal verification confirm the quality of safety mechanisms as per the Failure Mode Effect Analysis (FMEA) plan.
Standards certainly help with adoption, Hardee said, but there is a big variance in standards for functional safety versus security. “Hopefully the new ISO/SAE 21434 Cybersecurity standard will be a step in the right direction, but in general there is a lack of specific metrics for security verification compared with safety verification. Without metrics, the prevalent methodology is to verify what can reasonably be done, especially to check for known vulnerabilities. Best practice is currently to hand over the system to an attack lab (“red team” or “white hat” hackers) to try to break it. Common vulnerabilities databases help, but there is still much to do.”
At the end of the day, even though formal verification is ideally placed in safety critical workflows, it continues to experience adoption challenges due to requiring new skillsets beyond traditional design and verification. “The creation of new automotive and safety specific automated formal apps will drive higher levels of adoption. Additionally, better education on when and where to deploy formal capabilities across the larger safety tool chain would help increase adoption, Mentor’s Wiltgen said.
 |
 |
 |
 |
 |
 |
 |
 |
 |
Leave a Reply