A Hole in Ada Type Safety

Florian Weimer

Ada aims to restrict unsafe language features which break type safety to a set of constructs which can be easily spotted in source case. Examples include unchecked deallocation, unchecked conversion and explicit address handling. This note shows that a combination of safe-looking language features can be used to undermine type safety, too.

The standard way to show that type safety has been broken in a language is to implement a cast function Conversion from any type Source to any type Target:

   type Source is private;
   type Target is private;
function Conversion (S : Source) return Target;

This generic function can be used like Ada.Unchecked_Conversion:

with Ada.Text_IO;
with Ada.Unchecked_Conversion;

with Conversion;

procedure Convert_Test is
   type Integer_Access is access all Integer;
   J : aliased Integer;
   J_Access : Integer_Access := J'Access;
   function Convert is new Conversion (Integer_Access, Integer);
   function Unchecked_Convert is new Ada.Unchecked_Conversion
     (Integer_Access, Integer);
   Ada.Text_IO.Put_Line (Integer'Image (Convert (J_Access)));
   Ada.Text_IO.Put_Line (Integer'Image (Unchecked_Convert (J_Access)));
end Convert_Test;

How can we implement Conversion? It turns out that discriminant records with defaults combined with aliasing do the trick:

function Conversion (S : Source) return Target is
   type Source_Wrapper is tagged record
      S : Source;
   end record;
   type Target_Wrapper is tagged record
      T : Target;
   end record;
   type Selector is (Source_Field, Target_Field);
   type Magic (Sel : Selector := Target_Field) is record
      case Sel is
	 when Source_Field =>
	    S : Source_Wrapper;
	 when Target_Field =>
	    T : Target_Wrapper;
      end case;
   end record;
   M : Magic;
   function Convert (T : Target_Wrapper) return Target is
      M := (Sel => Source_Field, S => (S => S));
      return T.T;
   end Convert;
   return Convert (M.T);
end Conversion;

When the inner function Convert is called, the discriminant Sel of M has the value Target_Field, thus the component M.T can be dereferenced. The assignment statement in Convert changes the discriminant and the value. But the source value S is still reachable as an object of type Target because the parameter T aliases the component M.T, so the return statement executes without raising an exception.

The two tagged records are used to force that the inner Convert function receives its parameter by reference. Without them, an implementation would be free to pass the discriminant record Magic by copy, and aliasing would not occur.

Our implementation lacks the full power of Ada.Unchecked_Conversion because it does not support limited or unconstrained types. However, it is sufficient to break type safety.

Addendum: Robert A Duff noted that this was already known in the Ada 83 timeframe. According to paragraph 3.7.2(4) <http://www.adaic.org/resources/add_content/standards/95aarm/AARM_HTML/AA-3-7-2.html#I1973> in the standard (Ada 95 Annotated Reference Manual with Technical Corrigendum 1, MITRE Corporation, 2000, retrieved 2011-04-30), the call to Convert is erroneous on its own, and not the return statement which uses the stale reference.

Addendum (2015): A Rust variant (for the unsafe language extension) of this approach has been published as A Type Safety Hole in Unsafe Rust).


Florian Weimer
Home Blog (DE) Blog (EN) RSS Feeds Impressum