Ada Bindings and CI Improvements

.editorconfig

@@ -8,3 +8,6 @@ end_of_line = lf
 charset = utf-8
 trim_trailing_whitespace = true
 insert_final_newline = true
+
+[*.{ads,adb,gpr}]
+indent_size = 3

.github/workflows/ada.yml

@@ -15,20 +15,59 @@ jobs:
     steps:
     - uses: actions/checkout@master
 
-    - name: Install gnat
+    - name: Install alire
+      uses: alire-project/setup-alire@v5
+
+    - name: Install wolfssl Ada
+      working-directory: ./wrapper/Ada
+      run: alr install
+
+    - name: Build default.gpr
+      working-directory: ./wrapper/Ada
+      run: alr exec -- gprbuild default.gpr -j$(nproc)
+
+    - name: Run Ada wrapper tests
+      working-directory: ./wrapper/Ada/tests
+      run: alr run
+
+    - name: Run Ada examples
+      id: examples
+      working-directory: ./wrapper/Ada/examples
       run: |
-        sudo apt-get update
-        sudo apt-get install -y gnat gprbuild
+        alr build
+
+        echo "Running sha256_main example..."
+        alr run sha256_main
 
-    - name: Checkout wolfssl
-      uses: actions/checkout@master
-      with:
-        repository: wolfssl/wolfssl
-        path: wolfssl
+        echo "Running aes_verify_main example..."
+        alr run aes_verify_main
 
-    - name: Build wolfssl Ada
-      working-directory: ./wolfssl/wrapper/Ada
+        echo "Running rsa_verify_main example..."
+        alr run rsa_verify_main
+
+        echo "Running TLS server/client example..."
+        alr run tls_server_main &> server.log &
+        SERVER_PID=$!
+        sleep 1
+        echo "test message" | alr run tls_client_main --args=127.0.0.1
+        kill $SERVER_PID || true
+
+    - name: show errors
+      if: ${{ failure() && steps.examples.outcome == 'failure' }}
+      run: cat ./wrapper/Ada/examples/server.log
+
+    - name: Run Ada wrapper tests (valgrind)
+      working-directory: ./wrapper/Ada/tests
       run: |
-        mkdir obj
-        gprbuild default.gpr
-        gprbuild examples.gpr
+        sudo apt-get update
+        sudo apt-get install -y valgrind
+        valgrind --leak-check=full --error-exitcode=1 \
+          --suppressions=valgrind.supp ./bin/tests
+
+    - name: Run gnatprove on wolfssl
+      working-directory: ./wrapper/Ada
+      run: alr gnatprove --level=4 -P wolfssl.gpr -j 0 --warnings=error --checks-as-errors --proof-warnings -U
+
+    - name: Run gnatprove on examples
+      working-directory: ./wrapper/Ada/examples
+      run: alr gnatprove --level=4 -P examples.gpr -j 0 --warnings=error --checks-as-errors --proof-warnings -U

wolfssl/wolfcrypt/types.h

@@ -1348,6 +1348,7 @@ enum {
     DYNAMIC_TYPE_X509_ACERT   = 103,
     DYNAMIC_TYPE_OS_BUF       = 104,
     DYNAMIC_TYPE_ASCON        = 105,
+    DYNAMIC_TYPE_SHA          = 106,
     DYNAMIC_TYPE_SNIFFER_SERVER       = 1000,
     DYNAMIC_TYPE_SNIFFER_SESSION      = 1001,
     DYNAMIC_TYPE_SNIFFER_PB           = 1002,

wrapper/Ada/.gitignore

@@ -1 +1,4 @@
-obj
+/obj/
+/bin/
+/alire/
+/config/

wrapper/Ada/README.md

@@ -28,9 +28,9 @@ 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 for
 formal verification). To formally verify the Ada code in this repository
-open the examples.gpr with GNAT Studio and then select
+open the examples/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 -Pexamples.gpr --level=4 -j12` (`-j12` is there in
+line, use `gnatprove -Pexamples/examples.gpr --level=4 -j12` (`-j12` is there in
 order to instruct the prover to use 12 CPUs if available).
 
 ```
@@ -62,6 +62,8 @@ 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.
 
+**Note:** If you encounter a missing dependency error, it may be caused by the installed dependency being too old. In this case, either install a newer toolchain or decrease the required dependency version in your project.
+
 In order to use WolfSSL in a project, just add WolfSSL as a dependency by
 running `alr with wolfssl` within your project's directory.
 
@@ -84,28 +86,48 @@ and use gprbuild to build the source code.
 cd wrapper/Ada
 gprclean
 gprbuild default.gpr
+
+cd examples
 gprbuild examples.gpr
 
 cd obj/
 ./tls_server_main &
 ./tls_client_main 127.0.0.1
 ```
 
+If you are using Alire, you can build the library and examples with:
+
+```sh
+cd wrapper/Ada
+alr install
+
+cd examples
+alr build
+```
+
+You can also run the examples directly with Alire:
+
+```sh
+cd wrapper/Ada/examples
+alr run tls_server_main &
+alr run tls_client_main --args=127.0.0.1
+```
+
 On Windows, build the executables with:
 ```sh
