Initial implementation of secure server communication

Work in progress (only first request works).
- Found and fixed problem with `WolfSSL.Get_Error`
  - PR: wolfSSL/wolfssl#9083

Author: mgrojo

TODO.org

@@ -25,8 +25,11 @@
 
 * Server
 - [X] Consider implementing server state-machine and example
+  - [ ] Implement secure communications for the server
   - [ ] Implement server logic for CRUD
   - [ ] Add tests for the server
+  - [ ] Make the validation profile work for the server
+        either with the Workarounds package or making SPARKLib 15 to work.
 
 * Upgrades
   - [x] (discarded) Upgrade to GNATProve 15 and GNAT 15

libs/wolfssl

@@ -1,6 +1,7 @@
 with Ada.Streams;
 with Ada.Unchecked_Conversion;
 
+with CoAP_SPARK.Log;
 
 with Interfaces.C;
 
@@ -111,6 +112,7 @@ is
    begin
 
       Socket.Attached_Socket := (Exists => False);
+      Socket.Is_Server := Server;
 
       SPARK_Sockets.Create_Datagram_Socket (Socket => Socket.Attached_Socket);
 
@@ -133,7 +135,10 @@ is
 
       end if;
 
-      if Socket.Is_Secure then
+      if not Socket.Is_Secure then
+         Socket.Client_Address :=
+           (Sock_Addr => (Family => GNAT.Sockets.Family_Unspec));           
+      else
          Socket.Result := WolfSSL.Initialize;
 
          if Socket.Result /= WolfSSL.Success then
@@ -142,16 +147,31 @@ is
 
          --  Create and initialize WOLFSSL_CTX.
          WolfSSL.Create_Context
-           (Method => WolfSSL.DTLSv1_2_Client_Method, Context => Socket.Ctx);
+           (Method => (if Server then WolfSSL.DTLSv1_2_Server_Method
+                        else WolfSSL.DTLSv1_2_Client_Method),
+            Context => Socket.Ctx);
 
          if WolfSSL.Is_Valid (Socket.Ctx) then
 
+            WolfSSL.Set_Context_PSK_Server_Callback
+               (Context => Socket.Ctx, Callback => PSK_Server_Callback);
+
             WolfSSL.Create_WolfSSL (Context => Socket.Ctx, Ssl => Socket.Ssl);
 
             if WolfSSL.Is_Valid (Socket.Ssl) then
                if Server then
-                  WolfSSL.Set_PSK_Server_Callback
-                    (Ssl => Socket.Ssl, Callback => PSK_Server_Callback);
+                  --  Attach WolfSSL to the socket.
+                  Socket.Result :=
+                    WolfSSL.Attach
+                      (Ssl    => Socket.Ssl,
+                       Socket =>
+                         SPARK_Sockets.To_C (Socket.Attached_Socket.Socket));
+
+                  if Socket.Result /= WolfSSL.Success then
+                     Finalize (Socket);
+                     return;
+                  end if;
+
                else
                   WolfSSL.Set_PSK_Client_Callback
                     (Ssl => Socket.Ssl, Callback => PSK_Client_Callback);
@@ -161,6 +181,47 @@ is
       end if;
    end Initialize;
 
