From 79235a469824e27c52f26b1a763a1fc2fac8bae2 Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Wed, 6 Mar 2024 20:20:55 +0100 Subject: [PATCH 1/8] [Ada] Initial library support --- wrapper/Ada/wolfssl.gpr | 96 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 wrapper/Ada/wolfssl.gpr diff --git a/wrapper/Ada/wolfssl.gpr b/wrapper/Ada/wolfssl.gpr new file mode 100644 index 000000000..65d8cce6f --- /dev/null +++ b/wrapper/Ada/wolfssl.gpr @@ -0,0 +1,96 @@ +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"); + + for Source_Dirs use (".", + "../../", + "../../src", + "../../wolfcrypt/src"); + + -- 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 Object_Dir use "obj"; + for Library_Dir use "lib"; + for Create_Missing_Dirs use "True"; + + type Library_Type_Type is ("relocatable", "static", "static-pic"); + Library_Type : Library_Type_Type := external("LIBRARY_TYPE", "static"); + for Library_Kind use Library_Type; + + package Naming 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. + "-Wno-pragmas", + "-Wall", + "-Wextra", + "-Wunknown-pragmas", + "--param=ssp-buffer-size=1", + "-Waddress", + "-Warray-bounds", + "-Wbad-function-cast", + "-Wchar-subscripts", + "-Wcomment", + "-Wfloat-equal", + "-Wformat-security", + "-Wformat=2", + "-Wmaybe-uninitialized", + "-Wmissing-field-initializers", + "-Wmissing-noreturn", + "-Wmissing-prototypes", + "-Wnested-externs", + "-Wnormalized=id", + "-Woverride-init", + "-Wpointer-arith", + "-Wpointer-sign", + "-Wshadow", + "-Wsign-compare", + "-Wstrict-overflow=1", + "-Wstrict-prototypes", + "-Wswitch-enum", + "-Wundef", + "-Wunused", + "-Wunused-result", + "-Wunused-variable", + "-Wwrite-strings", + "-fwrapv") & External_As_List ("CFLAGS", " "); + + for Switches ("Ada") use ("-g") & External_As_List ("ADAFLAGS", " "); + end Compiler; + + 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 4a5373f21bde3c5cb441c74c59e2013163f67fab Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Fri, 5 Apr 2024 23:23:26 +0200 Subject: [PATCH 2/8] Add Ada/Alire files to gitignore --- .gitignore | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.gitignore b/.gitignore index 5bd31033f..d25a5bca1 100644 --- a/.gitignore +++ b/.gitignore @@ -433,3 +433,9 @@ MagicCrypto debian/changelog debian/control *.deb + +# Ada/Alire files +wrapper/Ada/alire/ +wrapper/Ada/config/ +wrapper/Ada/lib/ +wrapper/Ada/obj/ From 77cd3b837b6e1d1451bfcb2fcbaff6d5e72eb71e Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Fri, 5 Apr 2024 23:27:24 +0200 Subject: [PATCH 3/8] [Ada] Explicitly add netdb.h support --- wrapper/Ada/user_settings.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/wrapper/Ada/user_settings.h b/wrapper/Ada/user_settings.h index df4ada44e..3c444df5f 100644 --- a/wrapper/Ada/user_settings.h +++ b/wrapper/Ada/user_settings.h @@ -37,6 +37,9 @@ extern "C" { /* Usually comes from configure -> config.h */ #define HAVE_SYS_TIME_H +/* Explicitly define NETDB support */ +#define HAVE_NETDB_H + /* Features */ #define SINGLE_THREADED #define WOLFSSL_IGNORE_FILE_WARN /* Ignore *.c include warnings */ From afc1e9689974a992c3259c675a7e39a0145b1ce4 Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Fri, 5 Apr 2024 23:29:45 +0200 Subject: [PATCH 4/8] [Ada] Add initial Alire support, alpha version --- wrapper/Ada/alire.toml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 wrapper/Ada/alire.toml diff --git a/wrapper/Ada/alire.toml b/wrapper/Ada/alire.toml new file mode 100644 index 000000000..19fc8aa26 --- /dev/null +++ b/wrapper/Ada/alire.toml @@ -0,0 +1,15 @@ +name = "wolfss_ada" +description = "WolfSSL encryption library and its Ada bindings" +version = "5.7.0-dev" + +authors = ["Fernando Oleo Blanco"] +maintainers = ["Fernando Oleo Blanco "] +maintainers-logins = ["Irvise"] +licenses = "GPL-2.0-only" +website = "https://www.wolfssl.com/" +project-files = ["wolfssl.gpr"] +tags = ["ssl", "tls", "embedded", "spark"] + +#[origin] +#url="https://github.com/wolfSSL/wolfssl/releases/download/v5.6.6-stable/wolfssl-5.6.6.zip" +#hashes=['sha512:2d95d333c0b092dd7eface1b20221c33787cc847af11848c1eb845c5bd46e167b142cea09096c4981db94f8705f3e8499c2def2c6a648468e98442ba7b43c015'] From 8d49dce2cb3156a43741d3aaaee5c037e2cb0542 Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Sat, 6 Apr 2024 01:12:02 +0200 Subject: [PATCH 5/8] [Ada] Fix crate name in Alire --- wrapper/Ada/alire.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/wrapper/Ada/alire.toml b/wrapper/Ada/alire.toml index 19fc8aa26..1334e1343 100644 --- a/wrapper/Ada/alire.toml +++ b/wrapper/Ada/alire.toml @@ -1,4 +1,4 @@ -name = "wolfss_ada" +name = "wolfssl_ada" description = "WolfSSL encryption library and its Ada bindings" version = "5.7.0-dev" From ad25e9b0635483608b849cfbdd8e499e92c328bf Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Wed, 15 May 2024 22:33:29 +0200 Subject: [PATCH 6/8] [Ada] Clean Alire recipe --- wrapper/Ada/alire.toml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/wrapper/Ada/alire.toml b/wrapper/Ada/alire.toml index 1334e1343..7a963a78a 100644 --- a/wrapper/Ada/alire.toml +++ b/wrapper/Ada/alire.toml @@ -1,6 +1,6 @@ -name = "wolfssl_ada" +name = "wolfssl" description = "WolfSSL encryption library and its Ada bindings" -version = "5.7.0-dev" +version = "5.7.0" authors = ["Fernando Oleo Blanco"] maintainers = ["Fernando Oleo Blanco "] @@ -9,7 +9,3 @@ licenses = "GPL-2.0-only" website = "https://www.wolfssl.com/" project-files = ["wolfssl.gpr"] tags = ["ssl", "tls", "embedded", "spark"] - -#[origin] -#url="https://github.com/wolfSSL/wolfssl/releases/download/v5.6.6-stable/wolfssl-5.6.6.zip" -#hashes=['sha512:2d95d333c0b092dd7eface1b20221c33787cc847af11848c1eb845c5bd46e167b142cea09096c4981db94f8705f3e8499c2def2c6a648468e98442ba7b43c015'] From bec3cd8b6f7fb5f505a0ed7340445b962faf3afd Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Sun, 11 Aug 2024 18:36:54 +0200 Subject: [PATCH 7/8] Document Alire use --- wrapper/Ada/README.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md index 76f4b8e8b..9d10f76b3 100644 --- a/wrapper/Ada/README.md +++ b/wrapper/Ada/README.md @@ -53,6 +53,20 @@ Total 172 17 (10%) . 1 ## Compiler and Build System installation +### Recommended: [Alire](https://alire.ada.dev) +[Alire](https://alire.ada.dev) is a modern package manager for the Ada +ecosystem. The latest version is available for Windows, OSX, Linux and FreeBSD +systems. It can install a complete Ada toolchain if needed, see `alr install` +for more information. + +In order to use WolfSSL in a project, just add WolfSSL as a dependency by +running `alr with wolfssl` within your project's directory. + +If the project is to be verified with SPARK, just add `gnatprove` as a +dependency by running `alr with gnatprove` and then running `alr gnatprove`, +which will execute the SPARK solver. If you get warnings, it is recommended to +increase the prove level: `alr gnatprove --level=4`. + ### GNAT Community Edition 2021 Download and install the GNAT community Edition 2021 compiler and studio: https://www.adacore.com/download From 5ea22effcc8f74fb4f34730fca722873d0033ceb Mon Sep 17 00:00:00 2001 From: Fernando Oleo Blanco Date: Tue, 13 Aug 2024 10:56:25 +0200 Subject: [PATCH 8/8] Update documentation --- wrapper/Ada/README.md | 43 +++++++++++-------------------------------- 1 file changed, 11 insertions(+), 32 deletions(-) diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md index 9d10f76b3..d0cb2da28 100644 --- a/wrapper/Ada/README.md +++ b/wrapper/Ada/README.md @@ -28,7 +28,9 @@ Not only can the WolfSSL Ada binding be used in Ada applications but also SPARK applications (a subset of the Ada language suitable formal verification). To formally verify the Ada code in this repository open the client.gpr with GNAT Studio and then select -SPARK -> Prove All Sources and use Proof Level 2. +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 +order to instruct the prover to use 12 CPUs if available). ``` Summary of SPARK analysis @@ -67,19 +69,17 @@ dependency by running `alr with gnatprove` and then running `alr gnatprove`, which will execute the SPARK solver. If you get warnings, it is recommended to increase the prove level: `alr gnatprove --level=4`. -### GNAT Community Edition 2021 -Download and install the GNAT community Edition 2021 compiler and studio: -https://www.adacore.com/download +### GNAT FSF Compiler and GPRBuild manual installation +In May 2022 AdaCore announced the end of the GNAT Community releases. +Pre-built binaries for the GNAT FSF compiler and GPRBuild can be +downloaded and manually installed from here: +https://github.com/alire-project/GNAT-FSF-builds/releases +Make sure the executables for the compiler and GPRBuild are on the PATH +and use gprbuild to build the source code. -Linux Install: +#### Manual build of the project ```sh -chmod +x gnat-2021-20210519-x86_64-linux-bin -./gnat-2021-20210519-x86_64-linux-bin -``` - -```sh -export PATH="/opt/GNAT/2021/bin:$PATH" cd wrapper/Ada gprclean gprbuild default.gpr @@ -96,15 +96,6 @@ gprbuild -XOS=Windows default.gpr gprbuild -XOS=Windows client.gpr ``` - -### GNAT FSF Compiler and GPRBuild manual installation -In May 2022 AdaCore announced the end of the GNAT Community releases. -Pre-built binaries for the GNAT FSF compiler and GPRBuild can be -downloaded and manually installed from here: -https://github.com/alire-project/GNAT-FSF-builds/releases -Make sure the executables for the compiler and GPRBuild are on the PATH -and use gprbuild to build the source code. - ## Files The (D)TLS v1.3 client example in the Ada/SPARK programming language using the WolfSSL library can be found in the files: @@ -117,15 +108,3 @@ using the WolfSSL library can be found in the files: tls_server_main.adb tls_server.ads tls_server.adb - -A feature of the Ada language that is not part of SPARK is exceptions. -Some packages of the Ada standard library and GNAT specific packages -provided by the GNAT compiler can therefore not be used directly but -need to be put into wrapper packages that does not raise exceptions. -The packages that provide access to sockets and command line arguments -to applications implemented in the SPARK programming language can be -found in the files: -spark_sockets.ads -spark_sockets.adb -spark_terminal.ads -spark_terminal.adb