The implementations of the tls client and server applications can now be formally verified by the SPARK tools.

wrapper/Ada/spark_sockets.adb

@@ -0,0 +1,138 @@
+-- spark_sockets.adb
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
+with Interfaces.C;
+
+package body SPARK_Sockets is
+
+   function Inet_Addr (Image : String) return Optional_Inet_Addr is
+      A : Inet_Addr_Type;
+   begin
+      A := GNAT.Sockets.Inet_Addr (Image);
+      return (Exists => True, Addr => A);
+   exception
+      when others =>
+         return (Exists => False);
+   end Inet_Addr;
+
+   procedure Create_Socket (Socket : in out Optional_Socket) is
+      S : Socket_Type;
+   begin
+      GNAT.Sockets.Create_Socket (S);
+      Socket := (Exists => True, Socket => S);
+   exception
+      when others =>
+         Socket := (Exists => False);
+   end Create_Socket;
+
+   function Connect_Socket (Socket : Socket_Type;
+                            Server : Sock_Addr_Type)
+                            return Subprogram_Result is
+   begin
+      GNAT.Sockets.Connect_Socket (Socket, Server);
+      return Success;
+   exception
+      when others =>
+         return Failure;
+   end Connect_Socket;
+
+   function To_C (Socket : Socket_Type) return Integer is
+   begin
+      --  The call to GNAT.Sockets.To_C can never raise an exception.
+      return GNAT.Sockets.To_C (Socket);
+   end To_C;
+
+   procedure Close_Socket (Socket : in out Optional_Socket) is
+   begin
+      GNAT.Sockets.Close_Socket (Socket.Socket);
+      Socket := (Exists => False);
+   end Close_Socket;
+
+   function Set_Socket_Option (Socket : Socket_Type;
+                               Level  : Level_Type;
+                               Option : Option_Type)
+                               return Subprogram_Result is
+   begin
+      GNAT.Sockets.Set_Socket_Option (Socket, Level, Option);
+      return Success;
+   exception
+      when others =>
+         return Failure;
+   end Set_Socket_Option;
+
+   function Bind_Socket (Socket  : Socket_Type;
+                         Address : Sock_Addr_Type)
+                         return Subprogram_Result is
+   begin
+      GNAT.Sockets.Bind_Socket (Socket, Address);
+      return Success;
+   exception
+      when others =>
+         return Failure;
+   end Bind_Socket;
+
+   function Listen_Socket (Socket : Socket_Type;
+                           Length : Natural) return Subprogram_Result is
+   begin
+      GNAT.Sockets.Listen_Socket (Socket, Length);
+      return Success;
+   exception
+      when others =>
+         return Failure;
+   end Listen_Socket;
+
+   procedure Accept_Socket (Server  : Socket_Type;
+                            Socket  : out Optional_Socket;
+                            Address : out Sock_Addr_Type;
+                            Result  : out Subprogram_Result) is
+      C : Socket_Type;
+   begin
+      GNAT.Sockets.Accept_Socket (Server, C, Address);
+      Socket := (Exists => True, Socket => C);
+      Result := Success;
+   exception
+      when others =>
+         Socket := (Exists => False);
+         Address := (Family => GNAT.Sockets.Family_Unspec);
+         Result := Failure;
+   end Accept_Socket;
+
+   procedure To_C (Item       : String;
+                   Target     : out Byte_Array;
+                   Count      : out Byte_Index) is
+   begin
+      Interfaces.C.To_C (Item       => Item,
+                         Target     => Target,
+                         Count      => Count,
+                         Append_Nul => False);
+   end To_C;
+
+   procedure To_Ada (Item     : Byte_Array;
+                     Target   : out String;
+                     Count    : out Natural) is
+   begin
+      Interfaces.C.To_Ada (Item     => Item,
+                           Target   => Target,
+                           Count    => Count,
+                           Trim_Nul => False);
+   end To_Ada;
+
+end SPARK_Sockets;

wrapper/Ada/spark_sockets.ads

