Skip to content

Commit 3e63589

Browse files
JacobBarthelmehJacobBarthelmeh
authored
Merge pull request #6605 from dgarske/ada
Ada Bindings for wolfSSL
2 parents 10adca1 + 58ac578 commit 3e63589

23 files changed

Lines changed: 3852 additions & 1 deletion

‎examples/configs/user_settings_all.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ extern "C" {
125125
#define WOLFSSL_DER_TO_PEM
126126
#define WOLFSSL_CUSTOM_OID
127127
#define HAVE_OID_ENCODING
128-
//#define WOLFSSL_ASN_TEMPLATE /* Not enabled yet by default */
128+
#define WOLFSSL_ASN_TEMPLATE
129129

130130
/* Certificate Revocation */
131131
#define HAVE_OCSP

‎wrapper/Ada/README.md‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
# Ada Binding Example
2+
The source code for the Ada/SPARK binding of the WolfSSL library
3+
is the WolfSSL Ada package in the wolfssl.ads and wolfssl.adb files.
4+
5+
The source code here also demonstrates a TLS v1.3 server and client
6+
using the WolfSSL Ada binding. The implementation is cross-platform
7+
and compiles on Linux, Mac OS X and Windows.
8+
9+
Security: The WolfSSL Ada binding avoids usage of the
10+
Seconday Stack. The GNAT compiler has a number of hardening
11+
features for example Stack Scrubbing; the compiler can generate
12+
code to zero-out stack frames used by subprograms.
13+
Unfortunately this works well for the primary stack but not
14+
for the secondary stack. The GNAT User's Guide recommends
15+
avoiding the secondary stack using the restriction
16+
No_Secondary_Stack (see the GNAT configuration file gnat.adc
17+
which instructs compilation of the WolfSSL Ada binding under
18+
this restriction).
19+
20+
Portability: The WolfSSL Ada binding makes no usage of controlled types
21+
and has no dependency upon the Ada.Finalization package.
22+
Lighter Ada run-times for embedded systems often have
23+
the restriction No_Finalization. The WolfSSL Ada binding has
24+
been developed with maximum portability in mind.
25+
26+
Not only can the WolfSSL Ada binding be used in Ada applications but
27+
also SPARK applications (a subset of the Ada language suitable
28+
formal verification). To formally verify the Ada code in this repository
29+
open the client.gpr with GNAT Studio and then select
30+
SPARK -> Prove All Sources and use Proof Level 2.
31+
32+
Summary of SPARK analysis
33+
=========================
34+
35+
---------------------------------------------------------------------------------------------------------------
36+
SPARK Analysis results Total Flow CodePeer Provers Justified Unproved
37+
---------------------------------------------------------------------------------------------------------------
38+
Data Dependencies 2 2 . . . .
39+
Flow Dependencies . . . . . .
40+
Initialization 15 15 . . . .
41+
Non-Aliasing . . . . . .
42+
Run-time Checks 58 . . 58 (CVC4 85%, Trivial 15%) . .
43+
Assertions 6 . . 6 (CVC4) . .
44+
Functional Contracts 91 . . 91 (CVC4) . .
45+
LSP Verification . . . . . .
46+
Termination . . . . . .
47+
Concurrency . . . . . .
48+
---------------------------------------------------------------------------------------------------------------
49+
Total 172 17 (10%) . 155 (90%) . .
50+
51+
## Compiler and Build System installation
52+
53+
### GNAT Community Edition 2021
54+
Download and install the GNAT community Edition 2021 compiler and studio:
55+
https://www.adacore.com/download
56+
57+
Linux Install:
58+
59+
```sh
60+
chmod +x gnat-2021-20210519-x86_64-linux-bin
61+
./gnat-2021-20210519-x86_64-linux-bin
62+
```
63+
64+
```sh
65+
export PATH="/opt/GNAT/2021/bin:$PATH"
66+
cd wrapper/Ada
67+
gprclean
68+
gprbuild default.gpr
69+
gprbuild client.gpr
70+
71+
cd obj/
72+
./tls_server_main &
73+
./tls_client_main 127.0.0.1
74+
```
75+
76+
### GNAT FSF Compiler and GPRBuild manual installation
77+
In May 2022 AdaCore announced the end of the GNAT Community releases.
78+
Pre-built binaries for the GNAT FSF compiler and GPRBuild can be
79+
downloaded and manually installed from here:
80+
https://github.com/alire-project/GNAT-FSF-builds/releases
81+
Make sure the executables for the compiler and GPRBuild are on the PATH
82+
and use gprbuild to build the source code.
83+
84+
## Files
85+
The file c_tls_client_main.c and c_tls_server_main.c are the TLS v1.3
86+
server and client examples using the WolfSSL library implemented using
87+
the C programming language.
88+
89+
The translation of the C client example into the Ada/SPARK programming
90+
language can be found in the files:
91+
tls_client_main.adb
92+
tls_client.ads
93+
tls_client.adb
94+
95+
The translation of the C server example into the Ada/SPARK programming
96+
language can be found in the files:
97+
tls_server_main.adb
98+
tls_server.ads
99+
tls_server.adb
100+
101+
A feature of the Ada language that is not part of SPARK is exceptions.
102+
Some packages of the Ada standard library and GNAT specific packages
103+
provided by the GNAT compiler can therefore not be used directly but
104+
need to be put into wrapper packages that does not raise exceptions.
105+
The packages that provide access to sockets and command line arguments
106+
to applications implemented in the SPARK programming language can be
107+
found in the files:
108+
spark_sockets.ads
109+
spark_sockets.adb
110+
spark_terminal.ads
111+
spark_terminal.adb

‎wrapper/Ada/ada_binding.c‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
/* ada_binding.c
2+
*
3+
* Copyright (C) 2006-2023 wolfSSL Inc.
4+
*
5+
* This file is part of wolfSSL.
6+
*
7+
* wolfSSL is free software; you can redistribute it and/or modify
8+
* it under the terms of the GNU General Public License as published by
9+
* the Free Software Foundation; either version 2 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* wolfSSL is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU General Public License
18+
* along with this program; if not, write to the Free Software
19+
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
20+
*/
21+
22+
/* wolfSSL */
23+
#include <wolfssl/wolfcrypt/settings.h>
24+
#include <wolfssl/ssl.h>
25+
26+
/* These functions give access to the integer values of the enumeration
27+
constants used in WolfSSL. These functions make it possible
28+
for the WolfSSL implementation to change the values of the constants
29+
without the need to make a corresponding change in the Ada code. */
30+
extern int get_wolfssl_error_want_read(void);
31+
extern int get_wolfssl_error_want_write(void);
32+
extern int get_wolfssl_max_error_size (void);
33+
extern int get_wolfssl_success(void);
34+
extern int get_wolfssl_failure(void);
35+
extern int get_wolfssl_verify_none(void);
36+
extern int get_wolfssl_verify_peer(void);
37+
extern int get_wolfssl_verify_fail_if_no_peer_cert(void);
38+
extern int get_wolfssl_verify_client_once(void);
39+
extern int get_wolfssl_verify_post_handshake(void);
40+
extern int get_wolfssl_verify_fail_except_psk(void);
41+
extern int get_wolfssl_verify_default(void);
42+
43+
extern int get_wolfssl_filetype_asn1(void);
44+
extern int get_wolfssl_filetype_pem(void);
45+
extern int get_wolfssl_filetype_default(void);
46+
47+
extern int get_wolfssl_error_want_read(void) {
48+
return WOLFSSL_ERROR_WANT_READ;
49+
}
50+
51+
extern int get_wolfssl_error_want_write(void) {
52+
return WOLFSSL_ERROR_WANT_WRITE;
53+
}
54+
55+
extern int get_wolfssl_max_error_size(void) {
56+
return WOLFSSL_MAX_ERROR_SZ;
57+
}
58+
59+
extern int get_wolfssl_success(void) {
60+
return WOLFSSL_SUCCESS;
61+
}
62+
63+
extern int get_wolfssl_failure(void) {
64+
return WOLFSSL_FAILURE;
65+
}
66+
67+
extern int get_wolfssl_verify_none(void) {
68+
return WOLFSSL_VERIFY_NONE;
69+
}
70+
71+
extern int get_wolfssl_verify_peer(void) {
72+
return WOLFSSL_VERIFY_PEER;
73+
}
74+
75+
extern int get_wolfssl_verify_fail_if_no_peer_cert(void) {
76+
return WOLFSSL_VERIFY_FAIL_IF_NO_PEER_CERT;
77+
}
78+
79+
extern int get_wolfssl_verify_client_once(void) {
80+
return WOLFSSL_VERIFY_CLIENT_ONCE;
81+
}
82+
83+
extern int get_wolfssl_verify_post_handshake(void) {
84+
return WOLFSSL_VERIFY_POST_HANDSHAKE;
85+
}
86+
87+
extern int get_wolfssl_verify_fail_except_psk(void) {
88+
return WOLFSSL_VERIFY_FAIL_EXCEPT_PSK;
89+
}
90+
91+
extern int get_wolfssl_verify_default(void) {
92+
return WOLFSSL_VERIFY_DEFAULT;
93+
}
94+
95+
extern int get_wolfssl_filetype_asn1(void) {
96+
return WOLFSSL_FILETYPE_ASN1;
97+
}
98+
99+
extern int get_wolfssl_filetype_pem(void) {
100+
return WOLFSSL_FILETYPE_PEM;
101+
}
102+
103+
extern int get_wolfssl_filetype_default(void) {
104+
return WOLFSSL_FILETYPE_DEFAULT;
105+
}

0 commit comments

Comments
 (0)