-gprbuild -XOS=Windows default.gpr
+cd wrapper/Ada/examples
 gprbuild -XOS=Windows examples.gpr
 ```
 
 ## Files
 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
+examples/src/tls_client_main.adb
+examples/src/tls_client.ads
+examples/src/tls_client.adb
 
 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
-tls_server.adb
+examples/src/tls_server_main.adb
+examples/src/tls_server.ads
+examples/src/tls_server.adb

wrapper/Ada/ada_binding.c

@@ -26,7 +26,15 @@
 /* wolfSSL */
 #include <wolfssl/wolfcrypt/settings.h>
 #include <wolfssl/ssl.h>
+#include <wolfssl/wolfcrypt/rsa.h>
+#include <wolfssl/wolfcrypt/sha256.h>
+#include <wolfssl/wolfcrypt/aes.h>
 
+#include <stdlib.h>
+
+/* RSA instances are now dynamically allocated (no fixed pool). */
+/* SHA256 instances are now dynamically allocated (no fixed pool). */
+/* AES instances are now dynamically allocated (no fixed pool). */
 /* These functions give access to the integer values of the enumeration
    constants used in WolfSSL. These functions make it possible
    for the WolfSSL implementation to change the values of the constants
@@ -48,6 +56,31 @@ extern int get_wolfssl_filetype_asn1(void);
 extern int get_wolfssl_filetype_pem(void);
 extern int get_wolfssl_filetype_default(void);
 
+extern void* ada_new_rsa (void);
+extern void ada_free_rsa (void* key);
+
+extern void *ada_new_sha256 (void);
+extern void ada_free_sha256 (void* sha256);
+
+extern void* ada_new_aes (int devId);
+extern void ada_free_aes (void* aes);
+
+extern void* ada_new_rng (void);
+extern void ada_free_rng (void* rng);
+extern int ada_RsaSetRNG (RsaKey* key, WC_RNG* rng);
+
+extern int get_wolfssl_invalid_devid (void);
+
+extern int ada_md5 (void);
+extern int ada_sha (void);
+extern int ada_sha256 (void);
+extern int ada_sha384 (void);
+extern int ada_sha512 (void);
+extern int ada_sha3_224 (void);
+extern int ada_sha3_256 (void);
+extern int ada_sha3_384 (void);
+extern int ada_sha3_512 (void);
+
 extern int get_wolfssl_error_want_read(void) {
   return WOLFSSL_ERROR_WANT_READ;
 }
@@ -107,3 +140,111 @@ extern int get_wolfssl_filetype_pem(void) {
 extern int get_wolfssl_filetype_default(void) {
   return WOLFSSL_FILETYPE_DEFAULT;
 }
+
+extern void* ada_new_rsa (void)
+{
+  /* Allocate and initialize an RSA key using wolfCrypt's constructor. */
+  return (void*)wc_NewRsaKey(NULL, INVALID_DEVID, NULL);
+}
+
+extern void ada_free_rsa (void* key)
+{
+  /* Delete RSA key and release its memory. */
+  wc_DeleteRsaKey((RsaKey*)key, NULL);
+}
+
+extern void* ada_new_sha256 (void)
+{
+  return XMALLOC(sizeof(wc_Sha256), NULL, DYNAMIC_TYPE_SHA);
+}
+
+extern void ada_free_sha256 (void* sha256)
+{
+  XFREE(sha256, NULL, DYNAMIC_TYPE_SHA);
+}
+
+
+
+extern void* ada_new_aes (int devId)
+{
+  /* Allocate and initialize an AES object using wolfCrypt's constructor. */
+  return (void*)wc_AesNew(NULL, devId, NULL);
+}
+
+extern void ada_free_aes (void* aes)
+{
+  /* Delete AES object and release its memory. */
+  wc_AesDelete((Aes*)aes, NULL);
+}
+
+extern int get_wolfssl_invalid_devid (void)
+{
+  return INVALID_DEVID;
+}
+
+extern void* ada_new_rng (void)
+{
+  /* Allocate and initialize a WC_RNG using wolfCrypt's allocator.
+   * Per request: pass NULL and 0 to wc_rng_new (nonce, nonceSz).
+   */
+  return (void*)wc_rng_new(NULL, 0, NULL);
+}
+
+extern void ada_free_rng (void* rng)
+{
+  wc_rng_free((WC_RNG*)rng);
+}
+
+extern int ada_RsaSetRNG(RsaKey* key, WC_RNG* rng)
+{
+  int r = 0;
+#ifdef WC_RSA_BLINDING /* HIGHLY RECOMMENDED! */
+  r = wc_RsaSetRNG(key, rng);
+#endif
+  return r;
+}
+
+extern int ada_md5 (void)
+{
+  return WC_MD5;
+}
+
+extern int ada_sha (void)
+{
+  return WC_SHA;
+}
+
+extern int ada_sha256 (void)
+{
+  return WC_SHA256;
+}
+
+extern int ada_sha384 (void)
+{
+  return WC_SHA384;
+}
+
+extern int ada_sha512 (void)
+{
+  return WC_SHA512;
+}
+
+extern int ada_sha3_224 (void)
+{
+  return WC_SHA3_224;
+}
+
+extern int ada_sha3_256 (void)
+{
+  return WC_SHA3_256;
+}
+
+extern int ada_sha3_384 (void)
+{
+  return WC_SHA3_384;
+}
+
+extern int ada_sha3_512 (void)
+{
+  return WC_SHA3_512;
+}

wrapper/Ada/alire.toml

@@ -12,3 +12,6 @@ tags = ["ssl", "tls", "embedded", "spark"]
 
 [configuration.variables]
 STATIC_PSK = {type = "Boolean", default = false}
+
+[[depends-on]]
+gnatprove = "^13.2.1"

wrapper/Ada/default.gpr

@@ -11,17 +11,6 @@ project Default is
                         "../../src",
                         "../../wolfcrypt/src");
 
-   --  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",
-      "tls_server_main.adb",
-      "tls_server.ads",
-      "tls_server.adb");
-
    for Object_Dir use "obj";
 
    package Naming is