Updated README.md file. Added description of subprograms in the specification file of the WolfSSL package. Made it possible to get error codes through the WolfSSL API.

Author: joakim-strandberg

wrapper/Ada/README.md

@@ -1,6 +1,57 @@
 # Ada Binding Example
+The source code for the Ada/SPARK binding of the WolfSSL library
+is the WolfSSL Ada package in the wolfssl.ads and wolfssl.adb files.
 
-Download and install the GNAT community edition compiler and studio:
+The source code here also demonstrates a TLS v1.3 server and client
+using the WolfSSL Ada binding. The implementation is cross-platform
+and compiles on Linux, Mac OS X and Windows.
+
+Security: The WolfSSL Ada binding avoids usage of the
+Seconday Stack. The GNAT compiler has a number of hardening
+features for example Stack Scrubbing; the compiler can generate
+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
+which instructs compilation of the WolfSSL Ada binding under
+this restriction).
+
+Portability: The WolfSSL Ada binding makes no usage of controlled types
+and has no dependency upon the Ada.Finalization package.
+Lighter Ada run-times for embedded systems often have
+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
+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.
+
+Summary of SPARK analysis
+=========================
+
+---------------------------------------------------------------------------------------------------------------
+SPARK Analysis results        Total        Flow   CodePeer                       Provers   Justified   Unproved
+---------------------------------------------------------------------------------------------------------------
+Data Dependencies                 2           2          .                             .           .          .
+Flow Dependencies                 .           .          .                             .           .          .
+Initialization                   15          15          .                             .           .          .
+Non-Aliasing                      .           .          .                             .           .          .
+Run-time Checks                  58           .          .    58 (CVC4 85%, Trivial 15%)           .          .
+Assertions                        6           .          .                      6 (CVC4)           .          .
+Functional Contracts             91           .          .                     91 (CVC4)           .          .
+LSP Verification                  .           .          .                             .           .          .
+Termination                       .           .          .                             .           .          .
+Concurrency                       .           .          .                             .           .          .
+---------------------------------------------------------------------------------------------------------------
+Total                           172    17 (10%)          .                     155 (90%)           .          .
+
+## Compiler and Build System installation
+
+### GNAT Community Edition 2021
+Download and install the GNAT community Edition 2021 compiler and studio:
 https://www.adacore.com/download
 
 Linux Install:
@@ -14,9 +65,46 @@ chmod +x gnat-2021-20210519-x86_64-linux-bin
 export PATH="/opt/GNAT/2021/bin:$PATH"
 gprclean
 gprbuild default.gpr
+gprbuild client.gpr
 
-
-./c_tls_server_main
+cd obj/
 ./tls_server_main &