+   procedure Accept_Connection (Socket : in out Socket_Type) is
+   begin
+      if Socket.Is_Secure then
+         Socket.Result := WolfSSL.Accept_Connection (Socket.Ssl);
+         -- TODO factorize
+         if Socket.Result /= WolfSSL.Success then
+            declare
+               Error_Message : constant WolfSSL.Error_Message :=
+                 WolfSSL.Error
+                   (WolfSSL.Get_Error
+                      (Ssl => Socket.Ssl, Result => Socket.Result));
+            begin
+               CoAP_SPARK.Log.Put
+                 ("Error shutting-down: ", CoAP_SPARK.Log.Error);
+               CoAP_SPARK.Log.Put_Line
+                 (Error_Message.Text (1 .. Error_Message.Last),
+                  CoAP_SPARK.Log.Error);
+            end;
+            Finalize (Socket);
+            return;
+         end if;
+         Socket.Result := WolfSSL.Accept_Connection (Socket.Ssl);
+         if Socket.Result /= WolfSSL.Success then
+            declare
+               Error_Message : constant WolfSSL.Error_Message :=
+                 WolfSSL.Error
+                   (WolfSSL.Get_Error
+                      (Ssl => Socket.Ssl, Result => Socket.Result));
+            begin
+               CoAP_SPARK.Log.Put
+                 ("Error accepting connection: ", CoAP_SPARK.Log.Error);
+               CoAP_SPARK.Log.Put_Line
+                 (Error_Message.Text (1 .. Error_Message.Last),
+                  CoAP_SPARK.Log.Error);
+            end;
+            Finalize (Socket);
+            return;
+         end if;
+      end if;
+   end Accept_Connection;
+
    use type SPARK_Sockets.Family_Type;
 
    function Inet_Address (Host_Name : String) return SPARK_Sockets.Optional_Inet_Addr;
@@ -283,9 +344,16 @@ is
               constant Ada.Streams.Stream_Element_Array :=
                 To_Ada_Stream (Buffer);
          begin
-            Send_Socket
-              (Socket => Socket,
-               Item   => Data);
+            if Socket.Is_Server then
+               Send_Socket
+                 (Socket => Socket,
+                  Item   => Data,
+                  To     => Socket.Client_Address);
+            else
+               Send_Socket
+                 (Socket => Socket,
+                  Item   => Data);
+            end if;
          end;
       end if;
    end Send;
@@ -381,8 +449,15 @@ is
             Last : Ada.Streams.Stream_Element_Offset;
          begin
 
-            Receive_Socket
-              (Socket => Socket, Item => Data, Last => Last);
+            if Socket.Is_Server then
+               Receive_Socket
+                 (Socket => Socket,
+                  Item   => Data,
+                  Last   => Last,
+                  From   => Socket.Client_Address);
+            else
+               Receive_Socket (Socket => Socket, Item => Data, Last => Last);
+            end if;
 
             pragma Assert (Data'Length = Buffer'Length);
             Buffer (Buffer'First .. RFLX.RFLX_Builtin_Types.Index'Base (Last)) :=

src/coap_spark-channel.adb

@@ -35,6 +35,13 @@ is
      Relaxed_Initialization => Socket,
      Global                 => null;
 
+   procedure Accept_Connection
+     (Socket : in out Socket_Type)
+   with
+      Pre => Is_Valid (Socket),
+      Global =>
+         null;
+
    function Is_Valid (Socket : Socket_Type) return Boolean with
       Global =>
          null;
@@ -59,7 +66,6 @@ is
                       To     : Address_Type) with
       Pre => Is_Valid (Socket) and then
          Buffer'First = 1 and then
-         not Socket.Is_Secure and then
          Is_Valid (To),
       Global =>
          null;
@@ -82,7 +88,7 @@ is
                       Length :    out RFLX.RFLX_Builtin_Types.Length;
                       From   :    out Address_Type) with
       Relaxed_Initialization => (Buffer),
-      Pre => Is_Valid (Socket) and then Buffer'First = 1 and then not Socket.Is_Secure,
+      Pre => Is_Valid (Socket) and then Buffer'First = 1,
       Post =>
          Length <= Buffer'Length and then
          Buffer (Buffer'First .. RFLX.RFLX_Builtin_Types.Index'Base (Length))'Initialized and then
@@ -99,14 +105,15 @@ is
 private
 
    type Socket_Type (Is_Secure : Boolean) is record
+      Is_Server       : Boolean := False;
       Attached_Socket : SPARK_Sockets.Optional_Socket;
       case Is_Secure is
          when True =>
             Ssl    : WolfSSL.WolfSSL_Type;
             Ctx    : WolfSSL.Context_Type;
             Result : WolfSSL.Subprogram_Result;
          when False =>