@@ -0,0 +1,137 @@
+-- spark_sockets.ads
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
+--  GNAT Library packages.
+with GNAT.Sockets;
+
+--  The WolfSSL package.
+with WolfSSL;
+
+--  This is a wrapper package around the GNAT.Sockets package.
+--  GNAT.Sockets raises exceptions to signal errors but exceptions
+--  are not supported by SPARK. This package converts raised exceptions
+--  into returned enumeration values by functions indicating success
+--  or failure.
+--
+--  The intended use of this package is to demonstrate the usage
+--  of the WolfSSL Ada binding in Ada/SPARK code.
+package SPARK_Sockets with SPARK_Mode is
+
+   subtype Byte_Array is WolfSSL.Byte_Array;
+   subtype Byte_Index is WolfSSL.Byte_Index; use type Byte_Index;
+
+   subtype Port_Type is GNAT.Sockets.Port_Type;
+
+   subtype Level_Type is GNAT.Sockets.Level_Type;
+
+   subtype Socket_Type is GNAT.Sockets.Socket_Type;
+   subtype Option_Name is GNAT.Sockets.Option_Name;
+   subtype Option_Type is GNAT.Sockets.Option_Type;
+   subtype Family_Type is GNAT.Sockets.Family_Type;
+
+   subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type;
+   subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type;
+
+   Socket_Error : exception renames GNAT.Sockets.Socket_Error;
+
+   Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address;
+
+   Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level;
+
+   Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet;
+   use type GNAT.Sockets.Family_Type;
+
+   Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr;
+
+   subtype Subprogram_Result is WolfSSL.Subprogram_Result;
+   use type Subprogram_Result;
+
+   Success : Subprogram_Result renames WolfSSL.Success;
+   Failure : Subprogram_Result renames WolfSSL.Failure;
+
+   type Optional_Inet_Addr (Exists : Boolean := False) is record
+      case Exists is
+         when True  => Addr : Inet_Addr_Type;
+         when False => null;
+      end case;
+   end record;
+
+   function Inet_Addr (Image : String) return Optional_Inet_Addr;
+
+   type Optional_Socket (Exists : Boolean := False) is record
+      case Exists is
+         when True  => Socket : Socket_Type;
+         when False => null;
+      end case;
+   end record;
+
+   procedure Create_Socket (Socket : in out Optional_Socket) with
+      Pre => not Socket.Exists;
+
+   function Connect_Socket (Socket : Socket_Type;
+                            Server : Sock_Addr_Type)
+                            return Subprogram_Result;
+
+   function To_C (Socket : Socket_Type) return Integer with Inline;
+
+   --  Close a socket and more specifically a non-connected socket.
+   procedure Close_Socket (Socket : in out Optional_Socket) with
+      Pre  => Socket.Exists,
+      Post => not Socket.Exists;
+
+   function Set_Socket_Option (Socket : Socket_Type;
+                               Level  : Level_Type;
+                               Option : Option_Type)
+                               return Subprogram_Result;
+   --  Manipulate socket options.
+
+   function Bind_Socket (Socket  : Socket_Type;
+                         Address : Sock_Addr_Type)
+                         return Subprogram_Result;
+
+   function Listen_Socket (Socket : Socket_Type;
+                           Length : Natural) return Subprogram_Result;
+   --  To accept connections, a socket is first created with
+   --  Create_Socket, a willingness to accept incoming connections and
+   --  a queue Length for incoming connections are specified.
+   --  The queue length of 15 is an example value that should be
+   --  appropriate in usual cases. It can be adjusted according to each
+   --  application's particular requirements.
+
+   procedure Accept_Socket (Server  : Socket_Type;
+                            Socket  : out Optional_Socket;
+                            Address : out Sock_Addr_Type;
+                            Result  : out Subprogram_Result) with
+      Post => (if Result = Success then Socket.Exists else not Socket.Exists);
+
+   procedure To_C (Item       : String;
+                   Target     : out Byte_Array;
+                   Count      : out Byte_Index) with
+      Pre  => Item'Length <= Target'Length,
+      Post => Count <= Target'Last;
+
+   procedure To_Ada (Item     : Byte_Array;
+                     Target   : out String;
+                     Count    : out Natural) with
+      Pre  => Item'Length <= Target'Length,
+      Post => Count <= Target'Last;
+
+end SPARK_Sockets;

wrapper/Ada/spark_terminal.adb

@@ -0,0 +1,18 @@
+package body SPARK_Terminal is
+
+   procedure Set_Exit_Status (Status : Exit_Status) is
+   begin
+      Ada.Command_Line.Set_Exit_Status (Status);
+   end Set_Exit_Status;
+
+   function Argument_Count return Natural is
+   begin
+      return Ada.Command_Line.Argument_Count;
+   end Argument_Count;
+
+   function Argument (Number : Positive) return String is
+   begin
+      return Ada.Command_Line.Argument (Number);
+   end Argument;
+
+end SPARK_Terminal;

