Memory Safety by Design: A Proactive Approach to Embedded Systems Security

Embedded systems are becoming increasingly complex, and with that complexity comes increased risk. The rush to add features and connectivity can sometimes overshadow crucial security considerations, leading to vulnerabilities that can be exploited. Instead of treating security as an afterthought, what if you baked it into the development process from the start? This makes a "memory safety by design" approach necessary and is also the reason why tools like formal verification are becoming essential for developers.

The Rising Tide of Cyber Threats in Embedded Systems

The threat landscape is evolving. The EU Cyber Resilience Act (CRA) is a clear signal that regulators are taking embedded device security seriously. Manufacturers are now responsible for actively searching for vulnerabilities, fixing them, and disclosing them publicly. This includes releasing devices without known vulnerabilities, and maintaining security throughout the product's lifespan with timely updates. That's a tall order, especially when dealing with deeply embedded systems where resources are often limited.

This also extends beyond regulatory pressure. High-profile software failures in software-defined vehicles (SDVs) are a stark reminder of what happens when security isn't prioritized. The move towards centralized computing platforms can inadvertently create architectures with high coupling and low cohesion, making systems more complex and harder to maintain.

Essential Pillars of Memory Safety

How do you build memory safety into your embedded systems from the ground up? These are the basic pillars of memory safety:

• Vulnerability Identification: Start with a Software Bill of Materials (SBoM). Know what's in your software, and identify potential vulnerabilities in each component. Code hardening, fuzz testing, and architecture reviews are all valuable techniques.
• Proactive Toolchain Utilization: Leverage your compiler. Modern toolchains like GCC and Clang offer a wealth of options for detecting potential security flaws. Compiler warnings (e.g., -Wconversion, -Warray-bounds) can catch integer overflows, array bounds violations, and other memory-related issues. Static analysis can identify potential vulnerabilities before you even run the code.
• Microservices: OEMs are increasingly using microservices to implement features such as OTA (Over-The-Air) updates or user authentication. These ready-made solutions have technology-agnostic interfaces that offer cost and time savings. A well-structured modular monolith design makes it easier to extract these microservices, enhancing security by isolating root privileges.
• Regular Security Testing: Frequent testing is critical, and automation is your friend. Catch regressions and new vulnerabilities early.
• Secure Updates: Ensure updates are securely distributed, encrypted, and protected against tampering. Ideally, offer automatic installation options for ease of use (and to encourage users to actually install the updates).

The Power of Formal Verification and Abstract Interpretation

Traditional testing methods are good, but they aren't enough. They can only show the presence of bugs, not their absence. This is why we need formal verification.

Formal verification uses mathematical techniques to prove the correctness of your code. Tools like TrustInSoft Analyzer employ techniques such as abstract interpretation to analyze all possible execution paths and guarantee the absence of runtime errors, memory leaks, and other vulnerabilities. This gives you a mathematical guarantee that your code is memory-safe.

Think of it this way: static code analysis helps detect vulnerabilities related to buffer overflows or use-after-free, and formal verification is the method to achieving mathematical proof of memory-safe software.

Why is this important? Because memory vulnerabilities are a major source of security breaches. Buffer overflows, use-after-free errors, and integer overflows can all be exploited by attackers to gain control of your system. By eliminating these vulnerabilities before deployment, you can significantly reduce your attack surface.

Navigating Compliance Standards

Stringent requirements such as ISO 26262 for automotive, DO-178C for aerospace, and various cybersecurity compliance standards are growing priorities. Formal verification offers a pathway to meeting these requirements. By providing mathematical evidence of code correctness, you can demonstrate compliance with greater confidence.

Memory Safety Made Accessible

Memory safety is more than a "nice-to-have" feature; it's a critical requirement for modern embedded systems. The increasing complexity of these systems, coupled with the evolving threat landscape and stringent regulatory requirements, demands a proactive approach. By incorporating memory safety into the design process, leveraging advanced toolchains, and employing formal verification techniques, you can build more secure, reliable, and resilient embedded systems. If you are using C/C++/Rust, it's time to consider how you can start leveraging formal verification to eliminate runtime errors and achieve memory safety in your own projects.