Formal methods are the future of embedded software verification
Embedded electronics today are software-centric, which implies that the underlying code needs to be free of bugs and secure. In automotive, the rise of driver assistance systems and the pursuit of fully autonomous vehicles requires highly advanced and complex software. These critical systems should ideally be completely bug-free and secure, allowing no room for error. The critical software systems used in aerospace, though traditionally more robust and secure, are also becoming more complex and face similar issues. Software complexity is a key issue that the industry needs to address. Even on the consumer side, the upcoming EU Cyber Resilience Act will force manufacturers to take legal responsibility for vulnerabilities in their products. To address these issues formal methods offer a path forward.
Formal methods mathematically prove that code is error-free and works as specified. Although proposed for a long time, the complexity of implementing formal methods has held it back. TrustInSoft, a pioneer in formal verification, have now come to market with such a service, potentially changing the way companies verify their code. eeNews talks to Caroline Guillaume, Chief Executive Officer of TrustInSoft, about the issues that make formal methods a key tool in testing software for bugs and functionality, as well as its importance for the future of embedded software.
eeNews: Can you outline the key issues that formal methods resolve for C/C++ and explain how they accelerate code analysis for developers?
Formal methods leverage mathematical techniques to specify and verify the behaviour of software systems. This is particularly crucial for C/C++, languages known for their power but also for being prone to errors like buffer overflows, memory leaks, and null pointer dereferences that can lead to security vulnerabilities and system crashes.
The most crucial way formal methods resolve these issues is by ensuring memory safety through the mathematical proof of the absence of memory-related errors, such as buffer overflows and use-after-free vulnerabilities. TrustInSoft Analyzer provides a higher level of assurance than traditional testing by rigorously verifying code and, in effect, guaranteeing freedom from those sorts of errors.
Beyond memory safety, formal methods detect runtime errors like division by zero and integer overflows, which can cause unexpected program behaviour. They also verify that the code behaves as intended according to its specifications, ensuring functional correctness. Not only that, but formal methods help ensure adherence to coding standards like MISRA and CERT-C, often required in safety-critical industries.
Formal methods enable early bug detection, reducing the cost and effort of fixing them later in the development cycle. This resonates particularly well with the need for cost and time savings. By providing mathematical guarantees about code behavior, formal methods reduce the need for extensive testing. They also encourage developers to write more precise and well-defined code, leading to improved code quality and maintainability. Plus, tools like TrustInSoft Analyzer automate the verification process, making it more efficient and scalable. It’s essential to find those errors early, when they’re easiest and cheapest to fix.
eeNews: At Embedded World 2025, you announced code analysis services for C/C++/Rust hybrid code. As Rust is touted to be safer and more secure than C/C++, what issues need to be addressed when coding with Rust?
While Rust indeed offers significant safety advantages over C/C++ due to its memory safety features, it’s not a silver bullet. You might think of it as a strong shield, but one that still needs to be actively managed. When integrating Rust with C/C++, several issues need to be addressed. The interface between Rust and C/C++ code, the Foreign Function Interface (FFI) boundary, is a potential source of vulnerabilities. Incorrectly handled data types or memory management across the FFI boundary can lead to errors. You might think you’re safe, however, it’s like having a secure door but leaving the window open.
Rust allows developers to use “unsafe” code blocks to perform operations that the compiler cannot guarantee to be safe. While sometimes necessary for performance or interfacing with external libraries, unsafe code can introduce vulnerabilities if not carefully managed.
Keep in mind that Rust’s memory safety features do not prevent logic errors. Formal methods can help verify the functional correctness of Rust code, ensuring that it behaves as intended. Even with a safe language, you still need to make sure the logic is sound.
Rust projects rely on external crates (libraries), and vulnerabilities in these dependencies can affect the security of the entire project. You might have a fortress, but if your suppliers have weak links, you’re still vulnerable. Combining Rust and C/C++ code can increase the complexity of the system, making it more difficult to reason about and verify. It’s a bit like mixing two complex chemicals – you need to understand how they interact.
TrustInSoft’s code analysis services for C/C++/Rust hybrid code tackle these issues by providing comprehensive verification, analysing both Rust and C/C++ code to identify vulnerabilities and ensure memory safety. They also include FFI boundary analysis, verifying the correctness of data exchange and memory management across the FFI boundary, as well as unsafe code auditing, identifying and auditing unsafe code blocks to ensure they are used correctly and do not introduce vulnerabilities
eeNews: Traditional software testing has been relied on and still is in many cases, so why should formal methods be considered?
Traditional software testing is, of course, essential, but it does have limitations. Think about checking a bridge by driving a few trucks over it. You might be able to see if those trucks make it, but you don’t know if every vehicle will make it, especially the really heavy ones or the ones driven recklessly. Testing can only demonstrate the presence of bugs, not their absence. Formal methods, on the other hand, provide mathematical guarantees about code behaviour, offering a higher level of assurance.
Formal methods offer exhaustive verification, exploring all possible execution paths. To continue the metaphor, it gives you a blueprint that guarantees the bridge can handle any load, under any conditions. This is especially critical in safety-critical systems where a single bug can have catastrophic consequences.
Formal verification also enables early bug detection, identifying issues early in the development cycle, which significantly reduces the cost and effort of fixing them later. It’s much cheaper to fix a problem in the design phase than after the bridge is built.
Formal methods also encourage developers to write more precise and well-defined code, leading to improved code quality and maintainability. You have a well-documented and organised blueprint that makes it easier to maintain the bridge over time.
eeNews: The EU Cyber Resilience Act (CRA), which comes into force at the end of 2027, will hold manufacturers liable for actively searching for vulnerabilities, disclosing and fixing them throughout the product’s lifecycle. How do formal methods specifically address this need?
The EU Cyber Resilience Act places significant responsibility on manufacturers to ensure the cybersecurity of their products throughout their lifecycle. This is crucial, as manufacturers will now be legally responsible for the security of their products, not just at the time of release, but for years to come.
Formal methods provide a powerful tool for meeting these requirements by enabling proactive vulnerability detection. Instead of waiting for vulnerabilities to be discovered by attackers, formal methods can identify them early in the development cycle, before they can be exploited.
Formal methods also provide a comprehensive security analysis of the code, ensuring that all possible execution paths are checked for vulnerabilities. This is far more thorough than traditional testing, which can only cover a limited number of scenarios.
Perhaps most importantly, formal methods provide mathematical guarantees about the absence of memory safety vulnerabilities, giving manufacturers confidence in the security of their products.
Furthermore, formal methods can be used to continuously monitor the code for new vulnerabilities throughout the product’s lifecycle. This is crucial, as new vulnerabilities are constantly being discovered, and manufacturers need to be able to respond quickly to emerging threats.
Formal methods tools can generate reports that demonstrate compliance with the CRA requirements. This is essential for manufacturers who need to prove that they have taken reasonable steps to ensure the security of their products.
By using formal methods, manufacturers can proactively address cybersecurity risks and reduce their liability under the CRA. This brings the status quo from a reactive to a proactive approach to security, and formal methods are a key enabler of this shift.
eeNews: As we increasingly rely on factory automation, microservices-based architecture presents a viable path for OEMs to implement for OTA updates, user authentication, machine and IoT gateways, diagnostics, and machine setup. What value do formal methods bring to these scenarios?
Microservices architecture offers many benefits, including scalability, flexibility, and independent deployment. However, it also introduces new security challenges.
Securing each independent service in a microservices architecture is crucial for DevOps teams to prevent data breaches. Formal methods can help address these challenges by securing individual microservices, verifying the security of each microservice, and ensuring that it is free from vulnerabilities.
Formal methods can also be used to verify the correctness and security of interactions between microservices, ensuring that data is exchanged securely and that no vulnerabilities are introduced.
This technique can be used to ensure the integrity of data as it flows through the microservices architecture. This is critical for ensuring that data is not tampered with or corrupted as it moves between different services.
Finally, formal methods tools can automate the security analysis process, making it more efficient and scalable. This is essential for managing the complexity of microservices architectures, which can involve hundreds or even thousands of individual services.
eeNews: Apart from CRA, how are formal methods being applied to ensure compliance, and in which industries?
Formal methods are being applied in various industries to ensure compliance with safety and security standards. There’s a need to meet the increasingly stringent requirements of regulators and customers who demand secure and reliable products.
For example, in the automotive industry, ISO 26262, which is typically required by regulatory bodies, mandates the use of formal methods for safety-critical systems. This is a key market for TrustInSoft, as automotive manufacturers are increasingly relying on formal methods to ensure the safety of their vehicles.
In the aerospace industry, DO-178C requires the use of formal methods for the development of safety-critical airborne systems. This is another key market for TrustInSoft, as aerospace companies cannot afford to compromise on safety.
In the medical device industry, FDA regulations require the use of formal methods for the development of safety-critical medical devices. This is a particularly sensitive area, as failures in medical devices can have life-threatening consequences.
In the nuclear power industry, nuclear regulatory bodies require the use of formal methods for the development of safety-critical control systems. This is another area where safety is paramount, as failures in nuclear power plants can have catastrophic consequences.
In these industries, formal methods are used to verify that the software meets the required safety and security standards, reducing the risk of accidents, security breaches, and financial losses. This actively builds confidence in the software and ensures that it operates safely and reliably.
eeNews: What is your view on AI-generated code, and does it have an impact on applying formal methods, given that AI-generated code is often more verbose and could include code blocks written by hackers specifically to get developers to add backdoors unwittingly?
AI-generated code presents both opportunities and challenges for software development. While it can automate code generation and improve developer productivity, it also introduces new security risks. It’s a double-edged sword. It can speed up development, but it can also introduce new vulnerabilities if not used carefully. AI-generated code poses security risks as coding assistants are trained on public codebases, many of which contain vulnerable code.
The impact on applying formal methods is significant. For starters, AI-generated code can be more verbose and complex than human-written code, making it more difficult to analyse and verify. It’s like trying to understand a foreign language that is full of jargon and idioms.
Also, AI-generated code may contain vulnerabilities due to the training data used to generate it. If the training data includes vulnerable code, the AI may learn to generate similar code.
And, as you mentioned, there is a risk that AI-generated code could include backdoors or malicious code inserted by attackers. This is a particularly concerning threat, as it could allow attackers to gain unauthorised access to systems and data.
Therefore, the use of AI-generated code necessitates rigorous verification using formal methods to ensure its security and correctness. We need to look at AI-generated code with a healthy dose of skepticism and verify it thoroughly before deploying it.
eeNews: What markets are you seeing the most significant interest in formal methods, and why?
We are seeing the most significant interest in formal methods in several key markets. These are the markets where the cost of failure is high, and the benefits of formal methods are most apparent.
The automotive market is a prime example. Given the increasing complexity of automotive software and the stringent safety requirements of ISO 26262, automotive manufacturers are increasingly turning to formal methods to ensure the safety of their vehicles.
The aerospace market is another key area of interest. Due to the critical nature of airborne systems and the requirements of DO-178C, aerospace companies are heavily invested in formal methods to ensure the safety of their aircraft.
The industrial IoT market is also showing strong interest in formal methods. Increasing reliance on automation and the need to protect against cyberattacks is leading to IoT leaders recognising the value of formal methods in securing their systems.
The medical device market is another area of growing interest. Medical devices are safety-critical nature of medical devices and the requirements of FDA regulations, medical device manufacturers are increasingly adopting formal methods to ensure the safety of their products.
In these markets, the benefits of formal methods in terms of improved safety, security, and reliability are well-recognised.
eeNews: Given the development time for consumer products, are companies behind the curve in being prepared for compliance, and can formal methods help address this, considering the low-cost structure of the industry?
Many companies are indeed behind the curve in preparing for compliance with emerging cybersecurity regulations like the CRA. The development time for consumer products can be lengthy, and companies may not have fully integrated security considerations into their development processes.
Formal methods can help address this challenge by accelerating compliance by providing a more efficient and effective way to identify and fix vulnerabilities.
Formal methods can also reduce development costs. By identifying bugs early in the development cycle, formal methods can reduce the cost of fixing them later. It’s much cheaper to fix a problem in the design phase than after something has been put into production or out into the field.
Furthermore, formal methods can improve product quality. Formal methods can improve the overall quality of the product, leading to increased customer satisfaction and reduced warranty costs.
While formal methods may require an initial investment, the long-term benefits in terms of reduced risk, improved compliance, and lower development costs can outweigh the initial expense.
eeNews: As formal methods are purported to ensure 100% validation coverage, do they eliminate all risks, or are there still issues to be considered? Can formal methods help mitigate legal consequences by proving the code is safe?
Formal methods cannot protect against hardware errors, such as memory corruption or CPU failures. Environmental factors can also affect the behaviour of the system. Formal methods cannot account for environmental factors, such as radiation or extreme temperatures, that can affect the behaviour of the system.
However, formal verification can help mitigate legal consequences by providing evidence that the code was developed using rigorous and well-defined processes. By demonstrating that the code has been formally verified, companies can show that they have taken reasonable steps to ensure its safety and security. TrustInSoft’s tools provide comprehensive reports that can be used to demonstrate compliance with industry standards and regulations. You can provide evidence that the code was developed with due diligence and that reasonable steps were taken to ensure its safety and security.
Caroline Guillaume is the Chief Executive Officer of TrustInSoft. She has an extensive background working in the critical software industry, notably at Thales Digital Identity and Security where for 14 years she contributed to the Sales division, including as the VP of Sales – Software Monetization Europe and VP of Banking and Telecom Solutions Sales out of Singapore. She also previously worked as director of Product Marketing at Gemplus. Caroline holds an engineering degree from Télécom SudParis.
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