wrapper/Ada/spark_terminal.ads

@@ -0,0 +1,43 @@
+-- spark_sockets.ads
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
+with Ada.Command_Line;
+
+--  SPARK wrapper package around Ada.Command_Line and Interfaces.C
+--  packages because these packages lack contracts in their specification
+--  files that SPARK can use to verify the context in which
+--  subprograms can safely be called.
+package SPARK_Terminal with SPARK_Mode is
+
+   subtype Exit_Status is Ada.Command_Line.Exit_Status;
+
+   Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success;
+   Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure;
+
+   procedure Set_Exit_Status (Status : Exit_Status) with
+      Global => null;
+
+   function Argument_Count return Natural;
+
+   function Argument (Number : Positive) return String with
+      Pre => Number <= Argument_Count;
+
+end SPARK_Terminal;

wrapper/Ada/tls_client.adb

@@ -21,18 +21,13 @@
 
 --  Ada Standard Library packages.
 with Ada.Characters.Handling;
-with Ada.Command_Line;
 with Ada.Strings.Bounded;
-with Ada.Text_IO.Bounded_IO;
+with Ada.Text_IO;
 with Interfaces.C;
 
---  GNAT Library packages.
+with SPARK_Terminal;
-with GNAT.Sockets;
 
---  The WolfSSL package.
+package body Tls_Client with SPARK_Mode is
-with WolfSSL;
-
-package body Tls_Client is
 
    use type WolfSSL.Mode_Type;
    use type WolfSSL.Byte_Index;
@@ -42,13 +37,8 @@ package body Tls_Client is
 
    subtype Byte_Type is WolfSSL.Byte_Type;
 
-   package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200);
-   use all type Messages.Bounded_String;
-
    package Integer_IO is new Ada.Text_IO.Integer_IO (Integer);
 
-   package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages);
-
    procedure Put (Text : String) is
    begin
       Ada.Text_IO.Put (Text);
@@ -69,42 +59,39 @@ package body Tls_Client is
       Ada.Text_IO.New_Line;
    end New_Line;
 
-   procedure Put_Line (Text : Messages.Bounded_String) is
+   subtype Exit_Status is SPARK_Terminal.Exit_Status;
+
+   Exit_Status_Success : Exit_Status renames SPARK_Terminal.Exit_Status_Success;
+   Exit_Status_Failure : Exit_Status renames SPARK_Terminal.Exit_Status_Failure;
+
+   procedure Set (Status : Exit_Status) with Global => null is
    begin
-      Messages_IO.Put_Line (Text);
+      SPARK_Terminal.Set_Exit_Status (Status);
-   end Put_Line;
-
-   subtype Exit_Status is Ada.Command_Line.Exit_Status;
-
-   Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success;
-   Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure;
-
-   procedure Set (Status : Exit_Status) is
-   begin
-      Ada.Command_Line.Set_Exit_Status (Status);
    end Set;
 
-   subtype Port_Type is GNAT.Sockets.Port_Type;
+   subtype Port_Type is SPARK_Sockets.Port_Type;
 
-   subtype Level_Type is GNAT.Sockets.Level_Type;
+   subtype Level_Type is SPARK_Sockets.Level_Type;
 
-   subtype Socket_Type is GNAT.Sockets.Socket_Type;
+   subtype Socket_Type is SPARK_Sockets.Socket_Type;
-   subtype Option_Name is GNAT.Sockets.Option_Name;
+   subtype Option_Name is SPARK_Sockets.Option_Name;
-   subtype Option_Type is GNAT.Sockets.Option_Type;
+   subtype Option_Type is SPARK_Sockets.Option_Type;
-   subtype Family_Type is GNAT.Sockets.Family_Type;
+   subtype Family_Type is SPARK_Sockets.Family_Type;
 
-   subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type;
+   subtype Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type;
-   subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type;
+   subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type;
 
-   Socket_Error : exception renames GNAT.Sockets.Socket_Error;
+   use type Family_Type;
 
-   Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address;
+   Socket_Error : exception renames SPARK_Sockets.Socket_Error;
 
-   Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level;
+   Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address;
 
-   Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet;
+   Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level;
 
-   Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr;
+   Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet;
+
+   Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr;
 
    CERT_FILE : constant String := "../certs/client-cert.pem";
    KEY_FILE  : constant String := "../certs/client-key.pem";
