Merge pull request #7397 from dalybrown/expose-dtsl-in-ada

Expose DTLS in Ada wrapper and update examples

Author: JacobBarthelmeh

wrapper/Ada/.gitignore

@@ -0,0 +1 @@
+obj

wrapper/Ada/README.md

@@ -2,7 +2,7 @@
 The source code for the Ada/SPARK binding of the WolfSSL library
 is the WolfSSL Ada package in the wolfssl.ads and wolfssl.adb files.
 
-The source code here also demonstrates a TLS v1.3 server and client
+The source code here also demonstrates a (D)TLS v1.3 server and client
 using the WolfSSL Ada binding. The implementation is cross-platform
 and compiles on Linux, Mac OS X and Windows.
 
@@ -15,7 +15,8 @@ for the secondary stack. The GNAT User's Guide recommends
 avoiding the secondary stack using the restriction
 No_Secondary_Stack (see the GNAT configuration file gnat.adc
 which instructs compilation of the WolfSSL Ada binding under
-this restriction).
+this restriction). Note, however, that the examples do make use of the
+secondary stack.
 
 Portability: The WolfSSL Ada binding makes no usage of controlled types
 and has no dependency upon the Ada.Finalization package.
@@ -91,13 +92,13 @@ Make sure the executables for the compiler and GPRBuild are on the PATH
 and use gprbuild to build the source code.
 
 ## Files
-The TLS v1.3 client example in the Ada/SPARK programming language
+The (D)TLS v1.3 client example in the Ada/SPARK programming language
 using the WolfSSL library can be found in the files:
 tls_client_main.adb
 tls_client.ads
 tls_client.adb
 
-The TLS v1.3 server example in the Ada/SPARK programming language
+The (D)TLS v1.3 server example in the Ada/SPARK programming language
 using the WolfSSL library can be found in the files:
 tls_server_main.adb
 tls_server.ads

wrapper/Ada/default.gpr

@@ -26,10 +26,6 @@ project Default is
       for Spec_Suffix ("C") use ".h";
    end Naming;
 
