Formal Verification Why Testing Alone Is Not Enough: Software Security for Modern Vehicles

Related Vendors

dataTec AG

Wuxi InfiMotion Technology Co., Ltd.

Modern vehicle software is too complex for pure testing. Hidden execution paths, memory errors and multicore effects often remain undetected. Formal verification becomes a decisive factor here.

Most errors in embedded software for vehicles are not caused by missing functions. They result from hidden execution paths that violate safety, timing or memory assumptions under certain runtime conditions. These problems are often caused by undefined behavior, memory corruption or multicore interference and can go undetected for months or even years before they occur in real operation.

The challenge is not that these errors are unknown. Rather, they are invisible to traditional workflow verification. Unit tests, integration tests and hardware-in-the-loop tests can validate thousands of scenarios without ever reaching the paths that trigger the error. While static analysis helps reduce errors, it still misses the critical execution paths.

In modern vehicle software, these hidden paths are not uncommon, but an inherent consequence of real-time multicore scheduling. They arise from task scheduling, interrupts, cache effects, memory management and complex data interactions between dozens of ECUs and centralized vehicle computing platforms. Even a single error hidden among billions of possible execution paths will eventually surface once the software is deployed in a fleet of vehicles.

This is why critical vehicle failures still occur even after validation. Unfortunately, the error has always been there, it was just not tested.

Memory errors are a major cause of these failures. Problems such as buffer overflows, out-of-bounds accesses, post-release usage and integer overflows often do not immediately cause the system to crash. Instead, they affect system behavior unnoticed until a later event turns this hidden corruption into a visible error.

Memory corruption is the main method attackers use to compromise embedded vehicle systems remotely. In connected vehicles, hidden reliability flaws also become hidden cybersecurity vulnerabilities that can spread to entire fleets.

The core problem is not the availability of tools, but the coverage. Modern vehicle software has become too extensive and too complex for random sample-based tests to prove that critical errors are not actually present—no matter how many tests are performed. For this reason, detection-based verification is no longer sufficient, and mathematically comprehensive verification is required for ASIL C and ASIL D systems.

Increasing Software Complexity And Risks in Vehicle Systems

Modern vehicle architectures have evolved into tightly integrated, software-defined platforms. Centralized computing units and domain controllers now coordinate braking, steering, propulsion, perception, energy management and data connectivity. These systems execute millions of lines of software under strict real-time conditions.

The resulting state space is enormous and cannot be fully examined by tests alone. Interrupts, task scheduling, cache behavior, DMA transfers and inter-task communication create execution paths that are practically impossible to test. The reuse of software across vendors and model generations increases this risk. A latent error in a shared component can spread to entire fleets and persist for years.

Over-the-air (OTA) updates, the radio-based transmission of software updates to vehicles, accelerate software changes and shorten validation times. This increases the reliance on early verification to prevent bugs from entering production code, as late detection is costly and disruptive.

Why testing alone cannot close the security gap

Tests check the functional behavior, but cannot guarantee correctness. They can show that errors are present, but never prove that there are no errors. Embedded software runs under non-deterministic conditions that are influenced by scheduling, interrupts, asynchronous I/Os and sensor inputs. The number of possible runtime behaviors far exceeds the capabilities of any test strategy.

Coverage metrics offer only limited certainty. Issues such as race conditions and memory corruption often depend on rare time sequences and specific data patterns that may never occur in controlled test environments. Therefore, hidden errors often only come to light during integration, fleet operation or under specific time and load conditions, when they become costly and uncertain to fix.

Storage Security As A Structural Weakness

Memory safety violations are a constant risk in vehicle software. Issues such as buffer overflows, out-of-bounds accesses, use-after-free errors, integer overflows and null pointer dereferencing can lead to undefined behavior that affects error detection and compromises predictable system behavior.

C and C++ dominate vehicle development due to their performance and hardware access requirements. However, manual memory management leads to subtle errors that can remain undetected for a long time. Parallel execution further increases this risk as it leads to race conditions that result in unpredictable and hard-to-diagnose state corruption.

Languages such as Rust provide stronger guarantees for memory safety, but do not eliminate all risks in safety-critical systems. Rust code often interacts with hardware registers, RTOS kernels, DMA buffers and legacy C/C++ components and uses unsafe blocks for performance-critical paths. These conditions again lead to risks such as memory corruption, data conflicts and logic errors. Rust panics add another error mode that needs to be controlled. If not fully analyzed and limited, panic behavior can bypass error handling, break timing assumptions, and cause system failures that are difficult to predict through testing.

Static analysis and the risk of false negatives

Static analysis tools detect many errors early, but rely on approximations to remain computationally practical. This leads to false positives, which require manual checking, and false negatives, which overlook real errors.

False negatives are the biggest security risk. A single undetected memory safety issue can affect error handling and lead to a series of failures in various subsystems. These failures often occur during integration or fleet operations, when corrections are costly and recertification poses a major risk to delivery dates and regulatory compliance.

Economic reasons for evidence-based verification

The requirements for functional safety are becoming ever stricter. ISO 26262 increasingly demands proof that entire classes of error modes are eliminated at software level and not just mitigated by redundancy or monitoring. At the same time, the costs for validation and verification are rising rapidly. This is due to stricter safety standards and the growing economic consequences of delayed defect detection, recertification and fleet-wide corrections.

Together, these trends point to a shift from detection-based workflows to mathematically rigorous verification strategies for safety-critical automotive software.

From Recognition to Detection

Formal verification uses mathematical proofs instead of random execution. Techniques such as abstract interpretation enable a comprehensive analysis of all possible execution paths and inputs within defined limits.

For vehicle systems, this means that the absence of entire fault classes, such as memory safety violations and undefined behavior, must be verified. This eliminates false negatives and reduces false positives. Developers can confirm whether life-threatening failure modes in braking, steering, power management and perception systems can occur at all, rather than relying on probable test results.

Impact on development, security and cyber security

Comprehensive verification improves productivity by reducing false alarms and enabling earlier troubleshooting. It reduces rework, integration delays and recertification costs. For large, existing code bases and third-party components, mathematical verification provides objective assurance without extensive rework.

Formal verification strengthens functional safety by proving that dangerous behaviors cannot occur during runtime. This is critical in systems where software errors can directly lead to loss of braking, steering or drive control. From a cyber security perspective, eliminating memory security flaws reduces a large attack surface and thus improves vehicle safety.

Conclusion

Memory safety violations are a constant risk in vehicle software. Problems such as buffer overflows, out-of-bounds accesses, use-after-free errors, integer overflows and null pointer dereferencing can lead to undefined behavior that affects error detection and compromises predictable system behavior.

Mathematically complete verification offers a path from detection to proof. As software increasingly controls the core functions of vehicles, the transition from tested to mathematically verified software is a necessary development in vehicle construction.

(sg)

Tips & tricks for plastics professionals

Future trends in additive manufacturing