This article takes a look at the most common memory-related errors,
and compares how well Rust and Ada
prevent you from making them in the first place.

TL;DR:
Rust is better at outright preventing common memory-related errors,
however Ada’s avoidance of dynamic memory allocation
and support for formal proof of correctness
help you avoid many of the common errors altogether.

Foreword #

The Rust programming language has
exploded in popularity
in the last few years,
consistently ranking as one of the
most loved languages
in Stack Overflow’s
Developer Survey.
Designed by Mozilla to be memory-safe,
it’s steadily gaining ground as a viable alternative to languages like C++.
This focus on safety has invited comparisons with Ada;
An older, but battle-tested language designed for safety-critical industries.
Despite all the things they have in common,
a bitter
rivalry
has grown between the Ada and Rust communities.
For years I’ve been defending Ada online from a motley crew of
angry Rustaceans,
crusty old greybeards,
and
bitter old haters.
Most of whom either haven’t used it,
or haven’t used it since Reagan was in office.
I’ve been critical of Rust’s design in the past,
but have I actually given Rust a fair go?
When it comes to memory safety,
how do the two languages really stack up?
Does Rust offer us anything new that Ada doesn’t?
Let’s find out!

This article assumes you’re already familiar with the basics of Rust.
If you’re not, the best place to start is
Learn Rust,
particularly the
Rust Book.
For an introduction to Ada,
check out AdaCore’s
Introduction to Ada.

Before we begin,
it’s worth noting that
you can do a lot in Ada without ever allocating heap memory,
or even using pointers at all.
In fact, most guides on Ada programming recommend avoiding pointers altogether.
Language constructs such as in/out parameter modes,
creating dynamically sized arrays at runtime,
and the ability to return variable length arrays from functions
address many of the scenarios where pointers would be necessary in other languages.
Keep this in mind when reading:
You can avoid many of these situations altogether in Ada.

All the examples in this article are tested on an x86-64 machine running Debian 12,
with glibc 2.36;
Compiled with GCC 12.2.0,
GNAT native 14.2.1,
and rustc 1.80.1.

Common Memory Errors #

Memory Leaks #

CWE-401: Memory Leak
refers to a program failing to release the memory that it’s allocated.
Left unchecked, a leaky program could drain all your system’s memory.
The most common cause of
memory leaks
in C is mismatched malloc(), and free() statements.

While not impossible¹,
Rust does actually make leaking memory pretty difficult.
Variables in Rust are automatically deallocated when their owner goes out of scope.
Most of the time this means a variable will be deallocated at the end of the scope it’s declared in.

For
reference counted
smart pointers, like Rc and Arc,
Rust will automatically deallocate the memory they point to when the reference count reaches zero.

In Ada, pointers are called Access Types.
Like in C, they point at a memory location;
However unlike C, they’re not an address.
This means you can’t assign an address to an access variable,
or perform arithmetic on it.

In Ada, dynamically allocated memory needs to be deallocated manually with the generic
Ada.Unchecked_Deallocation procedure.
With unchecked
referring to checking whether the variable being deallocated is still in use.

While Ada’s
controlled types
do support implementing RAII-like functionality,
under normal circumstances forgetting to manually deallocate heap memory will cause it to leak.

The only scenario where Ada will automatically²
deallocate memory is when the user specifies a static size for an access type’s storage pool
using the Storage_Size aspect.
This controls exactly how many bytes of heap memory can be allocated for variables of a particular type.
If this is specified, the compiler automatically allocates all the required memory up front³,
and automatically deallocates it when the type goes out of scope.
If this pool is exhausted, the program will raise a Storage_Error exception.

procedure Access_Type_With_Explicit_Pool_Size is
   --  This sets aside a total of 128 bytes for the pool of Int_Access.
   --  Allocating more than 128 bytes will raise a Storage_Error exception.
   type Int_Access is access Integer
   with Storage_Size => 128;