@@ -112,24 +99,26 @@ package body Tls_Client is
 
    subtype Byte_Array is WolfSSL.Byte_Array;
 
-   function Argument_Count return Natural is
+   function Argument_Count return Natural renames
-   begin
+      SPARK_Terminal.Argument_Count;
-      return Ada.Command_Line.Argument_Count;
+
-   end Argument_Count;
+   function Argument (Number : Positive) return String with
+      Pre => Number <= Argument_Count;
 
    function Argument (Number : Positive) return String is
    begin
-      return Ada.Command_Line.Argument (Number);
+      return SPARK_Terminal.Argument (Number);
    end Argument;
 
-   procedure Run is
+   procedure Run (Ssl    : in out WolfSSL.WolfSSL_Type;
+                  Ctx    : in out WolfSSL.Context_Type;
+                  Client : in out SPARK_Sockets.Optional_Socket) is
       A : Sock_Addr_Type;
-      C : Socket_Type;  --  Client socket.
+      C : SPARK_Sockets.Optional_Socket renames Client;
       D : Byte_Array (1 .. 200);
       P : constant Port_Type := 11111;
 
-      Ssl : WolfSSL.WolfSSL_Type;
+      Addr : SPARK_Sockets.Optional_Inet_Addr;
-      Ctx : WolfSSL.Context_Type;
 
       Bytes_Written : Integer;
 
@@ -142,24 +131,44 @@ package body Tls_Client is
 
       Result : WolfSSL.Subprogram_Result;
    begin
-      if Argument_Count /= 1 then
+      if Argument_Count < 1 then
          Put_Line ("usage: tcl_client <IPv4 address>");
          return;
       end if;
-      GNAT.Sockets.Create_Socket (Socket => C);
+      SPARK_Sockets.Create_Socket (C);
+      if not C.Exists then
+         Put_Line ("ERROR: Failed to create socket.");
+         return;
+      end if;
 
+      Addr := SPARK_Sockets.Inet_Addr (Argument (1));
+      if not Addr.Exists or
+         (Addr.Exists and then Addr.Addr.Family /= Family_Inet)
+      then
+         Put_Line ("ERROR: please specify IPv4 address.");
+         SPARK_Sockets.Close_Socket (C);
+         Set (Exit_Status_Failure);
+         return;
+      end if;
       A := (Family => Family_Inet,
-            Addr   => GNAT.Sockets.Inet_Addr (Argument (1)),
+            Addr   => Addr.Addr,
             Port   => P);
 
-      GNAT.Sockets.Connect_Socket (Socket => C,
+      Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket,
-                                   Server => A);
+                                              Server => A);
+      if Result = Failure then
+         Put_Line ("ERROR: Failed to connect to server.");
+         SPARK_Sockets.Close_Socket (C);
+         Set (Exit_Status_Failure);
+         return;
+      end if;
 
       --  Create and initialize WOLFSSL_CTX.
       WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Client_Method,
                               Context => Ctx);
       if not WolfSSL.Is_Valid (Ctx) then
          Put_Line ("ERROR: failed to create WOLFSSL_CTX.");
+         SPARK_Sockets.Close_Socket (C);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -173,6 +182,8 @@ package body Tls_Client is
          Put (CERT_FILE);
          Put (", please check the file.");
          New_Line;
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -186,6 +197,8 @@ package body Tls_Client is
          Put (KEY_FILE);
          Put (", please check the file.");
          New_Line;
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -199,6 +212,8 @@ package body Tls_Client is
          Put (CA_FILE);
          Put (", please check the file.");
          New_Line;
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -207,15 +222,20 @@ package body Tls_Client is
       WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl);
       if not WolfSSL.Is_Valid (Ssl) then
          Put_Line ("ERROR: failed to create WOLFSSL object.");
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
 
       --  Attach wolfSSL to the socket.
       Result := WolfSSL.Attach (Ssl    => Ssl,
-                                Socket => GNAT.Sockets.To_C (C));
+                                Socket => SPARK_Sockets.To_C (C.Socket));
       if Result = Failure then
          Put_Line ("ERROR: Failed to set the file descriptor.");
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Ssl);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -223,6 +243,9 @@ package body Tls_Client is
       Result := WolfSSL.Connect (Ssl);
       if Result = Failure then
          Put_Line ("ERROR: failed to connect to wolfSSL.");
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Ssl);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -230,10 +253,9 @@ package body Tls_Client is
       Put ("Message for server: ");
       Ada.Text_IO.Get_Line (Text, Last);
 
