diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index 98573a2aa0..9e872fccd9 100644 --- a/wrapper/Ada/tls_client.adb +++ b/wrapper/Ada/tls_client.adb @@ -23,7 +23,8 @@ with Ada.Characters.Handling; with Ada.Strings.Bounded; with Ada.Text_IO; -with Interfaces.C; +with Ada.Directories; +with Interfaces.C.Strings; with SPARK_Terminal; @@ -40,8 +41,68 @@ package body Tls_Client with SPARK_Mode is subtype Byte_Type is WolfSSL.Byte_Type; + subtype chars_ptr is WolfSSL.chars_ptr; + subtype unsigned is WolfSSL.unsigned; + package Natural_IO is new Ada.Text_IO.Integer_IO (Natural); + function PSK_Client_Callback + (Unused : WolfSSL.WolfSSL_Type; + Hint : chars_ptr; + Identity : chars_ptr; + Id_Max_Length : unsigned; + Key : chars_ptr; + Key_Max_Length : unsigned) return unsigned + with Convention => C; + + function PSK_Client_Callback + (Unused : WolfSSL.WolfSSL_Type; + Hint : chars_ptr; + Identity : chars_ptr; + Id_Max_Length : unsigned; + Key : chars_ptr; + Key_Max_Length : unsigned) return unsigned + with + SPARK_Mode => Off + is + use type Interfaces.C.unsigned; + + Hint_String : constant String := Interfaces.C.Strings.Value (Hint); + + -- Identity is OpenSSL testing default for openssl s_client, keep same + Identity_String : constant String := "Client_identity"; + -- Test key in hex is 0x1a2b3c4d, in decimal 439,041,101 + Key_String : constant String := + Character'Val (26) + & Character'Val (43) + & Character'Val (60) + & Character'Val (77); + -- These values are aligned with test values in wolfssl/wolfssl/test.h + -- and wolfssl-examples/psk/server-psk.c for testing interoperability. + + begin + + Ada.Text_IO.Put_Line ("Hint: " & Hint_String); + + pragma Assert (Id_Max_Length >= Identity_String'Length); + + Interfaces.C.Strings.Update + (Item => Identity, + Offset => 0, + Str => Identity_String, + Check => False); + + pragma Assert (Key_Max_Length >= Key_String'Length); + + Interfaces.C.Strings.Update + (Item => Key, + Offset => 0, + Str => Key_String, + Check => False); + + return Key_String'Length; + end PSK_Client_Callback; + procedure Put (Text : String) is begin Ada.Text_IO.Put (Text); @@ -107,9 +168,9 @@ package body Tls_Client with SPARK_Mode is 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"; - CA_FILE : constant String := "../../../certs/ca-cert.pem"; + CERT_FILE : constant String := "../../certs/client-cert.pem"; + KEY_FILE : constant String := "../../certs/client-key.pem"; + CA_FILE : constant String := "../../certs/ca-cert.pem"; subtype Byte_Array is WolfSSL.Byte_Array; @@ -144,6 +205,7 @@ package body Tls_Client with SPARK_Mode is Result : WolfSSL.Subprogram_Result; DTLS : Boolean; + PSK : Boolean; begin Result := WolfSSL.Initialize; if Result /= Success then @@ -153,13 +215,18 @@ package body Tls_Client with SPARK_Mode is if Argument_Count < 1 or Argument_Count > 2 - or (Argument_Count = 2 and then Argument (2) /= "--dtls") + or (Argument_Count = 2 and then + Argument (2) /= "--dtls" and then + Argument (2) /= "--psk") then - Put_Line ("usage: tls_client_main [--dtls]"); + Put_Line ("usage: tls_client_main [--dtls | --psk]"); return; end if; - DTLS := (SPARK_Terminal.Argument_Count = 2); + if Argument_Count = 2 then + DTLS := (Argument (2) = "--dtls"); + PSK := (Argument (2) = "--psk"); + end if; if DTLS then SPARK_Sockets.Create_Datagram_Socket (C); @@ -221,49 +288,52 @@ package body Tls_Client with SPARK_Mode is (Context => Ctx, Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert); - -- Load client certificate into WOLFSSL_CTX. - Result := WolfSSL.Use_Certificate_File (Context => Ctx, - File => CERT_FILE, - Format => WolfSSL.Format_Pem); - if Result /= Success then - Put ("ERROR: failed to load "); - 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; + if not PSK then - -- Load client key into WOLFSSL_CTX. - Result := WolfSSL.Use_Private_Key_File (Context => Ctx, - File => KEY_FILE, - Format => WolfSSL.Format_Pem); - if Result /= Success then - Put ("ERROR: failed to load "); - 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; + -- Load client certificate into WOLFSSL_CTX. + Result := WolfSSL.Use_Certificate_File (Context => Ctx, + File => CERT_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + Put ("ERROR: failed to load "); + 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; - -- Load CA certificate into WOLFSSL_CTX. - Result := WolfSSL.Load_Verify_Locations (Context => Ctx, - File => CA_FILE, - Path => ""); - if Result /= Success then - Put ("ERROR: failed to load "); - Put (CA_FILE); - Put (", please check the file."); - New_Line; - SPARK_Sockets.Close_Socket (C); - WolfSSL.Free (Context => Ctx); - Set (Exit_Status_Failure); - return; + -- Load client key into WOLFSSL_CTX. + Result := WolfSSL.Use_Private_Key_File (Context => Ctx, + File => KEY_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + Put ("ERROR: failed to load "); + 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; + + -- Load CA certificate into WOLFSSL_CTX. + Result := WolfSSL.Load_Verify_Locations (Context => Ctx, + File => CA_FILE, + Path => ""); + if Result /= Success then + Put ("ERROR: failed to load "); + 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; end if; -- Create a WOLFSSL object. @@ -276,6 +346,13 @@ package body Tls_Client with SPARK_Mode is return; end if; + if PSK then + -- Use PSK for authentication. + WolfSSL.Set_PSK_Client_Callback + (Ssl => Ssl, + Callback => PSK_Client_Callback'Access); + end if; + if DTLS then Result := WolfSSL.DTLS_Set_Peer(Ssl => Ssl, Address => A); diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 4a91377efd..e17af00a5b 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -24,6 +24,8 @@ with Ada.Characters.Handling; with Ada.Strings.Bounded; with Ada.Text_IO.Bounded_IO; +with Interfaces.C.Strings; + with SPARK_Terminal; pragma Elaborate_All (SPARK_Terminal); package body Tls_Server with SPARK_Mode is @@ -35,6 +37,9 @@ package body Tls_Server with SPARK_Mode is Success : WolfSSL.Subprogram_Result renames WolfSSL.Success; + subtype chars_ptr is WolfSSL.chars_ptr; + subtype unsigned is WolfSSL.unsigned; + procedure Put (Char : Character) is begin Ada.Text_IO.Put (Char); @@ -87,14 +92,66 @@ package body Tls_Server with SPARK_Mode is 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"; - CA_FILE : constant String := "../../../certs/client-cert.pem"; + CERT_FILE : constant String := "../../certs/server-cert.pem"; + KEY_FILE : constant String := "../../certs/server-key.pem"; + CA_FILE : constant String := "../../certs/client-cert.pem"; subtype Byte_Array is WolfSSL.Byte_Array; Reply : constant Byte_Array := "I hear ya fa shizzle!"; + + function PSK_Server_Callback + (Unused : WolfSSL.WolfSSL_Type; + Identity : chars_ptr; + Key : chars_ptr; + Key_Max_Length : unsigned) return unsigned + with Convention => C; + + function PSK_Server_Callback + (Unused : WolfSSL.WolfSSL_Type; + Identity : chars_ptr; + Key : chars_ptr; + Key_Max_Length : unsigned) return unsigned + with + SPARK_Mode => Off + is + use type Interfaces.C.unsigned; + + -- Identity is OpenSSL testing default for openssl s_client, keep same + Identity_String : constant String := "Client_identity"; + -- Test key in hex is 0x1a2b3c4d, in decimal 439,041,101 + Key_String : constant String := + Character'Val (26) + & Character'Val (43) + & Character'Val (60) + & Character'Val (77); + -- These values are aligned with test values in wolfssl/wolfssl/test.h + -- and wolfssl-examples/psk/server-psk.c for testing interoperability. + + begin + + if Interfaces.C.Strings.Value + (Item => Identity, + Length => Identity_String'Length) /= Identity_String or else + Key_Max_Length < Key_String'Length + then + return 0; + end if; + + put_line (Interfaces.C.Strings.Value + (Item => Identity, + Length => Identity_String'Length) ); + + Interfaces.C.Strings.Update + (Item => Key, + Offset => 0, + Str => Key_String, + Check => False); + + return Key_String'Length; + end PSK_Server_Callback; + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; Ctx : in out WolfSSL.Context_Type; L : in out SPARK_Sockets.Optional_Socket; @@ -105,7 +162,7 @@ package body Tls_Server with SPARK_Mode is Ch : Character; Result : WolfSSL.Subprogram_Result; - DTLS : Boolean; + DTLS, PSK : Boolean; Shall_Continue : Boolean := True; Input : WolfSSL.Read_Result; @@ -119,14 +176,18 @@ package body Tls_Server with SPARK_Mode is end if; if SPARK_Terminal.Argument_Count > 1 - or (SPARK_Terminal.Argument_Count = 1 - and then SPARK_Terminal.Argument (1) /= "--dtls") + or (SPARK_Terminal.Argument_Count = 1 and then + SPARK_Terminal.Argument (1) /= "--dtls" and then + SPARK_Terminal.Argument (1) /= "--psk") then - Put_Line ("usage: tls_server_main [--dtls]"); + Put_Line ("usage: tls_server_main [--dtls | --psk]"); return; end if; - DTLS := (SPARK_Terminal.Argument_Count = 1); + if SPARK_Terminal.Argument_Count = 1 then + DTLS := (SPARK_Terminal.Argument (1) = "--dtls"); + PSK := (SPARK_Terminal.Argument (1) = "--psk"); + end if; if DTLS then SPARK_Sockets.Create_Datagram_Socket (Socket => L); @@ -197,63 +258,73 @@ package body Tls_Server with SPARK_Mode is return; end if; - -- Require mutual authentication. - WolfSSL.Set_Verify - (Context => Ctx, - Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert); + if not PSK then + -- Require mutual authentication. + WolfSSL.Set_Verify + (Context => Ctx, + Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert); - -- Check verify is set correctly (GitHub #7461) - if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then - Put ("Error: Verify does not match requested"); - New_Line; - return; - end if; + -- Check verify is set correctly (GitHub #7461) + if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then + Put ("Error: Verify does not match requested"); + New_Line; + return; + end if; - -- Load server certificates into WOLFSSL_CTX. - Result := WolfSSL.Use_Certificate_File (Context => Ctx, - File => CERT_FILE, - Format => WolfSSL.Format_Pem); - if Result /= Success then - Put ("ERROR: failed to load "); - Put (CERT_FILE); - Put (", please check the file."); - New_Line; - SPARK_Sockets.Close_Socket (L); - WolfSSL.Free (Context => Ctx); - Set (Exit_Status_Failure); - return; - end if; + -- Load server certificates into WOLFSSL_CTX. + Result := WolfSSL.Use_Certificate_File (Context => Ctx, + File => CERT_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + Put ("ERROR: failed to load "); + Put (CERT_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + Set (Exit_Status_Failure); + return; + end if; - -- Load server key into WOLFSSL_CTX. - Result := WolfSSL.Use_Private_Key_File (Context => Ctx, - File => KEY_FILE, - Format => WolfSSL.Format_Pem); - if Result /= Success then - Put ("ERROR: failed to load "); - Put (KEY_FILE); - Put (", please check the file."); - New_Line; - SPARK_Sockets.Close_Socket (L); - WolfSSL.Free (Context => Ctx); - Set (Exit_Status_Failure); - return; - end if; + -- Load server key into WOLFSSL_CTX. + Result := WolfSSL.Use_Private_Key_File (Context => Ctx, + File => KEY_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + Put ("ERROR: failed to load "); + Put (KEY_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + Set (Exit_Status_Failure); + return; + end if; - -- Load client certificate as "trusted" into WOLFSSL_CTX. - Result := WolfSSL.Load_Verify_Locations (Context => Ctx, - File => CA_FILE, - Path => ""); - if Result /= Success then - Put ("ERROR: failed to load "); - Put (CA_FILE); - Put (", please check the file."); - New_Line; - SPARK_Sockets.Close_Socket (L); - WolfSSL.Free (Context => Ctx); - Set (Exit_Status_Failure); - return; + -- Load client certificate as "trusted" into WOLFSSL_CTX. + Result := WolfSSL.Load_Verify_Locations (Context => Ctx, + File => CA_FILE, + Path => ""); + + if Result /= Success then + Put ("ERROR: failed to load "); + Put (CA_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + Set (Exit_Status_Failure); + return; + end if; end if; + if PSK then + -- Use PSK for authentication. + WolfSSL.Set_Context_PSK_Server_Callback + (Context => Ctx, + Callback => PSK_Server_Callback'Access); + end if; + while Shall_Continue loop pragma Loop_Invariant (not C.Exists); pragma Loop_Invariant (not WolfSSL.Is_Valid (Ssl)); diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb index b37b0a6672..9bdd07afd7 100644 --- a/wrapper/Ada/wolfssl.adb +++ b/wrapper/Ada/wolfssl.adb @@ -577,6 +577,51 @@ package body WolfSSL is end DTLS_Set_Peer; + procedure WolfSSL_Set_Psk_Client_Callback + (Ssl : WolfSSL_Type; + Cb : PSK_Client_Callback) + with + Convention => C, + External_Name => "wolfSSL_set_psk_client_callback", + Import => True; + + procedure Set_PSK_Client_Callback + (Ssl : WolfSSL_Type; + Callback : PSK_Client_Callback) is + begin + WolfSSL_Set_Psk_Client_Callback (Ssl, Callback); + end Set_PSK_Client_Callback; + + procedure WolfSSL_Set_Psk_Server_Callback + (Ssl : WolfSSL_Type; + Cb : PSK_Server_Callback) + with + Convention => C, + External_Name => "wolfSSL_set_psk_server_callback", + Import => True; + + procedure Set_PSK_Server_Callback + (Ssl : WolfSSL_Type; + Callback : PSK_Server_Callback) is + begin + WolfSSL_Set_Psk_Server_Callback (Ssl, Callback); + end Set_PSK_Server_Callback; + + procedure WolfSSL_CTX_Set_Psk_Server_Callback + (Ctx : Context_Type; + Cb : PSK_Server_Callback) + with + Convention => C, + External_Name => "wolfSSL_CTX_set_psk_server_callback", + Import => True; + + procedure Set_Context_PSK_Server_Callback + (Context : Context_Type; + Callback : PSK_Server_Callback) is + begin + WolfSSL_CTX_Set_Psk_Server_Callback (Context, Callback); + end Set_Context_PSK_Server_Callback; + function WolfSSL_Set_Fd (Ssl : WolfSSL_Type; Fd : int) return int with Convention => C, External_Name => "wolfSSL_set_fd", diff --git a/wrapper/Ada/wolfssl.ads b/wrapper/Ada/wolfssl.ads index a3a0393179..2a247a676c 100644 --- a/wrapper/Ada/wolfssl.ads +++ b/wrapper/Ada/wolfssl.ads @@ -20,7 +20,7 @@ -- with GNAT.Sockets; -with Interfaces.C; +with Interfaces.C.Strings; -- This package is annotated "with SPARK_Mode" that SPARK can verify -- the API of this package is used correctly. @@ -39,7 +39,10 @@ package WolfSSL with SPARK_Mode is -- Doesn't have to be called, though it will free any resources -- used by the library. + subtype unsigned is Interfaces.C.unsigned; + subtype char_array is Interfaces.C.char_array; -- Remove? + subtype chars_ptr is Interfaces.C.Strings.chars_ptr; subtype Byte_Type is Interfaces.C.char; subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000; @@ -297,6 +300,64 @@ package WolfSSL with SPARK_Mode is -- This function wraps the corresponding WolfSSL C function to allow -- clients to use Ada socket types when implementing a DTLS client. + type PSK_Client_Callback is access function + (Ssl : WolfSSL_Type; + Hint : chars_ptr; + Identity : chars_ptr; + Id_Max_Length : unsigned; + Key : chars_ptr; + Key_Max_Length : unsigned) + return unsigned with + Convention => C; + -- Return value is the key length on success or zero on error. + -- parameters: + -- Ssl - Pointer to the wolfSSL structure + -- Hint - A stored string that could be displayed to provide a + -- hint to the user. + -- Identity - The ID will be stored here. + -- Id_Max_Length - Size of the ID buffer. + -- Key - The key will be stored here. + -- Key_Max_Length - The max size of the key. + -- + -- The implementation of this callback will need `SPARK_Mode => Off` + -- since it will require the code to use the C memory model. + + procedure Set_PSK_Client_Callback + (Ssl : WolfSSL_Type; + Callback : PSK_Client_Callback) with + Pre => Is_Valid (Ssl); + -- Sets the PSK client side callback. + + + type PSK_Server_Callback is access function + (Ssl : WolfSSL_Type; + Identity : chars_ptr; + Key : chars_ptr; + Key_Max_Length : unsigned) + return unsigned with + Convention => C; + -- Return value is the key length on success or zero on error. + -- PSK server callback parameters: + -- Ssl - Reference to the wolfSSL structure + -- Identity - The ID will be stored here. + -- Key - The key will be stored here. + -- Key_Max_Length - The max size of the key. + -- + -- The implementation of this callback will need `SPARK_Mode => Off` + -- since it will require the code to use the C memory model. + + procedure Set_PSK_Server_Callback + (Ssl : WolfSSL_Type; + Callback : PSK_Server_Callback) with + Pre => Is_Valid (Ssl); + -- Sets the PSK Server side callback. + + procedure Set_Context_PSK_Server_Callback + (Context : Context_Type; + Callback : PSK_Server_Callback) with + Pre => Is_Valid (Context); + -- Sets the PSK callback for the server side in the WolfSSL Context. + function Attach (Ssl : WolfSSL_Type; Socket : Integer) return Subprogram_Result with