begin
   for I in 1 .. 16 loop
      declare
         Q : constant Int_Access := new Integer'(I);
      begin
         Put_Line (Q.all'Image);
      end;
   end loop;
end Access_Type_With_Explicit_Pool_Size;

Running Valgrind on the example above shows that the memory is indeed deallocated automatically.

Buffer Overflow #

CWE-119: Buffer Overflow
refers to reading or writing past the end of an array,
and into adjacent memory.
Buffer overflows are probably responsible for more
security vulnerabilities
than any other kind of bug,
and are a common technique for
jailbreaking
hardware.
The infamous
Morris Worm,
and Heartbleed
vulnerabilities both relied on buffer overflows.

void buffer_overflow() {
  char email_address[10];

  printf("Please enter your email address:n");
  // Modern versions of GCC will spew a litany of warnings about using 'gets'.
  gets(email_address);
  printf("Sending welcome email to %sn", email_address);
}

// $ gcc -o buffer_overflow buffer_overflow.c
// $ ./buffer_overflow
// $ Please enter your email address:
// $ anthony@this_will_overwrite_the_function's_return_address_on_the_stack.com
// $ Segmentation fault

One of the few things that Rust and Ada agree on is
runtime bounds checking.
Attempting to access an out-of-bounds array index will result in a ‘panic’.

fn overflow_this_buffer() {
    let mut buffer = [0; 10];

    let mut raw_input = String::new();
    println!("What array index should be cleared? ");
    io::stdin()
        .read_line(&mut raw_input)
        .expect("Failed to read line");
    let index: usize = raw_input
        .trim()
        .parse()
        .expect("Please enter a valid integer");

    buffer[index] = 0;
}

// $ cargo run
// $ What array index should be cleared?
// $ 12
// $ thread 'main' panicked at buffer_overflow.rs:14:5:
// $ index out of bounds: the len is 10 but the index is 12
// $ note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
// $ ...

Similar to Rust,
attempting to access an array index outside of its valid range will raise a
Constraint_Error exception at runtime,
which can be handled programmatically.
This is the same type of exception raised in the case of a scalar range constraint violation,
such as an integer overflow.

procedure Buffer_Overflow is
   Email_Address : String (1 .. 10);
begin
   Put_Line ("Please enter your email address:");
   Email_Address := Get_Line;
   Put_Line ("Sending welcome email to " & Email_Address);
exception
   when Constraint_Error =>
      Put_Line ("Buffer overflowed!");
end Buffer_Overflow;

--  $ alr run
--  $ Please enter your email address:
--  $ anthony@this_will_overflow_the_buffer.com
--  $ Buffer overflowed!

SPARK

SPARK is a subset of Ada which can be
formally verified.
Meaning that it’s possible to verify the absence of runtime errors in your code using formal methods.

All SPARK code is valid Ada,
but to determine whether the Ada code is valid SPARK I’m using
GNATprove.
GNATprove is a component of AdaCore’s GNAT
Ada compiler used to formally verify the correctness of SPARK code.
If you’re using Alire,
you can add GNATprove to your project by running alr with gnatprove.

Let’s see if we can reimplement the previous Rust example in SPARK,
and prove that a buffer overflow can’t occur.

procedure Overflow_This_Buffer
   with SPARK_Mode => On
is
   type Integer_Array is array (Positive range <>) of Integer;
   Int_Array : Integer_Array (1 .. 10) := [others => 1];
   Index_To_Clear : Integer;
begin
   Ada.Text_IO.Put ("What array index should be cleared? ");
   --  Read the new array size from stdin.
   Ada.Integer_Text_IO.Get (Index_To_Clear);

   Int_Array (Index_To_Clear) := 0;
end Overflow_This_Buffer;

Attempting to prove the absence of runtime errors gives us the following warnings:

buffer_overflow.adb:162:26: medium: unexpected exception might be raised
  162 |      Ada.Integer_Text_IO.Get (Index_To_Clear);
      |      ~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~

buffer_overflow.adb:164:18: medium: array index check might fail
  164 |      Int_Array (Index_To_Clear) := 0;
      |                 ^~~~~~~~~~~~~~
  reason for check: value must be a valid index into the array
  possible fix: postcondition of call at line 162 should mention Item 
  (for argument Index_To_Clear)
  162 |      Ada.Integer_Text_IO.Get (Index_To_Clear);
      |                         ^ here

The SPARK prover correctly notices that there’s nothing stopping us
from entering a value outside the array bounds.
It also points out that the Get
call we’re using to read the integer from stdin
can raise an unexpected Constraint_Error
at runtime if you type in anything that can’t be parsed as an integer.
To keep this example simple, we’ll ignore this warning and push on.
We’ll talk more about exceptions in SPARK
later
in the article.

If we wrap the Get call in a loop,
and poll the user continuously until we have a value within the array bounds,
SPARK can actually prove that a buffer overflow can’t occur.
(Remember to initialise the Index_To_Clear
variable to something outside this range!)

procedure Overflow_This_Buffer
   with SPARK_Mode => On
is
   type Integer_Array is array (Positive range <>) of Integer;
   Int_Array : Integer_Array (1 .. 10) := [others => 1];
   Index_To_Clear : Integer := Int_Array'First - 1;
begin
   while Index_To_Clear not in Int_Array'Range loop
      Ada.Text_IO.Put ("What array index should be cleared? ");
      --  Read the new array size from stdin.
      Ada.Integer_Text_IO.Get (Index_To_Clear);
   end loop;

   Int_Array (Index_To_Clear) := 0;
end Overflow_This_Buffer;

Use After Free #

CWE-416: Use After Free
refers to
dereferencing
a pointer after the value it points to has been freed.
The C standard specifies that doing so is
Undefined Behaviour
(ISO/IEC 9899:2018, Section J.2),
potentially leading to a variety of different stability and
security issues.
(ISO/IEC 9899:2018, Section 3.4.3).

Most of the time this just results in unpredictable behaviour because the pointer
now points to memory reallocated to something else.
But occasionally use-after-free’s
can be leveraged for something more sinister.

Rust’s borrow checker automatically prevents you from using a value after it’s been freed.
Calling drop to manually free a variable moves it,
meaning that any attempt to use it afterwards will raise a compile-time error.

fn use_after_free() {
    let greeting = "Hello, World!".to_string();
    drop(greeting);
    // This will trigger an error at compile-time, because the variable
    // `something` was moved by the first call to `std::mem::drop`.
    println!("{}", greeting);
}

Nothing prevents you from writing Ada code that dereferences an access type after it’s been freed;
However any access dereference triggers a runtime check to ensure it’s non-null.
Unlike in C,
freeing an access type in Ada automatically sets its value to null,
and any subsequent attempt to dereference it will raise a
Constraint_Error exception,
which can be caught and handled.

procedure Use_After_Free is
   type String_Access is access String;
   Example_String : String_Access := null;

   --  The Ada.Unchecked_Deallocation package is a generic package, and
   --  needs to be instantiated for each type to be deallocated.
   procedure Free is new
     Ada.Unchecked_Deallocation (String, String_Access);
begin
   Example_String := new String'("Hello, world!");
   Free (Example_String);

   --  This will raise a Constraint_Error exception at runtime.
   Put_Line (Example_String.all);
exception
   when Constraint_Error =>
      Put_Line ("Used after freed!");
end Use_After_Free;

The GNAT Ada compiler allows you to

disable runtime checking
with the -gnatp compiler switch.
In this case, dereferencing a null access type will result in the same kind of undefined behaviour you’d get in C.

Ada allows you to specify a null-excluding constraint on access types,
This restricts assignment to only non-null values,
and forbids any unchecked deallocation.

type Non_Null_String_Access is not null access String;
--  Since this is a 'null-excluding' access type, it must be initialised,
--  otherwise a Constraint_Error exception will occur immediately at runtime.
Example_String : Non_Null_String_Access := new String'("Hello, world!");
--  This will raise a compile-time error. The compiler won't let us
--  create an instance of Ada.Unchecked_Deallocation for a
--  null-excluding access type.
procedure Free is
  new Ada.Unchecked_Deallocation (String, Non_Null_String_Access);

SPARK

GNATprove will detect the use-after-free error in the above code,
and issue a warning⁴:

procedure Use_After_Free
   with SPARK_Mode => On
is
   type String_Access is access String;
   Example_String : String_Access;

   procedure Free is new Ada.Unchecked_Deallocation (String, String_Access);
begin
   Example_String := new String'("Hello, world!");
   Free (Example_String);

   --  This line will raise a warning during static analysis.
   Put_Line (Example_String.all);
end Use_After_Free;

use_after_free.adb:13:32: medium: pointer dereference check might fail
  13  |      Put_Line (Example_String.all);
      |                ~~~~~~~~~~~~~~~^~~

Note the removal of the exception handling block.
SPARK does technically allow run-time exception handling,
but only exceptions that are explicitly raised in the code.
Exceptions in SPARK are
complicated:
You can still explicitly raise exceptions with the raise statement,
but to be valid SPARK, the flow analyser will need to prove that the statement raising the exception can never actually be reached;
Making exceptions almost like a form of compile-time assertion.
This means that our Constraint_Error exception handler is unreachable,
and needs to be removed.

Double Free #

CWE-415: Double Free
refers to freeing a heap allocated variable more than once.
The C standard (as usual) specifies that doing so is Undefined Behaviour (ISO/IEC 9899:2018, Section J.2).
Double frees can be exploited in
various
ways
to cause all kinds of nonsense.

On Linux,
glibc
stores extra metadata about each allocated memory block right before the block’s address,
such as its size, and a magic number to identify it as a valid allocation.
When you pass an address to free,
glibc uses this metadata to determine the amount of memory being freed.
Freeing a small block of heap memory can place it in a cache of recently freed blocks,
known as a fast bin.
The next time you call malloc for a block of the same size,
glibc will give you the recently deallocated block from the fast bin,
rather than allocating new memory.
This process is much quicker than allocating a new block, hence the fast in the name.
Freeing the same address twice runs the risk of the same block being placed in the fast bin
multiple times.
This could lead to multiple subsequent memory allocations pointing to the same address.

This
article contains a great in-depth look at glibc’s heap implementation.

Rust’s borrow checker effectively prevents you from freeing the same variable more than once.
As mentioned earlier,
calling drop to free a variable will move it out of scope forever.

fn double_free() {
    let something = "Hello, World!".to_string();
    drop(something);
    // This will trigger an error at compile-time, because the variable
    // `something` was moved by the first call to `std::mem::drop`.
    drop(something);
}

According to
section 13.11.2
of the Ada Reference Manual,
freeing an access type with a null value has no effect,
just like in C (ISO/IEC 9899:2018, Section 7.22.3.3).
That’s a relief!
As mentioned earlier, freeing a pointer in Ada will automatically set its value to null,
preventing most accidental double free errors from causing any serious issues.

It’s still possible to cause a double free in Ada by creating an alias to a pointer.

procedure Double_Free is
   type String_Access is access String;

   Str_Acc       : String_Access;
   Str_Acc_Alias : String_Access;

   procedure Free is new Ada.Unchecked_Deallocation (String, String_Access);
begin
   Str_Acc := new String'("Hello, world!");
   Put_Line ("Pointer Address: " & Str_Acc.all'Address'Image);

   Str_Acc_Alias := Str_Acc;

   Free (Str_Acc);

   Put_Line ("Pointer Alias Address: " & Str_Acc_Alias.all'Address'Image);
   Free (Str_Acc_Alias);
exception
   when Program_Error =>
      Put_Line ("Program Error!");
end Double_Free;

--  $ alr run
--  $ Pointer Address:  25715368
--  $ Pointer Alias Address:  25715368
--  $ free(): double free detected in tcache 2
--  $ Program Error!

As you can see in the example above,
actually freeing the same memory location twice⁵ will raise a
Program_Error exception at runtime.
The below example shows how you can corrupt the heap by double freeing a pointer in Ada.
Again, Ada will raise a Program_Error exception when it gets the error signal from glibc,
which can be handled at runtime.

procedure Double_Free is
   type String_Access is access String;
   type String_Access_Array is array (1 .. 16) of String_Access;

   procedure Free is new Ada.Unchecked_Deallocation (String, String_Access);

   Str_Acc_Array   : String_Access_Array;
   Str_Acc_Array_2 : String_Access_Array;

   --  Create a pointer to alias one of the elements in the array.
   Str_Acc_Alias : String_Access;
begin
   for I in Str_Acc_Array'Range loop
      Str_Acc_Array (I) := new String'("Hello, world!");
   end loop;

   Str_Acc_Alias := Str_Acc_Array (8);

   for I in Str_Acc_Array'Range loop
      Free (Str_Acc_Array (I));
   end loop;

   --  Freeing the alias will add the same address to the fast bin twice,
   --  leading to a double free error.
   Free (Str_Acc_Alias);

   for I in Str_Acc_Array_2'Range loop
      Str_Acc_Array_2 (I) := new String'("Hello, again!");
   end loop;

exception
   when Program_Error =>
      Put_Line ("Program Error!");
end Double_Free;

--  $ alr run
--  $ malloc(): unaligned fastbin chunk detected 3
--  $ Program Error!

SPARK

Like Rust, SPARK has its own concept of
‘ownership’.
Assignment between access objects creates a transfer of ownership,
with the source object losing permission to read or write to the underlying allocated memory.

In this case, aliasing the string pointers in the examples above is not valid SPARK,
preventing us from causing this particular double free error.

alr gnatprove
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...

double_free.adb:14:13: error: "Str_Acc" is not readable
   14 |      Free (Str_Acc);
      |            ^~~~~~~
  object was moved at line 12 [E0010]
   12 |      Str_Acc_Alias := Str_Acc;
      |                       ^ here
  launch "gnatprove --explain=E0010" for more information

SPARK doesn’t allow you to use Unchecked_Deallocation
with a general access type (which we’ll discuss in more detail later),
so we can’t try to sidestep SPARK’s ownership system by doing something tricky like this:

procedure Double_Free
   with SPARK_Mode => On
is
   type String_Access is access all String;

   Str_Acc       : String_Access;
   Str_Acc_Alias : String_Access;

   procedure Free is new Ada.Unchecked_Deallocation (String, String_Access);
begin
   Str_Acc := new String'("Hello, world!");
   Put_Line (Str_Acc.all);

   --  Here we create an access to the dereferenced value of Str_Acc.
   Str_Acc_Alias := Str_Acc.all'Access;

   Free (Str_Acc);

   Free (Str_Acc_Alias);
end Double_Free;

SPARK sees what we’re up to and stops us in our tracks:

double_free.adb:13:17: error: instance of Unchecked_Deallocation with a 
  general access type is not allowed in SPARK
   13 |      procedure Free is new Ada.Unchecked_Deallocation (String, String_Access);
      |                ^~~~
  violation of aspect SPARK_Mode at line 6
    6 |     with SPARK_Mode => On
      |          ^ here

Race Conditions #

In a multi-threaded program,
a Race condition is a situation where the outcome of the program depends on the order in which the threads execute.
Because an operating system can switch between threads at any time in any order,
it’s impossible to guarantee when threads will access shared resources.
This really becomes a problem when two threads try to write to the same memory at the same time;
Leading to some of the most
infuriating,
time-consuming,
and
hair-ra