-      Interfaces.C.To_C (Item       => Text (1 .. Last),
+      SPARK_Sockets.To_C (Item       => Text (1 .. Last),
-                         Target     => D,
+                          Target     => D,
-                         Count      => Count,
+                          Count      => Count);
-                         Append_Nul => False);
       Bytes_Written := WolfSSL.Write (Ssl  => Ssl,
                                       Data => D (1 .. Count));
       if Bytes_Written < Last then
@@ -244,6 +266,9 @@ package body Tls_Client is
          Put (Last);
          Put ("bytes were sent");
          New_Line;
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Ssl);
+         WolfSSL.Free (Context => Ctx);
          return;
       end if;
 
@@ -251,19 +276,28 @@ package body Tls_Client is
       if Input.Result /= Success then
          Put_Line ("Read error.");
          Set (Exit_Status_Failure);
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Ssl);
+         WolfSSL.Free (Context => Ctx);
          return;
       end if;
-      Interfaces.C.To_Ada (Item     => Input.Buffer,
+      if Input.Buffer'Length > Text'Length then
-                           Target   => Text,
+         SPARK_Sockets.To_Ada (Item     => Input.Buffer (1 .. 200),
-                           Count    => Last,
+                               Target   => Text,
-                           Trim_Nul => False);
+                               Count    => Last);
+      else
+         SPARK_Sockets.To_Ada (Item     => Input.Buffer,
+                               Target   => Text,
+                               Count    => Last);
+      end if;
       Put ("Server: ");
       Put (Text (1 .. Last));
       New_Line;
 
-      GNAT.Sockets.Close_Socket (C);
+      SPARK_Sockets.Close_Socket (C);
       WolfSSL.Free (Ssl);
       WolfSSL.Free (Context => Ctx);
+      WolfSSL.Finalize;
    end Run;
 
 end Tls_Client;

wrapper/Ada/tls_client.ads

@@ -19,8 +19,19 @@
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
 
-package Tls_Client is
+--  The WolfSSL package.
+with WolfSSL; pragma Elaborate_All (WolfSSL);
 
-   procedure Run;
+with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets);
+
+package Tls_Client with SPARK_Mode is
+
+   procedure Run (Ssl    : in out WolfSSL.WolfSSL_Type;
+                  Ctx    : in out WolfSSL.Context_Type;
+                  Client : in out SPARK_Sockets.Optional_Socket) with
+      Pre  => (not Client.Exists and not
+                  WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)),
+      Post => (not Client.Exists and not WolfSSL.Is_Valid (Ssl) and
+                  not WolfSSL.Is_Valid (Ctx));
 
 end Tls_Client;

wrapper/Ada/tls_client_main.adb

@@ -19,11 +19,15 @@
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
 
-with Tls_Client; pragma Elaborate_All (Tls_Client);
+with Tls_Client;    pragma Elaborate_All (Tls_Client);
-
+with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets);
+with WolfSSL;       pragma Elaborate_All (WolfSSL);
 --  Application entry point for the Ada translation of the
 --  tls client v1.3 example in C.
 procedure Tls_Client_Main is
+   Ssl : WolfSSL.WolfSSL_Type;
+   Ctx : WolfSSL.Context_Type;
+   C   : SPARK_Sockets.Optional_Socket;
 begin
-   Tls_Client.Run;
+   Tls_Client.Run (Ssl, Ctx, Client => C);
 end Tls_Client_Main;

wrapper/Ada/tls_server.adb

@@ -21,17 +21,12 @@
 
 --  Ada Standard Library packages.
 with Ada.Characters.Handling;
-with Ada.Command_Line;
 with Ada.Strings.Bounded;
 with Ada.Text_IO.Bounded_IO;
 
---  GNAT Library packages.
+with SPARK_Terminal; pragma Elaborate_All (SPARK_Terminal);
-with GNAT.Sockets;
 
---  The WolfSSL package.
+package body Tls_Server with SPARK_Mode is
-with WolfSSL;
-
-package body Tls_Server is
 
    use type WolfSSL.Mode_Type;
    use type WolfSSL.Byte_Index;
@@ -39,52 +34,57 @@ package body Tls_Server is
 
    use all type WolfSSL.Subprogram_Result;
 
-   package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200);
+   procedure Put (Char : Character) is
-   use all type Messages.Bounded_String;
+   begin
+      Ada.Text_IO.Put (Char);
+   end Put;
 
