From db4ebfb77e053e3e3e032bcb4fd02af957cfb5ca Mon Sep 17 00:00:00 2001 From: mgrojo Date: Fri, 28 Mar 2025 18:16:06 +0100 Subject: [PATCH 1/4] Allow use of the library with an Alire pin - Allow enabling WOLFSSL_STATIC_PSK via an Alire configuration variable - `gnat.adc` applies unconditionally when using the library through Alire, so it has been renamed and used only in the default project file. - Clean-up of the Alire project file `wolfssl.gpr`. --- wrapper/Ada/alire.toml | 3 ++ wrapper/Ada/default.gpr | 4 +++ wrapper/Ada/{gnat.adc => restricted.adc} | 0 wrapper/Ada/wolfssl.gpr | 45 +++++++++++------------- 4 files changed, 27 insertions(+), 25 deletions(-) rename wrapper/Ada/{gnat.adc => restricted.adc} (100%) diff --git a/wrapper/Ada/alire.toml b/wrapper/Ada/alire.toml index 0334e4a11..025f0b5a5 100644 --- a/wrapper/Ada/alire.toml +++ b/wrapper/Ada/alire.toml @@ -9,3 +9,6 @@ licenses = "GPL-2.0-only" website = "https://www.wolfssl.com/" project-files = ["wolfssl.gpr"] tags = ["ssl", "tls", "embedded", "spark"] + +[configuration.variables] +STATIC_PSK = {type = "Boolean", default = false} \ No newline at end of file diff --git a/wrapper/Ada/default.gpr b/wrapper/Ada/default.gpr index 42dcd745c..c59c3e347 100644 --- a/wrapper/Ada/default.gpr +++ b/wrapper/Ada/default.gpr @@ -26,6 +26,10 @@ project Default is for Spec_Suffix ("C") use ".h"; end Naming; + package Builder is + for Global_Configuration_Pragmas use "restricted.adc"; + end Builder; + package Compiler is for Switches ("C") use ("-DWOLFSSL_USER_SETTINGS", -- Use the user_settings.h file. diff --git a/wrapper/Ada/gnat.adc b/wrapper/Ada/restricted.adc similarity index 100% rename from wrapper/Ada/gnat.adc rename to wrapper/Ada/restricted.adc diff --git a/wrapper/Ada/wolfssl.gpr b/wrapper/Ada/wolfssl.gpr index 65d8cce6f..060c2bc6a 100644 --- a/wrapper/Ada/wolfssl.gpr +++ b/wrapper/Ada/wolfssl.gpr @@ -1,10 +1,8 @@ +with "config/wolfssl_config.gpr"; + library project WolfSSL is for Library_Name use "wolfssl"; - -- for Library_Version use Project'Library_Name & ".so"; - type OS_Kind is ("Windows", "Linux_Or_Mac"); - - OS : OS_Kind := external ("OS", "Linux_Or_Mac"); for Languages use ("C", "Ada"); @@ -15,12 +13,13 @@ library project WolfSSL is -- Don't build the tls client or server application. -- They are not needed in order to build the library. - for Excluded_Source_Files use ("tls_client_main.adb", - "tls_client.ads", - "tls_client.adb", - "tls_server_main.adb", - "tls_server.ads", - "tls_server.adb"); + for Excluded_Source_Files use + ("tls_client_main.adb", + "tls_client.ads", + "tls_client.adb", + "tls_server_main.adb", + "tls_server.ads", + "tls_server.adb"); for Object_Dir use "obj"; for Library_Dir use "lib"; @@ -34,12 +33,19 @@ library project WolfSSL is for Spec_Suffix ("C") use ".h"; end Naming; - package Builder is - for Global_Configuration_Pragmas use "gnat.adc"; - end Builder; + C_Compiler_Config := (); + + case Wolfssl_Config.STATIC_PSK is + when "True" => + C_Compiler_Config := + ("-DWOLFSSL_STATIC_PSK" -- Enable the static PSK cipher support + ); + when others => + C_Compiler_Config := (); + end case; package Compiler is - for Switches ("C") use + for Switches ("C") use C_Compiler_Config & ("-DWOLFSSL_USER_SETTINGS", -- Use the user_settings.h file. "-Wno-pragmas", "-Wall", @@ -81,16 +87,5 @@ library project WolfSSL is package Binder is for Switches ("Ada") use ("-Es"); -- To include stack traces. end Binder; - --- case OS is --- when "Windows" => --- for Library_Options use ("-lm", -- To include the math library (used by WolfSSL). --- "-lcrypt32"); -- Needed on Windows. --- when "Linux_Or_Mac" => --- for Library_Options use ("-lm"); -- To include the math library (used by WolfSSL). --- end case; --- --- -- Put user options in front, for options like --as-needed. --- for Leading_Library_Options use External_As_List ("LDFLAGS", " "); end WolfSSl; From bf5009b544b7062972f2e4798cc06dafd69f4ebf Mon Sep 17 00:00:00 2001 From: mgrojo Date: Fri, 28 Mar 2025 18:38:22 +0100 Subject: [PATCH 2/4] Ada: fix initialization issue in examples Detected by ``` gnatprove -Pclient.gpr --level=4 -j12 ``` --- wrapper/Ada/tls_client.adb | 4 ++-- wrapper/Ada/tls_server.adb | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index 9e872fccd..4cd56c08b 100644 --- a/wrapper/Ada/tls_client.adb +++ b/wrapper/Ada/tls_client.adb @@ -204,8 +204,8 @@ package body Tls_Client with SPARK_Mode is Output : WolfSSL.Write_Result; Result : WolfSSL.Subprogram_Result; - DTLS : Boolean; - PSK : Boolean; + DTLS : Boolean := False; + PSK : Boolean := False; begin Result := WolfSSL.Initialize; if Result /= Success then diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index e17af00a5..3f1b3dc8a 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -162,7 +162,7 @@ package body Tls_Server with SPARK_Mode is Ch : Character; Result : WolfSSL.Subprogram_Result; - DTLS, PSK : Boolean; + DTLS, PSK : Boolean := True; Shall_Continue : Boolean := True; Input : WolfSSL.Read_Result; From 98eda78857cfc463e8980c30fa3f989c8be08e5f Mon Sep 17 00:00:00 2001 From: mgrojo Date: Fri, 28 Mar 2025 19:33:42 +0100 Subject: [PATCH 3/4] Ada: fix issues in tls_server.adb detected by gnatprove Checked with: ``` gnatprove -Pdefault.gpr --level=4 -j12 ``` --- wrapper/Ada/tls_server.adb | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 3f1b3dc8a..52ec6ac2e 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -139,10 +139,6 @@ package body Tls_Server with SPARK_Mode is return 0; end if; - put_line (Interfaces.C.Strings.Value - (Item => Identity, - Length => Identity_String'Length) ); - Interfaces.C.Strings.Update (Item => Key, Offset => 0, @@ -261,13 +257,15 @@ package body Tls_Server with SPARK_Mode is if not PSK then -- Require mutual authentication. WolfSSL.Set_Verify - (Context => Ctx, + (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; + Put_Line ("Error: Verify does not match requested"); + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + Set (Exit_Status_Failure); return; end if; From e6f09b8372ee227996a13c720a1fa5fa26a4320e Mon Sep 17 00:00:00 2001 From: mgrojo Date: Mon, 31 Mar 2025 23:27:31 +0200 Subject: [PATCH 4/4] Ada: fixes for the No_Secondary_Stack restriction - Align README.md and GPR files with the fact that the server no longer compiles with the No_Secondary_Stack restriction. - Fix include.am to reference the new name for the adc file. --- wrapper/Ada/README.md | 15 ++++++++------- wrapper/Ada/default.gpr | 14 ++++++++------ wrapper/Ada/{client.gpr => examples.gpr} | 6 +++--- wrapper/Ada/include.am | 2 +- wrapper/Ada/tls_server.adb | 8 ++++---- 5 files changed, 24 insertions(+), 21 deletions(-) rename wrapper/Ada/{client.gpr => examples.gpr} (92%) diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md index d0cb2da28..ac98f71ae 100644 --- a/wrapper/Ada/README.md +++ b/wrapper/Ada/README.md @@ -13,10 +13,11 @@ code to zero-out stack frames used by subprograms. Unfortunately this works well for the primary stack but not 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 +No_Secondary_Stack (see the GNAT configuration file restricted.adc which instructs compilation of the WolfSSL Ada binding under this restriction). Note, however, that the examples do make use of the -secondary stack. +secondary stack and the Alire project does not include this restriction, for +letting users of the library to define it at their level. Portability: The WolfSSL Ada binding makes no usage of controlled types and has no dependency upon the Ada.Finalization package. @@ -25,11 +26,11 @@ the restriction No_Finalization. The WolfSSL Ada binding has been developed with maximum portability in mind. Not only can the WolfSSL Ada binding be used in Ada applications but -also SPARK applications (a subset of the Ada language suitable +also SPARK applications (a subset of the Ada language suitable for formal verification). To formally verify the Ada code in this repository -open the client.gpr with GNAT Studio and then select +open the examples.gpr with GNAT Studio and then select SPARK -> Prove All Sources and use Proof Level 2. Or when using the command -line, use `gnatprove -Pclient.gpr --level=4 -j12` (`-j12` is there in +line, use `gnatprove -Pexamples.gpr --level=4 -j12` (`-j12` is there in order to instruct the prover to use 12 CPUs if available). ``` @@ -83,7 +84,7 @@ and use gprbuild to build the source code. cd wrapper/Ada gprclean gprbuild default.gpr -gprbuild client.gpr +gprbuild examples.gpr cd obj/ ./tls_server_main & @@ -93,7 +94,7 @@ cd obj/ On Windows, build the executables with: ```sh gprbuild -XOS=Windows default.gpr -gprbuild -XOS=Windows client.gpr +gprbuild -XOS=Windows examples.gpr ``` ## Files diff --git a/wrapper/Ada/default.gpr b/wrapper/Ada/default.gpr index c59c3e347..16809601b 100644 --- a/wrapper/Ada/default.gpr +++ b/wrapper/Ada/default.gpr @@ -11,17 +11,19 @@ project Default is "../../src", "../../wolfcrypt/src"); - -- Don't build the tls client application because it makes use + -- Don't build the tls application examples because they make use -- of the Secondary Stack due to usage of the Ada.Command_Line -- package. All other Ada source code does not use the secondary stack. - for Excluded_Source_Files use ("tls_client_main.adb", - "tls_client.ads", - "tls_client.adb"); + for Excluded_Source_Files use + ("tls_client_main.adb", + "tls_client.ads", + "tls_client.adb", + "tls_server_main.adb", + "tls_server.ads", + "tls_server.adb"); for Object_Dir use "obj"; - for Main use ("tls_server_main.adb"); - package Naming is for Spec_Suffix ("C") use ".h"; end Naming; diff --git a/wrapper/Ada/client.gpr b/wrapper/Ada/examples.gpr similarity index 92% rename from wrapper/Ada/client.gpr rename to wrapper/Ada/examples.gpr index cdbf3dedf..218f93e51 100644 --- a/wrapper/Ada/client.gpr +++ b/wrapper/Ada/examples.gpr @@ -1,4 +1,4 @@ -project Client is +project Examples is type OS_Kind is ("Windows", "Linux_Or_Mac"); OS : OS_Kind := external ("OS", "Linux_Or_Mac"); @@ -12,7 +12,7 @@ project Client is for Object_Dir use "obj"; - for Main use ("tls_client_main.adb"); + for Main use ("tls_server_main.adb", "tls_client_main.adb"); package Naming is for Spec_Suffix ("C") use ".h"; @@ -75,4 +75,4 @@ project Client is for Switches ("Ada") use ("-Es"); -- To include stack traces. end Binder; -end Client; +end Examples; diff --git a/wrapper/Ada/include.am b/wrapper/Ada/include.am index 3701e581c..cc2001e9a 100644 --- a/wrapper/Ada/include.am +++ b/wrapper/Ada/include.am @@ -4,7 +4,7 @@ EXTRA_DIST+= wrapper/Ada/README.md EXTRA_DIST+= wrapper/Ada/default.gpr -EXTRA_DIST+= wrapper/Ada/gnat.adc +EXTRA_DIST+= wrapper/Ada/restricted.adc EXTRA_DIST+= wrapper/Ada/ada_binding.c EXTRA_DIST+= wrapper/Ada/tls_client_main.adb EXTRA_DIST+= wrapper/Ada/tls_client.adb diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 52ec6ac2e..9cd30b9d3 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -122,10 +122,10 @@ package body Tls_Server with SPARK_Mode is 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); + (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.