Memory Safety in Ada and SPARK through Language Features and Tool Support

by Forough Goudarzi – Nov 15, 2023

Introduction

Memory safety bugs are among the most dangerous, stubborn and common software weaknesses. According to the rankings by Common Weakness Enumeration 2023 reports, the top of the list goes to out-of-bounds write, and there are other memory safety bugs among the top 15. Google (in 2021) and Microsoft (in 2019) revealed that more than 70% of their security bugs are due to memory safety issues. Given the extent and severity of the issues, the National Security Agency recommends that organizations adopt memory-safe programming languages.

Memory-safe languages help protect against these bugs and manage memory automatically rather than relying on programmer-provided checks, thus mitigating most memory safety issues. However, they differ in the level of protection, mechanisms, and support tools.

Ada and SPARK are strongly typed languages that provide memory safety through a combination of language features, run-time checks, and static and dynamic analysis tool support. These will be described in the following sections.

Features Supporting Memory Safety in Ada

Strong Typing: In Ada, each variable must be declared with a specific type, and type conversion needs to be explicit. This allows type consistency to be checked at compile-time, preventing a wide range of programming errors, such as Access of Resource Using Incompatible Type ('Type Confusion') and Improper Input Validation errors that can lead to memory safety issues.

Tasking: Ada’s tasking model implements concurrency safely, through constructs such as rendezvous and protected objects. Rendezvous provides synchronized communications between tasks and allows tasks to wait for each other at specific points in the program. Protected objects make sure that accessing shared resources is performed in a coordinated manner, enforcing “concurrent read, exclusive write”. Both constructs help prevent race conditions and data inconsistencies in concurrent applications. How protected objects can be applied in Ada is explained in this blog.

Parameter Modes: Parameter modes help ensure that data is passed between subprograms in a safe and controlled manner and prevent unauthorized memory access. There are three parameter modes: in, out, in out corresponding to input, output and both input and output parameters respectively. Thus a parameter defined with in mode cannot be modified within the subprogram.

Storage Pools: These are heap areas used for storing objects by dynamically allocating or deallocating memory. Ada provides a default memory pool for dynamic allocations, and also allows the user to define application-specific storage pools. With the latter feature, a user can implement the behavior of memory management for a given pointer type (for example, maintaining a pool of fixed-size blocks to avoid fragmentation, with constant time for allocation and deallocation).

Safe Pointers: In other languages, pointers are the main cause of many memory bugs, such as dereferencing a null or out-of-bounds pointer, use after free, and double free. Ada protects programmers from pointer dangers in the following ways:

Pointers in Ada are implemented through a more abstract, machine-independent facility known as “access types.” Values of these types have a default initial value that designates no object, and can designate both dynamically allocated objects as well as declared objects (i.e., those that are on a notional stack). Values designating allocated objects are created via the reserved word “new” as in some other languages. Values designating declared objects are created via the attribute ‘Access, applied to the declared object itself. No other means of creating values exists, absent an explicitly unchecked conversion, so the facility is safer than those that allow arbitrary creation of pointer values, say via addresses. The only way to deallocate is via an explicitly unchecked facility. Thus an access value is always meaningful, absent explicit use of an unchecked facility.

Providing alternative constructs that can be used instead of pointers. Parameter modes, unconstrained arrays, and dynamically sized objects without using a heap are constructs that can replace typical pointer usages. Below is an example of how unconstrained arrays can be used.

Excerpt showing passing an unconstrained array to a subprogram instead of using pointers

procedure Ex_Unconstrained_Arr is
   
   --  defines an unconstrained array type
   type Unconstrained_Arr is array (Natural range <>) of Float;
   
   -- defines a subprogram that gets an uncostrained array as input
   procedure InOut_Unconstrained_Arr (UA : in out Unconstrained_Arr) is
   begin
      for I in UA'Range loop
         UA (I) := UA (I) + 1.0;
      end loop;
   end InOut_Unconstrained_Arr;

   UA1 : Unconstrained_Arr := (3.2, 1.4, 1.6);