-   package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages);
+   procedure Put (Text : String) is
+   begin
+      Ada.Text_IO.Put (Text);
+   end Put;
 
    procedure Put_Line (Text : String) is
    begin
       Ada.Text_IO.Put_Line (Text);
    end Put_Line;
 
-   procedure Put_Line (Text : Messages.Bounded_String) is
+   procedure New_Line is
    begin
-      Messages_IO.Put_Line (Text);
+      Ada.Text_IO.New_Line;
-   end Put_Line;
+   end New_Line;
 
-   subtype Exit_Status is Ada.Command_Line.Exit_Status;
+   subtype Exit_Status is SPARK_Terminal.Exit_Status;
 
-   Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success;
+   Exit_Status_Success : Exit_Status renames SPARK_Terminal.Exit_Status_Success;
-   Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure;
+   Exit_Status_Failure : Exit_Status renames SPARK_Terminal.Exit_Status_Failure;
 
-   procedure Set (Status : Exit_Status) is
+   procedure Set (Status : Exit_Status) with Global => null is
    begin
-      Ada.Command_Line.Set_Exit_Status (Status);
+      SPARK_Terminal.Set_Exit_Status (Status);
    end Set;
 
-   subtype Port_Type is GNAT.Sockets.Port_Type;
+   subtype Port_Type is SPARK_Sockets.Port_Type;
 
-   subtype Level_Type is GNAT.Sockets.Level_Type;
+   subtype Level_Type is SPARK_Sockets.Level_Type;
 
-   subtype Socket_Type is GNAT.Sockets.Socket_Type;
+   subtype Socket_Type is SPARK_Sockets.Socket_Type;
-   subtype Option_Name is GNAT.Sockets.Option_Name;
+   subtype Option_Name is SPARK_Sockets.Option_Name;
-   subtype Option_Type is GNAT.Sockets.Option_Type;
+   subtype Option_Type is SPARK_Sockets.Option_Type;
-   subtype Family_Type is GNAT.Sockets.Family_Type;
+   subtype Family_Type is SPARK_Sockets.Family_Type;
 
-   subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type;
+   subtype Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type;
-   subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type;
+   subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type;
 
-   Socket_Error : exception renames GNAT.Sockets.Socket_Error;
+   Socket_Error : exception renames SPARK_Sockets.Socket_Error;
 
-   Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address;
+   Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address;
 
-   Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level;
+   Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level;
 
-   Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet;
+   Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet;
 
-   Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr;
+   Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr;
 
    CERT_FILE : constant String := "../certs/server-cert.pem";
    KEY_FILE  : constant String := "../certs/server-key.pem";
@@ -94,42 +94,64 @@ package body Tls_Server is
 
    Reply : constant Byte_Array := "I hear ya fa shizzle!";
 
-   procedure Run is
+   procedure Run (Ssl : in out WolfSSL.WolfSSL_Type;
+                  Ctx : in out WolfSSL.Context_Type;
+                  L   : in out SPARK_Sockets.Optional_Socket;
+                  C   : in out SPARK_Sockets.Optional_Socket) is
       A : Sock_Addr_Type;
-      L : Socket_Type;  --  Listener socket.
-      C : Socket_Type;  --  Client socket.
       P : constant Port_Type := 11111;
 
       Ch : Character;
 
-      Ssl : WolfSSL.WolfSSL_Type;
-
-      Ctx : WolfSSL.Context_Type;
       Result : WolfSSL.Subprogram_Result;
-      M : Messages.Bounded_String;
       Shall_Continue : Boolean := True;
 
       Bytes_Written : Integer;
 
       Input : WolfSSL.Read_Result;
+      Option : Option_Type;
    begin
