How 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.

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.

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.

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.

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.

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.

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.

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:

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.

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.