Merge pull request #6605 from dgarske/ada

Ada Bindings for wolfSSL

examples/configs/user_settings_all.h

@@ -125,7 +125,7 @@ extern "C" {
 #define WOLFSSL_DER_TO_PEM
 #define WOLFSSL_CUSTOM_OID
 #define HAVE_OID_ENCODING
-//#define WOLFSSL_ASN_TEMPLATE /* Not enabled yet by default */
+#define WOLFSSL_ASN_TEMPLATE
 
 /* Certificate Revocation */
 #define HAVE_OCSP

wrapper/Ada/README.md

@@ -0,0 +1,111 @@
+# 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
+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:
+
+```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
+gprbuild client.gpr
+
+cd obj/
+./tls_server_main &
+./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

@@ -0,0 +1,105 @@
+/* ada_binding.c
+ *
+ * Copyright (C) 2006-2023 wolfSSL Inc.
+ *
+ * This file is part of wolfSSL.
+ *
+ * wolfSSL is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * wolfSSL is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+ */
+
+/* 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);
+extern int get_wolfssl_verify_client_once(void);
+extern int get_wolfssl_verify_post_handshake(void);
+extern int get_wolfssl_verify_fail_except_psk(void);
+extern int get_wolfssl_verify_default(void);
+
+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;
+}
+
+extern int get_wolfssl_verify_peer(void) {
+ return WOLFSSL_VERIFY_PEER;
+}
+
+extern int get_wolfssl_verify_fail_if_no_peer_cert(void) {
+ return WOLFSSL_VERIFY_FAIL_IF_NO_PEER_CERT;
+}
+
+extern int get_wolfssl_verify_client_once(void) {
+ return WOLFSSL_VERIFY_CLIENT_ONCE;
+}
+
+extern int get_wolfssl_verify_post_handshake(void) {
+ return WOLFSSL_VERIFY_POST_HANDSHAKE;
+}
+
+extern int get_wolfssl_verify_fail_except_psk(void) {
+ return WOLFSSL_VERIFY_FAIL_EXCEPT_PSK;
+}
+
+extern int get_wolfssl_verify_default(void) {
+ return WOLFSSL_VERIFY_DEFAULT;
+}
+
+extern int get_wolfssl_filetype_asn1(void) {
+ return WOLFSSL_FILETYPE_ASN1;
+}
+
+extern int get_wolfssl_filetype_pem(void) {
+ return WOLFSSL_FILETYPE_PEM;
+}
+
+extern int get_wolfssl_filetype_default(void) {
+ return WOLFSSL_FILETYPE_DEFAULT;
+}