Menu
This post is Part 3 of a 3-part series derived from TrustInSoft’s latest white paper, “On the Road to Zero-Bug Vehicles by 2030.” To obtain a FREE copy, click here.
Software will drive the automotive industry for years to come. In Part 1 of this series, we looked at the key, software-driven trends expected to dominate the automotive sector over the next decade. In our previous post, we discussed five key challenges that could make or break many automotive OEMs and suppliers over the next ten years. Now, in the final installment of this series, we’ll examine an emerging technology that can help automotive companies meet those critical challenges by allowing them to guarantee their software is safe, reliable, and secure.
Exhaustive static analysis tools can be a significant, strategic part of the next-generation automotive software toolchain solution.
Exhaustive static analysis is a methodology that makes use of a variety of mathematical formal methods techniques to answer the questions users ask about their code. It takes the knowledge developed to guarantee the behavior of safety-critical systems and expands its scope to guarantee data security as well as safety and reliability.
Exhaustive static analysis can help automotive companies:
Exhaustive static analysis is also a framework where a broad range of formal methods collaborate. It contains algorithms that choose the right formal method according to the question being asked. And it can switch seamlessly from one formal method to another, depending on the problem it has been asked to solve.
In other words, exhaustive static analysis is a holistic approach, not one of brute force. Rather than trying to solve every problem using a single formal method, the framework has been designed to determine which combination of formal methods is best suited to solving the problem at hand and to apply those methods in the best way possible.
What’s more, exhaustive static analysis does all this in a way that does not disrupt the normal software development process. It brings the value of mathematical formal methods to software development in a way that’s practically invisible to the developer.
With an exhaustive static analysis framework, all the aforementioned selection and application of formal methods are invisible to the developer. From a users’ perspective, they are simply testing their code in a manner very similar to what they’re already accustomed.
The framework expands and automates the testing process. For example, by adding just a couple of lines of code to your test script, you can expand a limited set of test cases to a complete set of test cases covering the complete range of possible values for all input variables.
Again, you don’t need a Ph.D. in formal methods to use these tools. Any developer can handle them. Users don’t even need to be aware of the method the tool is using. They just express the problem and the tool does the analysis automatically. It’s extremely easy for users to find answers. The framework chooses the right tools for the problem and switches tools on the fly.
For example, our own platform, TrustInSoft Analyzer for C/C++, employs several abstract memory models to analyze the software being validated. This process is completely hidden from users. They needn’t know anything about them.
TrustInSoft Analyzer has been designed and developed so that no matter how a C/C++ developer programs, the tool will extract the meaning of the code so that the right formal methods are applied.
TrustInSoft Analyzer was even cited in a National Institute of Standards and Technology report to the White House[i] for having demonstrated that it can be used to formally guarantee that (1) no known undesired behaviors (bugs) are present in a system and that (2) the system behaves exactly according to its specification.[ii], [iii]
Using exhaustive static analysis, you can guarantee the absence of coding flaws—like buffer overflows, for example—that hackers exploit. That means it’s now possible to end the cat-and-mouse game of hackers finding vulnerabilities and developers scrambling to remove them. With exhaustive static analysis, you can eliminate all such flaws before hackers even have a chance to look for them.
In fact, you’ll eliminate many flaws conventional tools fail to catch. For example, using TrustInSoft Analyzer, existing test scripts downloaded from GitHub and a fuzzer, we recently uncovered thirteen undefined behaviors (UB) in the popular, open-source network protocol analyzer and IP packet sniffer Wireshark (Figure 2).[iv] These flaws had been in the Wireshark code for years, left undiscovered by other tools.
Then, if you want to go a step further, you can guarantee the absence of entire families of vulnerabilities in your code—exactly what the NIST told the White House.
Exhaustive static analysis enables companies to guarantee to customers and regulatory bodies that their applications are completely free of coding flaws and conform exactly to their functional requirements. These guarantees are essential in safety-critical applications, like those for autonomous driving, and in security-critical applications, like those for automotive connectivity.
One other benefit of exhaustive static analysis: developer satisfaction.
Exhaustive static analysis helps developers perfect the applications they’ve worked so hard to create. It helps them quickly find and eliminate those subtle coding errors that are so easy to make without even being aware of them… and that are so hard to track down after they’ve been made. It saves developers time. It makes them feel great about what they’ve built. All these factors can be advantageous in attracting and retaining the top-flight software development talent that will be harder and harder to come by over the next decade.
Plus, exhaustive static analysis does all this in an automated, fully-comprehensive manner. In short, exhaustive static analysis finds all the needles in your haystack.
Tracking down and eliminating undefined behaviors and guaranteeing the safety, security, and reliability of an automotive software application is an iterative, cumulative process. The process benefits from taking a step-by-step hierarchical approach, stepping from a basic level of proof to more advanced levels depending on what a given application requires.
For example, TrustInSoft Analyzer offers three levels of analysis.
Level 1 (testing) is the simplest to use. It is completely automated—as easy to use as launching a compilation of your code. Yet, Level 1 analysis will uncover a large portion of the bugs present in the code without yielding any false positives. The Wireshark analysis mentioned earlier was done exclusively with Level 1.
Level 1 is ideal for use in a continuous integration process and can thus help your organization transition to one. New bugs can be stripped daily, before they accumulate, without developers having to look for them. Daily use of Level 1 analysis helps prevent verification backlog.
Level 2 (exhaustive testing) will guarantee that all coding defects have been eliminated from your code. In other words, when you complete Level 2 testing and correction, you’ll have no bugs present that can be exploited by hackers or cause unexpected behaviors in your application. Use of Level 2 requires some operator intervention, but it has a very low false-positive rate (<10/10,000LOC on average). TrustInSoft Analyzer’s Level 2 analysis provides you with a guarantee of the security of your system if all the confirmed defects are corrected.
Finally, for those applications that need it, there is Level 3 (functional proof). TrustInSoft Analyzer’s Level 3 analysis guarantees your code fulfills its specification exactly. It is your best guarantee of safety. Functional proof takes longer and is more costly than defect testing, but for code that needs to be perfect—like safety-critical AD applications—it’s well worth it. The return is huge. You’ll have a guarantee that your critical application works exactly as specified.
In summary, exhaustive static analysis helps you deal with software complexity by automating your software verification. It eliminates the cat-and-mouse process of finding and fixing bugs through conventional testing. It guarantees safety, reliability and cybersecurity through the use of mathematical formal methods. And finally, it simplifies compliance with ISO 26262 and ISO 21434.
TrustInSoft Analyzer’s formal methods methodology verifies the semantics, or the meaning, of the source code, to be sure that no software defects exist.
Over the next ten years, the automotive industry will undergo a rapid transformation driven by trends in autonomous driving, connectivity, powertrain electrification, and shared mobility (ACES). The result will be rapid growth in the automotive software market, which will make software competencies the single biggest driver of success within the industry.
Automotive OEMs and their suppliers will be under extreme pressure to adopt new software development tools and methodologies to improve their productivity. Increased reliance on software within the industry will make it necessary to abandon traditional software testing methods and adopt automated verification strategies and tools that can guarantee safety, security, and reliability.
One such methodology, exhaustive static analysis, can provide guarantees that your automotive software application is 100% free of coding defects, impervious to cyberattack, and behaves exactly as specified. Exhaustive static analysis can help automotive industry players adapt to agile development and continuous integration practices, and ensure compliance with ISO 26262,
ISO 21434, and other safety and security regulations.
For more information on TrustInSoft Analyzer, visit our product page.
[i] Black, P.; Badger, L.; Guttman, B.; Fong, E.; Dramatically Reducing Software Vulnerabilities: Report to the White House Office of Science and Technology Policy; National Institute of Science and Technology (NIST), November 2016.
[ii] Bakker, P.; Providing assurance and trust in PolarSSL; May 2014
[iii] Regehr, J.; Comments on a Formal Verification of PolarSSL; https://blog.regehr.org, September 2015.
[iv] Zupkus, A; The Wireshark Challenge: how to ensure the security of open-source projects with formal methods; TrustInSoft, May 2020.
