From d20a096ffa799186ece5293c7e9cdce74add6b72 Mon Sep 17 00:00:00 2001 From: David Garske Date: Wed, 12 Jul 2023 10:46:09 -0700 Subject: [PATCH 1/6] Ada Bindings for wolfSSL. Credit Joakim Dahlgren Strandberg --- examples/configs/user_settings_all.h | 2 +- wolfcrypt/src/asn.c | 4 +- wrapper/Ada/README.md | 22 + wrapper/Ada/ada_binding.c | 86 ++++ wrapper/Ada/c_tls_client_main.c | 285 +++++++++++++ wrapper/Ada/c_tls_server_main.c | 361 ++++++++++++++++ wrapper/Ada/default.gpr | 69 ++++ wrapper/Ada/gnat.adc | 1 + wrapper/Ada/include.am | 19 + wrapper/Ada/tls_client.adb | 81 ++++ wrapper/Ada/tls_client.ads | 5 + wrapper/Ada/tls_client_main.adb | 8 + wrapper/Ada/tls_server.adb | 240 +++++++++++ wrapper/Ada/tls_server.ads | 5 + wrapper/Ada/tls_server_main.adb | 8 + wrapper/Ada/user_settings.h | 385 +++++++++++++++++ wrapper/Ada/wolfssl.adb | 597 +++++++++++++++++++++++++++ wrapper/Ada/wolfssl.ads | 262 ++++++++++++ wrapper/include.am | 1 + 19 files changed, 2438 insertions(+), 3 deletions(-) create mode 100644 wrapper/Ada/README.md create mode 100644 wrapper/Ada/ada_binding.c create mode 100644 wrapper/Ada/c_tls_client_main.c create mode 100644 wrapper/Ada/c_tls_server_main.c create mode 100644 wrapper/Ada/default.gpr create mode 100644 wrapper/Ada/gnat.adc create mode 100644 wrapper/Ada/include.am create mode 100644 wrapper/Ada/tls_client.adb create mode 100644 wrapper/Ada/tls_client.ads create mode 100644 wrapper/Ada/tls_client_main.adb create mode 100644 wrapper/Ada/tls_server.adb create mode 100644 wrapper/Ada/tls_server.ads create mode 100644 wrapper/Ada/tls_server_main.adb create mode 100644 wrapper/Ada/user_settings.h create mode 100644 wrapper/Ada/wolfssl.adb create mode 100644 wrapper/Ada/wolfssl.ads diff --git a/examples/configs/user_settings_all.h b/examples/configs/user_settings_all.h index c708a64e4f..c484b90bef 100644 --- a/examples/configs/user_settings_all.h +++ b/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 diff --git a/wolfcrypt/src/asn.c b/wolfcrypt/src/asn.c index 8373daee73..4ab33b0383 100644 --- a/wolfcrypt/src/asn.c +++ b/wolfcrypt/src/asn.c @@ -30648,9 +30648,9 @@ int wc_SetCustomExtension(Cert *cert, int critical, const char *oid, ext = &cert->customCertExt[cert->customCertExtCount]; - ext->oid = oid; + ext->oid = (char*)oid; ext->crit = (critical == 0) ? 0 : 1; - ext->val = der; + ext->val = (byte*)der; ext->valSz = derSz; cert->customCertExtCount++; diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md new file mode 100644 index 0000000000..64ca8d13a3 --- /dev/null +++ b/wrapper/Ada/README.md @@ -0,0 +1,22 @@ +# Ada Binding Example + +Download and install the GNAT community edition 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" +gprclean +gprbuild default.gpr + + +./c_tls_server_main +./tls_server_main & +./c_tls_client_main 127.0.0.1 +``` diff --git a/wrapper/Ada/ada_binding.c b/wrapper/Ada/ada_binding.c new file mode 100644 index 0000000000..8eff71bb8d --- /dev/null +++ b/wrapper/Ada/ada_binding.c @@ -0,0 +1,86 @@ +/* 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 + +#include + +// 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_success(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_success(void) { + return WOLFSSL_SUCCESS; +} + +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; +} diff --git a/wrapper/Ada/c_tls_client_main.c b/wrapper/Ada/c_tls_client_main.c new file mode 100644 index 0000000000..1723c841d6 --- /dev/null +++ b/wrapper/Ada/c_tls_client_main.c @@ -0,0 +1,285 @@ +/* c_tls_client_main.c + * + * Copyright (C) 2006-2023 wolfSSL Inc. + * + * This file is part of wolfSSL. (formerly known as CyaSSL) + * + * 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-1301, USA + */ + +#include + + +/* the usual suspects */ +#include +#include +#include + +/* socket includes */ +#include +#include +#include +#include + +/* wolfSSL */ +#ifndef WOLFSSL_USER_SETTINGS + #include +#endif +#include +#include +#include + +#define DEFAULT_PORT 11111 + +#define CERT_FILE "../certs/client-cert.pem" +#define KEY_FILE "../certs/client-key.pem" +#define CA_FILE "../certs/ca-cert.pem" + +#if defined(WOLFSSL_TLS13) && defined(HAVE_SECRET_CALLBACK) + +#ifndef WOLFSSL_SSLKEYLOGFILE_OUTPUT + #define WOLFSSL_SSLKEYLOGFILE_OUTPUT "sslkeylog.log" +#endif + +/* Callback function for TLS v1.3 secrets for use with Wireshark */ +static int Tls13SecretCallback(WOLFSSL* ssl, int id, const unsigned char* secret, + int secretSz, void* ctx) +{ + int i; + const char* str = NULL; + unsigned char clientRandom[32]; + int clientRandomSz; + XFILE fp = stderr; + if (ctx) { + fp = XFOPEN((const char*)ctx, "ab"); + if (fp == XBADFILE) { + return BAD_FUNC_ARG; + } + } + + clientRandomSz = (int)wolfSSL_get_client_random(ssl, clientRandom, + sizeof(clientRandom)); + + if (clientRandomSz <= 0) { + printf("Error getting client random %d\n", clientRandomSz); + } + +#if 0 + printf("TLS Client Secret CB: Rand %d, Secret %d\n", + clientRandomSz, secretSz); +#endif + + switch (id) { + case CLIENT_EARLY_TRAFFIC_SECRET: + str = "CLIENT_EARLY_TRAFFIC_SECRET"; break; + case EARLY_EXPORTER_SECRET: + str = "EARLY_EXPORTER_SECRET"; break; + case CLIENT_HANDSHAKE_TRAFFIC_SECRET: + str = "CLIENT_HANDSHAKE_TRAFFIC_SECRET"; break; + case SERVER_HANDSHAKE_TRAFFIC_SECRET: + str = "SERVER_HANDSHAKE_TRAFFIC_SECRET"; break; + case CLIENT_TRAFFIC_SECRET: + str = "CLIENT_TRAFFIC_SECRET_0"; break; + case SERVER_TRAFFIC_SECRET: + str = "SERVER_TRAFFIC_SECRET_0"; break; + case EXPORTER_SECRET: + str = "EXPORTER_SECRET"; break; + } + + fprintf(fp, "%s ", str); + for (i = 0; i < clientRandomSz; i++) { + fprintf(fp, "%02x", clientRandom[i]); + } + fprintf(fp, " "); + for (i = 0; i < secretSz; i++) { + fprintf(fp, "%02x", secret[i]); + } + fprintf(fp, "\n"); + + if (fp != stderr) { + XFCLOSE(fp); + } + + return 0; +} +#endif /* WOLFSSL_TLS13 && HAVE_SECRET_CALLBACK */ + +int main(int argc, char** argv) +{ + int ret = 0; +#ifdef WOLFSSL_TLS13 + int sockfd = SOCKET_INVALID; + struct sockaddr_in servAddr; + char buff[256]; + size_t len; + + /* declare wolfSSL objects */ + WOLFSSL_CTX* ctx = NULL; + WOLFSSL* ssl = NULL; + + /* Check for proper calling convention */ + if (argc != 2) { + printf("usage: %s \n", argv[0]); + return 0; + } + + /* Create a socket that uses an internet IPv4 address, + * Sets the socket to be stream based (TCP), + * 0 means choose the default protocol. */ + if ((sockfd = socket(AF_INET, SOCK_STREAM, 0)) == -1) { + fprintf(stderr, "ERROR: failed to create the socket\n"); + ret = -1; goto exit; + } + + /* Initialize the server address struct with zeros */ + memset(&servAddr, 0, sizeof(servAddr)); + + /* Fill in the server address */ + servAddr.sin_family = AF_INET; /* using IPv4 */ + servAddr.sin_port = htons(DEFAULT_PORT); /* on DEFAULT_PORT */ + + /* Get the server IPv4 address from the command line call */ + if (inet_pton(AF_INET, argv[1], &servAddr.sin_addr) != 1) { + fprintf(stderr, "ERROR: invalid address\n"); + ret = -1; goto exit; + } + + /* Connect to the server */ + if ((ret = connect(sockfd, (struct sockaddr*) &servAddr, sizeof(servAddr))) + == -1) { + fprintf(stderr, "ERROR: failed to connect\n"); + goto exit; + } + + /*---------------------------------*/ + /* Start of wolfSSL initialization and configuration */ + /*---------------------------------*/ +#if 0 + wolfSSL_Debugging_ON(); +#endif + + /* Initialize wolfSSL */ + if ((ret = wolfSSL_Init()) != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: Failed to initialize the library\n"); + goto exit; + } + + /* Create and initialize WOLFSSL_CTX */ + if ((ctx = wolfSSL_CTX_new(wolfTLSv1_3_client_method())) == NULL) { + fprintf(stderr, "ERROR: failed to create WOLFSSL_CTX\n"); + ret = -1; goto exit; + } + + /* Load client certificate into WOLFSSL_CTX */ + if ((ret = wolfSSL_CTX_use_certificate_file(ctx, CERT_FILE, WOLFSSL_FILETYPE_PEM)) + != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to load %s, please check the file.\n", + CERT_FILE); + goto exit; + } + + /* Load client key into WOLFSSL_CTX */ + if ((ret = wolfSSL_CTX_use_PrivateKey_file(ctx, KEY_FILE, WOLFSSL_FILETYPE_PEM)) + != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to load %s, please check the file.\n", + KEY_FILE); + goto exit; + } + + /* Load CA certificate into WOLFSSL_CTX */ + if ((ret = wolfSSL_CTX_load_verify_locations(ctx, CA_FILE, NULL)) + != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to load %s, please check the file.\n", + CA_FILE); + goto exit; + } + + /* Create a WOLFSSL object */ + if ((ssl = wolfSSL_new(ctx)) == NULL) { + fprintf(stderr, "ERROR: failed to create WOLFSSL object\n"); + ret = -1; goto exit; + } + + /* Attach wolfSSL to the socket */ + if ((ret = wolfSSL_set_fd(ssl, sockfd)) != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: Failed to set the file descriptor\n"); + goto exit; + } + +#ifdef HAVE_SECRET_CALLBACK + /* required for getting random used */ + wolfSSL_KeepArrays(ssl); + + /* optional logging for wireshark */ + wolfSSL_set_tls13_secret_cb(ssl, Tls13SecretCallback, + (void*)WOLFSSL_SSLKEYLOGFILE_OUTPUT); +#endif + + /* Connect to wolfSSL on the server side */ + if ((ret = wolfSSL_connect(ssl)) != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to connect to wolfSSL\n"); + goto exit; + } + +#ifdef HAVE_SECRET_CALLBACK + wolfSSL_FreeArrays(ssl); +#endif + + /* Get a message for the server from stdin */ + printf("Message for server: "); + memset(buff, 0, sizeof(buff)); + if (fgets(buff, sizeof(buff), stdin) == NULL) { + fprintf(stderr, "ERROR: failed to get message for server\n"); + ret = -1; goto exit; + } + len = strnlen(buff, sizeof(buff)); + + /* Send the message to the server */ + if ((ret = wolfSSL_write(ssl, buff, len)) != (int)len) { + fprintf(stderr, "ERROR: failed to write entire message\n"); + fprintf(stderr, "%d bytes of %d bytes were sent", ret, (int) len); + goto exit; + } + + /* Read the server data into our buff array */ + memset(buff, 0, sizeof(buff)); + if ((ret = wolfSSL_read(ssl, buff, sizeof(buff)-1)) < 0) { + fprintf(stderr, "ERROR: failed to read\n"); + goto exit; + } + + /* Print to stdout any data the server sends */ + printf("Server: %s\n", buff); + + /* Return reporting a success */ + ret = 0; + +exit: + /* Cleanup and return */ + if (sockfd != SOCKET_INVALID) + close(sockfd); /* Close the connection to the server */ + if (ssl) + wolfSSL_free(ssl); /* Free the wolfSSL object */ + if (ctx) + wolfSSL_CTX_free(ctx); /* Free the wolfSSL context object */ + wolfSSL_Cleanup(); /* Cleanup the wolfSSL environment */ +#else + printf("Example requires TLS v1.3\n"); +#endif + (void)argc; + (void)argv; + + return ret; +} diff --git a/wrapper/Ada/c_tls_server_main.c b/wrapper/Ada/c_tls_server_main.c new file mode 100644 index 0000000000..7b7c74a9e2 --- /dev/null +++ b/wrapper/Ada/c_tls_server_main.c @@ -0,0 +1,361 @@ +/* c_tls_server_main.c + * + * Copyright (C) 2006-2023 wolfSSL Inc. + * + * This file is part of wolfSSL. (formerly known as CyaSSL) + * + * 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-1301, USA + */ + +#include + + +/* the usual suspects */ +#include +#include +#include + +/* socket includes */ +#include +#include +#include +#include + +#define HAVE_SIGNAL +#ifdef HAVE_SIGNAL +#include /* signal */ +#endif + +/* wolfSSL */ +#ifndef WOLFSSL_USER_SETTINGS + #include +#endif +#include +#include +#include + +#define DEFAULT_PORT 11111 + +#define CERT_FILE "../certs/server-cert.pem" +#define KEY_FILE "../certs/server-key.pem" +#define CA_FILE "../certs/client-cert.pem" + + +#if defined(WOLFSSL_TLS13) && defined(HAVE_SECRET_CALLBACK) + +#ifndef WOLFSSL_SSLKEYLOGFILE_OUTPUT + #define WOLFSSL_SSLKEYLOGFILE_OUTPUT "sslkeylog.log" +#endif + +/* Callback function for TLS v1.3 secrets for use with Wireshark */ +static int Tls13SecretCallback(WOLFSSL* ssl, int id, const unsigned char* secret, + int secretSz, void* ctx) +{ + int i; + const char* str = NULL; + unsigned char serverRandom[32]; + int serverRandomSz; + XFILE fp = stderr; + if (ctx) { + fp = XFOPEN((const char*)ctx, "ab"); + if (fp == XBADFILE) { + return BAD_FUNC_ARG; + } + } + + serverRandomSz = (int)wolfSSL_get_server_random(ssl, serverRandom, + sizeof(serverRandom)); + + if (serverRandomSz <= 0) { + printf("Error getting server random %d\n", serverRandomSz); + } + +#if 0 + printf("TLS Server Secret CB: Rand %d, Secret %d\n", + serverRandomSz, secretSz); +#endif + + switch (id) { + case CLIENT_EARLY_TRAFFIC_SECRET: + str = "CLIENT_EARLY_TRAFFIC_SECRET"; break; + case EARLY_EXPORTER_SECRET: + str = "EARLY_EXPORTER_SECRET"; break; + case CLIENT_HANDSHAKE_TRAFFIC_SECRET: + str = "CLIENT_HANDSHAKE_TRAFFIC_SECRET"; break; + case SERVER_HANDSHAKE_TRAFFIC_SECRET: + str = "SERVER_HANDSHAKE_TRAFFIC_SECRET"; break; + case CLIENT_TRAFFIC_SECRET: + str = "CLIENT_TRAFFIC_SECRET_0"; break; + case SERVER_TRAFFIC_SECRET: + str = "SERVER_TRAFFIC_SECRET_0"; break; + case EXPORTER_SECRET: + str = "EXPORTER_SECRET"; break; + } + + fprintf(fp, "%s ", str); + for (i = 0; i < (int)serverRandomSz; i++) { + fprintf(fp, "%02x", serverRandom[i]); + } + fprintf(fp, " "); + for (i = 0; i < secretSz; i++) { + fprintf(fp, "%02x", secret[i]); + } + fprintf(fp, "\n"); + + if (fp != stderr) { + XFCLOSE(fp); + } + + return 0; +} +#endif /* WOLFSSL_TLS13 && HAVE_SECRET_CALLBACK */ + +static int mSockfd = SOCKET_INVALID; +static int mConnd = SOCKET_INVALID; +static int mShutdown = 0; + +#ifdef HAVE_SIGNAL +static void sig_handler(const int sig) +{ + fprintf(stderr, "SIGINT handled = %d.\n", sig); + + mShutdown = 1; + if (mConnd != SOCKET_INVALID) { + close(mConnd); /* Close the connection to the client */ + mConnd = SOCKET_INVALID; + } + if (mSockfd != SOCKET_INVALID) { + close(mSockfd); /* Close the socket listening for clients */ + mSockfd = SOCKET_INVALID; + } +} +#endif + + +// To execute the application: ./main +int main(int argc, char** argv) +{ + int ret = 0; +#ifdef WOLFSSL_TLS13 + struct sockaddr_in servAddr; + struct sockaddr_in clientAddr; + socklen_t size = sizeof(clientAddr); + char buff[256]; + size_t len; + const char* reply = "I hear ya fa shizzle!\n"; + int on; + + /* declare wolfSSL objects */ + WOLFSSL_CTX* ctx = NULL; + WOLFSSL* ssl = NULL; + +#ifdef HAVE_SIGNAL + signal(SIGINT, sig_handler); +#endif + + /* Initialize the server address struct with zeros */ + memset(&servAddr, 0, sizeof(servAddr)); + + /* Fill in the server address */ + servAddr.sin_family = AF_INET; /* using IPv4 */ + servAddr.sin_port = htons(DEFAULT_PORT); /* on DEFAULT_PORT */ + servAddr.sin_addr.s_addr = INADDR_ANY; /* from anywhere */ + + + /* Create a socket that uses an internet IPv4 address, + * Sets the socket to be stream based (TCP), + * 0 means choose the default protocol. */ + if ((mSockfd = socket(AF_INET, SOCK_STREAM, 0)) == -1) { + fprintf(stderr, "ERROR: failed to create the socket\n"); + goto exit; + } + + /* make sure server is setup for reuse addr/port */ + on = 1; + setsockopt(mSockfd, SOL_SOCKET, SO_REUSEADDR, + (char*)&on, (socklen_t)sizeof(on)); +#ifdef SO_REUSEPORT + setsockopt(mSockfd, SOL_SOCKET, SO_REUSEPORT, + (char*)&on, (socklen_t)sizeof(on)); +#endif + + /* Bind the server socket to our port */ + if (bind(mSockfd, (struct sockaddr*)&servAddr, sizeof(servAddr)) == -1) { + fprintf(stderr, "ERROR: failed to bind\n"); + goto exit; + } + + /* Listen for a new connection, allow 5 pending connections */ + if (listen(mSockfd, 5) == -1) { + fprintf(stderr, "ERROR: failed to listen\n"); + goto exit; + } + + /*---------------------------------*/ + /* Start of wolfSSL initialization and configuration */ + /*---------------------------------*/ +#if 0 + wolfSSL_Debugging_ON(); +#endif + + /* Initialize wolfSSL */ + if ((ret = wolfSSL_Init()) != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: Failed to initialize the library\n"); + goto exit; + } + + /* Create and initialize WOLFSSL_CTX */ + if ((ctx = wolfSSL_CTX_new(wolfTLSv1_3_server_method())) == NULL) { + fprintf(stderr, "ERROR: failed to create WOLFSSL_CTX\n"); + ret = -1; + goto exit; + } + + /* Require mutual authentication */ + wolfSSL_CTX_set_verify(ctx, + WOLFSSL_VERIFY_PEER | WOLFSSL_VERIFY_FAIL_IF_NO_PEER_CERT, NULL); + + /* Load server certificates into WOLFSSL_CTX */ + if ((ret = wolfSSL_CTX_use_certificate_file(ctx, CERT_FILE, + WOLFSSL_FILETYPE_PEM)) != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to load %s, please check the file.\n", + CERT_FILE); + goto exit; + } + + /* Load server key into WOLFSSL_CTX */ + if ((ret = wolfSSL_CTX_use_PrivateKey_file(ctx, KEY_FILE, + WOLFSSL_FILETYPE_PEM)) != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to load %s, please check the file.\n", + KEY_FILE); + goto exit; + } + + /* Load client certificate as "trusted" into WOLFSSL_CTX */ + if ((ret = wolfSSL_CTX_load_verify_locations(ctx, CA_FILE, NULL)) + != WOLFSSL_SUCCESS) { + fprintf(stderr, "ERROR: failed to load %s, please check the file.\n", + CA_FILE); + goto exit; + } + + /* Continue to accept clients until mShutdown is issued */ + while (!mShutdown) { + printf("Waiting for a connection...\n"); + + /* Accept client connections */ + if ((mConnd = accept(mSockfd, (struct sockaddr*)&clientAddr, &size)) + == -1) { + fprintf(stderr, "ERROR: failed to accept the connection\n\n"); + ret = -1; goto exit; + } + + /* Create a WOLFSSL object */ + if ((ssl = wolfSSL_new(ctx)) == NULL) { + fprintf(stderr, "ERROR: failed to create WOLFSSL object\n"); + ret = -1; goto exit; + } + + /* Attach wolfSSL to the socket */ + wolfSSL_set_fd(ssl, mConnd); + + #ifdef HAVE_SECRET_CALLBACK + /* required for getting random used */ + wolfSSL_KeepArrays(ssl); + + /* optional logging for wireshark */ + wolfSSL_set_tls13_secret_cb(ssl, Tls13SecretCallback, + (void*)WOLFSSL_SSLKEYLOGFILE_OUTPUT); + #endif + + /* Establish TLS connection */ + if ((ret = wolfSSL_accept(ssl)) != WOLFSSL_SUCCESS) { + fprintf(stderr, "wolfSSL_accept error = %d\n", + wolfSSL_get_error(ssl, ret)); + goto exit; + } + + printf("Client connected successfully\n"); + + #ifdef HAVE_SECRET_CALLBACK + wolfSSL_FreeArrays(ssl); + #endif + + /* Read the client data into our buff array */ + memset(buff, 0, sizeof(buff)); + if ((ret = wolfSSL_read(ssl, buff, sizeof(buff)-1)) < 0) { + fprintf(stderr, "ERROR: failed to read\n"); + goto exit; + } + + /* Print to stdout any data the client sends */ + printf("Client: %s\n", buff); + + /* Check for server shutdown command */ + if (strncmp(buff, "shutdown", 8) == 0) { + printf("Shutdown command issued!\n"); + mShutdown = 1; + } + + /* Write our reply into buff */ + memset(buff, 0, sizeof(buff)); + memcpy(buff, reply, strlen(reply)); + len = strnlen(buff, sizeof(buff)); + + /* Reply back to the client */ + if ((ret = wolfSSL_write(ssl, buff, len)) != (int)len) { + fprintf(stderr, "ERROR: failed to write\n"); + goto exit; + } + + /* Cleanup after this connection */ + wolfSSL_shutdown(ssl); + if (ssl) { + wolfSSL_free(ssl); /* Free the wolfSSL object */ + ssl = NULL; + } + if (mConnd != SOCKET_INVALID) { + close(mConnd); /* Close the connection to the client */ + mConnd = SOCKET_INVALID; + } + } + + printf("Shutdown complete\n"); + +exit: + /* Cleanup and return */ + if (ssl) + wolfSSL_free(ssl); /* Free the wolfSSL object */ + if (mConnd != SOCKET_INVALID) { + close(mConnd); /* Close the connection to the client */ + mConnd = SOCKET_INVALID; + } + if (mSockfd != SOCKET_INVALID) { + close(mSockfd); /* Close the socket listening for clients */ + mSockfd = SOCKET_INVALID; + } + if (ctx) + wolfSSL_CTX_free(ctx); /* Free the wolfSSL context object */ + wolfSSL_Cleanup(); /* Cleanup the wolfSSL environment */ + +#else + printf("Example requires TLS v1.3\n"); +#endif /* WOLFSSL_TLS13 */ + + (void)argc; + (void)argv; + + return ret; +} diff --git a/wrapper/Ada/default.gpr b/wrapper/Ada/default.gpr new file mode 100644 index 0000000000..3350eaa5c4 --- /dev/null +++ b/wrapper/Ada/default.gpr @@ -0,0 +1,69 @@ +project Default is + for Languages use ("C", "Ada"); + + for Source_Dirs use (".", + "../../", + "../../src", + "../../wolfcrypt/src"); + + for Object_Dir use "obj"; + + for Main use ("c_tls_client_main.c", + "c_tls_server_main.c", + "tls_server_main.adb"); + + 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", + "-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"); + end Compiler; + + package Linker is + for Switches ("C") use + ("-lm"); -- To include the math library (used by WolfSSL). + + for Switches ("Ada") use + ("-lm"); -- To include the math library (used by WolfSSL). + end Linker; + +end Default; diff --git a/wrapper/Ada/gnat.adc b/wrapper/Ada/gnat.adc new file mode 100644 index 0000000000..e479c000bb --- /dev/null +++ b/wrapper/Ada/gnat.adc @@ -0,0 +1 @@ +pragma Restrictions (No_Secondary_Stack); diff --git a/wrapper/Ada/include.am b/wrapper/Ada/include.am new file mode 100644 index 0000000000..7ef6f51c71 --- /dev/null +++ b/wrapper/Ada/include.am @@ -0,0 +1,19 @@ +# vim:ft=automake +# included from Top Level Makefile.am +# All paths should be given relative to the root + +EXTRA_DIST+= wrapper/Ada/README.md +EXTRA_DIST+= wrapper/Ada/default.gpr +EXTRA_DIST+= wrapper/Ada/gnat.adc +EXTRA_DIST+= wrapper/Ada/ada_binding.c +EXTRA_DIST+= wrapper/Ada/c_tls_client_main.c +EXTRA_DIST+= wrapper/Ada/c_tls_server_main.c +EXTRA_DIST+= wrapper/Ada/tls_client_main.adb +EXTRA_DIST+= wrapper/Ada/tls_client.adb +EXTRA_DIST+= wrapper/Ada/tls_client.ads +EXTRA_DIST+= wrapper/Ada/tls_server_main.adb +EXTRA_DIST+= wrapper/Ada/tls_server.adb +EXTRA_DIST+= wrapper/Ada/tls_server.ads +EXTRA_DIST+= wrapper/Ada/user_settings.h +EXTRA_DIST+= wrapper/Ada/wolfssl.adb +EXTRA_DIST+= wrapper/Ada/wolfssl.ads diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb new file mode 100644 index 0000000000..a1ade1afc0 --- /dev/null +++ b/wrapper/Ada/tls_client.adb @@ -0,0 +1,81 @@ +-- Ada Standard Library packages. +with Ada.Characters.Handling; +with Ada.Command_Line; +with Ada.Strings.Bounded; +with Ada.Text_IO.Bounded_IO; + +-- GNAT Library packages. +with GNAT.Sockets; + +-- The WolfSSL package. +with WolfSSL; + +package body Tls_Client is + + use type WolfSSL.Mode_Type; + use type WolfSSL.Byte_Index; + use type WolfSSL.Byte_Array; + + use all type WolfSSL.Subprogram_Result; + + package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); + use all type Messages.Bounded_String; + + package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); + + procedure Put_Line (Text : String) is + begin + Ada.Text_IO.Put_Line (Text); + end Put_Line; + + procedure Put_Line (Text : Messages.Bounded_String) is + begin + Messages_IO.Put_Line (Text); + end Put_Line; + + subtype Exit_Status is Ada.Command_Line.Exit_Status; + + Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; + Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + + procedure Set (Status : Exit_Status) is + begin + Ada.Command_Line.Set_Exit_Status (Status); + end Set; + + subtype Port_Type is GNAT.Sockets.Port_Type; + + subtype Level_Type is GNAT.Sockets.Level_Type; + + subtype Socket_Type is GNAT.Sockets.Socket_Type; + subtype Option_Name is GNAT.Sockets.Option_Name; + subtype Option_Type is GNAT.Sockets.Option_Type; + subtype Family_Type is GNAT.Sockets.Family_Type; + + subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + + Socket_Error : exception renames GNAT.Sockets.Socket_Error; + + Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + + Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + + Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + + Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + + CERT_FILE : constant String := "../certs/server-cert.pem"; + KEY_FILE : constant String := "../certs/server-key.pem"; + CA_FILE : constant String := "../certs/client-cert.pem"; + + subtype Byte_Array is WolfSSL.Byte_Array; + + procedure Run is + A : Sock_Addr_Type; + C : Socket_Type; -- Client socket. + begin + null; -- work in progress. + end Run; + +end Tls_Client; diff --git a/wrapper/Ada/tls_client.ads b/wrapper/Ada/tls_client.ads new file mode 100644 index 0000000000..9ff912b03f --- /dev/null +++ b/wrapper/Ada/tls_client.ads @@ -0,0 +1,5 @@ +package Tls_Client is + + procedure Run; + +end Tls_Client; diff --git a/wrapper/Ada/tls_client_main.adb b/wrapper/Ada/tls_client_main.adb new file mode 100644 index 0000000000..41e14a4d9a --- /dev/null +++ b/wrapper/Ada/tls_client_main.adb @@ -0,0 +1,8 @@ +with Tls_Client; pragma Elaborate_All (Tls_Client); + +-- Application entry point for the Ada translation of the +-- tls client v1.3 example in C. +procedure Tls_Client_Main is +begin + Tls_Client.Run; +end Tls_Client_Main; diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb new file mode 100644 index 0000000000..2b907fb1d3 --- /dev/null +++ b/wrapper/Ada/tls_server.adb @@ -0,0 +1,240 @@ +-- Ada Standard Library packages. +with Ada.Characters.Handling; +with Ada.Command_Line; +with Ada.Strings.Bounded; +with Ada.Text_IO.Bounded_IO; + +-- GNAT Library packages. +with GNAT.Sockets; + +-- The WolfSSL package. +with WolfSSL; + +package body Tls_Server is + + use type WolfSSL.Mode_Type; + use type WolfSSL.Byte_Index; + use type WolfSSL.Byte_Array; + + use all type WolfSSL.Subprogram_Result; + + package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); + use all type Messages.Bounded_String; + + package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); + + procedure Put_Line (Text : String) is + begin + Ada.Text_IO.Put_Line (Text); + end Put_Line; + + procedure Put_Line (Text : Messages.Bounded_String) is + begin + Messages_IO.Put_Line (Text); + end Put_Line; + + subtype Exit_Status is Ada.Command_Line.Exit_Status; + + Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; + Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + + procedure Set (Status : Exit_Status) is + begin + Ada.Command_Line.Set_Exit_Status (Status); + end Set; + + subtype Port_Type is GNAT.Sockets.Port_Type; + + subtype Level_Type is GNAT.Sockets.Level_Type; + + subtype Socket_Type is GNAT.Sockets.Socket_Type; + subtype Option_Name is GNAT.Sockets.Option_Name; + subtype Option_Type is GNAT.Sockets.Option_Type; + subtype Family_Type is GNAT.Sockets.Family_Type; + + subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + + Socket_Error : exception renames GNAT.Sockets.Socket_Error; + + Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + + Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + + Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + + Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + + CERT_FILE : constant String := "../certs/server-cert.pem"; + KEY_FILE : constant String := "../certs/server-key.pem"; + CA_FILE : constant String := "../certs/client-cert.pem"; + + subtype Byte_Array is WolfSSL.Byte_Array; + + Reply : constant Byte_Array := "I hear ya fa shizzle!"; + + procedure Run is + A : Sock_Addr_Type; + L : Socket_Type; -- Listener socket. + C : Socket_Type; -- Client socket. + P : constant Port_Type := 11111; + + Ch : Character; + + Ssl : WolfSSL.Optional_WolfSSL; + + Ctx : WolfSSL.Optional_Context; + Result : WolfSSL.Subprogram_Result; + M : Messages.Bounded_String; + Shall_Continue : Boolean := True; + + Bytes_Written : Integer; + + Input : WolfSSL.Read_Result; + begin + GNAT.Sockets.Create_Socket (Socket => L); + GNAT.Sockets.Set_Socket_Option (Socket => L, + Level => Socket_Level, + Option => (Name => Reuse_Address, + Enabled => True)); + GNAT.Sockets.Bind_Socket (Socket => L, + Address => (Family => Family_Inet, + Addr => Any_Inet_Addr, + Port => P)); + GNAT.Sockets.Listen_Socket (Socket => L, + Length => 5); + + -- Create and initialize WOLFSSL_CTX. + WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Server_Method, + Context => Ctx); + if not Ctx.Exists then + Put_Line ("ERROR: failed to create WOLFSSL_CTX."); + Set (Exit_Status_Failure); + return; + end if; + + -- Require mutual authentication. + WolfSSL.Set_Verify + (Context => Ctx.Instance, + Mode => WolfSSL.Verify_Peer & WolfSSL.Verify_Fail_If_No_Peer_Cert); + + -- Load server certificates into WOLFSSL_CTX. + Result := WolfSSL.Use_Certificate_File (Context => Ctx.Instance, + File => CERT_FILE, + Format => WolfSSL.Format_Pem); + if Result = Failure then + M := Messages.To_Bounded_String ("ERROR: failed to load "); + Messages.Append (M, CERT_FILE); + Messages.Append (M, ", please check the file."); + Put_Line (M); + Set (Exit_Status_Failure); + return; + end if; + + -- Load server key into WOLFSSL_CTX. + Result := WolfSSL.Use_Private_Key_File (Context => Ctx.Instance, + File => KEY_FILE, + Format => WolfSSL.Format_Pem); + if Result = Failure then + M := Messages.To_Bounded_String ("ERROR: failed to load "); + Messages.Append (M, KEY_FILE); + Messages.Append (M, ", please check the file."); + Put_Line (M); + Set (Exit_Status_Failure); + return; + end if; + + Put_Line ("success to here at least"); + + -- Load client certificate as "trusted" into WOLFSSL_CTX. + Result := WolfSSL.Load_Verify_Locations (Context => Ctx.Instance, + File => CA_FILE, + Path => ""); + if Result = Failure then + M := Messages.To_Bounded_String ("ERROR: failed to load "); + Messages.Append (M, CA_FILE); + Messages.Append (M, ", please check the file."); + Put_Line (M); + Set (Exit_Status_Failure); + return; + end if; + + while Shall_Continue loop + Put_Line ("Waiting for a connection..."); + begin + GNAT.Sockets.Accept_Socket (Server => L, + Socket => C, + Address => A); + exception + when Socket_Error => + Shall_Continue := False; + Put_Line ("ERROR: failed to accept the connection."); + end; + + -- Create a WOLFSSL object. + WolfSSL.Create_WolfSSL (Context => Ctx.Instance, Ssl => Ssl); + if not Ssl.Exists then + Put_Line ("ERROR: failed to create WOLFSSL object."); + Set (Exit_Status_Failure); + return; + end if; + + -- Attach wolfSSL to the socket. + Result := WolfSSL.Attach (Ssl => Ssl.Instance, + Socket => GNAT.Sockets.To_C (C)); + -- Establish TLS connection. + Result := WolfSSL.Accept_Connection (Ssl.Instance); + if Result = Failure then + Put_Line ("Accept error."); + Set (Exit_Status_Failure); + return; + end if; + + Put_Line ("Client connected successfully."); + + Input := WolfSSL.Read (Ssl.Instance); + + if Input.Result /= Success then + Put_Line ("Read error."); + Set (Exit_Status_Failure); + return; + end if; + + -- Print to stdout any data the client sends. + M := Messages.To_Bounded_String (""); + for I in Input.Buffer'Range loop + Ch := Character (Input.Buffer (I)); + if Ada.Characters.Handling.Is_Graphic (Ch) then + Messages.Append (M, Ch); + else + null; + -- Ignore the "newline" characters at end of message. + end if; + end loop; + Put_Line (M); + + -- Check for server shutdown command. + if Input.Last >= 8 then + if Input.Buffer (1 .. 8) = "shutdown" then + Put_Line ("Shutdown command issued!"); + Shall_Continue := False; + end if; + end if; + + Bytes_Written := WolfSSL.Write (Ssl.Instance, Reply); + if Bytes_Written /= Reply'Length then + Put_Line ("ERROR: failed to write."); + end if; + + Result := WolfSSL.Shutdown (Ssl.Instance); + WolfSSL.Free (Ssl); + GNAT.Sockets.Close_Socket (C); + + Put_Line ("Shutdown complete."); + end loop; + GNAT.Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + WolfSSL.Finalize; + end Run; + +end Tls_Server; diff --git a/wrapper/Ada/tls_server.ads b/wrapper/Ada/tls_server.ads new file mode 100644 index 0000000000..b32e974953 --- /dev/null +++ b/wrapper/Ada/tls_server.ads @@ -0,0 +1,5 @@ +package Tls_Server is + + procedure Run; + +end Tls_Server; diff --git a/wrapper/Ada/tls_server_main.adb b/wrapper/Ada/tls_server_main.adb new file mode 100644 index 0000000000..8dc6a3a5a7 --- /dev/null +++ b/wrapper/Ada/tls_server_main.adb @@ -0,0 +1,8 @@ +with Tls_Server; pragma Elaborate_All (Tls_Server); + +-- Application entry point for the Ada translation of the +-- tls server v1.3 example in C. +procedure Tls_Server_Main is +begin + Tls_Server.Run; +end Tls_Server_Main; diff --git a/wrapper/Ada/user_settings.h b/wrapper/Ada/user_settings.h new file mode 100644 index 0000000000..f77e8d480d --- /dev/null +++ b/wrapper/Ada/user_settings.h @@ -0,0 +1,385 @@ +/* user_settings.h + * + * 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 + */ + + +/* should be renamed to user_settings.h for customer use + * generated from configure options ./configure --enable-all + * + * Cleaned up by David Garske + */ + +#ifndef WOLFSSL_USER_SETTINGS_H +#define WOLFSSL_USER_SETTINGS_H + + +#ifdef __cplusplus +extern "C" { +#endif + +/* Usually comes from configure -> config.h */ +#define HAVE_SYS_TIME_H + +/* Features */ +#define SINGLE_THREADED +#define WOLFSSL_IGNORE_FILE_WARN /* Ignore *.c include warnings */ +#define WOLFSSL_PUBLIC_MP /* Make math API's public */ +#define WOLFSSL_ENCRYPTED_KEYS /* Support for encrypted keys PKCS8 */ +#define WOLFSSL_SYS_CA_CERTS /* Enable ability to load CA certs from OS */ + +#if 0 /* Not needed */ + #define KEEP_PEER_CERT /* Retain peer's certificate */ + #define KEEP_OUR_CERT /* Keep our certificate */ + #define WOLFSSL_ALWAYS_VERIFY_CB /* Always call verify callback (configured via wolfSSL_CTX_set_verify API) */ + #define WOLFSSL_VERIFY_CB_ALL_CERTS /* Call verify callback for all intermediate certs */ + #define WOLFSSL_ALWAYS_KEEP_SNI + #define WOLFSSL_EXTRA_ALERTS /* Allow sending other TLS alerts */ + #define HAVE_EX_DATA /* Enable "extra" EX data API's for user information in CTX/WOLFSSL */ + #define HAVE_EXT_CACHE + #define ATOMIC_USER /* Enable Atomic Record Layer callbacks */ + #define HAVE_PK_CALLBACKS /* Enable public key callbacks */ + #define WOLFSSL_ALT_NAMES /* Allow alternate cert chain validation to any trusted cert (not entire chain presented by peer) */ + #define HAVE_NULL_CIPHER /* Enable use of TLS cipher suites without cipher (clear text / no encryption) */ + #define WOLFSSL_HAVE_CERT_SERVICE + #define WOLFSSL_JNI + #define WOLFSSL_SEP /* certificate policy set extension */ + #define WOLFCRYPT_HAVE_SRP + #define WOLFSSL_HAVE_WOLFSCEP + #define HAVE_PKCS7 + #define WOLFSSL_SIGNER_DER_CERT + #define WOLFSSL_TRUST_PEER_CERT + #define WOLFSSL_WOLFSSH + #define WC_NO_ASYNC_THREADING +#endif + +/* TLS Features */ +#define WOLFSSL_TLS13 +#define WOLFSSL_EITHER_SIDE /* allow generic server/client method for WOLFSSL_CTX new */ +#define WOLFSSL_TLS13_NO_PEEK_HANDSHAKE_DONE + +/* DTLS */ +#if 0 + #define WOLFSSL_DTLS + #define WOLFSSL_MULTICAST + + /* DTLS v1.3 is not yet included with enable-all */ + //#define WOLFSSL_DTLS13 +#endif + +/* DG Disabled SSLv3 and TLSv1.0 - should avoid using */ +//#define WOLFSSL_ALLOW_SSLV3 +//#define WOLFSSL_ALLOW_TLSV10 + +/* TLS Extensions */ +#define HAVE_TLS_EXTENSIONS +#define HAVE_SUPPORTED_CURVES +#define HAVE_ONE_TIME_AUTH +#define HAVE_SNI +#define HAVE_ALPN +#define HAVE_MAX_FRAGMENT +#define HAVE_TRUNCATED_HMAC +#define HAVE_SESSION_TICKET +#define WOLFSSL_TICKET_HAVE_ID +#define WOLFSSL_FORCE_CACHE_ON_TICKET +#define HAVE_EXTENDED_MASTER +#define HAVE_TRUSTED_CA +#define HAVE_ENCRYPT_THEN_MAC +#define WOLFSSL_POST_HANDSHAKE_AUTH +#define WOLFSSL_SEND_HRR_COOKIE /* Used by DTLS v1.3 */ +#define HAVE_ANON /* anon cipher suites */ +#define HAVE_FALLBACK_SCSV /* TLS_FALLBACK_SCSV */ +#define WOLFSSL_EARLY_DATA +#define HAVE_SERVER_RENEGOTIATION_INFO + +/* TLS Session Cache */ +#define SESSION_CERTS +#define PERSIST_SESSION_CACHE +#define PERSIST_CERT_CACHE + +/* Key and Certificate Generation */ +#define WOLFSSL_KEY_GEN +#define WOLFSSL_CERT_GEN +#define WOLFSSL_CERT_REQ +#define WOLFSSL_CERT_EXT +#define WOLFSSL_MULTI_ATTRIB +#define HAVE_SMIME +#define WOLFSSL_DER_LOAD +#define ASN_BER_TO_DER /* BER to DER support */ +#define WOLFSSL_HAVE_ISSUER_NAMES /* Store pointers to issuer name components and their lengths and encodings */ +#define WOLFSSL_SUBJ_DIR_ATTR /* Enable support for SubjectDirectoryAttributes extension */ +#define WOLFSSL_SUBJ_INFO_ACC /* Enable support for SubjectInfoAccess extension */ +#define WOLFSSL_CERT_NAME_ALL /* Adds more certificate name capability at the cost of taking up more memory. Adds initials, givenname, dnQualifer for example */ +#define WOLFSSL_FPKI /* Enable support for FPKI (Federal PKI) extensions */ +#define WOLFSSL_AKID_NAME /* Enable support for full AuthorityKeyIdentifier extension. Only supports copying full AKID from an existing certificate */ +#define HAVE_CTS /* Ciphertext stealing interface */ +#define WOLFSSL_PEM_TO_DER +#define WOLFSSL_DER_TO_PEM +#define WOLFSSL_CUSTOM_OID +#define HAVE_OID_ENCODING +#define WOLFSSL_ASN_TEMPLATE + +/* Certificate Revocation */ +#define HAVE_OCSP +#define HAVE_CERTIFICATE_STATUS_REQUEST +#define HAVE_CERTIFICATE_STATUS_REQUEST_V2 +#define HAVE_CRL +#define HAVE_CRL_IO +#define HAVE_IO_TIMEOUT +//#define HAVE_CRL_MONITOR /* DG Disabled (Monitors CRL files on filesystem) - not portable feature */ + + +#if 1 + /* sp_int.c */ + #define WOLFSSL_SP_MATH_ALL +#else + /* Fast math key size 4096-bit max */ + #define USE_FAST_MATH +#endif +//#define HAVE___UINT128_T 1 /* DG commented: May not be portable */ + +/* Max Sizes */ +#define RSA_MAX_SIZE 4096 +#define FP_MAX_BITS 8192 +#define SP_INT_BITS 4096 + + +/* Timing Resistance */ +#define TFM_TIMING_RESISTANT +#define ECC_TIMING_RESISTANT +#define WC_RSA_BLINDING + +/* DH Key Sizes */ +#define HAVE_FFDHE_2048 +#define HAVE_FFDHE_3072 +#define WOLFSSL_DH_EXTRA /* Enable additional DH key import/export */ +#define HAVE_DH_DEFAULT_PARAMS + +/* ECC Features */ +#define HAVE_ECC +#define TFM_ECC256 +#define ECC_SHAMIR +#define WOLFSSL_CUSTOM_CURVES /* enable other curves (not just prime) */ +#define HAVE_ECC_SECPR2 +#define HAVE_ECC_SECPR3 +#define HAVE_ECC_BRAINPOOL +#define HAVE_ECC_KOBLITZ +#define HAVE_ECC_CDH /* Co-factor */ +#define HAVE_COMP_KEY /* Compressed key support */ +#define FP_ECC /* Fixed point caching - speed repeated operations against same key */ +#define HAVE_ECC_ENCRYPT +#define WOLFCRYPT_HAVE_ECCSI +#define WOLFCRYPT_HAVE_SAKKE +#define WOLFSSL_ECDSA_DETERMINISTIC_K_VARIANT + +/* RSA */ +#define WC_RSA_PSS +#define WOLFSSL_PSS_LONG_SALT +#define WC_RSA_NO_PADDING + +/* AES */ +#define HAVE_AES_DECRYPT +#define HAVE_AES_ECB +#define WOLFSSL_AES_DIRECT +#define WOLFSSL_AES_COUNTER +#define HAVE_AESGCM +#define GCM_TABLE_4BIT +#define WOLFSSL_AESGCM_STREAM +#define HAVE_AESCCM +#define WOLFSSL_AES_OFB +#define WOLFSSL_AES_CFB +#define WOLFSSL_AES_XTS +#define HAVE_AES_KEYWRAP +#define WOLFSSL_AES_CBC_LENGTH_CHECKS +#define WOLFSSL_USE_ALIGN +#define WOLFSSL_AES_SIV + +/* Hashing */ +#define WOLFSSL_SHA224 +#define WOLFSSL_SHA512 +#define WOLFSSL_SHA384 +#define WOLFSSL_SHAKE256 +#define WOLFSSL_SHA3 +#define WOLFSSL_HASH_FLAGS /* enable hash flag API's */ +#define WOLFSSL_SHAKE256 + +/* Additional Algorithms */ +#define HAVE_HASHDRBG +#define HAVE_CURVE25519 +#define HAVE_ED25519 +#define WOLFSSL_ED25519_STREAMING_VERIFY +#define CURVED25519_SMALL +#define HAVE_ED448 +#define WOLFSSL_ED448_STREAMING_VERIFY +#define HAVE_CURVE448 +#define HAVE_POLY1305 +#define HAVE_CHACHA +#define HAVE_XCHACHA +#define HAVE_HKDF +#define HAVE_X963_KDF +#define WOLFSSL_CMAC +#define WOLFSSL_DES_ECB +#define HAVE_BLAKE2 +#define HAVE_BLAKE2B +#define HAVE_BLAKE2S +#define WOLFSSL_SIPHASH +#define HAVE_KEYING_MATERIAL +#define WOLFSSL_HAVE_PRF + +/* Encrypted Client Hello */ +#define HAVE_HPKE +#define HAVE_ECH + +/* Non-Standard Algorithms (DG disabled) */ +//#define HAVE_CAMELLIA +//#define WOLFSSL_RIPEMD +//#define HAVE_SCRYPT +//#define WOLFSSL_MD2 +//#define WOLFSSL_ALLOW_RC4 + +/* Encoding */ +#define WOLFSSL_BASE16 +#define WOLFSSL_BASE64_ENCODE + + +/* Openssl compatibility */ +#if 0 /* DG Disabled */ + /* Openssl compatibility API's */ + #define OPENSSL_EXTRA + #define OPENSSL_ALL + #define HAVE_OPENSSL_CMD + #define SSL_TXT_TLSV1_2 + #define SSL_TXT_TLSV1_1 + #define OPENSSL_NO_SSL2 + #define OPENSSL_NO_SSL3 + #define NO_OLD_RNGNAME + #define NO_OLD_WC_NAMES + #define NO_OLD_SSL_NAMES + #define NO_OLD_SHA_NAMES + #define NO_OLD_MD5_NAME + #define OPENSSL_NO_EC /* macro to enable ECC in openssl */ + #define WOLFSSL_VERBOSE_ERRORS + #define ERROR_QUEUE_PER_THREAD + #define WOLFSSL_ERROR_CODE_OPENSSL + #define HAVE_WOLFSSL_SSL_H 1 + #define OPENSSL_COMPATIBLE_DEFAULTS + + /* Openssl compatibility application specific */ + #define WOLFSSL_LIBWEBSOCKETS + #define WOLFSSL_OPENSSH + #define WOLFSSL_QT + #define FORTRESS + #define HAVE_WEBSERVER + #define HAVE_LIGHTY + #define WOLFSSL_NGINX + #define WOLFSSL_HAPROXY + #define HAVE_STUNNEL + #define WOLFSSL_ASIO + #define ASIO_USE_WOLFSSL + #define BOOST_ASIO_USE_WOLFSSL + #define WOLFSSL_OPENVPN + + #define NO_WOLFSSL_STUB +#endif + +/* TLS static cipher support - off by default */ +#if 0 + #define WOLFSSL_STATIC_RSA + #define WOLFSSL_STATIC_DH + #define WOLFSSL_STATIC_PSK +#endif + +/* TLS sniffer support - off by default */ +#if 0 + #define WOLFSSL_STATIC_EPHEMERAL + #define WOLFSSL_SNIFFER +#endif + +/* Deprecated */ +#define NO_DSA +#define NO_MD4 +#define NO_MD5 +#define NO_OLD_TLS + +/* Used to manually test disable edge cases */ +#ifdef TEST_DISABLES + #define NO_SESSION_CACHE + + //#define NO_ECC256 + //#define NO_ECC_KEY_EXPORT + //#define NO_ECC_DHE + //#define NO_ECC_SIGN + //#define NO_ECC_VERIFY + + //#define NO_RSA + #define NO_DH + + #define NO_SHA + #define NO_SHA256 + #ifdef NO_SHA256 + #undef WOLFSSL_SHA224 + #endif + #define NO_SHA512 + #ifdef NO_SHA512 + #undef WOLFSSL_SHA384 + #undef WOLFSSL_SHA512 + #undef HAVE_ED25519 + #endif + + //#define NO_KDF + //#define NO_HMAC + + #define NO_RC4 + #define NO_DES3 + //#define NO_AES + #define NO_AES_CBC + #define WOLFSSL_NO_SHAKE128 + + #define NO_PSK + #define NO_PWDBASED + + //#define WOLFSSL_NO_TLS12 + + //#define NO_64BIT + #define WOLFSSL_SP_NO_MALLOC + #define NO_FILESYSTEM + #define NO_WRITEV + + #define NO_ERROR_STRINGS + //#define NO_WOLFSSL_CLIENT + //#define NO_WOLFSSL_SERVER + + #define NO_MULTIBYTE_PRINT + //#define NO_ASN_TIME + //#define NO_ASN_CRYPT + //#define NO_CODING + #define NO_SIG_WRAPPER + //#define NO_HASH_WRAPPER + //#define WC_NO_HARDEN + + //#define NO_CERTS + //#define NO_ASN +#endif + +#ifdef __cplusplus +} +#endif + + +#endif /* WOLFSSL_USER_SETTINGS_H */ diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb new file mode 100644 index 0000000000..d136f92e19 --- /dev/null +++ b/wrapper/Ada/wolfssl.adb @@ -0,0 +1,597 @@ +with Interfaces.C.Strings; + +package body WolfSSL is + + subtype size_t is Interfaces.C.size_t; use type size_t; + + subtype long is Interfaces.C.long; + + function Get_WolfSSL_Success return int with + Convention => C, + External_Name => "get_wolfssl_success", + Import => True; + + WOLFSSL_SUCCESS : constant int := Get_WolfSSL_Success; + + function Initialize_WolfSSL return int with + Convention => C, + External_Name => "wolfSSL_Init", + Import => True; + + function Finalize_WolfSSL return int with + Convention => C, + External_Name => "wolfSSL_Cleanup", + Import => True; + + procedure Finalize is + Result : constant int := Finalize_WolfSSL; + begin + if Result /= WOLFSSL_SUCCESS then + raise Cleanup_Error; + end if; + end Finalize; + + function WolfTLSv1_2_Server_Method return Method_Type with + Convention => C, + External_Name => "wolfTLSv1_2_server_method", + Import => True; + + function TLSv1_2_Server_Method return Method_Type is + begin + return WolfTLSv1_2_Server_Method; + end TLSv1_2_Server_Method; + + function WolfTLSv1_3_Server_Method return Method_Type with + Convention => C, + External_Name => "wolfTLSv1_3_server_method", + Import => True; + + function TLSv1_3_Server_Method return Method_Type is + begin + return WolfTLSv1_3_Server_Method; + end TLSv1_3_Server_Method; + + function WolfSSL_CTX_new (Method : Method_Type) + return Context_Type with + Convention => C, External_Name => "wolfSSL_CTX_new", Import => True; + + procedure Create_Context (Method : Method_Type; + Context : out Optional_Context) is + C : constant Context_Type := WolfSSL_CTX_new (Method); + begin + if C = null then + Context := (Exists => False); + else + Context := (Exists => True, Instance => C); + end if; + end Create_Context; + + procedure WolfSSL_CTX_free (Context : Context_Type) with + Convention => C, External_Name => "wolfSSL_CTX_free", Import => True; + + procedure Free (Context : in out Optional_Context) is + begin + WolfSSL_CTX_free (Context.Instance); + Context := (Exists => False); + end Free; + + type Opaque_X509_Store_Context is limited null record; + type X509_Store_Context is access Opaque_X509_Store_Context with + Convention => C; + + type Verify_Callback is access function + (A : int; + Context : X509_Store_Context) + return int + with Convention => C; + + procedure WolfSSL_CTX_Set_Verify (Context : Context_Type; + Mode : int; + Callback : Verify_Callback) with + Convention => C, + External_Name => "wolfSSL_CTX_set_verify", + Import => True; + -- This function sets the verification method for remote peers and + -- also allows a verify callback to be registered with the SSL + -- context. The verify callback will be called only when a + -- verification failure has occurred. If no verify callback is + -- desired, the NULL pointer can be used for verify_callback. + -- The verification mode of peer certificates is a logically OR'd + -- list of flags. The possible flag values include: + -- SSL_VERIFY_NONE Client mode: the client will not verify the + -- certificate received from the server and the handshake will + -- continue as normal. Server mode: the server will not send a + -- certificate request to the client. As such, client verification + -- will not be enabled. SSL_VERIFY_PEER Client mode: the client will + -- verify the certificate received from the server during the + -- handshake. This is turned on by default in wolfSSL, therefore, + -- using this option has no effect. Server mode: the server will send + -- a certificate request to the client and verify the client + -- certificate received. SSL_VERIFY_FAIL_IF_NO_PEER_CERT Client mode: + -- no effect when used on the client side. Server mode: + -- the verification will fail on the server side if the client fails + -- to send a certificate when requested to do so (when using + -- SSL_VERIFY_PEER on the SSL server). + -- SSL_VERIFY_FAIL_EXCEPT_PSK Client mode: no effect when used on + -- the client side. Server mode: the verification is the same as + -- SSL_VERIFY_FAIL_IF_NO_PEER_CERT except in the case of a + -- PSK connection. If a PSK connection is being made then the + -- connection will go through without a peer cert. + + function "&" (Left, Right : Mode_Type) return Mode_Type is + L : constant Unsigned_32 := Unsigned_32 (Left); + R : constant Unsigned_32 := Unsigned_32 (Right); + begin + return Mode_Type (L and R); + end "&"; + + procedure Set_Verify (Context : Context_Type; + Mode : Mode_Type) is + begin + WolfSSL_CTX_Set_Verify (Context => Context, + Mode => int (Mode), + Callback => null); + end Set_Verify; + + function Use_Certificate_File (Context : Context_Type; + File : char_array; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_CTX_use_certificate_file", + Import => True; + + function Use_Certificate_File (Context : Context_Type; + File : String; + Format : File_Format) + return Subprogram_Result is + C : size_t; + F : char_array (1 .. File'Length + 1); + Result : int; + begin + Interfaces.C.To_C (Item => File, + Target => F, + Count => C, + Append_Nul => True); + Result := Use_Certificate_File (Context, F (1 .. C), int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Certificate_File; + + function Use_Certificate_Buffer (Context : Context_Type; + Input : char_array; + Size : long; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_CTX_use_certificate_buffer", + Import => True; + + function Use_Certificate_Buffer (Context : Context_Type; + Input : char_array; + Format : File_Format) + return Subprogram_Result is + Result : int; + begin + Result := Use_Certificate_Buffer (Context, Input, + Input'Length, int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Certificate_Buffer; + + function Use_Private_Key_File (Context : Context_Type; + File : char_array; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_CTX_use_PrivateKey_file", + Import => True; + + function Use_Private_Key_File (Context : Context_Type; + File : String; + Format : File_Format) + return Subprogram_Result is + C : size_t; + F : char_array (1 .. File'Length + 1); + Result : int; + begin + Interfaces.C.To_C (Item => File, + Target => F, + Count => C, + Append_Nul => True); + Result := Use_Private_Key_File (Context, F (1 .. C), int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Private_Key_File; + + function Use_Private_Key_Buffer (Context : Context_Type; + Input : char_array; + Size : long; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_CTX_use_PrivateKey_buffer", + Import => True; + + function Use_Private_Key_Buffer (Context : Context_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result is + Result : int; + begin + Result := Use_Private_Key_Buffer (Context, Input, + Input'Length, int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Private_Key_Buffer; + + function Load_Verify_Locations1 + (Context : Context_Type; + File : char_array; + Path : char_array) return int with + Convention => C, + External_Name => "wolfSSL_CTX_load_verify_locations", + Import => True; + -- This function loads PEM-formatted CA certificate files into + -- the SSL context (WOLFSSL_CTX). These certificates will be treated + -- as trusted root certificates and used to verify certs received + -- from peers during the SSL handshake. The root certificate file, + -- provided by the file argument, may be a single certificate or a + -- file containing multiple certificates. If multiple CA certs are + -- included in the same file, wolfSSL will load them in the same order + -- they are presented in the file. The path argument is a pointer to + -- the name of a directory that contains certificates of trusted + -- root CAs. If the value of file is not NULL, path may be specified + -- as NULL if not needed. If path is specified and NO_WOLFSSL_DIR was + -- not defined when building the library, wolfSSL will load all + -- CA certificates located in the given directory. This function will + -- attempt to load all files in the directory. This function expects + -- PEM formatted CERT_TYPE file with header "--BEGIN CERTIFICATE--". + + subtype char_array_ptr is Interfaces.C.Strings.char_array_access; + + function Load_Verify_Locations2 + (Context : Context_Type; + File : char_array; + Path : char_array_ptr) return int with + Convention => C, + External_Name => "wolfSSL_CTX_load_verify_locations", + Import => True; + + function Load_Verify_Locations3 + (Context : Context_Type; + File : char_array_ptr; + Path : char_array) return int with + Convention => C, + External_Name => "wolfSSL_CTX_load_verify_locations", + Import => True; + + function Load_Verify_Locations4 + (Context : Context_Type; + File : char_array_ptr; + Path : char_array_ptr) return int with + Convention => C, + External_Name => "wolfSSL_CTX_load_verify_locations", + Import => True; + + function Load_Verify_Locations (Context : Context_Type; + File : String; + Path : String) + return Subprogram_Result is + FC : size_t; -- File Count, specifies the characters used in F. + F : aliased char_array := (1 .. File'Length + 1 => '#'); + + PC : size_t; -- Path Count, specifies the characters used in P. + P : aliased char_array := (1 .. Path'Length + 1 => '#'); + + Result : int; + begin + if File = "" then + if Path = "" then + Result := Load_Verify_Locations4 (Context, null, null); + else + Interfaces.C.To_C (Item => Path, + Target => P, + Count => PC, + Append_Nul => True); + Result := Load_Verify_Locations3 (Context, null, P); + end if; + else + Interfaces.C.To_C (Item => File, + Target => F, + Count => FC, + Append_Nul => True); + if Path = "" then + Result := Load_Verify_Locations2 (Context, F, null); + else + Interfaces.C.To_C (Item => Path, + Target => P, + Count => PC, + Append_Nul => True); + Interfaces.C.To_C (Item => Path, + Target => P, + Count => PC, + Append_Nul => True); + Result := Load_Verify_Locations1 (Context, F, P); + end if; + end if; + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Load_Verify_Locations; + + function Load_Verify_Buffer1 + (Context : Context_Type; + Input : char_array; + Size : int; + Format : int) return int with + Convention => C, + External_Name => "wolfSSL_CTX_load_verify_buffer", + Import => True; + -- This function loads a CA certificate buffer into the WOLFSSL + -- Context. It behaves like the non-buffered version, only differing + -- in its ability to be called with a buffer as input instead of + -- a file. The buffer is provided by the in argument of size sz. + -- format specifies the format type of the buffer; SSL_FILETYPE_ASN1 + -- or SSL_FILETYPE_PEM. More than one CA certificate may be loaded + -- per buffer as long as the format is in PEM. Please see + -- the examples for proper usage. + + function Load_Verify_Buffer (Context : Context_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result is + Result : int; + begin + Result := Load_Verify_Buffer1 (Context => Context, + Input => Input, + Size => Input'Length, + Format => int(Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Load_Verify_Buffer; + + function WolfSSL_New (Context : Context_Type) + return WolfSSL_Type with + Convention => C, + External_Name => "wolfSSL_new", + Import => True; + + procedure Create_WolfSSL (Context : Context_Type; + Ssl : out Optional_WolfSSL) is + Result : WolfSSL_Type := WolfSSL_New (Context); + begin + if Result /= null then + Ssl := (Exists => True, + Instance => Result); + else + Ssl := (Exists => False); + end if; + end Create_WolfSSL; + + function WolfSSL_Set_Fd (Ssl : WolfSSL_Type; Fd : int) return int with + Convention => C, + External_Name => "wolfSSL_set_fd", + Import => True; + + function Attach (Ssl : WolfSSL_Type; + Socket : Integer) + return Subprogram_Result is + Result : int := WolfSSL_Set_Fd (Ssl, int (Socket)); + begin + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Attach; + + procedure WolfSSL_Keep_Arrays (Ssl : WolfSSL_Type) with + Convention => C, + External_Name => "wolfSSL_KeepArrays", + Import => True; + + procedure Keep_Arrays (Ssl : WolfSSL_Type) is + begin + WolfSSL_Keep_Arrays (Ssl); + end Keep_Arrays; + + function WolfSSL_Accept (Ssl : WolfSSL_Type) return int with + Convention => C, + External_Name => "wolfSSL_accept", + Import => True; + + function Accept_Connection (Ssl : WolfSSL_Type) + return Subprogram_Result is + Result : int := WolfSSL_Accept (Ssl); + begin + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Accept_Connection; + + procedure WolfSSL_Free_Arrays (Ssl : WolfSSL_Type) with + Convention => C, + External_Name => "wolfSSL_FreeArrays", + Import => True; + + procedure Free_Arrays (Ssl : WolfSSL_Type) is + begin + WolfSSL_Free_Arrays (Ssl); + end Free_Arrays; + + function WolfSSL_Read (Ssl : WolfSSL_Type; + Data : out char_array; + Sz : int) return int with + Convention => C, + External_Name => "wolfSSL_read", + Import => True; + -- This function reads sz bytes from the SSL session (ssl) internal + -- read buffer into the buffer data. The bytes read are removed from + -- the internal receive buffer. If necessary wolfSSL_read() will + -- negotiate an SSL/TLS session if the handshake has not already + -- been performed yet by wolfSSL_connect() or wolfSSL_accept(). + -- The SSL/TLS protocol uses SSL records which have a maximum size + -- of 16kB (the max record size can be controlled by the + -- MAX_RECORD_SIZE define in /wolfssl/internal.h). As such, wolfSSL + -- needs to read an entire SSL record internally before it is able + -- to process and decrypt the record. Because of this, a call to + -- wolfSSL_read() will only be able to return the maximum buffer + -- size which has been decrypted at the time of calling. There may + -- be additional not-yet-decrypted data waiting in the internal + -- wolfSSL receive buffer which will be retrieved and decrypted with + -- the next call to wolfSSL_read(). If sz is larger than the number + -- of bytes in the internal read buffer, SSL_read() will return + -- the bytes available in the internal read buffer. If no bytes are + -- buffered in the internal read buffer yet, a call to wolfSSL_read() + -- will trigger processing of the next record. + -- + -- The integer returned is the number of bytes read upon success. + -- 0 will be returned upon failure. This may be caused by a either + -- a clean (close notify alert) shutdown or just that the peer closed + -- the connection. Call wolfSSL_get_error() for the specific + -- error code. SSL_FATAL_ERROR will be returned upon failure when + -- either an error occurred or, when using non-blocking sockets, + -- the SSL_ERROR_WANT_READ or SSL_ERROR_WANT_WRITE error was received + -- and and the application needs to call wolfSSL_read() again. + -- Use wolfSSL_get_error() to get a specific error code. + + function Read (Ssl : WolfSSL_Type) return Read_Result is + Data : char_array (1 .. Byte_Index'Last); + Size : int; + begin + Size := WolfSSL_Read (Ssl, Data, int (Byte_Index'Last)); + if Size < 0 then + return (Result => Failure, Last => 0); + else + return (Result => Success, + Last => Byte_Index (Size), + Buffer => Data (1 .. Byte_Index (Size))); + end if; + end Read; + + function WolfSSL_Write (Ssl : WolfSSL_Type; + Data : char_array; + Sz : int) return int with + Convention => C, + External_Name => "wolfSSL_write", + Import => True; + + function Write (Ssl : WolfSSL_Type; + Data : Byte_Array) return Integer is + Size : constant int := Data'Length; + Result : int; + begin + Result := WolfSSL_Write (Ssl, Data, Size); + return Integer (Result); + end Write; + + function WolfSSL_Shutdown (Ssl : WolfSSL_Type) return int with + Convention => C, + External_Name => "wolfSSL_shutdown", + Import => True; + -- This function shuts down an active SSL/TLS connection using + -- the SSL session, ssl. This function will try to send a + -- "close notify" alert to the peer. The calling application can + -- choose to wait for the peer to send its "close notify" alert + -- in response or just go ahead and shut down the underlying + -- connection after directly calling wolfSSL_shutdown (to save + -- resources). Either option is allowed by the TLS specification. + -- If the underlying connection will be used again in the future, + -- the complete two_directional shutdown procedure must be performed + -- to keep synchronization intact between the peers. + -- wolfSSL_shutdown() works with both blocking and non_blocking I/O. + -- When the underlying I/O is non_blocking, wolfSSL_shutdown() will + -- return an error if the underlying I/O could not satisfy the needs + -- of wolfSSL_shutdown() to continue. In this case, a call to + -- wolfSSL_get_error() will yield either SSL_ERROR_WANT_READ or + -- SSL_ERROR_WANT_WRITE. The calling process must then repeat + -- the call to wolfSSL_shutdown() when the underlying I/O is ready. + + function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result is + Result : constant int := WolfSSL_Shutdown (Ssl); + begin + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Shutdown; + + function WolfSSL_Connect (Ssl : WolfSSL_Type) return int with + Convention => C, + External_Name => "wolfSSL_connect", + Import => True; + -- This function is called on the client side and initiates + -- an SSL/TLS handshake with a server. When this function is called, + -- the underlying communication channel has already been set up. + -- wolfSSL_connect() works with both blocking and non_blocking I/O. + -- When the underlying I/O is non_blocking, wolfSSL_connect() will + -- return when the underlying I/O could not satisfy the needs + -- of wolfSSL_connect to continue the handshake. In this case, + -- a call to wolfSSL_get_error() will yield either + -- SSL_ERROR_WANT_READ or SSL_ERROR_WANT_WRITE. The calling process + -- must then repeat the call to wolfSSL_connect() when + -- the underlying I/O is ready and wolfSSL will pick up where + -- it left off. When using a non_blocking socket, nothing needs + -- to be done, but select() can be used to check for the required + -- condition. If the underlying I/O is blocking, wolfSSL_connect() + -- will only return once the handshake has been finished or an error + -- occurred. wolfSSL takes a different approach to certificate + -- verification than OpenSSL does. The default policy for the client + -- is to verify the server, this means that if you don't load CAs + -- to verify the server you'll get a connect error, + -- unable to verify (_155). It you want to mimic OpenSSL behavior + -- of having SSL_connect succeed even if verifying the server fails + -- and reducing security you can do this by calling: + -- SSL_CTX_set_verify(ctx, SSL_VERIFY_NONE, 0); before calling + -- SSL_new(); Though it's not recommended. + + function Connect (Ssl : WolfSSL_Type) return Subprogram_Result is + Result : constant int := WolfSSL_Connect (Ssl); + begin + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Connect; + + procedure WolfSSL_Free (Ssl : WolfSSL_Type) with + Convention => C, + External_Name => "wolfSSL_free", + Import => True; + + procedure Free (Ssl : in out Optional_WolfSSL) is + begin + if Ssl.Exists then + WolfSSL_Free (Ssl.Instance); + end if; + Ssl := (Exists => False); + end Free; + + Result : constant int := Initialize_WolfSSL; +begin + if Result /= WOLFSSL_SUCCESS then + raise Initialization_Error; + end if; +end WolfSSL; diff --git a/wrapper/Ada/wolfssl.ads b/wrapper/Ada/wolfssl.ads new file mode 100644 index 0000000000..b237b2b443 --- /dev/null +++ b/wrapper/Ada/wolfssl.ads @@ -0,0 +1,262 @@ +with Interfaces.C; + +-- This package is annotated "with SPARK_Mode" that SPARK can verify +-- the API of this package is used correctly. The body of this package +-- cannot be formally verified since it calls C functions and uses +-- access-to-object types which are not part of the SPARK subset of +-- the Ada programming language. +package WolfSSL with SPARK_Mode is + + procedure Finalize; + -- Must be called before application exit. + + Initialization_Error : exception; + -- Raised if error was encountered during initialization of the + -- WolfSSL library. The WolfSSL libray is initialized during + -- elaboration time. + + Cleanup_Error : exception; + -- Raised if error was encountered during application shutdown + -- and cleanup of resources allocated by WolfSSL has failed. + + subtype char_array is Interfaces.C.char_array; -- Remove? + + subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000; + subtype Byte_Array is Interfaces.C.char_array; + + type Subprogram_Result is (Success, Failure); + + type Context_Type is limited private; + + type Optional_Context (Exists : Boolean := False) is record + case Exists is + when True => Instance : Context_Type; + when False => null; + end case; + end record; + + type Method_Type is limited private; + + function TLSv1_2_Server_Method return Method_Type; + function TLSv1_3_Server_Method return Method_Type; + + procedure Create_Context (Method : Method_Type; + Context : out Optional_Context); + -- Create and initialize a WolfSSL context. + + procedure Free (Context : in out Optional_Context) with + Pre => Context.Exists, + Post => not Context.Exists; + + type Mode_Type is private; + + function "&" (Left, Right : Mode_Type) return Mode_Type; + + Verify_None : constant Mode_Type; + + Verify_Peer : constant Mode_Type; + + Verify_Fail_If_No_Peer_Cert : constant Mode_Type; + + Verify_Client_Once : constant Mode_Type; + + Verify_Post_Handshake : constant Mode_Type; + + Verify_Fail_Except_Psk : constant Mode_Type; + + Verify_Default : constant Mode_Type; + + procedure Set_Verify (Context : Context_Type; + Mode : Mode_Type); + + type File_Format is private; + + Format_Asn1 : constant File_Format; + Format_Pem : constant File_Format; + Format_Default : constant File_Format; + + function Use_Certificate_File (Context : Context_Type; + File : String; + Format : File_Format) + return Subprogram_Result; + + function Use_Certificate_Buffer (Context : Context_Type; + Input : char_array; + Format : File_Format) + return Subprogram_Result; + + function Use_Private_Key_File (Context : Context_Type; + File : String; + Format : File_Format) + return Subprogram_Result; + + function Use_Private_Key_Buffer (Context : Context_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result; + + function Load_Verify_Locations (Context : Context_Type; + File : String; + Path : String) + return Subprogram_Result; + + function Load_Verify_Buffer (Context : Context_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result; + + type WolfSSL_Type is limited private; + + type Optional_WolfSSL (Exists : Boolean := False) is record + case Exists is + when True => Instance : WolfSSL_Type; + when False => null; + end case; + end record; + + procedure Create_WolfSSL (Context : Context_Type; + Ssl : out Optional_WolfSSL); + + -- Attach wolfSSL to the socket. + function Attach (Ssl : WolfSSL_Type; + Socket : Integer) + return Subprogram_Result; + + procedure Keep_Arrays (Ssl : WolfSSL_Type); + -- Don't free temporary arrays at end of handshake. + + procedure Free_Arrays (Ssl : WolfSSL_Type); + -- User doesn't need temporary arrays anymore, Free. + + function Accept_Connection (Ssl : WolfSSL_Type) + return Subprogram_Result; + + -- This record type has discriminants with default values to be able + -- to compile this code under the restriction no secondary stack. + type Read_Result (Result : Subprogram_Result := Failure; + Last : Byte_Index := Byte_Index'Last) is record + case Result is + when Success => Buffer : Byte_Array (1 .. Last); + when Failure => null; + end case; + end record; + + function Read (Ssl : WolfSSL_Type) return Read_Result; + + -- The number of bytes written is returned. + function Write (Ssl : WolfSSL_Type; Data : Byte_Array) return Integer; + + function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result; + + procedure Free (Ssl : in out Optional_WolfSSL) with + Pre => Ssl.Exists, + Post => not Ssl.Exists; + + function Connect (Ssl : WolfSSL_Type) return Subprogram_Result; + +private + pragma SPARK_Mode (Off); + + subtype int is Interfaces.C.int; use type int; + + type Opaque_Method is limited null record; + type Opaque_Context is limited null record; + type Opaque_WolfSSL is limited null record; + + -- Access-to-object types with convention C uses the same amount of + -- memory for storing pointers as is done in the C programming + -- language. The following access type definitions are used in + -- the Ada binding to the WolfSSL library: + type Context_Type is access Opaque_Context with Convention => C; + type Method_Type is access Opaque_Method with Convention => C; + type WolfSSL_Type is access Opaque_WolfSSL with Convention => C; + + subtype Unsigned_32 is Interfaces.Unsigned_32; use type Unsigned_32; + + type Mode_Type is new Unsigned_32; + + -- The following imported subprograms are used to initialize + -- the constants defined in the public part of this package + -- specification. They cannot therefore be moved to the body + -- of this package. + + function WolfSSL_Verify_None return int with + Convention => C, + External_Name => "get_wolfssl_verify_none", + Import => True; + + function WolfSSL_Verify_Peer return int with + Convention => C, + External_Name => "get_wolfssl_verify_peer", + Import => True; + + function WolfSSL_Verify_Fail_If_No_Peer_Cert return int with + Convention => C, + External_Name => "get_wolfssl_verify_fail_if_no_peer_cert", + Import => True; + + function WolfSSL_Verify_Client_Once return int with + Convention => C, + External_Name => "get_wolfssl_verify_client_once", + Import => True; + + function WolfSSL_Verify_Post_Handshake return int with + Convention => C, + External_Name => "get_wolfssl_verify_post_handshake", + Import => True; + + function WolfSSL_Verify_Fail_Except_Psk return int with + Convention => C, + External_Name => "get_wolfssl_verify_fail_except_psk", + Import => True; + + function WolfSSL_Verify_Default return int with + Convention => C, + External_Name => "get_wolfssl_verify_default", + Import => True; + + Verify_None : constant Mode_Type := Mode_Type (WolfSSL_Verify_None); + Verify_Peer : constant Mode_Type := Mode_Type (WolfSSL_Verify_Peer); + + Verify_Fail_If_No_Peer_Cert : constant Mode_Type := + Mode_Type (WolfSSL_Verify_Fail_If_No_Peer_Cert); + + Verify_Client_Once : constant Mode_Type := + Mode_Type (WolfSSL_Verify_Client_Once); + + Verify_Post_Handshake : constant Mode_Type := + Mode_Type (WolfSSL_Verify_Post_Handshake); + + Verify_Fail_Except_Psk : constant Mode_Type := + Mode_Type (WolfSSL_Verify_Fail_Except_Psk); + + Verify_Default : constant Mode_Type := + Mode_Type (WolfSSL_Verify_Default); + + type File_Format is new Unsigned_32; + + function WolfSSL_Filetype_Asn1 return int with + Convention => C, + External_Name => "get_wolfssl_filetype_asn1", + Import => True; + + function WolfSSL_Filetype_Pem return int with + Convention => C, + External_Name => "get_wolfssl_filetype_pem", + Import => True; + + function WolfSSL_Filetype_Default return int with + Convention => C, + External_Name => "get_wolfssl_filetype_default", + Import => True; + + Format_Asn1 : constant File_Format := + File_Format (WolfSSL_Filetype_Asn1); + + Format_Pem : constant File_Format := + File_Format (WolfSSL_Filetype_Pem); + + Format_Default : constant File_Format := + File_Format (WolfSSL_Filetype_Default); + +end WolfSSL; diff --git a/wrapper/include.am b/wrapper/include.am index d966d4bd8d..0bdcbc78ff 100644 --- a/wrapper/include.am +++ b/wrapper/include.am @@ -2,6 +2,7 @@ # included from Top Level Makefile.am # All paths should be given relative to the root +include wrapper/Ada/include.am include wrapper/CSharp/include.am EXTRA_DIST+= wrapper/python/README.md From 45d8a5b04c771984e17ec99ddb8efd6d59ad84ee Mon Sep 17 00:00:00 2001 From: Joakim Strandberg Date: Thu, 13 Jul 2023 16:49:22 +0200 Subject: [PATCH 2/6] Ada version of TLS v1.3 client application implemented --- wrapper/Ada/ada_binding.c | 8 +- wrapper/Ada/c_tls_server_main.c | 2 +- wrapper/Ada/client.gpr | 69 +++++++++++ wrapper/Ada/default.gpr | 8 +- wrapper/Ada/tls_client.adb | 196 ++++++++++++++++++++++++++++++- wrapper/Ada/tls_client.ads | 21 ++++ wrapper/Ada/tls_client_main.adb | 21 ++++ wrapper/Ada/tls_server.adb | 57 ++++++--- wrapper/Ada/tls_server.ads | 20 ++++ wrapper/Ada/tls_server_main.adb | 21 ++++ wrapper/Ada/wolfssl.adb | 197 +++++++++++++++++++++++++++----- wrapper/Ada/wolfssl.ads | 131 ++++++++++++++------- 12 files changed, 657 insertions(+), 94 deletions(-) create mode 100644 wrapper/Ada/client.gpr diff --git a/wrapper/Ada/ada_binding.c b/wrapper/Ada/ada_binding.c index 8eff71bb8d..9403b5c78f 100644 --- a/wrapper/Ada/ada_binding.c +++ b/wrapper/Ada/ada_binding.c @@ -24,10 +24,10 @@ #include -// 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. +/* 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_success(void); extern int get_wolfssl_verify_none(void); extern int get_wolfssl_verify_peer(void); diff --git a/wrapper/Ada/c_tls_server_main.c b/wrapper/Ada/c_tls_server_main.c index 7b7c74a9e2..161b3b8641 100644 --- a/wrapper/Ada/c_tls_server_main.c +++ b/wrapper/Ada/c_tls_server_main.c @@ -144,7 +144,7 @@ static void sig_handler(const int sig) #endif -// To execute the application: ./main +/* To execute the application: ./main */ int main(int argc, char** argv) { int ret = 0; diff --git a/wrapper/Ada/client.gpr b/wrapper/Ada/client.gpr new file mode 100644 index 0000000000..0642337c6f --- /dev/null +++ b/wrapper/Ada/client.gpr @@ -0,0 +1,69 @@ +project Client is + for Languages use ("C", "Ada"); + + for Source_Dirs use (".", + "../../", + "../../src", + "../../wolfcrypt/src"); + + for Object_Dir use "obj"; + + for Main use ("tls_client_main.adb"); + + package Naming is + for Spec_Suffix ("C") use ".h"; + end Naming; + + 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"); + + for Switches ("Ada") use ("-g"); + end Compiler; + + package Linker is + for Switches ("C") use + ("-lm"); -- To include the math library (used by WolfSSL). + + for Switches ("Ada") use + ("-lm"); -- To include the math library (used by WolfSSL). + end Linker; + + package Binder is + for Switches ("Ada") use ("-Es"); -- To include stack traces. + end Binder; + +end Client; diff --git a/wrapper/Ada/default.gpr b/wrapper/Ada/default.gpr index 3350eaa5c4..dc4c5014f6 100644 --- a/wrapper/Ada/default.gpr +++ b/wrapper/Ada/default.gpr @@ -22,7 +22,7 @@ project Default is package Compiler is for Switches ("C") use - ("-DWOLFSSL_USER_SETTINGS", + ("-DWOLFSSL_USER_SETTINGS", -- Use the user_settings.h file. "-Wno-pragmas", "-Wall", "-Wextra", @@ -56,6 +56,8 @@ project Default is "-Wunused-variable", "-Wwrite-strings", "-fwrapv"); + + for Switches ("Ada") use ("-g"); end Compiler; package Linker is @@ -66,4 +68,8 @@ project Default is ("-lm"); -- To include the math library (used by WolfSSL). end Linker; + package Binder is + for Switches ("Ada") use ("-Es"); -- To include stack traces. + end Binder; + end Default; diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index a1ade1afc0..97d43babeb 100644 --- a/wrapper/Ada/tls_client.adb +++ b/wrapper/Ada/tls_client.adb @@ -1,8 +1,30 @@ +-- tls_client.adb +-- +-- 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 +-- + -- Ada Standard Library packages. with Ada.Characters.Handling; with Ada.Command_Line; with Ada.Strings.Bounded; with Ada.Text_IO.Bounded_IO; +with Interfaces.C; -- GNAT Library packages. with GNAT.Sockets; @@ -18,16 +40,35 @@ package body Tls_Client is use all type WolfSSL.Subprogram_Result; + subtype Byte_Type is WolfSSL.Byte_Type; + package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); use all type Messages.Bounded_String; + package Integer_IO is new Ada.Text_IO.Integer_IO (Integer); + package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); + procedure Put (Text : String) is + begin + Ada.Text_IO.Put (Text); + end Put; + + procedure Put (Number : Integer) is + begin + Integer_IO.Put (Item => Number, Width => 0, Base => 10); + end Put; + procedure Put_Line (Text : String) is begin Ada.Text_IO.Put_Line (Text); end Put_Line; + procedure New_Line is + begin + Ada.Text_IO.New_Line; + end New_Line; + procedure Put_Line (Text : Messages.Bounded_String) is begin Messages_IO.Put_Line (Text); @@ -65,17 +106,164 @@ package body Tls_Client is Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; - CERT_FILE : constant String := "../certs/server-cert.pem"; - KEY_FILE : constant String := "../certs/server-key.pem"; - CA_FILE : constant String := "../certs/client-cert.pem"; + CERT_FILE : constant String := "../certs/client-cert.pem"; + KEY_FILE : constant String := "../certs/client-key.pem"; + CA_FILE : constant String := "../certs/ca-cert.pem"; subtype Byte_Array is WolfSSL.Byte_Array; + function Argument_Count return Natural is + begin + return Ada.Command_Line.Argument_Count; + end Argument_Count; + + function Argument (Number : Positive) return String is + begin + return Ada.Command_Line.Argument (Number); + end Argument; + procedure Run is A : Sock_Addr_Type; C : Socket_Type; -- Client socket. + D : Byte_Array (1 .. 200); + P : constant Port_Type := 11111; + + Ssl : WolfSSL.WolfSSL_Type; + Ctx : WolfSSL.Context_Type; + + Bytes_Written : Integer; + + Count : WolfSSL.Byte_Index; + + Text : String (1 .. 200); + Last : Integer; + + Input : WolfSSL.Read_Result; + + Result : WolfSSL.Subprogram_Result; begin - null; -- work in progress. + if Argument_Count /= 1 then + Put_Line ("usage: tcl_client "); + return; + end if; + GNAT.Sockets.Create_Socket (Socket => C); + + A := (Family => Family_Inet, + Addr => GNAT.Sockets.Inet_Addr (Argument (1)), + Port => P); + + GNAT.Sockets.Connect_Socket (Socket => C, + Server => A); + + -- Create and initialize WOLFSSL_CTX. + WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Client_Method, + Context => Ctx); + if not WolfSSL.Is_Valid (Ctx) then + Put_Line ("ERROR: failed to create WOLFSSL_CTX."); + Set (Exit_Status_Failure); + return; + end if; + + -- Load client certificate into WOLFSSL_CTX. + Result := WolfSSL.Use_Certificate_File (Context => Ctx, + File => CERT_FILE, + Format => WolfSSL.Format_Pem); + if Result = Failure then + Put ("ERROR: failed to load "); + Put (CERT_FILE); + Put (", please check the file."); + New_Line; + Set (Exit_Status_Failure); + return; + end if; + + -- Load client key into WOLFSSL_CTX. + Result := WolfSSL.Use_Private_Key_File (Context => Ctx, + File => KEY_FILE, + Format => WolfSSL.Format_Pem); + if Result = Failure then + Put ("ERROR: failed to load "); + Put (KEY_FILE); + Put (", please check the file."); + New_Line; + Set (Exit_Status_Failure); + return; + end if; + + -- Load CA certificate into WOLFSSL_CTX. + Result := WolfSSL.Load_Verify_Locations (Context => Ctx, + File => CA_FILE, + Path => ""); + if Result = Failure then + Put ("ERROR: failed to load "); + Put (CA_FILE); + Put (", please check the file."); + New_Line; + Set (Exit_Status_Failure); + return; + end if; + + -- Create a WOLFSSL object. + WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl); + if not WolfSSL.Is_Valid (Ssl) then + Put_Line ("ERROR: failed to create WOLFSSL object."); + Set (Exit_Status_Failure); + return; + end if; + + -- Attach wolfSSL to the socket. + Result := WolfSSL.Attach (Ssl => Ssl, + Socket => GNAT.Sockets.To_C (C)); + if Result = Failure then + Put_Line ("ERROR: Failed to set the file descriptor."); + Set (Exit_Status_Failure); + return; + end if; + + Result := WolfSSL.Connect (Ssl); + if Result = Failure then + Put_Line ("ERROR: failed to connect to wolfSSL."); + Set (Exit_Status_Failure); + return; + end if; + + Put ("Message for server: "); + Ada.Text_IO.Get_Line (Text, Last); + + Interfaces.C.To_C (Item => Text (1 .. Last), + Target => D, + Count => Count, + Append_Nul => False); + Bytes_Written := WolfSSL.Write (Ssl => Ssl, + Data => D (1 .. Count)); + if Bytes_Written < Last then + Put ("ERROR: failed to write entire message"); + New_Line; + Put (Bytes_Written); + Put (" bytes of "); + Put (Last); + Put ("bytes were sent"); + New_Line; + return; + end if; + + Input := WolfSSL.Read (Ssl); + if Input.Result /= Success then + Put_Line ("Read error."); + Set (Exit_Status_Failure); + return; + end if; + Interfaces.C.To_Ada (Item => Input.Buffer, + Target => Text, + Count => Last, + Trim_Nul => False); + Put ("Server: "); + Put (Text (1 .. Last)); + New_Line; + + GNAT.Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); end Run; end Tls_Client; diff --git a/wrapper/Ada/tls_client.ads b/wrapper/Ada/tls_client.ads index 9ff912b03f..3b651f4f89 100644 --- a/wrapper/Ada/tls_client.ads +++ b/wrapper/Ada/tls_client.ads @@ -1,3 +1,24 @@ +-- tls_client.ads +-- +-- 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 +-- + package Tls_Client is procedure Run; diff --git a/wrapper/Ada/tls_client_main.adb b/wrapper/Ada/tls_client_main.adb index 41e14a4d9a..0cb7b89f3b 100644 --- a/wrapper/Ada/tls_client_main.adb +++ b/wrapper/Ada/tls_client_main.adb @@ -1,3 +1,24 @@ +-- tls_client_main.adb +-- +-- 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 +-- + with Tls_Client; pragma Elaborate_All (Tls_Client); -- Application entry point for the Ada translation of the diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 2b907fb1d3..4b213fc3c5 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -1,3 +1,24 @@ +-- tls_server.adb +-- +-- 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 +-- + -- Ada Standard Library packages. with Ada.Characters.Handling; with Ada.Command_Line; @@ -81,9 +102,9 @@ package body Tls_Server is Ch : Character; - Ssl : WolfSSL.Optional_WolfSSL; + Ssl : WolfSSL.WolfSSL_Type; - Ctx : WolfSSL.Optional_Context; + Ctx : WolfSSL.Context_Type; Result : WolfSSL.Subprogram_Result; M : Messages.Bounded_String; Shall_Continue : Boolean := True; @@ -107,7 +128,7 @@ package body Tls_Server is -- Create and initialize WOLFSSL_CTX. WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Server_Method, Context => Ctx); - if not Ctx.Exists then + if not WolfSSL.Is_Valid (Ctx) then Put_Line ("ERROR: failed to create WOLFSSL_CTX."); Set (Exit_Status_Failure); return; @@ -115,11 +136,11 @@ package body Tls_Server is -- Require mutual authentication. WolfSSL.Set_Verify - (Context => Ctx.Instance, + (Context => Ctx, Mode => WolfSSL.Verify_Peer & WolfSSL.Verify_Fail_If_No_Peer_Cert); -- Load server certificates into WOLFSSL_CTX. - Result := WolfSSL.Use_Certificate_File (Context => Ctx.Instance, + Result := WolfSSL.Use_Certificate_File (Context => Ctx, File => CERT_FILE, Format => WolfSSL.Format_Pem); if Result = Failure then @@ -132,7 +153,7 @@ package body Tls_Server is end if; -- Load server key into WOLFSSL_CTX. - Result := WolfSSL.Use_Private_Key_File (Context => Ctx.Instance, + Result := WolfSSL.Use_Private_Key_File (Context => Ctx, File => KEY_FILE, Format => WolfSSL.Format_Pem); if Result = Failure then @@ -144,10 +165,8 @@ package body Tls_Server is return; end if; - Put_Line ("success to here at least"); - -- Load client certificate as "trusted" into WOLFSSL_CTX. - Result := WolfSSL.Load_Verify_Locations (Context => Ctx.Instance, + Result := WolfSSL.Load_Verify_Locations (Context => Ctx, File => CA_FILE, Path => ""); if Result = Failure then @@ -172,18 +191,24 @@ package body Tls_Server is end; -- Create a WOLFSSL object. - WolfSSL.Create_WolfSSL (Context => Ctx.Instance, Ssl => Ssl); - if not Ssl.Exists then + WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl); + if not WolfSSL.Is_Valid (Ssl) then Put_Line ("ERROR: failed to create WOLFSSL object."); Set (Exit_Status_Failure); return; end if; -- Attach wolfSSL to the socket. - Result := WolfSSL.Attach (Ssl => Ssl.Instance, + Result := WolfSSL.Attach (Ssl => Ssl, Socket => GNAT.Sockets.To_C (C)); + if Result = Failure then + Put_Line ("ERROR: Failed to set the file descriptor."); + Set (Exit_Status_Failure); + return; + end if; + -- Establish TLS connection. - Result := WolfSSL.Accept_Connection (Ssl.Instance); + Result := WolfSSL.Accept_Connection (Ssl); if Result = Failure then Put_Line ("Accept error."); Set (Exit_Status_Failure); @@ -192,7 +217,7 @@ package body Tls_Server is Put_Line ("Client connected successfully."); - Input := WolfSSL.Read (Ssl.Instance); + Input := WolfSSL.Read (Ssl); if Input.Result /= Success then Put_Line ("Read error."); @@ -221,12 +246,12 @@ package body Tls_Server is end if; end if; - Bytes_Written := WolfSSL.Write (Ssl.Instance, Reply); + Bytes_Written := WolfSSL.Write (Ssl, Reply); if Bytes_Written /= Reply'Length then Put_Line ("ERROR: failed to write."); end if; - Result := WolfSSL.Shutdown (Ssl.Instance); + Result := WolfSSL.Shutdown (Ssl); WolfSSL.Free (Ssl); GNAT.Sockets.Close_Socket (C); diff --git a/wrapper/Ada/tls_server.ads b/wrapper/Ada/tls_server.ads index b32e974953..fccb6610b0 100644 --- a/wrapper/Ada/tls_server.ads +++ b/wrapper/Ada/tls_server.ads @@ -1,3 +1,23 @@ +-- tls_server.ads +-- +-- 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 +-- package Tls_Server is procedure Run; diff --git a/wrapper/Ada/tls_server_main.adb b/wrapper/Ada/tls_server_main.adb index 8dc6a3a5a7..7f34503355 100644 --- a/wrapper/Ada/tls_server_main.adb +++ b/wrapper/Ada/tls_server_main.adb @@ -1,3 +1,24 @@ +-- tls_server_main.ads +-- +-- 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 +-- + with Tls_Server; pragma Elaborate_All (Tls_Server); -- Application entry point for the Ada translation of the diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb index d136f92e19..85c69d279e 100644 --- a/wrapper/Ada/wolfssl.adb +++ b/wrapper/Ada/wolfssl.adb @@ -1,3 +1,24 @@ +-- wolfssl.adb +-- +-- 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 +-- + with Interfaces.C.Strings; package body WolfSSL is @@ -31,6 +52,11 @@ package body WolfSSL is end if; end Finalize; + function Is_Valid (Context : Context_Type) return Boolean is + begin + return Context /= null; + end Is_Valid; + function WolfTLSv1_2_Server_Method return Method_Type with Convention => C, External_Name => "wolfTLSv1_2_server_method", @@ -51,28 +77,33 @@ package body WolfSSL is return WolfTLSv1_3_Server_Method; end TLSv1_3_Server_Method; + function WolfTLSv1_3_Client_Method return Method_Type with + Convention => C, + External_Name => "wolfTLSv1_3_client_method", + Import => True; + + function TLSv1_3_Client_Method return Method_Type is + begin + return WolfTLSv1_3_Client_Method; + end TLSv1_3_Client_Method; + function WolfSSL_CTX_new (Method : Method_Type) return Context_Type with Convention => C, External_Name => "wolfSSL_CTX_new", Import => True; procedure Create_Context (Method : Method_Type; - Context : out Optional_Context) is - C : constant Context_Type := WolfSSL_CTX_new (Method); + Context : out Context_Type) is begin - if C = null then - Context := (Exists => False); - else - Context := (Exists => True, Instance => C); - end if; + Context := WolfSSL_CTX_new (Method); end Create_Context; procedure WolfSSL_CTX_free (Context : Context_Type) with Convention => C, External_Name => "wolfSSL_CTX_free", Import => True; - procedure Free (Context : in out Optional_Context) is + procedure Free (Context : in out Context_Type) is begin - WolfSSL_CTX_free (Context.Instance); - Context := (Exists => False); + WolfSSL_CTX_free (Context); + Context := null; end Free; type Opaque_X509_Store_Context is limited null record; @@ -145,6 +176,7 @@ package body WolfSSL is File : String; Format : File_Format) return Subprogram_Result is + Ctx : constant Context_Type := Context; C : size_t; F : char_array (1 .. File'Length + 1); Result : int; @@ -153,7 +185,7 @@ package body WolfSSL is Target => F, Count => C, Append_Nul => True); - Result := Use_Certificate_File (Context, F (1 .. C), int (Format)); + Result := Use_Certificate_File (Ctx, F (1 .. C), int (Format)); if Result = WOLFSSL_SUCCESS then return Success; else @@ -197,6 +229,7 @@ package body WolfSSL is File : String; Format : File_Format) return Subprogram_Result is + Ctx : constant Context_Type := Context; C : size_t; F : char_array (1 .. File'Length + 1); Result : int; @@ -205,7 +238,7 @@ package body WolfSSL is Target => F, Count => C, Append_Nul => True); - Result := Use_Private_Key_File (Context, F (1 .. C), int (Format)); + Result := Use_Private_Key_File (Ctx, F (1 .. C), int (Format)); if Result = WOLFSSL_SUCCESS then return Success; else @@ -290,6 +323,7 @@ package body WolfSSL is File : String; Path : String) return Subprogram_Result is + Ctx : constant Context_Type := Context; FC : size_t; -- File Count, specifies the characters used in F. F : aliased char_array := (1 .. File'Length + 1 => '#'); @@ -300,13 +334,13 @@ package body WolfSSL is begin if File = "" then if Path = "" then - Result := Load_Verify_Locations4 (Context, null, null); + Result := Load_Verify_Locations4 (Ctx, null, null); else Interfaces.C.To_C (Item => Path, Target => P, Count => PC, Append_Nul => True); - Result := Load_Verify_Locations3 (Context, null, P); + Result := Load_Verify_Locations3 (Ctx, null, P); end if; else Interfaces.C.To_C (Item => File, @@ -314,7 +348,7 @@ package body WolfSSL is Count => FC, Append_Nul => True); if Path = "" then - Result := Load_Verify_Locations2 (Context, F, null); + Result := Load_Verify_Locations2 (Ctx, F, null); else Interfaces.C.To_C (Item => Path, Target => P, @@ -324,7 +358,9 @@ package body WolfSSL is Target => P, Count => PC, Append_Nul => True); - Result := Load_Verify_Locations1 (Context, F, P); + Result := Load_Verify_Locations1 (Context => Ctx, + File => F, + Path => P); end if; end if; if Result = WOLFSSL_SUCCESS then @@ -334,7 +370,7 @@ package body WolfSSL is end if; end Load_Verify_Locations; - function Load_Verify_Buffer1 + function Load_Verify_Buffer (Context : Context_Type; Input : char_array; Size : int; @@ -357,7 +393,7 @@ package body WolfSSL is return Subprogram_Result is Result : int; begin - Result := Load_Verify_Buffer1 (Context => Context, + Result := Load_Verify_Buffer (Context => Context, Input => Input, Size => Input'Length, Format => int(Format)); @@ -368,6 +404,11 @@ package body WolfSSL is end if; end Load_Verify_Buffer; + function Is_Valid (Ssl : WolfSSL_Type) return Boolean is + begin + return Ssl /= null; + end Is_Valid; + function WolfSSL_New (Context : Context_Type) return WolfSSL_Type with Convention => C, @@ -375,16 +416,114 @@ package body WolfSSL is Import => True; procedure Create_WolfSSL (Context : Context_Type; - Ssl : out Optional_WolfSSL) is - Result : WolfSSL_Type := WolfSSL_New (Context); + Ssl : out WolfSSL_Type) is + begin + Ssl := WolfSSL_New (Context); + end Create_WolfSSL; + + function Use_Certificate_File (Ssl : WolfSSL_Type; + File : char_array; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_use_certificate_file", + Import => True; + + function Use_Certificate_File (Ssl : WolfSSL_Type; + File : String; + Format : File_Format) + return Subprogram_Result is + C : size_t; + F : char_array (1 .. File'Length + 1); + Result : int; begin - if Result /= null then - Ssl := (Exists => True, - Instance => Result); + Interfaces.C.To_C (Item => File, + Target => F, + Count => C, + Append_Nul => True); + Result := Use_Certificate_File (Ssl, F (1 .. C), int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; else - Ssl := (Exists => False); + return Failure; end if; - end Create_WolfSSL; + end Use_Certificate_File; + + function Use_Certificate_Buffer (Ssl : WolfSSL_Type; + Input : char_array; + Size : long; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_use_certificate_buffer", + Import => True; + + function Use_Certificate_Buffer (Ssl : WolfSSL_Type; + Input : char_array; + Format : File_Format) + return Subprogram_Result is + Result : int; + begin + Result := Use_Certificate_Buffer (Ssl, Input, + Input'Length, int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Certificate_Buffer; + + function Use_Private_Key_File (Ssl : WolfSSL_Type; + File : char_array; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_use_PrivateKey_file", + Import => True; + + function Use_Private_Key_File (Ssl : WolfSSL_Type; + File : String; + Format : File_Format) + return Subprogram_Result is + C : size_t; + F : char_array (1 .. File'Length + 1); + Result : int; + begin + Interfaces.C.To_C (Item => File, + Target => F, + Count => C, + Append_Nul => True); + Result := Use_Private_Key_File (Ssl, F (1 .. C), int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Private_Key_File; + + function Use_Private_Key_Buffer (Ssl : WolfSSL_Type; + Input : char_array; + Size : long; + Format : int) + return int with + Convention => C, + External_Name => "wolfSSL_use_PrivateKey_buffer", + Import => True; + + function Use_Private_Key_Buffer (Ssl : WolfSSL_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result is + Result : int; + begin + Result := Use_Private_Key_Buffer (Ssl, Input, + Input'Length, int (Format)); + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Use_Private_Key_Buffer; function WolfSSL_Set_Fd (Ssl : WolfSSL_Type; Fd : int) return int with Convention => C, @@ -581,12 +720,12 @@ package body WolfSSL is External_Name => "wolfSSL_free", Import => True; - procedure Free (Ssl : in out Optional_WolfSSL) is + procedure Free (Ssl : in out WolfSSL_Type) is begin - if Ssl.Exists then - WolfSSL_Free (Ssl.Instance); + if Ssl /= null then + WolfSSL_Free (Ssl); end if; - Ssl := (Exists => False); + Ssl := null; end Free; Result : constant int := Initialize_WolfSSL; diff --git a/wrapper/Ada/wolfssl.ads b/wrapper/Ada/wolfssl.ads index b237b2b443..02c04ef332 100644 --- a/wrapper/Ada/wolfssl.ads +++ b/wrapper/Ada/wolfssl.ads @@ -1,10 +1,28 @@ +-- wolfssl.ads +-- +-- 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 +-- + with Interfaces.C; -- This package is annotated "with SPARK_Mode" that SPARK can verify --- the API of this package is used correctly. The body of this package --- cannot be formally verified since it calls C functions and uses --- access-to-object types which are not part of the SPARK subset of --- the Ada programming language. +-- the API of this package is used correctly. package WolfSSL with SPARK_Mode is procedure Finalize; @@ -21,6 +39,7 @@ package WolfSSL with SPARK_Mode is subtype char_array is Interfaces.C.char_array; -- Remove? + subtype Byte_Type is Interfaces.C.char; subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000; subtype Byte_Array is Interfaces.C.char_array; @@ -28,25 +47,22 @@ package WolfSSL with SPARK_Mode is type Context_Type is limited private; - type Optional_Context (Exists : Boolean := False) is record - case Exists is - when True => Instance : Context_Type; - when False => null; - end case; - end record; + function Is_Valid (Context : Context_Type) return Boolean; type Method_Type is limited private; function TLSv1_2_Server_Method return Method_Type; function TLSv1_3_Server_Method return Method_Type; + function TLSv1_3_Client_Method return Method_Type; procedure Create_Context (Method : Method_Type; - Context : out Optional_Context); + Context : out Context_Type); -- Create and initialize a WolfSSL context. + -- If successful Is_Valid (Context) = True, otherwise False. - procedure Free (Context : in out Optional_Context) with - Pre => Context.Exists, - Post => not Context.Exists; + procedure Free (Context : in out Context_Type) with + Pre => Is_Valid (Context), + Post => not Is_Valid (Context); type Mode_Type is private; @@ -67,7 +83,8 @@ package WolfSSL with SPARK_Mode is Verify_Default : constant Mode_Type; procedure Set_Verify (Context : Context_Type; - Mode : Mode_Type); + Mode : Mode_Type) with + Pre => Is_Valid (Context); type File_Format is private; @@ -78,58 +95,89 @@ package WolfSSL with SPARK_Mode is function Use_Certificate_File (Context : Context_Type; File : String; Format : File_Format) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Context); function Use_Certificate_Buffer (Context : Context_Type; Input : char_array; Format : File_Format) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Context); function Use_Private_Key_File (Context : Context_Type; File : String; Format : File_Format) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Context); function Use_Private_Key_Buffer (Context : Context_Type; Input : Byte_Array; Format : File_Format) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Context); function Load_Verify_Locations (Context : Context_Type; File : String; Path : String) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Context); function Load_Verify_Buffer (Context : Context_Type; Input : Byte_Array; Format : File_Format) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Context); type WolfSSL_Type is limited private; - type Optional_WolfSSL (Exists : Boolean := False) is record - case Exists is - when True => Instance : WolfSSL_Type; - when False => null; - end case; - end record; + function Is_Valid (Ssl : WolfSSL_Type) return Boolean; procedure Create_WolfSSL (Context : Context_Type; - Ssl : out Optional_WolfSSL); + Ssl : out WolfSSL_Type) with + Pre => Is_Valid (Context); + + + function Use_Certificate_File (Ssl : WolfSSL_Type; + File : String; + Format : File_Format) + return Subprogram_Result with + Pre => Is_Valid (Ssl); + + function Use_Certificate_Buffer (Ssl : WolfSSL_Type; + Input : char_array; + Format : File_Format) + return Subprogram_Result with + Pre => Is_Valid (Ssl); + + function Use_Private_Key_File (Ssl : WolfSSL_Type; + File : String; + Format : File_Format) + return Subprogram_Result with + Pre => Is_Valid (Ssl); + + function Use_Private_Key_Buffer (Ssl : WolfSSL_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result with + Pre => Is_Valid (Ssl); -- Attach wolfSSL to the socket. function Attach (Ssl : WolfSSL_Type; Socket : Integer) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Ssl); - procedure Keep_Arrays (Ssl : WolfSSL_Type); + procedure Keep_Arrays (Ssl : WolfSSL_Type) with + Pre => Is_Valid (Ssl); -- Don't free temporary arrays at end of handshake. - procedure Free_Arrays (Ssl : WolfSSL_Type); + procedure Free_Arrays (Ssl : WolfSSL_Type) with + Pre => Is_Valid (Ssl); -- User doesn't need temporary arrays anymore, Free. function Accept_Connection (Ssl : WolfSSL_Type) - return Subprogram_Result; + return Subprogram_Result with + Pre => Is_Valid (Ssl); -- This record type has discriminants with default values to be able -- to compile this code under the restriction no secondary stack. @@ -141,18 +189,23 @@ package WolfSSL with SPARK_Mode is end case; end record; - function Read (Ssl : WolfSSL_Type) return Read_Result; + function Read (Ssl : WolfSSL_Type) return Read_Result with + Pre => Is_Valid (Ssl); -- The number of bytes written is returned. - function Write (Ssl : WolfSSL_Type; Data : Byte_Array) return Integer; + function Write (Ssl : WolfSSL_Type; + Data : Byte_Array) return Integer with + Pre => Is_Valid (Ssl); - function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result; + function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result with + Pre => Is_Valid (Ssl); - procedure Free (Ssl : in out Optional_WolfSSL) with - Pre => Ssl.Exists, - Post => not Ssl.Exists; + procedure Free (Ssl : in out WolfSSL_Type) with + Pre => Is_Valid (Ssl), + Post => not Is_Valid (Ssl); - function Connect (Ssl : WolfSSL_Type) return Subprogram_Result; + function Connect (Ssl : WolfSSL_Type) return Subprogram_Result with + Pre => Is_Valid (Ssl); private pragma SPARK_Mode (Off); From f49ffc0353e363421bc641e7a94ee2672ee024df Mon Sep 17 00:00:00 2001 From: Joakim Strandberg Date: Fri, 14 Jul 2023 20:30:34 +0200 Subject: [PATCH 3/6] The implementations of the tls client and server applications can now be formally verified by the SPARK tools. --- wrapper/Ada/spark_sockets.adb | 138 ++++++++++++++++++++++ wrapper/Ada/spark_sockets.ads | 137 +++++++++++++++++++++ wrapper/Ada/spark_terminal.adb | 18 +++ wrapper/Ada/spark_terminal.ads | 43 +++++++ wrapper/Ada/tls_client.adb | 154 ++++++++++++++---------- wrapper/Ada/tls_client.ads | 15 ++- wrapper/Ada/tls_client_main.adb | 10 +- wrapper/Ada/tls_server.adb | 203 ++++++++++++++++++++------------ wrapper/Ada/tls_server.ads | 18 ++- wrapper/Ada/tls_server_main.adb | 12 +- 10 files changed, 603 insertions(+), 145 deletions(-) create mode 100644 wrapper/Ada/spark_sockets.adb create mode 100644 wrapper/Ada/spark_sockets.ads create mode 100644 wrapper/Ada/spark_terminal.adb create mode 100644 wrapper/Ada/spark_terminal.ads diff --git a/wrapper/Ada/spark_sockets.adb b/wrapper/Ada/spark_sockets.adb new file mode 100644 index 0000000000..e315f230e3 --- /dev/null +++ b/wrapper/Ada/spark_sockets.adb @@ -0,0 +1,138 @@ +-- spark_sockets.adb +-- +-- 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 +-- + +with Interfaces.C; + +package body SPARK_Sockets is + + function Inet_Addr (Image : String) return Optional_Inet_Addr is + A : Inet_Addr_Type; + begin + A := GNAT.Sockets.Inet_Addr (Image); + return (Exists => True, Addr => A); + exception + when others => + return (Exists => False); + end Inet_Addr; + + procedure Create_Socket (Socket : in out Optional_Socket) is + S : Socket_Type; + begin + GNAT.Sockets.Create_Socket (S); + Socket := (Exists => True, Socket => S); + exception + when others => + Socket := (Exists => False); + end Create_Socket; + + function Connect_Socket (Socket : Socket_Type; + Server : Sock_Addr_Type) + return Subprogram_Result is + begin + GNAT.Sockets.Connect_Socket (Socket, Server); + return Success; + exception + when others => + return Failure; + end Connect_Socket; + + function To_C (Socket : Socket_Type) return Integer is + begin + -- The call to GNAT.Sockets.To_C can never raise an exception. + return GNAT.Sockets.To_C (Socket); + end To_C; + + procedure Close_Socket (Socket : in out Optional_Socket) is + begin + GNAT.Sockets.Close_Socket (Socket.Socket); + Socket := (Exists => False); + end Close_Socket; + + function Set_Socket_Option (Socket : Socket_Type; + Level : Level_Type; + Option : Option_Type) + return Subprogram_Result is + begin + GNAT.Sockets.Set_Socket_Option (Socket, Level, Option); + return Success; + exception + when others => + return Failure; + end Set_Socket_Option; + + function Bind_Socket (Socket : Socket_Type; + Address : Sock_Addr_Type) + return Subprogram_Result is + begin + GNAT.Sockets.Bind_Socket (Socket, Address); + return Success; + exception + when others => + return Failure; + end Bind_Socket; + + function Listen_Socket (Socket : Socket_Type; + Length : Natural) return Subprogram_Result is + begin + GNAT.Sockets.Listen_Socket (Socket, Length); + return Success; + exception + when others => + return Failure; + end Listen_Socket; + + procedure Accept_Socket (Server : Socket_Type; + Socket : out Optional_Socket; + Address : out Sock_Addr_Type; + Result : out Subprogram_Result) is + C : Socket_Type; + begin + GNAT.Sockets.Accept_Socket (Server, C, Address); + Socket := (Exists => True, Socket => C); + Result := Success; + exception + when others => + Socket := (Exists => False); + Address := (Family => GNAT.Sockets.Family_Unspec); + Result := Failure; + end Accept_Socket; + + procedure To_C (Item : String; + Target : out Byte_Array; + Count : out Byte_Index) is + begin + Interfaces.C.To_C (Item => Item, + Target => Target, + Count => Count, + Append_Nul => False); + end To_C; + + procedure To_Ada (Item : Byte_Array; + Target : out String; + Count : out Natural) is + begin + Interfaces.C.To_Ada (Item => Item, + Target => Target, + Count => Count, + Trim_Nul => False); + end To_Ada; + +end SPARK_Sockets; diff --git a/wrapper/Ada/spark_sockets.ads b/wrapper/Ada/spark_sockets.ads new file mode 100644 index 0000000000..ee9864c6ff --- /dev/null +++ b/wrapper/Ada/spark_sockets.ads @@ -0,0 +1,137 @@ +-- spark_sockets.ads +-- +-- 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 +-- + +-- GNAT Library packages. +with GNAT.Sockets; + +-- The WolfSSL package. +with WolfSSL; + +-- This is a wrapper package around the GNAT.Sockets package. +-- GNAT.Sockets raises exceptions to signal errors but exceptions +-- are not supported by SPARK. This package converts raised exceptions +-- into returned enumeration values by functions indicating success +-- or failure. +-- +-- The intended use of this package is to demonstrate the usage +-- of the WolfSSL Ada binding in Ada/SPARK code. +package SPARK_Sockets with SPARK_Mode is + + subtype Byte_Array is WolfSSL.Byte_Array; + subtype Byte_Index is WolfSSL.Byte_Index; use type Byte_Index; + + subtype Port_Type is GNAT.Sockets.Port_Type; + + subtype Level_Type is GNAT.Sockets.Level_Type; + + subtype Socket_Type is GNAT.Sockets.Socket_Type; + subtype Option_Name is GNAT.Sockets.Option_Name; + subtype Option_Type is GNAT.Sockets.Option_Type; + subtype Family_Type is GNAT.Sockets.Family_Type; + + subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + + Socket_Error : exception renames GNAT.Sockets.Socket_Error; + + Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + + Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + + Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + use type GNAT.Sockets.Family_Type; + + Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + + subtype Subprogram_Result is WolfSSL.Subprogram_Result; + use type Subprogram_Result; + + Success : Subprogram_Result renames WolfSSL.Success; + Failure : Subprogram_Result renames WolfSSL.Failure; + + type Optional_Inet_Addr (Exists : Boolean := False) is record + case Exists is + when True => Addr : Inet_Addr_Type; + when False => null; + end case; + end record; + + function Inet_Addr (Image : String) return Optional_Inet_Addr; + + type Optional_Socket (Exists : Boolean := False) is record + case Exists is + when True => Socket : Socket_Type; + when False => null; + end case; + end record; + + procedure Create_Socket (Socket : in out Optional_Socket) with + Pre => not Socket.Exists; + + function Connect_Socket (Socket : Socket_Type; + Server : Sock_Addr_Type) + return Subprogram_Result; + + function To_C (Socket : Socket_Type) return Integer with Inline; + + -- Close a socket and more specifically a non-connected socket. + procedure Close_Socket (Socket : in out Optional_Socket) with + Pre => Socket.Exists, + Post => not Socket.Exists; + + function Set_Socket_Option (Socket : Socket_Type; + Level : Level_Type; + Option : Option_Type) + return Subprogram_Result; + -- Manipulate socket options. + + function Bind_Socket (Socket : Socket_Type; + Address : Sock_Addr_Type) + return Subprogram_Result; + + function Listen_Socket (Socket : Socket_Type; + Length : Natural) return Subprogram_Result; + -- To accept connections, a socket is first created with + -- Create_Socket, a willingness to accept incoming connections and + -- a queue Length for incoming connections are specified. + -- The queue length of 15 is an example value that should be + -- appropriate in usual cases. It can be adjusted according to each + -- application's particular requirements. + + procedure Accept_Socket (Server : Socket_Type; + Socket : out Optional_Socket; + Address : out Sock_Addr_Type; + Result : out Subprogram_Result) with + Post => (if Result = Success then Socket.Exists else not Socket.Exists); + + procedure To_C (Item : String; + Target : out Byte_Array; + Count : out Byte_Index) with + Pre => Item'Length <= Target'Length, + Post => Count <= Target'Last; + + procedure To_Ada (Item : Byte_Array; + Target : out String; + Count : out Natural) with + Pre => Item'Length <= Target'Length, + Post => Count <= Target'Last; + +end SPARK_Sockets; diff --git a/wrapper/Ada/spark_terminal.adb b/wrapper/Ada/spark_terminal.adb new file mode 100644 index 0000000000..14bfb4b1fb --- /dev/null +++ b/wrapper/Ada/spark_terminal.adb @@ -0,0 +1,18 @@ +package body SPARK_Terminal is + + procedure Set_Exit_Status (Status : Exit_Status) is + begin + Ada.Command_Line.Set_Exit_Status (Status); + end Set_Exit_Status; + + function Argument_Count return Natural is + begin + return Ada.Command_Line.Argument_Count; + end Argument_Count; + + function Argument (Number : Positive) return String is + begin + return Ada.Command_Line.Argument (Number); + end Argument; + +end SPARK_Terminal; diff --git a/wrapper/Ada/spark_terminal.ads b/wrapper/Ada/spark_terminal.ads new file mode 100644 index 0000000000..1c516ca7b3 --- /dev/null +++ b/wrapper/Ada/spark_terminal.ads @@ -0,0 +1,43 @@ +-- spark_sockets.ads +-- +-- 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 +-- + +with Ada.Command_Line; + +-- SPARK wrapper package around Ada.Command_Line and Interfaces.C +-- packages because these packages lack contracts in their specification +-- files that SPARK can use to verify the context in which +-- subprograms can safely be called. +package SPARK_Terminal with SPARK_Mode is + + subtype Exit_Status is Ada.Command_Line.Exit_Status; + + Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; + Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + + procedure Set_Exit_Status (Status : Exit_Status) with + Global => null; + + function Argument_Count return Natural; + + function Argument (Number : Positive) return String with + Pre => Number <= Argument_Count; + +end SPARK_Terminal; diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index 97d43babeb..a003033538 100644 --- a/wrapper/Ada/tls_client.adb +++ b/wrapper/Ada/tls_client.adb @@ -21,18 +21,13 @@ -- Ada Standard Library packages. with Ada.Characters.Handling; -with Ada.Command_Line; with Ada.Strings.Bounded; -with Ada.Text_IO.Bounded_IO; +with Ada.Text_IO; with Interfaces.C; --- GNAT Library packages. -with GNAT.Sockets; +with SPARK_Terminal; --- The WolfSSL package. -with WolfSSL; - -package body Tls_Client is +package body Tls_Client with SPARK_Mode is use type WolfSSL.Mode_Type; use type WolfSSL.Byte_Index; @@ -42,13 +37,8 @@ package body Tls_Client is subtype Byte_Type is WolfSSL.Byte_Type; - package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); - use all type Messages.Bounded_String; - package Integer_IO is new Ada.Text_IO.Integer_IO (Integer); - package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); - procedure Put (Text : String) is begin Ada.Text_IO.Put (Text); @@ -69,42 +59,39 @@ package body Tls_Client is Ada.Text_IO.New_Line; end New_Line; - procedure Put_Line (Text : Messages.Bounded_String) is - begin - Messages_IO.Put_Line (Text); - end Put_Line; - - subtype Exit_Status is Ada.Command_Line.Exit_Status; + subtype Exit_Status is SPARK_Terminal.Exit_Status; - Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; - Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + Exit_Status_Success : Exit_Status renames SPARK_Terminal.Exit_Status_Success; + Exit_Status_Failure : Exit_Status renames SPARK_Terminal.Exit_Status_Failure; - procedure Set (Status : Exit_Status) is + procedure Set (Status : Exit_Status) with Global => null is begin - Ada.Command_Line.Set_Exit_Status (Status); + SPARK_Terminal.Set_Exit_Status (Status); end Set; - subtype Port_Type is GNAT.Sockets.Port_Type; + subtype Port_Type is SPARK_Sockets.Port_Type; + + subtype Level_Type is SPARK_Sockets.Level_Type; - subtype Level_Type is GNAT.Sockets.Level_Type; + subtype Socket_Type is SPARK_Sockets.Socket_Type; + subtype Option_Name is SPARK_Sockets.Option_Name; + subtype Option_Type is SPARK_Sockets.Option_Type; + subtype Family_Type is SPARK_Sockets.Family_Type; - subtype Socket_Type is GNAT.Sockets.Socket_Type; - subtype Option_Name is GNAT.Sockets.Option_Name; - subtype Option_Type is GNAT.Sockets.Option_Type; - subtype Family_Type is GNAT.Sockets.Family_Type; + subtype Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type; - subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; - subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + use type Family_Type; - Socket_Error : exception renames GNAT.Sockets.Socket_Error; + Socket_Error : exception renames SPARK_Sockets.Socket_Error; - Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address; - Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level; - Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet; - Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr; CERT_FILE : constant String := "../certs/client-cert.pem"; KEY_FILE : constant String := "../certs/client-key.pem"; @@ -112,24 +99,26 @@ package body Tls_Client is subtype Byte_Array is WolfSSL.Byte_Array; - function Argument_Count return Natural is - begin - return Ada.Command_Line.Argument_Count; - end Argument_Count; + function Argument_Count return Natural renames + SPARK_Terminal.Argument_Count; + + function Argument (Number : Positive) return String with + Pre => Number <= Argument_Count; function Argument (Number : Positive) return String is begin - return Ada.Command_Line.Argument (Number); + return SPARK_Terminal.Argument (Number); end Argument; - procedure Run is + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + Client : in out SPARK_Sockets.Optional_Socket) is A : Sock_Addr_Type; - C : Socket_Type; -- Client socket. + C : SPARK_Sockets.Optional_Socket renames Client; D : Byte_Array (1 .. 200); P : constant Port_Type := 11111; - Ssl : WolfSSL.WolfSSL_Type; - Ctx : WolfSSL.Context_Type; + Addr : SPARK_Sockets.Optional_Inet_Addr; Bytes_Written : Integer; @@ -142,24 +131,44 @@ package body Tls_Client is Result : WolfSSL.Subprogram_Result; begin - if Argument_Count /= 1 then + if Argument_Count < 1 then Put_Line ("usage: tcl_client "); return; end if; - GNAT.Sockets.Create_Socket (Socket => C); + SPARK_Sockets.Create_Socket (C); + if not C.Exists then + Put_Line ("ERROR: Failed to create socket."); + return; + end if; + Addr := SPARK_Sockets.Inet_Addr (Argument (1)); + if not Addr.Exists or + (Addr.Exists and then Addr.Addr.Family /= Family_Inet) + then + Put_Line ("ERROR: please specify IPv4 address."); + SPARK_Sockets.Close_Socket (C); + Set (Exit_Status_Failure); + return; + end if; A := (Family => Family_Inet, - Addr => GNAT.Sockets.Inet_Addr (Argument (1)), + Addr => Addr.Addr, Port => P); - GNAT.Sockets.Connect_Socket (Socket => C, - Server => A); + Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket, + Server => A); + if Result = Failure then + Put_Line ("ERROR: Failed to connect to server."); + SPARK_Sockets.Close_Socket (C); + Set (Exit_Status_Failure); + return; + end if; -- Create and initialize WOLFSSL_CTX. WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Client_Method, Context => Ctx); if not WolfSSL.Is_Valid (Ctx) then Put_Line ("ERROR: failed to create WOLFSSL_CTX."); + SPARK_Sockets.Close_Socket (C); Set (Exit_Status_Failure); return; end if; @@ -173,6 +182,8 @@ package body Tls_Client is Put (CERT_FILE); Put (", please check the file."); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -186,6 +197,8 @@ package body Tls_Client is Put (KEY_FILE); Put (", please check the file."); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -199,6 +212,8 @@ package body Tls_Client is Put (CA_FILE); Put (", please check the file."); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -207,15 +222,20 @@ package body Tls_Client is WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl); if not WolfSSL.Is_Valid (Ssl) then Put_Line ("ERROR: failed to create WOLFSSL object."); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; -- Attach wolfSSL to the socket. Result := WolfSSL.Attach (Ssl => Ssl, - Socket => GNAT.Sockets.To_C (C)); + Socket => SPARK_Sockets.To_C (C.Socket)); if Result = Failure then Put_Line ("ERROR: Failed to set the file descriptor."); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -223,6 +243,9 @@ package body Tls_Client is Result := WolfSSL.Connect (Ssl); if Result = Failure then Put_Line ("ERROR: failed to connect to wolfSSL."); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -230,10 +253,9 @@ package body Tls_Client is Put ("Message for server: "); Ada.Text_IO.Get_Line (Text, Last); - Interfaces.C.To_C (Item => Text (1 .. Last), - Target => D, - Count => Count, - Append_Nul => False); + 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 @@ -244,6 +266,9 @@ package body Tls_Client is Put (Last); Put ("bytes were sent"); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); return; end if; @@ -251,19 +276,28 @@ package body Tls_Client is if Input.Result /= Success then Put_Line ("Read error."); Set (Exit_Status_Failure); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); return; end if; - Interfaces.C.To_Ada (Item => Input.Buffer, - Target => Text, - Count => Last, - Trim_Nul => False); + if Input.Buffer'Length > Text'Length then + SPARK_Sockets.To_Ada (Item => Input.Buffer (1 .. 200), + Target => Text, + Count => Last); + else + SPARK_Sockets.To_Ada (Item => Input.Buffer, + Target => Text, + Count => Last); + end if; Put ("Server: "); Put (Text (1 .. Last)); New_Line; - GNAT.Sockets.Close_Socket (C); + SPARK_Sockets.Close_Socket (C); WolfSSL.Free (Ssl); WolfSSL.Free (Context => Ctx); + WolfSSL.Finalize; end Run; end Tls_Client; diff --git a/wrapper/Ada/tls_client.ads b/wrapper/Ada/tls_client.ads index 3b651f4f89..50a52b3ccd 100644 --- a/wrapper/Ada/tls_client.ads +++ b/wrapper/Ada/tls_client.ads @@ -19,8 +19,19 @@ -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA -- -package Tls_Client is +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); - procedure Run; +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); + +package Tls_Client with SPARK_Mode is + + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + Client : in out SPARK_Sockets.Optional_Socket) with + Pre => (not Client.Exists and not + WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)), + Post => (not Client.Exists and not WolfSSL.Is_Valid (Ssl) and + not WolfSSL.Is_Valid (Ctx)); end Tls_Client; diff --git a/wrapper/Ada/tls_client_main.adb b/wrapper/Ada/tls_client_main.adb index 0cb7b89f3b..ab50dab842 100644 --- a/wrapper/Ada/tls_client_main.adb +++ b/wrapper/Ada/tls_client_main.adb @@ -19,11 +19,15 @@ -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA -- -with Tls_Client; pragma Elaborate_All (Tls_Client); - +with Tls_Client; pragma Elaborate_All (Tls_Client); +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); +with WolfSSL; pragma Elaborate_All (WolfSSL); -- Application entry point for the Ada translation of the -- tls client v1.3 example in C. procedure Tls_Client_Main is + Ssl : WolfSSL.WolfSSL_Type; + Ctx : WolfSSL.Context_Type; + C : SPARK_Sockets.Optional_Socket; begin - Tls_Client.Run; + Tls_Client.Run (Ssl, Ctx, Client => C); end Tls_Client_Main; diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 4b213fc3c5..1eaca1349b 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -21,17 +21,12 @@ -- Ada Standard Library packages. with Ada.Characters.Handling; -with Ada.Command_Line; with Ada.Strings.Bounded; with Ada.Text_IO.Bounded_IO; --- GNAT Library packages. -with GNAT.Sockets; +with SPARK_Terminal; pragma Elaborate_All (SPARK_Terminal); --- The WolfSSL package. -with WolfSSL; - -package body Tls_Server is +package body Tls_Server with SPARK_Mode is use type WolfSSL.Mode_Type; use type WolfSSL.Byte_Index; @@ -39,52 +34,57 @@ package body Tls_Server is use all type WolfSSL.Subprogram_Result; - package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); - use all type Messages.Bounded_String; + procedure Put (Char : Character) is + begin + Ada.Text_IO.Put (Char); + end Put; - package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); + procedure Put (Text : String) is + begin + Ada.Text_IO.Put (Text); + end Put; procedure Put_Line (Text : String) is begin Ada.Text_IO.Put_Line (Text); end Put_Line; - procedure Put_Line (Text : Messages.Bounded_String) is + procedure New_Line is begin - Messages_IO.Put_Line (Text); - end Put_Line; + Ada.Text_IO.New_Line; + end New_Line; - subtype Exit_Status is Ada.Command_Line.Exit_Status; + subtype Exit_Status is SPARK_Terminal.Exit_Status; - Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; - Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + Exit_Status_Success : Exit_Status renames SPARK_Terminal.Exit_Status_Success; + Exit_Status_Failure : Exit_Status renames SPARK_Terminal.Exit_Status_Failure; - procedure Set (Status : Exit_Status) is + procedure Set (Status : Exit_Status) with Global => null is begin - Ada.Command_Line.Set_Exit_Status (Status); + SPARK_Terminal.Set_Exit_Status (Status); end Set; - subtype Port_Type is GNAT.Sockets.Port_Type; + subtype Port_Type is SPARK_Sockets.Port_Type; - subtype Level_Type is GNAT.Sockets.Level_Type; + subtype Level_Type is SPARK_Sockets.Level_Type; - subtype Socket_Type is GNAT.Sockets.Socket_Type; - subtype Option_Name is GNAT.Sockets.Option_Name; - subtype Option_Type is GNAT.Sockets.Option_Type; - subtype Family_Type is GNAT.Sockets.Family_Type; + subtype Socket_Type is SPARK_Sockets.Socket_Type; + subtype Option_Name is SPARK_Sockets.Option_Name; + subtype Option_Type is SPARK_Sockets.Option_Type; + subtype Family_Type is SPARK_Sockets.Family_Type; - subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; - subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + subtype Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type; - Socket_Error : exception renames GNAT.Sockets.Socket_Error; + Socket_Error : exception renames SPARK_Sockets.Socket_Error; - Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address; - Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level; - Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet; - Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr; CERT_FILE : constant String := "../certs/server-cert.pem"; KEY_FILE : constant String := "../certs/server-key.pem"; @@ -94,42 +94,64 @@ package body Tls_Server is Reply : constant Byte_Array := "I hear ya fa shizzle!"; - procedure Run is + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + L : in out SPARK_Sockets.Optional_Socket; + C : in out SPARK_Sockets.Optional_Socket) is A : Sock_Addr_Type; - L : Socket_Type; -- Listener socket. - C : Socket_Type; -- Client socket. P : constant Port_Type := 11111; Ch : Character; - Ssl : WolfSSL.WolfSSL_Type; - - Ctx : WolfSSL.Context_Type; Result : WolfSSL.Subprogram_Result; - M : Messages.Bounded_String; Shall_Continue : Boolean := True; Bytes_Written : Integer; Input : WolfSSL.Read_Result; + Option : Option_Type; begin - GNAT.Sockets.Create_Socket (Socket => L); - GNAT.Sockets.Set_Socket_Option (Socket => L, - Level => Socket_Level, - Option => (Name => Reuse_Address, - Enabled => True)); - GNAT.Sockets.Bind_Socket (Socket => L, - Address => (Family => Family_Inet, - Addr => Any_Inet_Addr, - Port => P)); - GNAT.Sockets.Listen_Socket (Socket => L, - Length => 5); + SPARK_Sockets.Create_Socket (Socket => L); + if not L.Exists then + Put_Line ("ERROR: Failed to create socket."); + return; + end if; + + Option := (Name => Reuse_Address, Enabled => True); + Result := SPARK_Sockets.Set_Socket_Option (Socket => L.Socket, + Level => Socket_Level, + Option => Option); + if Result = Failure then + Put_Line ("ERROR: Failed to set socket option."); + SPARK_Sockets.Close_Socket (L); + return; + end if; + + A := (Family => Family_Inet, + Addr => Any_Inet_Addr, + Port => P); + Result := SPARK_Sockets.Bind_Socket (Socket => L.Socket, + Address => A); + if Result = Failure then + Put_Line ("ERROR: Failed to bind socket."); + SPARK_Sockets.Close_Socket (L); + return; + end if; + + Result := SPARK_Sockets.Listen_Socket (Socket => L.Socket, + Length => 5); + if Result = Failure then + Put_Line ("ERROR: Failed to configure listener socket."); + SPARK_Sockets.Close_Socket (L); + return; + end if; -- Create and initialize WOLFSSL_CTX. WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Server_Method, Context => Ctx); if not WolfSSL.Is_Valid (Ctx) then Put_Line ("ERROR: failed to create WOLFSSL_CTX."); + SPARK_Sockets.Close_Socket (L); Set (Exit_Status_Failure); return; end if; @@ -144,10 +166,12 @@ package body Tls_Server is File => CERT_FILE, Format => WolfSSL.Format_Pem); if Result = Failure then - M := Messages.To_Bounded_String ("ERROR: failed to load "); - Messages.Append (M, CERT_FILE); - Messages.Append (M, ", please check the file."); - Put_Line (M); + Put ("ERROR: failed to load "); + Put (CERT_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -157,10 +181,12 @@ package body Tls_Server is File => KEY_FILE, Format => WolfSSL.Format_Pem); if Result = Failure then - M := Messages.To_Bounded_String ("ERROR: failed to load "); - Messages.Append (M, KEY_FILE); - Messages.Append (M, ", please check the file."); - Put_Line (M); + Put ("ERROR: failed to load "); + Put (KEY_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -170,39 +196,53 @@ package body Tls_Server is File => CA_FILE, Path => ""); if Result = Failure then - M := Messages.To_Bounded_String ("ERROR: failed to load "); - Messages.Append (M, CA_FILE); - Messages.Append (M, ", please check the file."); - Put_Line (M); + Put ("ERROR: failed to load "); + Put (CA_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; while Shall_Continue loop + pragma Loop_Invariant (not C.Exists and + not WolfSSL.Is_Valid (Ssl) and + WolfSSL.Is_Valid (Ctx)); + Put_Line ("Waiting for a connection..."); - begin - GNAT.Sockets.Accept_Socket (Server => L, - Socket => C, - Address => A); - exception - when Socket_Error => - Shall_Continue := False; - Put_Line ("ERROR: failed to accept the connection."); - end; + SPARK_Sockets.Accept_Socket (Server => L.Socket, + Socket => C, + Address => A, + Result => Result); + if Result = Failure then + Put_Line ("ERROR: failed to accept the connection."); + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + return; + end if; -- Create a WOLFSSL object. WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl); if not WolfSSL.Is_Valid (Ssl) then Put_Line ("ERROR: failed to create WOLFSSL object."); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; -- Attach wolfSSL to the socket. Result := WolfSSL.Attach (Ssl => Ssl, - Socket => GNAT.Sockets.To_C (C)); + Socket => SPARK_Sockets.To_C (C.Socket)); if Result = Failure then Put_Line ("ERROR: Failed to set the file descriptor."); + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -211,6 +251,10 @@ package body Tls_Server is Result := WolfSSL.Accept_Connection (Ssl); if Result = Failure then Put_Line ("Accept error."); + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -218,25 +262,27 @@ package body Tls_Server is Put_Line ("Client connected successfully."); Input := WolfSSL.Read (Ssl); - if Input.Result /= Success then Put_Line ("Read error."); + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; -- Print to stdout any data the client sends. - M := Messages.To_Bounded_String (""); for I in Input.Buffer'Range loop Ch := Character (Input.Buffer (I)); if Ada.Characters.Handling.Is_Graphic (Ch) then - Messages.Append (M, Ch); + Put (Ch); else null; -- Ignore the "newline" characters at end of message. end if; end loop; - Put_Line (M); + New_Line; -- Check for server shutdown command. if Input.Last >= 8 then @@ -252,12 +298,15 @@ package body Tls_Server is end if; Result := WolfSSL.Shutdown (Ssl); + if Result = Failure then + Put_Line ("ERROR: Failed to shutdown WolfSSL context."); + end if; WolfSSL.Free (Ssl); - GNAT.Sockets.Close_Socket (C); + SPARK_Sockets.Close_Socket (C); Put_Line ("Shutdown complete."); end loop; - GNAT.Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (L); WolfSSL.Free (Context => Ctx); WolfSSL.Finalize; end Run; diff --git a/wrapper/Ada/tls_server.ads b/wrapper/Ada/tls_server.ads index fccb6610b0..142fad2ce5 100644 --- a/wrapper/Ada/tls_server.ads +++ b/wrapper/Ada/tls_server.ads @@ -18,8 +18,22 @@ -- along with this program; if not, write to the Free Software -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA -- -package Tls_Server is - procedure Run; +-- SPARK wrapper package around GNAT Library packages. +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); + +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); + +package Tls_Server with SPARK_Mode is + + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + L : in out SPARK_Sockets.Optional_Socket; + C : in out SPARK_Sockets.Optional_Socket) with + Pre => (not C.Exists and not L.Exists and not + WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)), + Post => (not C.Exists and not L.Exists and not + WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)); end Tls_Server; diff --git a/wrapper/Ada/tls_server_main.adb b/wrapper/Ada/tls_server_main.adb index 7f34503355..80b3a88d79 100644 --- a/wrapper/Ada/tls_server_main.adb +++ b/wrapper/Ada/tls_server_main.adb @@ -21,9 +21,19 @@ with Tls_Server; pragma Elaborate_All (Tls_Server); +-- SPARK wrapper package around GNAT Library packages. +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); + +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); + -- Application entry point for the Ada translation of the -- tls server v1.3 example in C. procedure Tls_Server_Main is + Ssl : WolfSSL.WolfSSL_Type; + Ctx : WolfSSL.Context_Type; + L : SPARK_Sockets.Optional_Socket; + C : SPARK_Sockets.Optional_Socket; begin - Tls_Server.Run; + Tls_Server.Run (Ssl, Ctx, L, C); end Tls_Server_Main; From 71b28caa096864cd3e52b47b27f3d1aa7b2d444f Mon Sep 17 00:00:00 2001 From: Joakim Strandberg Date: Fri, 14 Jul 2023 22:20:39 +0200 Subject: [PATCH 4/6] Added Initialize and Finalize functions to initialize and cleanup resources of the WolfSSL library. Removed definitions of exceptions. --- wrapper/Ada/tls_client.adb | 11 ++++++++++- wrapper/Ada/tls_server.adb | 12 +++++++++++- wrapper/Ada/wolfssl.adb | 23 +++++++++++++++-------- wrapper/Ada/wolfssl.ads | 16 +++++----------- 4 files changed, 41 insertions(+), 21 deletions(-) diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index a003033538..9ebbb43b42 100644 --- a/wrapper/Ada/tls_client.adb +++ b/wrapper/Ada/tls_client.adb @@ -131,6 +131,12 @@ package body Tls_Client with SPARK_Mode is Result : WolfSSL.Subprogram_Result; begin + Result := WolfSSL.Initialize; + if Result = Failure then + Put_Line ("ERROR: Failed to initialize the WolfSSL library."); + return; + end if; + if Argument_Count < 1 then Put_Line ("usage: tcl_client "); return; @@ -297,7 +303,10 @@ package body Tls_Client with SPARK_Mode is SPARK_Sockets.Close_Socket (C); WolfSSL.Free (Ssl); WolfSSL.Free (Context => Ctx); - WolfSSL.Finalize; + Result := WolfSSL.Finalize; + if Result = Failure then + Put_Line ("ERROR: Failed to finalize the WolfSSL library."); + end if; end Run; end Tls_Client; diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 1eaca1349b..377db03a0a 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -111,6 +111,12 @@ package body Tls_Server with SPARK_Mode is Input : WolfSSL.Read_Result; Option : Option_Type; begin + Result := WolfSSL.Initialize; + if Result = Failure then + Put_Line ("ERROR: Failed to initialize the WolfSSL library."); + return; + end if; + SPARK_Sockets.Create_Socket (Socket => L); if not L.Exists then Put_Line ("ERROR: Failed to create socket."); @@ -308,7 +314,11 @@ package body Tls_Server with SPARK_Mode is end loop; SPARK_Sockets.Close_Socket (L); WolfSSL.Free (Context => Ctx); - WolfSSL.Finalize; + Result := WolfSSL.Finalize; + if Result = Failure then + Put_Line ("ERROR: Failed to finalize the WolfSSL library."); + return; + end if; end Run; end Tls_Server; diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb index 85c69d279e..8ce762540f 100644 --- a/wrapper/Ada/wolfssl.adb +++ b/wrapper/Ada/wolfssl.adb @@ -44,11 +44,23 @@ package body WolfSSL is External_Name => "wolfSSL_Cleanup", Import => True; - procedure Finalize is + function Initialize return Subprogram_Result is + Result : constant int := Initialize_WolfSSL; + begin + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; + end if; + end Initialize; + + function Finalize return Subprogram_Result is Result : constant int := Finalize_WolfSSL; begin - if Result /= WOLFSSL_SUCCESS then - raise Cleanup_Error; + if Result = WOLFSSL_SUCCESS then + return Success; + else + return Failure; end if; end Finalize; @@ -728,9 +740,4 @@ package body WolfSSL is Ssl := null; end Free; - Result : constant int := Initialize_WolfSSL; -begin - if Result /= WOLFSSL_SUCCESS then - raise Initialization_Error; - end if; end WolfSSL; diff --git a/wrapper/Ada/wolfssl.ads b/wrapper/Ada/wolfssl.ads index 02c04ef332..4fa7783960 100644 --- a/wrapper/Ada/wolfssl.ads +++ b/wrapper/Ada/wolfssl.ads @@ -25,17 +25,13 @@ with Interfaces.C; -- the API of this package is used correctly. package WolfSSL with SPARK_Mode is - procedure Finalize; - -- Must be called before application exit. + type Subprogram_Result is (Success, Failure); - Initialization_Error : exception; - -- Raised if error was encountered during initialization of the - -- WolfSSL library. The WolfSSL libray is initialized during - -- elaboration time. + function Initialize return Subprogram_Result; + -- Must be called before usage of the WolfSSL library. - Cleanup_Error : exception; - -- Raised if error was encountered during application shutdown - -- and cleanup of resources allocated by WolfSSL has failed. + function Finalize return Subprogram_Result; + -- Must be called before application exit to cleanup resources. subtype char_array is Interfaces.C.char_array; -- Remove? @@ -43,8 +39,6 @@ package WolfSSL with SPARK_Mode is subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000; subtype Byte_Array is Interfaces.C.char_array; - type Subprogram_Result is (Success, Failure); - type Context_Type is limited private; function Is_Valid (Context : Context_Type) return Boolean; From 00b90adc97cebd4f914221b27467aceebab7dc46 Mon Sep 17 00:00:00 2001 From: Joakim Strandberg Date: Mon, 17 Jul 2023 01:22:06 +0200 Subject: [PATCH 5/6] 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. --- wrapper/Ada/README.md | 96 ++++++++++- wrapper/Ada/ada_binding.c | 21 ++- wrapper/Ada/tls_client.adb | 58 ++++--- wrapper/Ada/tls_server.adb | 48 +++--- wrapper/Ada/wolfssl.adb | 227 ++++++++++--------------- wrapper/Ada/wolfssl.ads | 329 +++++++++++++++++++++++++++++++++++-- 6 files changed, 573 insertions(+), 206 deletions(-) diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md index 64ca8d13a3..0e0d39e011 100644 --- a/wrapper/Ada/README.md +++ b/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 \ No newline at end of file diff --git a/wrapper/Ada/ada_binding.c b/wrapper/Ada/ada_binding.c index 9403b5c78f..0becb0e7e0 100644 --- a/wrapper/Ada/ada_binding.c +++ b/wrapper/Ada/ada_binding.c @@ -21,14 +21,17 @@ /* wolfSSL */ #include - #include /* 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; } diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index 9ebbb43b42..a60f5618a4 100644 --- a/wrapper/Ada/tls_client.adb +++ b/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; diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 377db03a0a..797d23caed 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -31,8 +31,9 @@ package body Tls_Server 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; + Success : WolfSSL.Subprogram_Result renames WolfSSL.Success; procedure Put (Char : Character) is begin @@ -106,13 +107,12 @@ package body Tls_Server with SPARK_Mode is Result : WolfSSL.Subprogram_Result; Shall_Continue : Boolean := True; - Bytes_Written : Integer; - - Input : WolfSSL.Read_Result; + Input : WolfSSL.Read_Result; + Output : WolfSSL.Write_Result; Option : Option_Type; begin Result := WolfSSL.Initialize; - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: Failed to initialize the WolfSSL library."); return; end if; @@ -127,7 +127,7 @@ package body Tls_Server with SPARK_Mode is Result := SPARK_Sockets.Set_Socket_Option (Socket => L.Socket, Level => Socket_Level, Option => Option); - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: Failed to set socket option."); SPARK_Sockets.Close_Socket (L); return; @@ -138,7 +138,7 @@ package body Tls_Server with SPARK_Mode is Port => P); Result := SPARK_Sockets.Bind_Socket (Socket => L.Socket, Address => A); - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: Failed to bind socket."); SPARK_Sockets.Close_Socket (L); return; @@ -146,7 +146,7 @@ package body Tls_Server with SPARK_Mode is Result := SPARK_Sockets.Listen_Socket (Socket => L.Socket, Length => 5); - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: Failed to configure listener socket."); SPARK_Sockets.Close_Socket (L); return; @@ -171,7 +171,7 @@ package body Tls_Server 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."); @@ -186,7 +186,7 @@ package body Tls_Server 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."); @@ -201,7 +201,7 @@ package body Tls_Server 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."); @@ -213,16 +213,16 @@ package body Tls_Server with SPARK_Mode is end if; while Shall_Continue loop - pragma Loop_Invariant (not C.Exists and - not WolfSSL.Is_Valid (Ssl) and - WolfSSL.Is_Valid (Ctx)); + pragma Loop_Invariant (not C.Exists); + pragma Loop_Invariant (not WolfSSL.Is_Valid (Ssl)); + pragma Loop_Invariant (WolfSSL.Is_Valid (Ctx)); Put_Line ("Waiting for a connection..."); SPARK_Sockets.Accept_Socket (Server => L.Socket, Socket => C, Address => A, Result => Result); - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: failed to accept the connection."); SPARK_Sockets.Close_Socket (L); WolfSSL.Free (Context => Ctx); @@ -243,7 +243,7 @@ package body Tls_Server 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."); WolfSSL.Free (Ssl); SPARK_Sockets.Close_Socket (L); @@ -255,7 +255,7 @@ package body Tls_Server with SPARK_Mode is -- Establish TLS connection. Result := WolfSSL.Accept_Connection (Ssl); - if Result = Failure then + if Result /= Success then Put_Line ("Accept error."); WolfSSL.Free (Ssl); SPARK_Sockets.Close_Socket (L); @@ -268,7 +268,7 @@ package body Tls_Server with SPARK_Mode is Put_Line ("Client connected successfully."); Input := WolfSSL.Read (Ssl); - if Input.Result /= Success then + if not Input.Success then Put_Line ("Read error."); WolfSSL.Free (Ssl); SPARK_Sockets.Close_Socket (L); @@ -298,13 +298,15 @@ package body Tls_Server with SPARK_Mode is end if; end if; - Bytes_Written := WolfSSL.Write (Ssl, Reply); - if Bytes_Written /= Reply'Length then - Put_Line ("ERROR: failed to write."); + Output := WolfSSL.Write (Ssl, Reply); + if not Output.Success then + Put_Line ("ERROR: write failure."); + elsif Output.Bytes_Written /= Reply'Length then + Put_Line ("ERROR: failed to write full response."); end if; Result := WolfSSL.Shutdown (Ssl); - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: Failed to shutdown WolfSSL context."); end if; WolfSSL.Free (Ssl); @@ -315,7 +317,7 @@ package body Tls_Server with SPARK_Mode is SPARK_Sockets.Close_Socket (L); WolfSSL.Free (Context => Ctx); Result := WolfSSL.Finalize; - if Result = Failure then + if Result /= Success then Put_Line ("ERROR: Failed to finalize the WolfSSL library."); return; end if; diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb index 8ce762540f..f1eac8f8ae 100644 --- a/wrapper/Ada/wolfssl.adb +++ b/wrapper/Ada/wolfssl.adb @@ -26,11 +26,7 @@ package body WolfSSL is subtype size_t is Interfaces.C.size_t; use type size_t; subtype long is Interfaces.C.long; - - function Get_WolfSSL_Success return int with - Convention => C, - External_Name => "get_wolfssl_success", - Import => True; + subtype unsigned_long is Interfaces.C.unsigned_long; WOLFSSL_SUCCESS : constant int := Get_WolfSSL_Success; @@ -47,21 +43,13 @@ package body WolfSSL is function Initialize return Subprogram_Result is Result : constant int := Initialize_WolfSSL; begin - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Initialize; function Finalize return Subprogram_Result is Result : constant int := Finalize_WolfSSL; begin - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Finalize; function Is_Valid (Context : Context_Type) return Boolean is @@ -79,6 +67,16 @@ package body WolfSSL is return WolfTLSv1_2_Server_Method; end TLSv1_2_Server_Method; + function WolfTLSv1_2_Client_Method return Method_Type with + Convention => C, + External_Name => "wolfTLSv1_2_client_method", + Import => True; + + function TLSv1_2_Client_Method return Method_Type is + begin + return WolfTLSv1_2_Client_Method; + end TLSv1_2_Client_Method; + function WolfTLSv1_3_Server_Method return Method_Type with Convention => C, External_Name => "wolfTLSv1_3_server_method", @@ -198,11 +196,7 @@ package body WolfSSL is Count => C, Append_Nul => True); Result := Use_Certificate_File (Ctx, F (1 .. C), int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Certificate_File; function Use_Certificate_Buffer (Context : Context_Type; @@ -222,11 +216,7 @@ package body WolfSSL is begin Result := Use_Certificate_Buffer (Context, Input, Input'Length, int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Certificate_Buffer; function Use_Private_Key_File (Context : Context_Type; @@ -251,11 +241,7 @@ package body WolfSSL is Count => C, Append_Nul => True); Result := Use_Private_Key_File (Ctx, F (1 .. C), int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Private_Key_File; function Use_Private_Key_Buffer (Context : Context_Type; @@ -275,11 +261,7 @@ package body WolfSSL is begin Result := Use_Private_Key_Buffer (Context, Input, Input'Length, int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Private_Key_Buffer; function Load_Verify_Locations1 @@ -375,11 +357,7 @@ package body WolfSSL is Path => P); end if; end if; - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Load_Verify_Locations; function Load_Verify_Buffer @@ -390,14 +368,6 @@ package body WolfSSL is Convention => C, External_Name => "wolfSSL_CTX_load_verify_buffer", Import => True; - -- This function loads a CA certificate buffer into the WOLFSSL - -- Context. It behaves like the non-buffered version, only differing - -- in its ability to be called with a buffer as input instead of - -- a file. The buffer is provided by the in argument of size sz. - -- format specifies the format type of the buffer; SSL_FILETYPE_ASN1 - -- or SSL_FILETYPE_PEM. More than one CA certificate may be loaded - -- per buffer as long as the format is in PEM. Please see - -- the examples for proper usage. function Load_Verify_Buffer (Context : Context_Type; Input : Byte_Array; @@ -409,11 +379,7 @@ package body WolfSSL is Input => Input, Size => Input'Length, Format => int(Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Load_Verify_Buffer; function Is_Valid (Ssl : WolfSSL_Type) return Boolean is @@ -454,11 +420,7 @@ package body WolfSSL is Count => C, Append_Nul => True); Result := Use_Certificate_File (Ssl, F (1 .. C), int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Certificate_File; function Use_Certificate_Buffer (Ssl : WolfSSL_Type; @@ -478,11 +440,7 @@ package body WolfSSL is begin Result := Use_Certificate_Buffer (Ssl, Input, Input'Length, int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Certificate_Buffer; function Use_Private_Key_File (Ssl : WolfSSL_Type; @@ -506,11 +464,7 @@ package body WolfSSL is Count => C, Append_Nul => True); Result := Use_Private_Key_File (Ssl, F (1 .. C), int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Private_Key_File; function Use_Private_Key_Buffer (Ssl : WolfSSL_Type; @@ -530,11 +484,7 @@ package body WolfSSL is begin Result := Use_Private_Key_Buffer (Ssl, Input, Input'Length, int (Format)); - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Use_Private_Key_Buffer; function WolfSSL_Set_Fd (Ssl : WolfSSL_Type; Fd : int) return int with @@ -547,11 +497,7 @@ package body WolfSSL is return Subprogram_Result is Result : int := WolfSSL_Set_Fd (Ssl, int (Socket)); begin - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Attach; procedure WolfSSL_Keep_Arrays (Ssl : WolfSSL_Type) with @@ -573,11 +519,7 @@ package body WolfSSL is return Subprogram_Result is Result : int := WolfSSL_Accept (Ssl); begin - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Accept_Connection; procedure WolfSSL_Free_Arrays (Ssl : WolfSSL_Type) with @@ -631,12 +573,14 @@ package body WolfSSL is Size : int; begin Size := WolfSSL_Read (Ssl, Data, int (Byte_Index'Last)); - if Size < 0 then - return (Result => Failure, Last => 0); + if Size <= 0 then + return (Success => False, + Last => 0, + Code => Subprogram_Result (Size)); else - return (Result => Success, - Last => Byte_Index (Size), - Buffer => Data (1 .. Byte_Index (Size))); + return (Success => True, + Last => Byte_Index (Size), + Buffer => Data (1 .. Byte_Index (Size))); end if; end Read; @@ -648,83 +592,39 @@ package body WolfSSL is Import => True; function Write (Ssl : WolfSSL_Type; - Data : Byte_Array) return Integer is + Data : Byte_Array) return Write_Result is Size : constant int := Data'Length; Result : int; begin Result := WolfSSL_Write (Ssl, Data, Size); - return Integer (Result); + if Result > 0 then + return (Success => True, + Bytes_Written => Byte_Index (Result)); + else + return (Success => False, Code => Subprogram_Result (Result)); + end if; end Write; function WolfSSL_Shutdown (Ssl : WolfSSL_Type) return int with Convention => C, External_Name => "wolfSSL_shutdown", Import => True; - -- This function shuts down an active SSL/TLS connection using - -- the SSL session, ssl. This function will try to send a - -- "close notify" alert to the peer. The calling application can - -- choose to wait for the peer to send its "close notify" alert - -- in response or just go ahead and shut down the underlying - -- connection after directly calling wolfSSL_shutdown (to save - -- resources). Either option is allowed by the TLS specification. - -- If the underlying connection will be used again in the future, - -- the complete two_directional shutdown procedure must be performed - -- to keep synchronization intact between the peers. - -- wolfSSL_shutdown() works with both blocking and non_blocking I/O. - -- When the underlying I/O is non_blocking, wolfSSL_shutdown() will - -- return an error if the underlying I/O could not satisfy the needs - -- of wolfSSL_shutdown() to continue. In this case, a call to - -- wolfSSL_get_error() will yield either SSL_ERROR_WANT_READ or - -- SSL_ERROR_WANT_WRITE. The calling process must then repeat - -- the call to wolfSSL_shutdown() when the underlying I/O is ready. function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result is Result : constant int := WolfSSL_Shutdown (Ssl); begin - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Shutdown; function WolfSSL_Connect (Ssl : WolfSSL_Type) return int with Convention => C, External_Name => "wolfSSL_connect", Import => True; - -- This function is called on the client side and initiates - -- an SSL/TLS handshake with a server. When this function is called, - -- the underlying communication channel has already been set up. - -- wolfSSL_connect() works with both blocking and non_blocking I/O. - -- When the underlying I/O is non_blocking, wolfSSL_connect() will - -- return when the underlying I/O could not satisfy the needs - -- of wolfSSL_connect to continue the handshake. In this case, - -- a call to wolfSSL_get_error() will yield either - -- SSL_ERROR_WANT_READ or SSL_ERROR_WANT_WRITE. The calling process - -- must then repeat the call to wolfSSL_connect() when - -- the underlying I/O is ready and wolfSSL will pick up where - -- it left off. When using a non_blocking socket, nothing needs - -- to be done, but select() can be used to check for the required - -- condition. If the underlying I/O is blocking, wolfSSL_connect() - -- will only return once the handshake has been finished or an error - -- occurred. wolfSSL takes a different approach to certificate - -- verification than OpenSSL does. The default policy for the client - -- is to verify the server, this means that if you don't load CAs - -- to verify the server you'll get a connect error, - -- unable to verify (_155). It you want to mimic OpenSSL behavior - -- of having SSL_connect succeed even if verifying the server fails - -- and reducing security you can do this by calling: - -- SSL_CTX_set_verify(ctx, SSL_VERIFY_NONE, 0); before calling - -- SSL_new(); Though it's not recommended. function Connect (Ssl : WolfSSL_Type) return Subprogram_Result is Result : constant int := WolfSSL_Connect (Ssl); begin - if Result = WOLFSSL_SUCCESS then - return Success; - else - return Failure; - end if; + return Subprogram_Result (Result); end Connect; procedure WolfSSL_Free (Ssl : WolfSSL_Type) with @@ -740,4 +640,49 @@ package body WolfSSL is Ssl := null; end Free; + function WolfSSL_Get_Error (Ssl : WolfSSL_Type; + Ret : int) return int with + Convention => C, + External_Name => "wolfSSL_get_error", + Import => True; + + function Get_Error (Ssl : WolfSSL_Type; + Result : Subprogram_Result) return Error_Code is + begin + return Error_Code (WolfSSL_Get_Error (Ssl, int (Result))); + end Get_Error; + + procedure WolfSSL_Error_String (Error : unsigned_long; + Data : out Byte_Array; + Size : unsigned_long) with + Convention => C, + External_Name => "wolfSSL_ERR_error_string_n", + Import => True; + + function Error (Code : Error_Code) return Error_Message is + S : String (1 .. Error_Message_Index'Last); + B : Byte_Array (1 .. size_t (Error_Message_Index'Last)); + C : Natural; + begin + WolfSSL_Error_String (Error => unsigned_long (Code), + Data => B, + Size => unsigned_long (B'Last)); + Interfaces.C.To_Ada (Item => B, + Target => S, + Count => C, + Trim_Nul => True); + return (Last => C, + Text => S (1 .. C)); + end Error; + + function Get_WolfSSL_Max_Error_Size return int with + Convention => C, + External_Name => "get_wolfssl_max_error_size", + Import => True; + + function Max_Error_Size return Natural is + begin + return Natural (Get_WolfSSL_Max_Error_Size); + end Max_Error_Size; + end WolfSSL; diff --git a/wrapper/Ada/wolfssl.ads b/wrapper/Ada/wolfssl.ads index 4fa7783960..a3f536e5d4 100644 --- a/wrapper/Ada/wolfssl.ads +++ b/wrapper/Ada/wolfssl.ads @@ -25,13 +25,18 @@ with Interfaces.C; -- the API of this package is used correctly. package WolfSSL with SPARK_Mode is - type Subprogram_Result is (Success, Failure); + type Subprogram_Result is new Integer; + Success : constant Subprogram_Result; + Failure : constant Subprogram_Result; function Initialize return Subprogram_Result; - -- Must be called before usage of the WolfSSL library. + -- Initializes the wolfSSL library for use. Must be called once per + -- application and before any other call to the library. function Finalize return Subprogram_Result; - -- Must be called before application exit to cleanup resources. + -- Un-initializes the wolfSSL library from further use. + -- Doesn't have to be called, though it will free any resources + -- used by the library. subtype char_array is Interfaces.C.char_array; -- Remove? @@ -40,45 +45,86 @@ package WolfSSL with SPARK_Mode is subtype Byte_Array is Interfaces.C.char_array; type Context_Type is limited private; + -- Instances of this type are called SSL Contexts. function Is_Valid (Context : Context_Type) return Boolean; + -- Indicates if the SSL Context has successfully been initialized. + -- If initialized, the SSL Context has allocated resources + -- that needs to be deallocated before application exit. type Method_Type is limited private; function TLSv1_2_Server_Method return Method_Type; + -- This function is used to indicate that the application is a server + -- and will only support the TLS 1.2 protocol. + + function TLSv1_2_Client_Method return Method_Type; + -- This function is used to indicate that the application is a client + -- and will only support the TLS 1.2 protocol. + function TLSv1_3_Server_Method return Method_Type; + -- This function is used to indicate that the application is a server + -- and will only support the TLS 1.3 protocol. + function TLSv1_3_Client_Method return Method_Type; + -- This function is used to indicate that the application is a client + -- and will only support the TLS 1.3 protocol. procedure Create_Context (Method : Method_Type; Context : out Context_Type); - -- Create and initialize a WolfSSL context. + -- This function creates a new SSL context, taking a desired SSL/TLS + -- protocol method for input. -- If successful Is_Valid (Context) = True, otherwise False. procedure Free (Context : in out Context_Type) with Pre => Is_Valid (Context), Post => not Is_Valid (Context); + -- This function frees an allocated SSL Context object. type Mode_Type is private; function "&" (Left, Right : Mode_Type) return Mode_Type; Verify_None : constant Mode_Type; + -- Client mode: the client will not verify the certificate received + -- from the server and the handshake will continue as normal. + -- + -- Server mode: the server will not send a certificate request to + -- the client. As such, client verification will not be enabled. Verify_Peer : constant Mode_Type; + -- Client mode: the client will verify the certificate received from + -- the server during the handshake. This is turned on by default + -- in wolfSSL, therefore, using this option has no effect. + -- + -- Server mode: the server will send a certificate request to + -- the client and verify the client certificate received. Verify_Fail_If_No_Peer_Cert : constant Mode_Type; + -- Client mode: no effect when used on the client side. + -- + -- Server mode: the verification will fail on the server side if + -- the client fails to send a certificate when requested to do so + -- (when using Verify_Peer on the SSL server). Verify_Client_Once : constant Mode_Type; Verify_Post_Handshake : constant Mode_Type; Verify_Fail_Except_Psk : constant Mode_Type; + -- Client mode: no effect when used on the client side. + -- + -- Server mode: the verification is the same as + -- Verify_Fail_If_No_Peer_Cert except in the case of a PSK connection. + -- If a PSK connection is being made then the connection + -- will go through without a peer cert. Verify_Default : constant Mode_Type; procedure Set_Verify (Context : Context_Type; Mode : Mode_Type) with Pre => Is_Valid (Context); + -- This function sets the verification method for remote peers type File_Format is private; @@ -91,115 +137,334 @@ package WolfSSL with SPARK_Mode is Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Context); + -- This function loads a certificate file into the SSL context. + -- The file is provided by the file argument. The format argument + -- specifies the format type of the file, either ASN1 or + -- PEM file types. Please see the examples for proper usage. function Use_Certificate_Buffer (Context : Context_Type; Input : char_array; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Context); + -- This function loads a certificate buffer into the SSL Context. + -- It behaves like the non-buffered version (Use_Certificate_File), + -- only differing in its ability to be called with a buffer as input + -- instead of a file. The buffer is provided by the Input argument. + -- Format specifies the format type of the buffer; ASN1 or PEM. + -- Please see the examples for proper usage. function Use_Private_Key_File (Context : Context_Type; File : String; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Context); + -- This function loads a private key file into the SSL context. + -- The file is provided by the File argument. The Format argument + -- specifies the format type of the file - ASN1 or PEM. + -- Please see the examples for proper usage. function Use_Private_Key_Buffer (Context : Context_Type; Input : Byte_Array; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Context); + -- This function loads a private key buffer into the SSL Context. + -- It behaves like the non-buffered version (Use_Private_Key_File), + -- only differing in its ability to be called with a buffer as input + -- instead of a file. The buffer is provided by the Input argument. + -- Format specifies the format type of the buffer; ASN1 or PEM. + -- Please see the examples for proper usage. function Load_Verify_Locations (Context : Context_Type; File : String; Path : String) return Subprogram_Result with Pre => Is_Valid (Context); + -- This function loads PEM-formatted CA certificate files into + -- the SSL context. These certificates will be treated as trusted + -- root certificates and used to verify certs received from peers + -- during the SSL handshake. The root certificate file, + -- provided by the File argument, may be a single certificate or + -- a file containing multiple certificates. If multiple CA certs + -- are included in the same file, wolfSSL will load them in the same + -- order they are presented in the file. The path argument is + -- a pointer to the name of a directory that contains certificates + -- of trusted root CAs. If the value of File is not empty "", + -- path may be specified as "" if not needed. If path is specified + -- and NO_WOLFSSL_DIR was not defined when building the library, + -- wolfSSL will load all CA certificates located in the given + -- directory. This function will attempt to load all files in + -- the directory. This function expects PEM formatted CERT_TYPE file + -- with header "--BEGIN CERTIFICATE--". function Load_Verify_Buffer (Context : Context_Type; Input : Byte_Array; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Context); + -- This function loads a CA certificate buffer into the SSL + -- Context. It behaves like the non-buffered version, only differing + -- in its ability to be called with a buffer as input instead of + -- a file. The buffer is provided by the Input argument. + -- Format specifies the format type of the buffer; ASN1 or PEM. + -- More than one CA certificate may be loaded + -- per buffer as long as the format is in PEM. + -- Please see the examples for proper usage. type WolfSSL_Type is limited private; + -- Instances of this type are called SSL Sessions. function Is_Valid (Ssl : WolfSSL_Type) return Boolean; + -- Indicates if the SSL Session has successfully been initialized. + -- If initialized, the SSL Session has allocated resources + -- that needs to be deallocated before application exit. procedure Create_WolfSSL (Context : Context_Type; Ssl : out WolfSSL_Type) with Pre => Is_Valid (Context); - + -- This function creates a new SSL session, taking an already created + -- SSL context as input. + -- If successful Is_Valid (Ssl) = True, otherwise False. function Use_Certificate_File (Ssl : WolfSSL_Type; File : String; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- This function loads a certificate file into the SSL session. + -- The certificate file is provided by the file argument. + -- The format argument specifies the format type of the file + -- either ASN1 or PEM. function Use_Certificate_Buffer (Ssl : WolfSSL_Type; Input : char_array; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- This function loads a certificate buffer into the SSL session + -- object. It behaves like the non-buffered version, only differing + -- in its ability to be called with a buffer as input instead + -- of a file. The buffer is provided by the Input argument. + -- Format specifies the format type of the buffer; ASN1 or PEM. + -- Please see the examples for proper usage. function Use_Private_Key_File (Ssl : WolfSSL_Type; File : String; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- This function loads a private key file into the SSL session. + -- The key file is provided by the File argument. The Format argument + -- specifies the format type of the file - ASN1 or PEM. function Use_Private_Key_Buffer (Ssl : WolfSSL_Type; Input : Byte_Array; Format : File_Format) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- This function loads a private key buffer into the SSL session + -- object. It behaves like the non-buffered version, only differing + -- in its ability to be called with a buffer as input instead + -- of a file. The buffer is provided by the Input argument. + -- Format specifies the format type of the buffer; ASN1 or PEM. + -- Please see the examples for proper usage. - -- Attach wolfSSL to the socket. function Attach (Ssl : WolfSSL_Type; Socket : Integer) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- Attach wolfSSL to the socket. + -- + -- This function assigns a file descriptor (Socket) as + -- the input/output facility for the SSL connection. + -- Typically this will be a socket file descriptor. procedure Keep_Arrays (Ssl : WolfSSL_Type) with Pre => Is_Valid (Ssl); - -- Don't free temporary arrays at end of handshake. + -- Normally, at the end of the SSL handshake, wolfSSL frees + -- temporary arrays. Calling this function before the handshake + -- begins will prevent wolfSSL from freeing temporary arrays. + -- Temporary arrays may be needed for things such as + -- wolfSSL_get_keys() or PSK hints. When the user is done with + -- temporary arrays, either Free_Arrays(..) may be called to free + -- the resources immediately, or alternatively the resources will + -- be freed when the associated SSL object is freed. procedure Free_Arrays (Ssl : WolfSSL_Type) with Pre => Is_Valid (Ssl); - -- User doesn't need temporary arrays anymore, Free. + -- Normally, at the end of the SSL handshake, wolfSSL frees temporary + -- arrays. If Keep_Arrays(..) has been called before the handshake, + -- wolfSSL will not free temporary arrays. This function explicitly + -- frees temporary arrays and should be called when the user is done + -- with temporary arrays and does not want to wait for the SSL object + -- to be freed to free these resources. function Accept_Connection (Ssl : WolfSSL_Type) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- The name of this function is not Accept (..) because the word + -- "accept" is a reserved keyword in the Ada language. + -- + -- This function is called on the server side and waits for an + -- SSL client to initiate the SSL/TLS handshake. When this function + -- is called, the underlying communication channel has already been + -- set up. This function works with both blocking and + -- non-blocking I/O. When the underlying I/O is non-blocking, + -- Accept_Connection (..) will return when the underlying I/O could + -- not satisfy the needs of Accept_Connection (..) to continue + -- the handshake. In this case, a call to Get_Error(..) will + -- yield either Error_Want_Read or Error_Want_Write. + -- The calling process must then repeat the call to + -- Accept_Connection (..) when data is available to read and + -- wolfSSL will pick up where it left off. When using a + -- non_blocking socket, nothing needs to be done, but select() can + -- be used to check for the required condition. + -- If the underlying I/O is blocking, Accept_Connection (..) will + -- only return once the handshake has been finished or + -- an error occurred. -- This record type has discriminants with default values to be able - -- to compile this code under the restriction no secondary stack. - type Read_Result (Result : Subprogram_Result := Failure; - Last : Byte_Index := Byte_Index'Last) is record - case Result is - when Success => Buffer : Byte_Array (1 .. Last); - when Failure => null; + -- to compile this code under the restriction No Secondary Stack. + type Read_Result (Success : Boolean := False; + Last : Byte_Index := Byte_Index'Last) is record + case Success is + when True => Buffer : Byte_Array (1 .. Last); + when False => Code : Subprogram_Result; -- Error code end case; end record; function Read (Ssl : WolfSSL_Type) return Read_Result with Pre => Is_Valid (Ssl); + -- This function reads a number of bytes from the SSL session (ssl) + -- internal read buffer into the buffer data. The bytes read are + -- removed from the internal receive buffer. + -- If necessary Read(..) will negotiate an SSL/TLS session + -- if the handshake has not already + -- been performed yet by Connect(..) or Accept_Connection (..). + -- The SSL/TLS protocol uses SSL records which have a maximum size + -- of 16kB (the max record size can be controlled by the + -- MAX_RECORD_SIZE define in /wolfssl/internal.h). As such, wolfSSL + -- needs to read an entire SSL record internally before it is able + -- to process and decrypt the record. Because of this, a call to + -- Read(..) will only be able to return the maximum buffer + -- size which has been decrypted at the time of calling. There may + -- be additional not-yet-decrypted data waiting in the internal + -- wolfSSL receive buffer which will be retrieved and decrypted with + -- the next call to Read(..). + + -- This record type has discriminants with default values to be able + -- to compile this code under the restriction No Secondary Stack. + type Write_Result (Success : Boolean := False) is record + case Success is + when True => Bytes_Written : Byte_Index; + when False => Code : Subprogram_Result; -- Error code + end case; + end record; - -- The number of bytes written is returned. function Write (Ssl : WolfSSL_Type; - Data : Byte_Array) return Integer with + Data : Byte_Array) return Write_Result with Pre => Is_Valid (Ssl); + -- The number of bytes written is returned. + -- This function writes bytes from the buffer, Data, + -- to the SSL connection, ssl. If necessary, Write(..) will + -- negotiate an SSL/TLS session if the handshake has not already + -- been performed yet by Connect(..) or Accept_Connection(..). + -- Write(..) works with both blocking and non-blocking I/O. + -- When the underlying I/O is non-blocking, Write(..) will return + -- when the underlying I/O could not satisfy the needs of Write(..) + -- to continue. In this case, a call to Get_Error(..) will + -- yield either Error_Want_Read or Error_Want_Write. + -- The calling process must then repeat the call to Write(..) + -- when the underlying I/O is ready. If the underlying I/O is + -- blocking, Write(..) will only return once the buffer data + -- has been completely written or an error occurred. function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- This function shuts down an active SSL/TLS connection using + -- the SSL session, ssl. This function will try to send a + -- "close notify" alert to the peer. The calling application can + -- choose to wait for the peer to send its "close notify" alert + -- in response or just go ahead and shut down the underlying + -- connection after directly calling wolfSSL_shutdown (to save + -- resources). Either option is allowed by the TLS specification. + -- If the underlying connection will be used again in the future, + -- the complete two_directional shutdown procedure must be performed + -- to keep synchronization intact between the peers. + -- Shutdown(..) works with both blocking and non_blocking I/O. + -- When the underlying I/O is non_blocking, Shutdown(..) will + -- return an error if the underlying I/O could not satisfy the needs + -- of Shutdown(..) to continue. In this case, a call to + -- Get_Error(..) will yield either Error_Want_Read or + -- Error_Want_Write. The calling process must then repeat + -- the call to Shutdown() when the underlying I/O is ready. procedure Free (Ssl : in out WolfSSL_Type) with Pre => Is_Valid (Ssl), Post => not Is_Valid (Ssl); + -- Frees the resources allocated by the SSL session object. function Connect (Ssl : WolfSSL_Type) return Subprogram_Result with Pre => Is_Valid (Ssl); + -- This function is called on the client side and initiates + -- an SSL/TLS handshake with a server. When this function is called, + -- the underlying communication channel has already been set up. + -- Connect(..) works with both blocking and non_blocking I/O. + -- When the underlying I/O is non_blocking, Connect(..) will + -- return when the underlying I/O could not satisfy the needs + -- of wolfSSL_connect to continue the handshake. In this case, + -- a call to Get_Error(..) will yield either + -- Error_Want_Read or SSL_ERROR_WANT_WRITE. The calling process + -- must then repeat the call to Connect(..) when + -- the underlying I/O is ready and wolfSSL will pick up where + -- it left off. When using a non_blocking socket, nothing needs + -- to be done, but select() can be used to check for the required + -- condition. If the underlying I/O is blocking, Connect(..) + -- will only return once the handshake has been finished or an error + -- occurred. wolfSSL takes a different approach to certificate + -- verification than OpenSSL does. The default policy for the client + -- is to verify the server, this means that if you don't load CAs + -- to verify the server you'll get a connect error, + -- unable to verify. It you want to mimic OpenSSL behavior + -- of having SSL_connect succeed even if verifying the server fails + -- and reducing security you can do this by calling: + -- Set_Verify (Ctx, Verify_None, 0); before calling + -- Create_WolfSSL(...); Though it's not recommended. + + type Error_Code is new Integer; + + Error_Want_Read : constant Error_Code; + Error_Want_Write : constant Error_Code; + + function Get_Error (Ssl : WolfSSL_Type; + Result : Subprogram_Result) return Error_Code; + -- This function returns a unique error code describing why + -- the previous API function call (Connect, Accept_Connection, + -- Read, Write, etc.) resulted in an error return code. + -- After Get_Error is called and returns the unique error code, + -- wolfSSL_ERR_error_string() may be called to get a human readable + -- error string. + + subtype Error_Message_Index is Natural range 0 .. 80; + -- The default error message length is 80 in WolfSSL unless + -- configured to another value. See the result + -- of the Max_Error_Size function. + + type Error_Message (Last : Error_Message_Index := 0) is record + Text : String (1 .. Last); + end record; + + function Error (Code : Error_Code) return Error_Message; + -- This function converts an error code returned by Get_Error(..) + -- into a more human readable error string. Code is the error code + -- returned by Get_error(). The maximum length of error strings is + -- 80 characters by default, as defined by MAX_ERROR_SZ + -- is wolfssl/wolfcrypt/error.h. + + function Max_Error_Size return Natural; + -- Returns the value of the defined MAX_ERROR_SZ integer + -- in wolfssl/wolfcrypt/error.h. private pragma SPARK_Mode (Off); @@ -306,4 +571,36 @@ private Format_Default : constant File_Format := File_Format (WolfSSL_Filetype_Default); + function Get_WolfSSL_Success return int with + Convention => C, + External_Name => "get_wolfssl_success", + Import => True; + + function Get_WolfSSL_Failure return int with + Convention => C, + External_Name => "get_wolfssl_failure", + Import => True; + + Success : constant Subprogram_Result := + Subprogram_Result (Get_WolfSSL_Success); + + Failure : constant Subprogram_Result := + Subprogram_Result (Get_WolfSSL_Failure); + + function Get_WolfSSL_Error_Want_Read return int with + Convention => C, + External_Name => "get_wolfssl_error_want_read", + Import => True; + + function Get_WolfSSL_Error_Want_Write return int with + Convention => C, + External_Name => "get_wolfssl_error_want_write", + Import => True; + + Error_Want_Read : constant Error_Code := + Error_Code (Get_WolfSSL_Error_Want_Read); + + Error_Want_Write : constant Error_Code := + Error_Code (Get_WolfSSL_Error_Want_Write); + end WolfSSL; From 58ac57861f3d4768dfbd41dbf235ad72cea490ea Mon Sep 17 00:00:00 2001 From: Joakim Strandberg Date: Mon, 17 Jul 2023 19:50:05 +0200 Subject: [PATCH 6/6] Updated the README.md file and made sure that using default.gpr to build the Ada TLS server application does not try to build the Ada TCL client application that makes use of the secondary stack. --- wrapper/Ada/README.md | 1 + wrapper/Ada/default.gpr | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md index 0e0d39e011..67c73c4c0d 100644 --- a/wrapper/Ada/README.md +++ b/wrapper/Ada/README.md @@ -63,6 +63,7 @@ chmod +x 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 diff --git a/wrapper/Ada/default.gpr b/wrapper/Ada/default.gpr index dc4c5014f6..37227b6f5c 100644 --- a/wrapper/Ada/default.gpr +++ b/wrapper/Ada/default.gpr @@ -6,6 +6,13 @@ project Default is "../../src", "../../wolfcrypt/src"); + -- Don't build the tls client application because it makes 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"); + for Object_Dir use "obj"; for Main use ("c_tls_client_main.c",