Joakim Strandberg 8794e3f2f6 Updated the Ada wrapper README.md file and removed mention of the c_tls_client_main.c and c_tls_server_main.c files. 1 tahun lalu
..
README.md 8794e3f2f6 Updated the Ada wrapper README.md file and removed mention of the c_tls_client_main.c and c_tls_server_main.c files. 1 tahun lalu
ada_binding.c 00b90adc97 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. 1 tahun lalu
client.gpr b6a11b8b01 Updated the README.md and updated client.gpr 1 tahun lalu
default.gpr b6a11b8b01 Updated the README.md and updated client.gpr 1 tahun lalu
gnat.adc d20a096ffa Ada Bindings for wolfSSL. Credit Joakim Dahlgren Strandberg <joakimds@kth.se> 1 tahun lalu
include.am 6893123edf Removed references to the c implementations of the client and server 1 tahun lalu
spark_sockets.adb f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
spark_sockets.ads f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
spark_terminal.adb f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
spark_terminal.ads f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
tls_client.adb 278f395542 Made sure the relative paths for finding the certificates is correct. 1 tahun lalu
tls_client.ads f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
tls_client_main.adb f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
tls_server.adb 278f395542 Made sure the relative paths for finding the certificates is correct. 1 tahun lalu
tls_server.ads f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
tls_server_main.adb f49ffc0353 The implementations of the tls client and server applications can now be formally verified by the SPARK tools. 1 tahun lalu
user_settings.h c76b0a0237 removed the C examples only keeping Ada code in the Ada wrapper example directory 1 tahun lalu
wolfssl.adb 00b90adc97 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. 1 tahun lalu
wolfssl.ads 00b90adc97 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. 1 tahun lalu

README.md

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.

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 Secondary 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:

chmod +x gnat-2021-20210519-x86_64-linux-bin
./gnat-2021-20210519-x86_64-linux-bin
export PATH="/opt/GNAT/2021/bin:$PATH"
cd wrapper/Ada
gprclean
gprbuild default.gpr
gprbuild client.gpr

cd obj/
./tls_server_main &
./tls_client_main 127.0.0.1

On Windows, build the executables with:

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 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

The 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

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