Below is a Q&A session with Fabrice Derepas, Chief Evangelist and Cofounder of TrustInSoft. Fabrice got his start in the telecoms industry as a systems architect and then worked as the CTO for startup companies. Fabrice joined the CEA, a French technology research laboratory, in 2003, where he was a head of lab and managed a department, led programs, and provided strategy for the CEA-LIST institute. Fabrice has a Ph.D. from the University of Paris 7, as well as an engineering degree from the Ecole Polytechnique.
Chief Evangelist and Co-Founder of TrustInSoft
What are formal methods for code analysis?
Formal methods are a mathematically rigorous approach to software verification. Instead of relying solely on testing, you can create a formal model of your code. This model captures the code’s behavior and interactions using the language of mathematics. It allows developers and testers to prove properties of code that lead to proving the correctness of their software systems. While these techniques have historically been limited to specialized experts and limited applications, revolutionary advances in tools, practices, and training within the formal methods community have facilitated the application of formal methods at a greater scale.
Formal methods are much more than just complicated mathematical techniques. Here’s how they translate to real benefits for your C/C++ projects:
- Exhaustive Analysis: Traditional testing can miss hidden bugs lurking in complex code. Formal methods, on the other hand, systematically explore all possible code paths, aiming to identify every potential issue. This significantly reduces the risk of undefined behavior (UBs) causing crashes, vulnerabilities, and unpredictable program behavior.
- Mathematical Guarantees: Beyond simply finding bugs, formal methods allow us to reason about the code’s properties mathematically. This enables us to provide you with mathematical proof that your code adheres to specific safety and security requirements.
How do formal methods exhaustively detect runtime errors?
- Property Verification: C and C++ comes with rules, like “do not read or write outside the bounds of an array”. By storing data values and knowing the source code, formal methods define desired properties the code must uphold. These properties often relate to safety and security aspects, like avoiding memory leaks, null pointer exceptions, or buffer overflows – all potential sources of runtime errors.
- Exhaustive Exploration: Formal verification methods systematically explore all possible execution paths within the formal model. This can involve techniques like model checking, which essentially “runs” the model through all its permutations to identify any violations of the defined properties.
How can formal methods help with ISO 26262 certification?
Formal verification allows for a sound analysis of the source code. TrustInSoft Analyzer is a TUV SUD ISO 26262 qualified tool for ISO 26262 certification up to ASIL D. TrustInSoft Analyzer allows you to focus on critical safety alarms with much fewer false positives than traditional static analysis tools. Target awareness and input generalization allow you to move through the development process faster with less effort and reduced HW/HIL cycles.
Use of Formal methods in software development life cycle
Formal verification helps developers and testers shift left in the SDLC. By bringing mathematical proof of the absence of undefined behavior at the source code level you can verify earlier, from the development of the code, that it is safe, secure, and reliable. With target emulation, you can also test the code as if on the final hardware, making it easier for teams to speed up the development process and efficiently work remotely.
Which industries use formal methods?
Critical safety formal methods tools originating from research labs and applied to critical code in aeronautic software for rockets are now used today to verify code in industries such as defense, industrial IoT, consumer devices, telecom, automotive, and medical devices.
Why use formal methods for static application security testing (SAST)?
Formal methods elevate SAST by offering a more rigorous and mathematically-backed approach. Unlike traditional methods relying on patterns, they analyze every possible code execution path, significantly reducing the risk of missing critical vulnerabilities. Formal methods go beyond just detection, providing mathematical proof that the code adheres to specific security properties. This translates to a higher level of assurance and a significant reduction in the attack surface by proactively eliminating undefined behavior, a major security threat in C/C++. Additionally, the formal verification process aids in code maintainability by generating clear reports, ultimately leading to more secure and reliable applications.
What is abstract interpretation?
Abstract interpretation is a formal technique used in computer science for statically analyzing programs. Unlike traditional testing that executes the code, static analysis examines the code itself, and its possible values to infer properties about its behavior. This optimized approach enables developers to run the equivalent of billions of tests (including software unit entry points, control and data flows, and exit points) in one test execution without the need for supercomputer-level resources.
Can I use formal methods to catch undefined behaviors in my C/C++ code, like buffer overflows or null pointer exceptions?
Formal methods are designed to catch all undefined behaviors including buffer overflows, null pointer exceptions, and use-after-free. TrustInSoft Analyzer is a sound tool that can guarantee that all bugs are found with no false negatives.
How much effort is involved in formally verifying a piece of C/C++ code compared to traditional testing?
Before exhaustive static analysis tools, there was additional effort involved. Using modern tools, you can analyze billions of inputs within seconds. TrustInSoft’s interactive GUI helps developers locate critical errors in the source code and guarantees a sound analysis without false negatives.
How well do formal methods handle complex C/C++ features like memory management and pointers?
TrustInSoft Analyzer is designed to detect all undefined behaviors including memory management issues and pointer issues with advanced exhaustive analysis using abstract interpretation.
What are the limitations of formal verification for C/C++ code? Are there certain types of bugs it can’t catch?
TrustInSoft’s formal methods analysis catches all undefined behaviors. This means all critical errors that could affect the functional safety or cybersecurity of the code are detected. It takes a syntactic approach and can interpret the meaning behind the code, meaning there could be a stylistic best practice “bug”. For bugs related to functional behavior other techniques, not described here, can be used.
Does using formal methods require a strong background in mathematics and logic?
Thanks to exhaustive static analysis tools like TrustInSoft Analyzer, you can easily take an incremental approach to safety, security, and reliability. You can start by verifying your own tests, then use input generalization to test the equivalent of billions of tests simultaneously, and for the most critical code obtain mathematical proof of zero undefined behaviors.
How does the cost-benefit analysis of formal verification compare to other techniques like static analysis tools?
TrustInSoft Analyzer overcomes the limits of traditional static analysis such as a large false positive rate and missed detection of critical undefined behavior. TrustInSoft is an advanced and highly accurate exhaustive analysis tool that can determine that the code will behave as specified. It also includes architecture awareness (implementation dependent information such as endianness, padding in structures) which allows for analysis without the physical target connected to the host. This means that tests can be run sooner in the development lifecycle without the physical target, and test capacity can increase leading to decreased costs for testing on the physical target of each developer/tester.
About TrustInSoft
TrustInSoft develops solutions that validate mission-critical software and eliminate attack vectors. TrustInSoft Analyzers reduce cyber risks, lower the cost of designing safety-critical systems, and reduce liabilities. Founded in 2013, the Paris-based company provides software developers, testers, and integrators with TrustInSoft Analyzer, an exhaustive static analysis tool that interprets source code using formal methods to detect all of the most frequent and dangerous families of threats and coding errors before deployment. TrustInSoft also offers professional services and expertise to formally audit safety and security-critical existing software components. For more information, visit https://trust-in-soft.com.
Learn more about TrustInSoft and get in touch with our exhaustive static analysis experts.
Related Categories