Three Paths To Memory Safety for Embedded

Memory problems are a constant worry for teams developing software for embedded systems. Whether you are building a doorbell, a self-driving car, a printer or an airplane. As much as 70% of security vulnerabilities are due to memory issues. On top of that, a lot of effort is spent on trying to find as many problems during development as possible. And still, problems always slip through.

In this presentation, we will look at three paths to memory safety that provide increasing guarantees and make software more safe and secure:

• The memory safe subset of the MISRA C/C++ rules that catch defects before they are merged into your main branch
• Rust as a memory and type safe language that prevents memory corruption
• Ada SPARK as a memory and type safe language with provable absence of runtime errors and optional provable functional correctness.

For each of the options, we will look at how easy it is to adapt, what the benefits are, what type of guarantees you can derive from the technology as well as some actual use cases of the technology in real-world projects.

This is a must-watch presentation if you are building embedded systems that have to be safe and secure and if you are wondering on how to make your systems more memory safe.

What this presentation is about and why it matters

How do you keep embedded software safe when the codebase is growing, regulations are tightening, and the usual C and C++ habits still dominate? Mark Hermeling approaches that tension through a keynote that mixes terminology cleanup, concrete code examples, and a walk through safer development paths, with Ada and SPARK as the main anchor points. He also brings in Rust, static analysis, formal methods, and agentic AI, showing where each fits in a realistic embedded workflow. If you work on safety-critical or security-sensitive systems, or you are looking for a clearer way to talk about memory safety, this session gives you a useful map.

Who will benefit the most from this presentation

• Embedded software engineer responsible for C or C++ code, especially if you are inheriting a large existing codebase
• Safety or security engineer who needs to explain memory safety in practical terms to a team
• Tech lead or architect evaluating Rust, Ada, or formal methods for a new or critical subsystem
• Developer working under functional-safety or cybersecurity pressure, with update and compliance concerns
• Engineering manager exploring where AI-assisted development can fit into verification-heavy workflows

What you need to know

You will get the most from this talk if you are comfortable reading basic embedded code and familiar with the usual problems around arrays, pointers, runtime checks, and build-time diagnostics.

• General familiarity with C or C++ is helpful
• Some awareness of Rust basics will make the comparison easier
• It helps to know what static analysis is, even if you have not used formal methods before
• A rough understanding of embedded safety or security constraints will make the examples land faster

Glossary (terms used in this talk)

• LLM (large language model): A statistical machine learning model trained on large corpora of text to generate or analyze natural language outputs.
• MISRA: A widely used set of guidelines for writing safer and more portable C and C++ code in embedded systems.
• SPARK: A subset of Ada designed to support formal verification by restricting language features that complicate reasoning. It is commonly used to prove properties such as absence of runtime errors or functional correctness.
• SMT solver (Satisfiability Modulo Theories solver): A solver that determines whether logical constraints are satisfiable under theories such as integers, arrays, and bit-vectors. These solvers are widely used in symbolic execution, concolic testing, and other automated reasoning tasks.
• loop invariant: A condition that remains true before and after each iteration of a loop. Loop invariants help prove that a loop preserves important properties while it runs.
• loop variant: An expression that changes in a controlled way across loop iterations and is used to prove termination. A loop variant typically decreases toward a bound, showing that repeated execution cannot continue forever.
• precondition: A requirement that must hold before a function or procedure is called. Preconditions make contracts explicit and allow callers and verification tools to reason about valid inputs.
• postcondition: A requirement that must hold after a function or procedure completes. Postconditions describe the guaranteed outcome of a routine when its preconditions are satisfied.

Toolbox (mentioned in this talk)

• AdaCore GNAT Pro: An Ada and SPARK toolchain for building, analyzing, and verifying Ada-based embedded software. It includes compiler and proof tooling used for safety-focused development.
• GNATprove: A formal verification tool for SPARK that checks program properties such as absence of runtime errors and contract compliance. It is used to prove properties statically rather than relying only on testing.
• ALIRE: A package manager and build tool for Ada and SPARK projects. It helps fetch dependencies and manage toolchains for Ada-based development workflows.
• CodeSonar: A static analysis platform for finding defects, security issues, and code-quality problems in C and C++ projects. It is commonly used to catch memory and control-flow issues before runtime.
• GitLab Ultimate: GitLab’s higher-tier platform that adds advanced security scanning and workflow features to CI/CD pipelines. It can surface vulnerabilities in merge requests and support approval workflows.
• AddressSanitizer: A compiler-based runtime checker that detects memory errors such as buffer overflows and use-after-free bugs during execution. It is often used in testing to catch defects that static checks may miss.

Final thoughts

Practical, opinionated, and unusually broad in scope, this keynote gives you a way to think about memory safety that goes beyond slogans. The real value is the vocabulary and mental model shift, from runtime errors to contracts, proofs, and where AI can or cannot help. It will be especially useful if you live in embedded C or C++, are responsible for critical software, or are exploring Ada, SPARK, or Rust as part of a safer workflow. The talk leaves you with a serious question: what would change if correctness were designed in, not chased afterward?

This overview is AI-generated from the session transcript. Spot an issue? Let us know.