-   package Builder is
-      for Global_Configuration_Pragmas use "gnat.adc";
-   end Builder;
-
    package Compiler is
       for Switches ("C") use
          ("-DWOLFSSL_USER_SETTINGS", --  Use the user_settings.h file.

wrapper/Ada/spark_sockets.adb

@@ -19,6 +19,7 @@
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
 
+with Ada.Streams;
 with Interfaces.C;
 
 package body SPARK_Sockets is
@@ -33,16 +34,35 @@ package body SPARK_Sockets is
          return (Exists => False);
    end Inet_Addr;
 
-   procedure Create_Socket (Socket : in out Optional_Socket) is
+   procedure Create_Socket
+     (Socket : in out Optional_Socket;
+      Family : GNAT.Sockets.Family_Type;
+      Mode   : GNAT.Sockets.Mode_Type) is
       S : Socket_Type;
    begin
-      GNAT.Sockets.Create_Socket (S);
+      GNAT.Sockets.Create_Socket (S, Family, Mode);
       Socket := (Exists => True, Socket => S);
    exception
       when others =>
          Socket := (Exists => False);
    end Create_Socket;
 
+   procedure Create_Stream_Socket (Socket : in out Optional_Socket) is
+   begin
+      Create_Socket
+        (Socket => Socket,
+         Family => GNAT.Sockets.Family_Inet,
+         Mode   => GNAT.Sockets.Socket_Stream);
+   end Create_Stream_Socket;
+
+   procedure Create_Datagram_Socket (Socket : in out Optional_Socket) is
+   begin
+      Create_Socket
+        (Socket => Socket,
+         Family => GNAT.Sockets.Family_Inet,
+         Mode   => GNAT.Sockets.Socket_Datagram);
+   end Create_Datagram_Socket;
+
    function Connect_Socket (Socket : Socket_Type;
                             Server : Sock_Addr_Type)
                             return Subprogram_Result is
@@ -99,6 +119,22 @@ package body SPARK_Sockets is
          return Failure;
    end Listen_Socket;
 
+   function Receive_Socket
+     (Socket : Socket_Type)
+      return Subprogram_Result is
+
+      Item : Ada.Streams.Stream_Element_Array (1 .. 4096);
+      Last : Ada.Streams.Stream_Element_Offset;
+      From : GNAT.Sockets.Sock_Addr_Type;
+
+   begin
+      GNAT.Sockets.Receive_Socket (Socket, Item, Last, From);
+      return Success;
+   exception
+      when others =>
+         return Failure;
+   end Receive_Socket;
+
    procedure Accept_Socket (Server  : Socket_Type;
                             Socket  : out Optional_Socket;
                             Address : out Sock_Addr_Type;

wrapper/Ada/spark_sockets.ads

@@ -83,7 +83,10 @@ package SPARK_Sockets with SPARK_Mode is
       end case;
    end record;
 
-   procedure Create_Socket (Socket : in out Optional_Socket) with
+   procedure Create_Stream_Socket (Socket : in out Optional_Socket) with
+      Pre => not Socket.Exists;
+
+   procedure Create_Datagram_Socket (Socket : in out Optional_Socket) with
       Pre => not Socket.Exists;
 
    function Connect_Socket (Socket : Socket_Type;
@@ -116,6 +119,8 @@ package SPARK_Sockets with SPARK_Mode is
    --  appropriate in usual cases. It can be adjusted according to each
    --  application's particular requirements.
 
+   function Receive_Socket (Socket : Socket_Type) return Subprogram_Result;
+
    procedure Accept_Socket (Server  : Socket_Type;
                             Socket  : out Optional_Socket;
                             Address : out Sock_Addr_Type;

wrapper/Ada/tls_client.adb

@@ -47,12 +47,18 @@ package body Tls_Client with SPARK_Mode is
       Ada.Text_IO.Put (Text);
    end Put;
 
-   procedure Put (Number : Natural) is
+   procedure Put (Number : Natural)
+   with
+     Annotate => (GNATprove, Might_Not_Return)
+   is
    begin
       Natural_IO.Put (Item => Number, Width => 0, Base => 10);
    end Put;
 
-   procedure Put (Number : Byte_Index) is
+   procedure Put (Number : Byte_Index)
+   with
+     Annotate => (GNATprove, Might_Not_Return)
+   is
    begin
       Natural_IO.Put (Item => Natural (Number), Width => 0, Base => 10);
    end Put;
@@ -137,21 +143,37 @@ package body Tls_Client with SPARK_Mode is
       Output : WolfSSL.Write_Result;
 
       Result : WolfSSL.Subprogram_Result;
+      DTLS   : Boolean;
    begin
       Result := WolfSSL.Initialize;
       if Result /= Success then
          Put_Line ("ERROR: Failed to initialize the WolfSSL library.");
          return;
       end if;
 
-      if Argument_Count < 1 then
-         Put_Line ("usage: tcl_client <IPv4 address>");
+      if Argument_Count < 1
+         or Argument_Count > 2
+         or (Argument_Count = 2 and then Argument (2) /= "--dtls")
+      then
+         Put_Line ("usage: tls_client_main <IPv4 address> [--dtls]");
          return;
       end if;
-      SPARK_Sockets.Create_Socket (C);
+
+      DTLS := (SPARK_Terminal.Argument_Count = 2);
+
+      if DTLS then
+         SPARK_Sockets.Create_Datagram_Socket (C);
+      else
+         SPARK_Sockets.Create_Stream_Socket (C);
+      end if;
+
       if not C.Exists then
-         Put_Line ("ERROR: Failed to create socket.");
-         return;
+         declare
+            Mode : constant String := (if DTLS then "datagram" else "stream");
+         begin
+            Put_Line ("ERROR: Failed to create " & Mode & " socket.");
+            return;
+         end;
       end if;
 
       Addr := SPARK_Sockets.Inet_Addr (Argument (1));
@@ -167,25 +189,38 @@ package body Tls_Client with SPARK_Mode is
             Addr   => Addr.Addr,
             Port   => P);
 
-      Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket,
-                                              Server => A);
-      if Result /= Success then
-         Put_Line ("ERROR: Failed to connect to server.");
-         SPARK_Sockets.Close_Socket (C);
-         Set (Exit_Status_Failure);
-         return;
+      if not DTLS then
+         Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket,
+                                                 Server => A);
+         if Result /= Success then
+            Put_Line ("ERROR: Failed to connect to server.");
+            SPARK_Sockets.Close_Socket (C);
+            Set (Exit_Status_Failure);
+            return;
+         end if;
       end if;
 
       --  Create and initialize WOLFSSL_CTX.
-      WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Client_Method,
-                              Context => Ctx);
+      WolfSSL.Create_Context
+        (Method  =>
+           (if DTLS then
+               WolfSSL.DTLSv1_3_Client_Method
+            else
+               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;
 
+      --  Require mutual authentication.
+      WolfSSL.Set_Verify
+         (Context => Ctx,
+          Mode    => WolfSSL.Verify_Peer & WolfSSL.Verify_Fail_If_No_Peer_Cert);
+
       --  Load client certificate into WOLFSSL_CTX.
       Result := WolfSSL.Use_Certificate_File (Context => Ctx,
                                               File    => CERT_FILE,
@@ -241,6 +276,19 @@ package body Tls_Client with SPARK_Mode is
          return;
       end if;
 
+      if DTLS then
+         Result := WolfSSL.DTLS_Set_Peer(Ssl     => Ssl,
+                                         Address => A);
+         if Result /= Success then
+            Put_Line ("ERROR: Failed to set the DTLS peer.");
+            SPARK_Sockets.Close_Socket (C);
+            WolfSSL.Free (Ssl);
+            WolfSSL.Free (Context => Ctx);
+            Set (Exit_Status_Failure);
+            return;
+         end if;
+      end if;
+
       --  Attach wolfSSL to the socket.
       Result := WolfSSL.Attach (Ssl    => Ssl,
                                 Socket => SPARK_Sockets.To_C (C.Socket));

wrapper/Ada/tls_client.ads

@@ -32,6 +32,7 @@ package Tls_Client with SPARK_Mode is
       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));
+                  not WolfSSL.Is_Valid (Ctx)),
+     Annotate => (GNATprove, Might_Not_Return);
 
 end Tls_Client;