How Language Design Impacts Security | AdaCore

Request Pricing

Download

Tools

Compilation Toolchain

GNAT Pro

GNAT Pro for Ada

GNAT Pro for C/C++

GNAT Pro for Rust

Formal Proof

SPARK Pro

Static Analysis

GNAT Static Analysis for Ada

CodeSonar for C/C++

Dynamic Analysis

GNAT Dynamic Analysis Suite

Services

Training & Services

Enterprise Training

Public Training

Mentorship

Get an Overview<br>Explore All Offerings

Ready To Go?<br>Contact a Technical Expert

Languages

Ada

C/C++

Rust

SPARK

Ready To Go?<br>Contact a Technical Expert

Industries

Avionics

Automotive

Defense

Medical

Rail

Security

Space

Learn how NVIDIA Adopted SPARK for Security-Critical Software Development<br>View Case Study

Company

About AdaCore

Careers

Partners

Careers<br>View Opportunities

Explore Resources

Publications

Papers

Books

Videos

AdaCore Digest

More Resources

Newsroom

Blog

Case Studies

Events

AdaCore's GitHub

The AdaCore Blog<br>Explore

Learn Ada & SPARK<br>Explore

Community

Academia

Download

Get Started with Ada<br>Learn More

Support

GNAT Tracker Login

Cybersecurity Center

Release Notes

Documentation

Development Logs

Product Roadmap<br>Learn More

Jun 30, 2026How Language Design Impacts Security

There is a lot of talk about memory-safe programming languages such as Rust, Ada, and SPARK, and how they help programmers write safer, more secure code by avoiding many of the issues that trigger undefined behavior in languages like C and C++. Most of this talk makes broad sweeping statements, and to be fair, I have been guilty of that as well.<br>In discussing some of this with my colleagues this past week, I realized that it is not very difficult to make a table and clearly state what types of problems can be mitigated. We have a very detailed classification of common programming problems in the form of the CWE list. We can create a table listing each CWE and/or CWE class, along with how each programming language addresses that category. You will find the table below.<br>But first, we need to clarify the memory-safe languages, the mitigation capabilities they offer, and how we document each CWE's applicability to each language.<br>Our table will not include all CWEs; only those that at least one of the languages can prevent. For example, CWE-327, Use of a broken/risky cryptographic algorithm, is not covered. This is not something that a language can help with.<br>Our table will use ‘No’ if the language does not provide protection against a particular CWE, ‘Dynamic’ if the protection is a run-time protection, and ‘Static’ if it is a compile-time protection. The difference is clear: a stack-based buffer overrun (CWE-121) in Ada and Rust is caught at runtime; in SPARK mode Silver, it is caught statically before runtime during the GNATprove run.<br>The first column documents safe Rust. We will not consider unsafe Rust, as many of the protections go out of the window. Unsafe Rust is needed, for example, if you need access to device memory in an embedded setting, but a design best practice is to handle that in an abstraction layer and return to safe Rust directly above it. We marked Rust as having Runtime protection for Integer Overflow and Underflow (CWE-190, CWE-191), with a footnote that this applies only to debug builds or release builds with overflow-checks=true.<br>The second column documents pure Ada, without pragma Suppress or Unchecked_* usage. These features are sometimes used in accessing hardware, though rarely, as Ada allows hardware memory to be described through Representation clauses. They are also used in C-interoperability. The best practice is to realize that you are fighting the language when you need these language features, and to sit down and see if there is a better way to design the software.<br>The third column covers SPARK mode Silver. SPARK code in which GNATprove does not have any unproven check_messages and no warnings. You will see a couple of concurrency warnings, for example, that SPARK cannot cover statically. A good reference for the SPARK Modes is the following booklet by Thales and AdaCore:<br>https://www.adacore.com/books/implementation-guidance-spark.

The CWEs are grouped into base groups, with their children underneath them. We roll the results up to the group if the results are all the same. For example, on CWE119, we roll SPARK Silver up to ‘Static’, but leave Rust and Ada as ‘--’ as some of the children rows are Runtime and some are Static.<br>For the concurrency-related CWEs, we have assumed the use of Ada/SPARK on a single core with the Ravenscar profile, which uses a priority ceiling protocol using protected objects.

Want to learn more? Contact a technical expert here.

Author

Mark Hermeling

Head of Technical Marketing, AdaCore Mark has over 25 years’ experience in software development tools for high-integrity, secure, embedded and real-time systems across automotive, aerospace, defence and industrial domains. As Head of Technical Marketing at AdaCore, he links technical capabilities...