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/wrapper/Ada/README.md b/wrapper/Ada/README.md new file mode 100644 index 0000000000..67c73c4c0d --- /dev/null +++ b/wrapper/Ada/README.md @@ -0,0 +1,111 @@ +# Ada Binding Example +The source code for the Ada/SPARK binding of the WolfSSL library +is the WolfSSL Ada package in the wolfssl.ads and wolfssl.adb files. + +The source code here also demonstrates a TLS v1.3 server and client +using the WolfSSL Ada binding. The implementation is cross-platform +and compiles on Linux, Mac OS X and Windows. + +Security: The WolfSSL Ada binding avoids usage of the +Seconday Stack. The GNAT compiler has a number of hardening +features for example Stack Scrubbing; the compiler can generate +code to zero-out stack frames used by subprograms. +Unfortunately this works well for the primary stack but not +for the secondary stack. The GNAT User's Guide recommends +avoiding the secondary stack using the restriction +No_Secondary_Stack (see the GNAT configuration file gnat.adc +which instructs compilation of the WolfSSL Ada binding under +this restriction). + +Portability: The WolfSSL Ada binding makes no usage of controlled types +and has no dependency upon the Ada.Finalization package. +Lighter Ada run-times for embedded systems often have +the restriction No_Finalization. The WolfSSL Ada binding has +been developed with maximum portability in mind. + +Not only can the WolfSSL Ada binding be used in Ada applications but +also SPARK applications (a subset of the Ada language suitable +formal verification). To formally verify the Ada code in this repository +open the client.gpr with GNAT Studio and then select +SPARK -> Prove All Sources and use Proof Level 2. + +Summary of SPARK analysis +========================= + +--------------------------------------------------------------------------------------------------------------- +SPARK Analysis results Total Flow CodePeer Provers Justified Unproved +--------------------------------------------------------------------------------------------------------------- +Data Dependencies 2 2 . . . . +Flow Dependencies . . . . . . +Initialization 15 15 . . . . +Non-Aliasing . . . . . . +Run-time Checks 58 . . 58 (CVC4 85%, Trivial 15%) . . +Assertions 6 . . 6 (CVC4) . . +Functional Contracts 91 . . 91 (CVC4) . . +LSP Verification . . . . . . +Termination . . . . . . +Concurrency . . . . . . +--------------------------------------------------------------------------------------------------------------- +Total 172 17 (10%) . 155 (90%) . . + +## Compiler and Build System installation + +### GNAT Community Edition 2021 +Download and install the GNAT community Edition 2021 compiler and studio: +https://www.adacore.com/download + +Linux Install: + +```sh +chmod +x gnat-2021-20210519-x86_64-linux-bin +./gnat-2021-20210519-x86_64-linux-bin +``` + +```sh +export PATH="/opt/GNAT/2021/bin:$PATH" +cd wrapper/Ada +gprclean +gprbuild default.gpr +gprbuild client.gpr + +cd obj/ +./tls_server_main & +./tls_client_main 127.0.0.1 +``` + +### GNAT FSF Compiler and GPRBuild manual installation +In May 2022 AdaCore announced the end of the GNAT Community releases. +Pre-built binaries for the GNAT FSF compiler and GPRBuild can be +downloaded and manually installed from here: +https://github.com/alire-project/GNAT-FSF-builds/releases +Make sure the executables for the compiler and GPRBuild are on the PATH +and use gprbuild to build the source code. + +## Files +The file c_tls_client_main.c and c_tls_server_main.c are the TLS v1.3 +server and client examples using the WolfSSL library implemented using +the C programming language. + +The translation of the C client example into the Ada/SPARK programming +language can be found in the files: +tls_client_main.adb +tls_client.ads +tls_client.adb + +The translation of the C server example into the Ada/SPARK programming +language can be found in the files: +tls_server_main.adb +tls_server.ads +tls_server.adb + +A feature of the Ada language that is not part of SPARK is exceptions. +Some packages of the Ada standard library and GNAT specific packages +provided by the GNAT compiler can therefore not be used directly but +need to be put into wrapper packages that does not raise exceptions. +The packages that provide access to sockets and command line arguments +to applications implemented in the SPARK programming language can be +found in the files: +spark_sockets.ads +spark_sockets.adb +spark_terminal.ads +spark_terminal.adb \ No newline at end of file diff --git a/wrapper/Ada/ada_binding.c b/wrapper/Ada/ada_binding.c new file mode 100644 index 0000000000..0becb0e7e0 --- /dev/null +++ b/wrapper/Ada/ada_binding.c @@ -0,0 +1,105 @@ +/* ada_binding.c + * + * Copyright (C) 2006-2023 wolfSSL Inc. + * + * This file is part of wolfSSL. + * + * wolfSSL is free software; you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation; either version 2 of the License, or + * (at your option) any later version. + * + * wolfSSL is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA + */ + +/* wolfSSL */ +#include +#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); +extern int get_wolfssl_verify_client_once(void); +extern int get_wolfssl_verify_post_handshake(void); +extern int get_wolfssl_verify_fail_except_psk(void); +extern int get_wolfssl_verify_default(void); + +extern int get_wolfssl_filetype_asn1(void); +extern int get_wolfssl_filetype_pem(void); +extern int get_wolfssl_filetype_default(void); + +extern int get_wolfssl_error_want_read(void) { + return WOLFSSL_ERROR_WANT_READ; +} + +extern int get_wolfssl_error_want_write(void) { + return WOLFSSL_ERROR_WANT_WRITE; +} + +extern int get_wolfssl_max_error_size(void) { + return WOLFSSL_MAX_ERROR_SZ; +} + +extern int get_wolfssl_success(void) { + return WOLFSSL_SUCCESS; +} + +extern int get_wolfssl_failure(void) { + return WOLFSSL_FAILURE; +} + +extern int get_wolfssl_verify_none(void) { + return WOLFSSL_VERIFY_NONE; +} + +extern int get_wolfssl_verify_peer(void) { + return WOLFSSL_VERIFY_PEER; +} + +extern int get_wolfssl_verify_fail_if_no_peer_cert(void) { + return WOLFSSL_VERIFY_FAIL_IF_NO_PEER_CERT; +} + +extern int get_wolfssl_verify_client_once(void) { + return WOLFSSL_VERIFY_CLIENT_ONCE; +} + +extern int get_wolfssl_verify_post_handshake(void) { + return WOLFSSL_VERIFY_POST_HANDSHAKE; +} + +extern int get_wolfssl_verify_fail_except_psk(void) { + return WOLFSSL_VERIFY_FAIL_EXCEPT_PSK; +} + +extern int get_wolfssl_verify_default(void) { + return WOLFSSL_VERIFY_DEFAULT; +} + +extern int get_wolfssl_filetype_asn1(void) { + return WOLFSSL_FILETYPE_ASN1; +} + +extern int get_wolfssl_filetype_pem(void) { + return WOLFSSL_FILETYPE_PEM; +} + +extern int get_wolfssl_filetype_default(void) { + return WOLFSSL_FILETYPE_DEFAULT; +} 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..161b3b8641 --- /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/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 new file mode 100644 index 0000000000..37227b6f5c --- /dev/null +++ b/wrapper/Ada/default.gpr @@ -0,0 +1,82 @@ +project Default is + for Languages use ("C", "Ada"); + + for Source_Dirs use (".", + "../../", + "../../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", + "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", -- 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 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/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 new file mode 100644 index 0000000000..a60f5618a4 --- /dev/null +++ b/wrapper/Ada/tls_client.adb @@ -0,0 +1,328 @@ +-- 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.Strings.Bounded; +with Ada.Text_IO; +with Interfaces.C; + +with SPARK_Terminal; + +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; + + subtype Byte_Index is WolfSSL.Byte_Index; + + Success : WolfSSL.Subprogram_Result renames WolfSSL.Success; + + subtype Byte_Type is WolfSSL.Byte_Type; + + 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 : Natural) is + begin + Natural_IO.Put (Item => Number, Width => 0, Base => 10); + end Put; + + procedure Put (Number : Byte_Index) is + begin + Natural_IO.Put (Item => Natural (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; + + subtype Exit_Status is SPARK_Terminal.Exit_Status; + + 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) with Global => null is + begin + SPARK_Terminal.Set_Exit_Status (Status); + end Set; + + subtype Port_Type is SPARK_Sockets.Port_Type; + + subtype Level_Type is SPARK_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 Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type; + + use type Family_Type; + + Socket_Error : exception renames SPARK_Sockets.Socket_Error; + + Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address; + + Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level; + + Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet; + + 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"; + CA_FILE : constant String := "../certs/ca-cert.pem"; + + subtype Byte_Array is WolfSSL.Byte_Array; + + 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 SPARK_Terminal.Argument (Number); + end Argument; + + 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 : SPARK_Sockets.Optional_Socket renames Client; + D : Byte_Array (1 .. 200); + P : constant Port_Type := 11111; + + Addr : SPARK_Sockets.Optional_Inet_Addr; + + Count : WolfSSL.Byte_Index; + + Text : String (1 .. 200); + Last : Natural; + + Input : WolfSSL.Read_Result; + Output : WolfSSL.Write_Result; + + Result : WolfSSL.Subprogram_Result; + begin + Result := WolfSSL.Initialize; + if Result /= Success then + Put_Line ("ERROR: Failed to initialize the WolfSSL library."); + return; + end if; + + if Argument_Count < 1 then + Put_Line ("usage: tcl_client "); + return; + end if; + 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 => Addr.Addr, + Port => P); + + Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket, + Server => A); + if Result /= Success 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; + + -- Load client certificate into WOLFSSL_CTX. + Result := WolfSSL.Use_Certificate_File (Context => Ctx, + File => CERT_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + Put ("ERROR: failed to load "); + 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; + + -- Load client key into WOLFSSL_CTX. + Result := WolfSSL.Use_Private_Key_File (Context => Ctx, + File => KEY_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + Put ("ERROR: failed to load "); + 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; + + -- Load CA certificate into WOLFSSL_CTX. + Result := WolfSSL.Load_Verify_Locations (Context => Ctx, + File => CA_FILE, + Path => ""); + if Result /= Success then + Put ("ERROR: failed to load "); + 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; + + -- 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 (C); + WolfSSL.Free (Context => Ctx); + Set (Exit_Status_Failure); + return; + end if; + + -- Attach wolfSSL to the socket. + Result := WolfSSL.Attach (Ssl => Ssl, + Socket => SPARK_Sockets.To_C (C.Socket)); + if Result /= Success 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; + + Result := WolfSSL.Connect (Ssl); + if Result /= Success 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; + + Put ("Message for server: "); + Ada.Text_IO.Get_Line (Text, Last); + + SPARK_Sockets.To_C (Item => Text (1 .. Last), + Target => D, + Count => Count); + 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 (Output.Bytes_Written); + Put (" bytes of "); + Put (Last); + Put ("bytes were sent"); + New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); + return; + end if; + + Input := WolfSSL.Read (Ssl); + if not Input.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; + 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; + + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); + Result := WolfSSL.Finalize; + if Result /= Success then + Put_Line ("ERROR: Failed to finalize the WolfSSL library."); + end if; + 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..50a52b3ccd --- /dev/null +++ b/wrapper/Ada/tls_client.ads @@ -0,0 +1,37 @@ +-- 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 +-- + +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); + +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 new file mode 100644 index 0000000000..ab50dab842 --- /dev/null +++ b/wrapper/Ada/tls_client_main.adb @@ -0,0 +1,33 @@ +-- 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); +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 (Ssl, Ctx, Client => C); +end Tls_Client_Main; diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb new file mode 100644 index 0000000000..797d23caed --- /dev/null +++ b/wrapper/Ada/tls_server.adb @@ -0,0 +1,326 @@ +-- 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.Strings.Bounded; +with Ada.Text_IO.Bounded_IO; + +with SPARK_Terminal; pragma Elaborate_All (SPARK_Terminal); + +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; + + Success : WolfSSL.Subprogram_Result renames WolfSSL.Success; + + procedure Put (Char : Character) is + begin + Ada.Text_IO.Put (Char); + end Put; + + 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 New_Line is + begin + Ada.Text_IO.New_Line; + end New_Line; + + subtype Exit_Status is SPARK_Terminal.Exit_Status; + + 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) with Global => null is + begin + SPARK_Terminal.Set_Exit_Status (Status); + end Set; + + subtype Port_Type is SPARK_Sockets.Port_Type; + + subtype Level_Type is SPARK_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 Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type; + + Socket_Error : exception renames SPARK_Sockets.Socket_Error; + + Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address; + + Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level; + + Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet; + + 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"; + 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 (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; + P : constant Port_Type := 11111; + + Ch : Character; + + Result : WolfSSL.Subprogram_Result; + Shall_Continue : Boolean := True; + + Input : WolfSSL.Read_Result; + Output : WolfSSL.Write_Result; + Option : Option_Type; + begin + Result := WolfSSL.Initialize; + if Result /= Success 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."); + 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 /= Success 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 /= Success 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 /= Success 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; + + -- Require mutual authentication. + WolfSSL.Set_Verify + (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, + File => CERT_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + 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; + + -- Load server key into WOLFSSL_CTX. + Result := WolfSSL.Use_Private_Key_File (Context => Ctx, + File => KEY_FILE, + Format => WolfSSL.Format_Pem); + if Result /= Success then + 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; + + -- Load client certificate as "trusted" into WOLFSSL_CTX. + Result := WolfSSL.Load_Verify_Locations (Context => Ctx, + File => CA_FILE, + Path => ""); + if Result /= Success then + 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); + 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 /= Success 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 => SPARK_Sockets.To_C (C.Socket)); + if Result /= Success 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; + + -- Establish TLS connection. + Result := WolfSSL.Accept_Connection (Ssl); + if Result /= Success 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; + + Put_Line ("Client connected successfully."); + + Input := WolfSSL.Read (Ssl); + if not Input.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. + for I in Input.Buffer'Range loop + Ch := Character (Input.Buffer (I)); + if Ada.Characters.Handling.Is_Graphic (Ch) then + Put (Ch); + else + null; + -- Ignore the "newline" characters at end of message. + end if; + end loop; + New_Line; + + -- 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; + + 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 /= Success then + Put_Line ("ERROR: Failed to shutdown WolfSSL context."); + end if; + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (C); + + Put_Line ("Shutdown complete."); + end loop; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + Result := WolfSSL.Finalize; + if Result /= Success then + Put_Line ("ERROR: Failed to finalize the WolfSSL library."); + return; + end if; + 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..142fad2ce5 --- /dev/null +++ b/wrapper/Ada/tls_server.ads @@ -0,0 +1,39 @@ +-- 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 +-- + +-- 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 new file mode 100644 index 0000000000..80b3a88d79 --- /dev/null +++ b/wrapper/Ada/tls_server_main.adb @@ -0,0 +1,39 @@ +-- 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); + +-- 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 (Ssl, Ctx, L, C); +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..f1eac8f8ae --- /dev/null +++ b/wrapper/Ada/wolfssl.adb @@ -0,0 +1,688 @@ +-- 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 + + subtype size_t is Interfaces.C.size_t; use type size_t; + + subtype long is Interfaces.C.long; + subtype unsigned_long is Interfaces.C.unsigned_long; + + 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; + + function Initialize return Subprogram_Result is + Result : constant int := Initialize_WolfSSL; + begin + return Subprogram_Result (Result); + end Initialize; + + function Finalize return Subprogram_Result is + Result : constant int := Finalize_WolfSSL; + begin + return Subprogram_Result (Result); + 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", + Import => True; + + function TLSv1_2_Server_Method return Method_Type is + begin + 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", + Import => True; + + function TLSv1_3_Server_Method return Method_Type is + begin + 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 Context_Type) is + begin + 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 Context_Type) is + begin + WolfSSL_CTX_free (Context); + Context := null; + 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 + Ctx : constant Context_Type := Context; + 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 (Ctx, F (1 .. C), int (Format)); + return Subprogram_Result (Result); + 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)); + return Subprogram_Result (Result); + 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 + Ctx : constant Context_Type := Context; + 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 (Ctx, F (1 .. C), int (Format)); + return Subprogram_Result (Result); + 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)); + return Subprogram_Result (Result); + 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 + Ctx : constant Context_Type := Context; + 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 (Ctx, null, null); + else + Interfaces.C.To_C (Item => Path, + Target => P, + Count => PC, + Append_Nul => True); + Result := Load_Verify_Locations3 (Ctx, 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 (Ctx, 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 => Ctx, + File => F, + Path => P); + end if; + end if; + return Subprogram_Result (Result); + end Load_Verify_Locations; + + function Load_Verify_Buffer + (Context : Context_Type; + Input : char_array; + Size : int; + Format : int) return int with + Convention => C, + External_Name => "wolfSSL_CTX_load_verify_buffer", + Import => True; + + function Load_Verify_Buffer (Context : Context_Type; + Input : Byte_Array; + Format : File_Format) + return Subprogram_Result is + Result : int; + begin + Result := Load_Verify_Buffer (Context => Context, + Input => Input, + Size => Input'Length, + Format => int(Format)); + return Subprogram_Result (Result); + 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, + External_Name => "wolfSSL_new", + Import => True; + + procedure Create_WolfSSL (Context : Context_Type; + 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 + Interfaces.C.To_C (Item => File, + Target => F, + Count => C, + Append_Nul => True); + Result := Use_Certificate_File (Ssl, F (1 .. C), int (Format)); + return Subprogram_Result (Result); + 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)); + return Subprogram_Result (Result); + 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)); + return Subprogram_Result (Result); + 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)); + return Subprogram_Result (Result); + end Use_Private_Key_Buffer; + + 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 + return Subprogram_Result (Result); + 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 + return Subprogram_Result (Result); + 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 (Success => False, + Last => 0, + Code => Subprogram_Result (Size)); + else + return (Success => True, + 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 Write_Result is + Size : constant int := Data'Length; + Result : int; + begin + Result := WolfSSL_Write (Ssl, Data, Size); + 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; + + function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result is + Result : constant int := WolfSSL_Shutdown (Ssl); + begin + return Subprogram_Result (Result); + end Shutdown; + + function WolfSSL_Connect (Ssl : WolfSSL_Type) return int with + Convention => C, + External_Name => "wolfSSL_connect", + Import => True; + + function Connect (Ssl : WolfSSL_Type) return Subprogram_Result is + Result : constant int := WolfSSL_Connect (Ssl); + begin + return Subprogram_Result (Result); + end Connect; + + procedure WolfSSL_Free (Ssl : WolfSSL_Type) with + Convention => C, + External_Name => "wolfSSL_free", + Import => True; + + procedure Free (Ssl : in out WolfSSL_Type) is + begin + if Ssl /= null then + WolfSSL_Free (Ssl); + end if; + 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 new file mode 100644 index 0000000000..a3f536e5d4 --- /dev/null +++ b/wrapper/Ada/wolfssl.ads @@ -0,0 +1,606 @@ +-- 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. +package WolfSSL with SPARK_Mode is + + type Subprogram_Result is new Integer; + Success : constant Subprogram_Result; + Failure : constant Subprogram_Result; + + function Initialize return Subprogram_Result; + -- 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; + -- 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? + + 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; + + 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); + -- 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; + + 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 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. + + 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); + -- 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); + -- 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 (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; + + function Write (Ssl : WolfSSL_Type; + 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); + + 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); + + 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; 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