begin

   InOut_Unconstrained_Arr (UA1);
   for I in UA1'Range loop
         Put_Line (Float'Image (UA1 (I)));
   end loop;

end Ex_Unconstrained_Arr;

Detecting an attempt to dereference a null pointer (Access Check). The null value is a special access type value that does not designate any object. Any attempt to dereference that value raises a run-time exception. The null value is provided as the default initialization any time a variable of an access type is created, so it is not possible to have an uninitialized pointer in Ada. When a variable of an access type is unchecked deallocated it is set to null, preventing that variable from being the source of a double free.

Excerpt showing Access Check fails due to null pointer dereferencing

procedure Ex_Access_Check is

   type Integer_Ptr is access Integer;
   Ptr : Integer_Ptr; -- Default initialized to null
   B : Integer;

begin
  -- accessing a null pointer --> raises Constraint_Error
  Ptr.all := 10;

  -- null pointer dereferencing --> raises Constraint_Error
  B := Ptr.all;
   
end Ex_Access_Check;

Preventing dangling references to declared objects through compile-time and run-time accessibility checks. Ada provides an attribute (‘Access) that returns an access value designating the declared object to which the attribute is applied. Use of the resulting access value is rejected by the compiler if it could create a dangling reference (see Accessibility Check below). A similar check is applied at run-time when converting a value from one access type to another.

Supporting user-defined storage management to prevent dangling references. Manual storage reclamation needs to be programmed with extreme care, since deallocating an object too soon can cause a dangling reference, while deallocating too late (or not at all) can lead to storage leakage. Ada provides a mitigating solution: controlled types, through which the programmer can define the semantics of operations that are invoked automatically during object creation, assignment, and destruction. This facility can be used to implement storage management strategies such as reference counts. Since deallocation occurs automatically and only when safe, dangling references are prevented.

Preventing null pointer dereferencing using subtype with null exclusion which ensures that null values are not assigned to an access subtype.

Excerpt showing Access Check fails due to assigning null value to a null exclusion access type

procedure Ex_Null_Exclusion is

type Integer_Ptr is access Integer;

-- defines A as null exclusion access type ensures the input of procedure -- is not a null pointer
procedure Print (A : not null Integer_Ptr) is
 begin
   Put_Line (A.all'Img);
   -- No need for the compiler to generate a run-time check that
   -- A is non-null
end Print;

end Ex_Null_Exclusion;

Run-Time Checks and Exceptions: Ada performs several run-time checks, and among them the following contribute to mitigating memory safety errors. If a check fails an exception is raised that can be handled properly to prevent unsafe conditions.

Index Check: Ada performs bounds checking on array accesses and operations at run-time to verify that the index used to access a specific component is within the array bounds. This ensures that memory outside the bounds of an array is not accessed, preventing buffer overflows. Failing an Index Check will raise Constraint_Error and prevent undefined / unsafe behavior.

Excerpt showing Index Check fails

procedure  Ex_Index_Check is

   type Integer_Array is
     array (Positive range <>) of Integer;

   function Inc_Value_Of (A : Integer_Array; I : Integer)
                      return Integer
   is
   
   begin
      return A (I)+10;
   end Inc_Value_Of;

   Arr_1 : Integer_Array (1 .. 10) := (others => 1);
             
   Arr_2 : Integer_Array (1 .. 5) := (others => 0);         

begin
   -- raises Constraint_Error as Index Check fails
   -- in the call of Inc_Value_Of(Arr_2, 10) 
   Arr_1 (10) := Inc_Value_Of (Arr_2, 10);

end Ex_Index_Check;

Overflow Check: This verifies that the value of a scalar object is within the specified range of its type; with Ada, there is no wraparound. While wrapping scalars might be an intended behavior in some circumstances, it can lead to software bugs including memory issues. One example is when the result is used to determine the offset or size in memory allocation. Failing this check raises Constraint_Error. If wrapping semantics is desired, the programmer can use a modular (unsigned) integer type.

Excerpt showing Overflow Check fails

procedure  Ex_Overflow_Check is

   A : Integer := Integer'Last;
begin

   -- raises Constraint_Error due to integer wraparound
   A := A + 1;
end  Ex_Overflow_Check;

Range Check: Verifies that a scalar value is within a specific range. Ada allows user-defined types and subtypes with a specified range (an invariant on values of the type or subtype). This is useful when the type represents values such as size, length, frequency, speed, etc. which have application-specific ranges. Range checks ensure that assignment to a variable does not violate the type/subtype invariant; a violation would introduce undefined behavior, possibly including unsafe memory accesses.

Excerpt showing Range Check fails

procedure Ex_Range_Check is

   subtype Sub_Int is Integer range 1 .. 50;

   I : Sub_Int;

begin
   I := 52;  -- raises Constraint_Error
end Ex_Range_Check;

Storage Check: Verifies that when new objects are created, either on the stack or in a Storage Pool, there is enough memory space, and if not, the Storage_Error exception is raised. This check can help prevent out-of-bounds read and write.

Discriminant Check: Ensures that accessing fields in a variant record is safe. When a program tries to access a field that is not valid for a variant record, Constraint_Error is raised, preventing Reliance on Data/Memory Layout and Access of Resource Using Incompatible Type ('Type Confusion') errors.

Excerpt showing Discriminant Check fails

procedure Ex_Discriminant_Check is

   type Message_Type is (Number, Pointer);

      type Message_Buffer (MT : Message_Type) is record
   case MT is
    when Number =>
           Num : Integer;
    when Pointer =>
           Ptr : access Integer;
end case;
   end record;

    Number_MB : Message_Buffer (MT => Number);
   Var : Integer := 0;
begin

   Number_MB.Num := 21; -- OK
   Var := Number_MB.Ptr.all;  -- raises Constraint_Error 

end Ex_Discriminant_Check;

Length Check: Makes sure that in array assignments both arrays have the same length. This helps to avoid out-of-bounds read and write in array operations.

Excerpt showing Length Check fails

procedure Ex_Length_Check is

   type Integer_Array is
     array (Positive range <>) of Integer;

   Arr_1 : Integer_Array (1 .. 10);
   Arr_2 : Integer_Array (1 .. 9) :=
             (others => 1);

begin

  -- Length Check fails --> raises Constraint_Error
  Arr_2 := Arr1;
 
  end Ex_Length_Check;

Accessibility Check: This check, introduced earlier, prevents dangling references for access values designating declared objects (the checks apply to access types designating subprograms as well, but that does not involve memory management). The check can be done at compile-time, generally, because access objects cannot exist longer than their corresponding types, and the compiler can use that fact to determine if the possibility for a dangling reference exists.
To explain, consider an access type named “A,” designating objects of some type named “D”. Object “O” is an existing, (aliased) declared object of type D. We can legally create a value of type A designating O under the right circumstances.
Specifically, access values designating declared objects are created by applying the attribute ‘Access to the intended object, i.e., O’Access in our case. The type for the resulting access value is determined by the context, let’s say A. The compiler can then compare the “lifetime” of this access type A to the lifetime of the declared object O, rejecting the code if the lifetime of O is not at least as long as that of A.
The compiler uses the lifetime of the access type in the comparison because no objects of an access type can exist longer than the access type itself. Therefore, if the lifetime of A is longer than that of O, there might exist some variable somewhere, of type A, that could become a dangling pointer if assigned a value designating O. To preclude that possibility, O‘Access is illegal in that specific situation.
For example, in the following excerpt, the access type Integer_Ptr is the target type for the access value M’Access because that is the type for the left-hand side of the assignment. However, Integer_Ptr has a longer lifetime than M, hence, M’Access is illegal. If it were legal, the assignment to the non-local variable Ptr would be a dangling reference.

Excerpt showing Accessibility Check fails

procedure Ex_Accessibility_Check is
   type Integer_Ptr is access all Integer;
   Ptr : Integer_Ptr := new Integer'(10);
begin

   declare
      M : aliased Integer;
   begin
  
      -- this is rejected by the compiler because the Accessibility Check fails  
      Ptr :=  M'Access;
      end;

   Ptr.all := 20; -- if the Accessibility Check were not performed,
                           -- Ptr.all would be a dangling reference
end Ex_Accessibility_Check;

In the example above, the check occurs at compile-time. This is the general case. Failures appear early in the project life-cycle, prior to deployment, so they are both dramatically less expensive to correct and impose no overhead during execution. However, in some circumstances the check must occur at run-time. In those cases, an exception is raised if the check fails.

Features Supporting Memory Safety in SPARK

SPARK is a language (based on Ada) and a toolset that supports formal verification of program properties ranging from secure information flow to full functional correctness. SPARK provides the applicable memory safety features from Ada (user-defined storage pools are not in SPARK), but the checks (except Storage Check) are statically proven before the code is executed. In addition, SPARK defines an ownership concept, enhancing memory-safety when dealing with pointers.

Allocated Objects Ownership: SPARK uses an ownership system inspired by Rust and a set of rules for managing access types to simplify the verification and specification of a program's behavior during pointer operations.

The ownership rules ensure that any allocated object has a single owning reference at any given point in the program's execution. An object’s ownership may change over time - through moving or borrowing - but at any given point in time, every object has a single owner, see this blog for more information.

The single-owner model statically prevents dangling references and unsafe concurrent access to allocated objects.

Tools Supporting Memory Safety in Ada and SPARK

Practically, the features of a programming language alone are insufficient to prevent all memory safety issues. However, analysis tools can help detect potential memory issues in software early in the development life cycle, when they are least expensive to correct. AdaCore provides a variety of static and dynamic analysis tools for Ada and SPARK, and they are particularly useful in high-integrity applications. Among the following tools, the first three are used for Ada code, the last one for SPARK, and GNATstack can be used for both.

GNATfuzz: Memory issues might only happen in response to unusual inputs, therefore they can be difficult to find through traditional testing, such as unit and integration testing. GNATfuzz can detect corner case vulnerabilities by automatic, repeated, and highly frequent execution of tests and generation of new test cases.

Ada code can be fuzzed more effectively than code written in less memory-safe languages, since Ada’s run-time checks can capture faulty behavior including memory faults.

CodePeer: CodePeer is an Ada source code analyzer that detects run-time and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors easily at any stage of the development life-cycle. It can detect the following memory vulnerabilities.

Buffer overflow/underflow
Variant record field violation
Use of incorrect type in inheritance hierarchy
Race condition
Use of uninitialized variables
Null pointer dereferencing
Incorrect arguments in call
Missing/Incorrect synchronization
Infinite loop

GNATcheck: This static analysis tool lets developers define a set of coding rules (e.g. a set of permitted language features) and then checks the source code against them. Among its capabilities, it can detect memory vulnerabilities such as uses of uninitialized local variables, incorrect assumptions about array bounds, infinite recursion, and incorrect data alignment.

GNATstack: This static analysis tool computes the maximum required stack usage for each task in an Ada or SPARK program. It performs per-subprogram stack usage computation and control flow analysis.

GNATstack can analyze complex code, including object-oriented applications using dynamic dispatching, and determine the maximum stack usage automatically.

GNATprove: This SPARK-specifics static analysis tool performs the following:

Language conformance: Checks SPARK source code for conformance with the SPARK language specification which includes borrow checking
Flow analysis: Checks the initialisation of variables and subprograms’ input/output dependencies
Deductive verification (program proof): Checks the absence of run-time errors, validity of critical program properties, and functional correctness with respect to formally specified requirements

Posted in #memory safety #safe programming languages #Ada #SPARK

About Forough Goudarzi

Forough holds a Ph.D. in Electronic and Computer Engineering from Brunel University London. She has prior experience as a research fellow and technical author, as well as a background in the telecommunications industry.