-      GNAT.Sockets.Create_Socket (Socket => L);
+      SPARK_Sockets.Create_Socket (Socket => L);
-      GNAT.Sockets.Set_Socket_Option (Socket => L,
+      if not L.Exists then
-                                      Level  => Socket_Level,
+         Put_Line ("ERROR: Failed to create socket.");
-                                      Option => (Name    => Reuse_Address,
+         return;
-                                                 Enabled => True));
+      end if;
-      GNAT.Sockets.Bind_Socket (Socket  => L,
+
-                                Address => (Family => Family_Inet,
+      Option := (Name => Reuse_Address, Enabled => True);
-                                            Addr   => Any_Inet_Addr,
+      Result := SPARK_Sockets.Set_Socket_Option (Socket => L.Socket,
-                                            Port   => P));
+                                                 Level  => Socket_Level,
-      GNAT.Sockets.Listen_Socket (Socket => L,
+                                                 Option => Option);
-                                  Length => 5);
+      if Result = Failure then
+         Put_Line ("ERROR: Failed to set socket option.");
+         SPARK_Sockets.Close_Socket (L);
+         return;
+      end if;
+
+      A := (Family => Family_Inet,
+            Addr   => Any_Inet_Addr,
+            Port   => P);
+      Result := SPARK_Sockets.Bind_Socket (Socket  => L.Socket,
+                                           Address => A);
+      if Result = Failure then
+         Put_Line ("ERROR: Failed to bind socket.");
+         SPARK_Sockets.Close_Socket (L);
+         return;
+      end if;
+
+      Result := SPARK_Sockets.Listen_Socket (Socket => L.Socket,
+                                             Length => 5);
+      if Result = Failure then
+         Put_Line ("ERROR: Failed to configure listener socket.");
+         SPARK_Sockets.Close_Socket (L);
+         return;
+      end if;
 
       --  Create and initialize WOLFSSL_CTX.
       WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Server_Method,
                               Context => Ctx);
       if not WolfSSL.Is_Valid (Ctx) then
          Put_Line ("ERROR: failed to create WOLFSSL_CTX.");
+         SPARK_Sockets.Close_Socket (L);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -144,10 +166,12 @@ package body Tls_Server is
                                               File    => CERT_FILE,
                                               Format  => WolfSSL.Format_Pem);
       if Result = Failure then
-         M := Messages.To_Bounded_String ("ERROR: failed to load ");
+         Put ("ERROR: failed to load ");
-         Messages.Append (M, CERT_FILE);
+         Put (CERT_FILE);
-         Messages.Append (M, ", please check the file.");
+         Put (", please check the file.");
-         Put_Line (M);
+         New_Line;
+         SPARK_Sockets.Close_Socket (L);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -157,10 +181,12 @@ package body Tls_Server is
                                               File    => KEY_FILE,
                                               Format  => WolfSSL.Format_Pem);
       if Result = Failure then
-         M := Messages.To_Bounded_String ("ERROR: failed to load ");
+         Put ("ERROR: failed to load ");
-         Messages.Append (M, KEY_FILE);
+         Put (KEY_FILE);
-         Messages.Append (M, ", please check the file.");
+         Put (", please check the file.");
-         Put_Line (M);
+         New_Line;
+         SPARK_Sockets.Close_Socket (L);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
@@ -170,39 +196,53 @@ package body Tls_Server is
                                                File    => CA_FILE,
                                                Path    => "");
       if Result = Failure then
-         M := Messages.To_Bounded_String ("ERROR: failed to load ");
+         Put ("ERROR: failed to load ");
-         Messages.Append (M, CA_FILE);
+         Put (CA_FILE);
-         Messages.Append (M, ", please check the file.");
+         Put (", please check the file.");
-         Put_Line (M);
+         New_Line;
+         SPARK_Sockets.Close_Socket (L);
+         WolfSSL.Free (Context => Ctx);
          Set (Exit_Status_Failure);
          return;
       end if;
 
       while Shall_Continue loop
+         pragma Loop_Invariant (not C.Exists and
+                                   not WolfSSL.Is_Valid (Ssl) and
+                                   WolfSSL.Is_Valid (Ctx));
+
          Put_Line ("Waiting for a connection...");
-         begin
+         SPARK_Sockets.Accept_Socket (Server  => L.Socket,
-            GNAT.Sockets.Accept_Socket (Server  => L,
+                                      Socket  => C,
-                                        Socket  => C,
+                                      Address => A,
-                                        Address => A);
+                                      Result  => Result);
-         exception
+         if Result = Failure then
-            when Socket_Error =>
+            Put_Line ("ERROR: failed to accept the connection.");
-               Shall_Continue := False;
+            SPARK_Sockets.Close_Socket (L);
-               Put_Line ("ERROR: failed to accept the connection.");
+            WolfSSL.Free (Context => Ctx);
-         end;
+            return;
+         end if;
 
          --  Create a WOLFSSL object.
          WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl);
          if not WolfSSL.Is_Valid (Ssl) then
             Put_Line ("ERROR: failed to create WOLFSSL object.");