-            null;
+            Client_Address : Address_Type;
       end case;
    end record;
 

src/coap_spark-channel.ads

@@ -13,8 +13,7 @@ is
    use type Types.Index;
 
    procedure Read (Ctx : FSM.Context;
-                   Skt : in out CoAP_SPARK.Channel.Socket_Type;
-                   To : CoAP_SPARK.Channel.Address_Type) with
+                   Skt : in out CoAP_SPARK.Channel.Socket_Type) with
       Pre =>
          FSM.Initialized (Ctx)
          and then FSM.Has_Data (Ctx, FSM.C_Transport)
@@ -40,15 +39,13 @@ is
          (Ctx,
           FSM.C_Transport,
           Buffer (Buffer'First .. Buffer'First - 2 + Types.Index (Size + 1)));
-      Channel.Send_To
+      Channel.Send
          (Skt,
-          Buffer (Buffer'First .. Buffer'First - 2 + Types.Index (Size + 1)),
-          To);
+          Buffer (Buffer'First .. Buffer'First - 2 + Types.Index (Size + 1)));
    end Read;
 
    procedure Write (Ctx  : in out FSM.Context;
-                    Skt  : in out CoAP_SPARK.Channel.Socket_Type;
-                    From : out CoAP_SPARK.Channel.Address_Type) with
+                    Skt  : in out CoAP_SPARK.Channel.Socket_Type) with
       Pre =>
          FSM.Initialized (Ctx)
          and then FSM.Needs_Data (Ctx, FSM.C_Transport)
@@ -61,7 +58,7 @@ is
          with Relaxed_Initialization;
       Length : RFLX.RFLX_Builtin_Types.Length;
    begin
-      Channel.Receive (Skt, Buffer, Length, From);
+      Channel.Receive (Skt, Buffer, Length);
       if
          Length > 0
          and then Length <= FSM.Write_Buffer_Size (Ctx, FSM.C_Transport)
@@ -77,29 +74,28 @@ is
       (Ctx : in out FSM.Context;
        Skt : in out CoAP_SPARK.Channel.Socket_Type)
    is
-      Client_Address : CoAP_SPARK.Channel.Address_Type;
+      use type FSM.State;
    begin
 
-      if Skt.Is_Secure then
-         -- Not implemented yet.
-         CoAP_SPARK.Log.Put_Line ("Secure server not implemented yet.", CoAP_SPARK.Log.Error);
-         Ctx.E.Current_Status := CoAP_SPARK.Unexpected_Case;
-         return;
-      end if;
-
       while FSM.Active (Ctx) loop
          pragma Loop_Invariant (FSM.Initialized (Ctx));
          pragma Loop_Invariant (CoAP_SPARK.Channel.Is_Valid (Skt));
+
+         CoAP_SPARK.Log.Put_Line (FSM.Next_State (Ctx)'Image, CoAP_SPARK.Log.Info);
+         if FSM.Next_State (Ctx) = FSM.S_Receive_Request then
+            CoAP_SPARK.Channel.Accept_Connection (Skt);
+         end if;
+
          for C in FSM.Channel'Range loop
             pragma Loop_Invariant (FSM.Initialized (Ctx));
-            exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
-            if CoAP_SPARK.Channel.Is_Valid (Client_Address) and then FSM.Has_Data (Ctx, C) then
-               Read (Ctx, Skt, To => Client_Address);
+            if FSM.Needs_Data (Ctx, C) then
+               Write (Ctx, Skt);
             end if;
             exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
-            if FSM.Needs_Data (Ctx, C) then
-               Write (Ctx, Skt, From => Client_Address);
+            if FSM.Has_Data (Ctx, C) then
+               Read (Ctx, Skt);
             end if;
+            exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
          end loop;
          exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
          FSM.Run (Ctx);