-./c_tls_client_main 127.0.0.1
+./tls_client_main 127.0.0.1
 ```
+
+### 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 file c_tls_client_main.c and c_tls_server_main.c are the TLS v1.3
+server and client examples using the WolfSSL library implemented using
+the C programming language.
+
+The translation of the C client example into the Ada/SPARK programming
+language can be found in the files:
+tls_client_main.adb
+tls_client.ads
+tls_client.adb
+
+The translation of the C server example into the Ada/SPARK programming
+language 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

wrapper/Ada/ada_binding.c

@@ -21,14 +21,17 @@
 
 /* wolfSSL */
 #include <wolfssl/wolfcrypt/settings.h>
-
 #include <wolfssl/ssl.h>
 
 /* 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
    without the need to make a corresponding change in the Ada code. */
+extern int get_wolfssl_error_want_read(void);
+extern int get_wolfssl_error_want_write(void);
+extern int get_wolfssl_max_error_size (void);
 extern int get_wolfssl_success(void);
+extern int get_wolfssl_failure(void);
 extern int get_wolfssl_verify_none(void);
 extern int get_wolfssl_verify_peer(void);
 extern int get_wolfssl_verify_fail_if_no_peer_cert(void);
@@ -41,10 +44,26 @@ extern int get_wolfssl_filetype_asn1(void);
 extern int get_wolfssl_filetype_pem(void);
 extern int get_wolfssl_filetype_default(void);
 
+extern int get_wolfssl_error_want_read(void) {
+  return WOLFSSL_ERROR_WANT_READ;
+}
+
+extern int get_wolfssl_error_want_write(void) {
+  return WOLFSSL_ERROR_WANT_WRITE;
+}
+
+extern int get_wolfssl_max_error_size(void) {
+  return WOLFSSL_MAX_ERROR_SZ;
+}
+
 extern int get_wolfssl_success(void) {
   return WOLFSSL_SUCCESS;
 }
 
+extern int get_wolfssl_failure(void) {
+  return WOLFSSL_FAILURE;
+}
+
 extern int get_wolfssl_verify_none(void) {
   return WOLFSSL_VERIFY_NONE;
 }

wrapper/Ada/tls_client.adb

@@ -32,21 +32,29 @@ package body Tls_Client with SPARK_Mode is
    use type WolfSSL.Mode_Type;
    use type WolfSSL.Byte_Index;
    use type WolfSSL.Byte_Array;
+   use type WolfSSL.Subprogram_Result;
 
-   use all type WolfSSL.Subprogram_Result;
+   subtype Byte_Index is WolfSSL.Byte_Index;
+
+   Success : WolfSSL.Subprogram_Result renames WolfSSL.Success;
 
    subtype Byte_Type is WolfSSL.Byte_Type;
 
-   package Integer_IO is new Ada.Text_IO.Integer_IO (Integer);
+   package Natural_IO is new Ada.Text_IO.Integer_IO (Natural);
 
    procedure Put (Text : String) is
    begin
       Ada.Text_IO.Put (Text);
    end Put;
 
-   procedure Put (Number : Integer) is
+   procedure Put (Number : Natural) is
+   begin
+      Natural_IO.Put (Item => Number, Width => 0, Base => 10);
+   end Put;
+
+   procedure Put (Number : Byte_Index) is
    begin
-      Integer_IO.Put (Item => Number, Width => 0, Base => 10);
+      Natural_IO.Put (Item => Natural (Number), Width => 0, Base => 10);
    end Put;
 
    procedure Put_Line (Text : String) is
@@ -120,19 +128,18 @@ package body Tls_Client with SPARK_Mode is
 
       Addr : SPARK_Sockets.Optional_Inet_Addr;
 
-      Bytes_Written : Integer;
-
       Count : WolfSSL.Byte_Index;
 
       Text : String (1 .. 200);
-      Last : Integer;
+      Last : Natural;
 
-      Input : WolfSSL.Read_Result;
+      Input  : WolfSSL.Read_Result;
+      Output : WolfSSL.Write_Result;
 
       Result : WolfSSL.Subprogram_Result;
    begin
       Result := WolfSSL.Initialize;
-      if Result = Failure then
+      if Result /= Success then
          Put_Line ("ERROR: Failed to initialize the WolfSSL library.");
          return;
       end if;
@@ -162,7 +169,7 @@ package body Tls_Client with SPARK_Mode is
 
       Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket,
                                               Server => A);
-      if Result = Failure then
+      if Result /= Success then
          Put_Line ("ERROR: Failed to connect to server.");
          SPARK_Sockets.Close_Socket (C);
          Set (Exit_Status_Failure);
@@ -183,7 +190,7 @@ package body Tls_Client with SPARK_Mode is
       Result := WolfSSL.Use_Certificate_File (Context => Ctx,
                                               File    => CERT_FILE,
                                               Format  => WolfSSL.Format_Pem);
-      if Result = Failure then
+      if Result /= Success then
          Put ("ERROR: failed to load ");
          Put (CERT_FILE);
          Put (", please check the file.");
@@ -198,7 +205,7 @@ package body Tls_Client with SPARK_Mode is
       Result := WolfSSL.Use_Private_Key_File (Context => Ctx,
                                               File    => KEY_FILE,
                                               Format  => WolfSSL.Format_Pem);
-      if Result = Failure then
+      if Result /= Success then
          Put ("ERROR: failed to load ");
          Put (KEY_FILE);
          Put (", please check the file.");
@@ -213,7 +220,7 @@ package body Tls_Client with SPARK_Mode is
       Result := WolfSSL.Load_Verify_Locations (Context => Ctx,
                                                File    => CA_FILE,
                                                Path    => "");
-      if Result = Failure then
+      if Result /= Success then
          Put ("ERROR: failed to load ");
          Put (CA_FILE);
          Put (", please check the file.");
@@ -237,7 +244,7 @@ package body Tls_Client with SPARK_Mode is
       --  Attach wolfSSL to the socket.
       Result := WolfSSL.Attach (Ssl    => Ssl,
                                 Socket => SPARK_Sockets.To_C (C.Socket));
-      if Result = Failure then
+      if Result /= Success then
          Put_Line ("ERROR: Failed to set the file descriptor.");
          SPARK_Sockets.Close_Socket (C);
          WolfSSL.Free (Ssl);
@@ -247,7 +254,7 @@ package body Tls_Client with SPARK_Mode is
       end if;
 
       Result := WolfSSL.Connect (Ssl);
-      if Result = Failure then
+      if Result /= Success then
          Put_Line ("ERROR: failed to connect to wolfSSL.");
          SPARK_Sockets.Close_Socket (C);
          WolfSSL.Free (Ssl);
@@ -262,12 +269,21 @@ package body Tls_Client with SPARK_Mode is
       SPARK_Sockets.To_C (Item       => Text (1 .. Last),
                           Target     => D,
                           Count      => Count);
-      Bytes_Written := WolfSSL.Write (Ssl  => Ssl,
-                                      Data => D (1 .. Count));
-      if Bytes_Written < Last then
+      Output := WolfSSL.Write (Ssl  => Ssl,
+                               Data => D (1 .. Count));
+      if not Output.Success then
+         Put ("ERROR: write failure");
+         New_Line;
+         SPARK_Sockets.Close_Socket (C);
+         WolfSSL.Free (Ssl);
+         WolfSSL.Free (Context => Ctx);
+         return;
+      end if;
+
+      if Natural (Output.Bytes_Written) < Last then
          Put ("ERROR: failed to write entire message");
          New_Line;
-         Put (Bytes_Written);
+         Put (Output.Bytes_Written);
          Put (" bytes of ");
          Put (Last);
          Put ("bytes were sent");
@@ -279,7 +295,7 @@ package body Tls_Client with SPARK_Mode is
       end if;
 
       Input := WolfSSL.Read (Ssl);
-      if Input.Result /= Success then
+      if not Input.Success then
          Put_Line ("Read error.");
          Set (Exit_Status_Failure);
          SPARK_Sockets.Close_Socket (C);
@@ -304,7 +320,7 @@ package body Tls_Client with SPARK_Mode is
       WolfSSL.Free (Ssl);
       WolfSSL.Free (Context => Ctx);
       Result := WolfSSL.Finalize;
-      if Result = Failure then
+      if Result /= Success then
          Put_Line ("ERROR: Failed to finalize the WolfSSL library.");
       end if;
    end Run;