+            SPARK_Sockets.Close_Socket (L);
+            SPARK_Sockets.Close_Socket (C);
+            WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
          end if;
 
          --  Attach wolfSSL to the socket.
          Result := WolfSSL.Attach (Ssl    => Ssl,
-                                   Socket => GNAT.Sockets.To_C (C));
+                                   Socket => SPARK_Sockets.To_C (C.Socket));
          if Result = Failure then
             Put_Line ("ERROR: Failed to set the file descriptor.");
+            WolfSSL.Free (Ssl);
+            SPARK_Sockets.Close_Socket (L);
+            SPARK_Sockets.Close_Socket (C);
+            WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
          end if;
@@ -211,6 +251,10 @@ package body Tls_Server is
          Result := WolfSSL.Accept_Connection (Ssl);
          if Result = Failure then
             Put_Line ("Accept error.");
+            WolfSSL.Free (Ssl);
+            SPARK_Sockets.Close_Socket (L);
+            SPARK_Sockets.Close_Socket (C);
+            WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
          end if;
@@ -218,25 +262,27 @@ package body Tls_Server is
          Put_Line ("Client connected successfully.");
 
          Input := WolfSSL.Read (Ssl);
-
          if Input.Result /= Success then
             Put_Line ("Read error.");
+            WolfSSL.Free (Ssl);
+            SPARK_Sockets.Close_Socket (L);
+            SPARK_Sockets.Close_Socket (C);
+            WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
          end if;
 
          --  Print to stdout any data the client sends.
-         M := Messages.To_Bounded_String ("");
          for I in Input.Buffer'Range loop
             Ch := Character (Input.Buffer (I));
             if Ada.Characters.Handling.Is_Graphic (Ch) then
-               Messages.Append (M, Ch);
+               Put (Ch);
             else
                null;
                --  Ignore the "newline" characters at end of message.
             end if;
          end loop;
-         Put_Line (M);
+         New_Line;
 
          --  Check for server shutdown command.
          if Input.Last >= 8  then
@@ -252,12 +298,15 @@ package body Tls_Server is
          end if;
 
          Result := WolfSSL.Shutdown (Ssl);
+         if Result = Failure then
+            Put_Line ("ERROR: Failed to shutdown WolfSSL context.");
+         end if;
          WolfSSL.Free (Ssl);
-         GNAT.Sockets.Close_Socket (C);
+         SPARK_Sockets.Close_Socket (C);
 
          Put_Line ("Shutdown complete.");
       end loop;
-      GNAT.Sockets.Close_Socket (L);
+      SPARK_Sockets.Close_Socket (L);
       WolfSSL.Free (Context => Ctx);
       WolfSSL.Finalize;
    end Run;

wrapper/Ada/tls_server.ads

@@ -18,8 +18,22 @@
 -- along with this program; if not, write to the Free Software
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
-package Tls_Server is
 
-   procedure Run;
+--  SPARK wrapper package around GNAT Library packages.
+with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets);
+
+--  The WolfSSL package.
+with WolfSSL; pragma Elaborate_All (WolfSSL);
+
+package Tls_Server with SPARK_Mode is
+
+   procedure Run (Ssl : in out WolfSSL.WolfSSL_Type;
+                  Ctx : in out WolfSSL.Context_Type;
+                  L   : in out SPARK_Sockets.Optional_Socket;
+                  C   : in out SPARK_Sockets.Optional_Socket) with
+      Pre  => (not C.Exists and not L.Exists and not
+                  WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)),
+      Post => (not C.Exists and not L.Exists and not
+                  WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx));
 
 end Tls_Server;

wrapper/Ada/tls_server_main.adb

@@ -21,9 +21,19 @@
 
 with Tls_Server; pragma Elaborate_All (Tls_Server);
 
+--  SPARK wrapper package around GNAT Library packages.
+with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets);
+
+--  The WolfSSL package.
+with WolfSSL; pragma Elaborate_All (WolfSSL);
+
 --  Application entry point for the Ada translation of the
 --  tls server v1.3 example in C.
 procedure Tls_Server_Main is
+   Ssl : WolfSSL.WolfSSL_Type;
+   Ctx : WolfSSL.Context_Type;
+   L   : SPARK_Sockets.Optional_Socket;
+   C   : SPARK_Sockets.Optional_Socket;
 begin
-   Tls_Server.Run;
+   Tls_Server.Run (Ssl, Ctx, L, C);
 end Tls_Server_Main;