Ada Bindings for wolfSSL

[dgarske]

Description

Ada Bindings for wolfSSL. TLS server and client.

Credit @joakim-strandberg Joakim Dahlgren Strandberg joakimds@kth.se

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                  52           .          .    52 (CVC4 85%, Trivial 15%)           .          .
Assertions                        2           .          .                      2 (CVC4)           .          .
Functional Contracts             88           .          .                     88 (CVC4)           .          .
LSP Verification                  .           .          .                             .           .          .
Termination                       .           .          .                             .           .          .
Concurrency                       .           .          .                             .           .          .
---------------------------------------------------------------------------------------------------------------
Total                           159    17 (11%)          .                     142 (89%)           .          .


max steps used for successful proof: 1

Testing

See wrapper/Ada/README.md

Checklist

• added tests
• updated/added doxygen
• updated appropriate READMEs
• Updated manual and documentation

[dgarske]

FYI: Only issue is C++ style comments. Please use C style /* */. Thanks

[check-source-text] [2 of 2] [8ab723e42e]
C++-style comments:
./wrapper/Ada/c_tls_server_main.c:147:// To execute the application: ./main
./wrapper/Ada/ada_binding.c:27:// These functions give access to the integer values of the enumeration
./wrapper/Ada/ada_binding.c:28:// constants used in WolfSSL. These functions make it possible
./wrapper/Ada/ada_binding.c:29:// for the WolfSSL implementation to change the values of the constants
./wrapper/Ada/ada_binding.c:30:// without the need to make a corresponding change in the Ada code.
    check-source-text fail_C

[joakim-strandberg]

I have added the Ada tls v1.3 client application and updated the WolfSSL Ada package. I seem to have trouble uploading the changes:
joakim@joakim-N8xEJEK:/wolfssl/wrapper/Ada$ git commit -m 'Ada version of TLS v1.3 client application implemented'
[ada 45d8a5b] Ada version of TLS v1.3 client application implemented
12 files changed, 657 insertions(+), 94 deletions(-)
create mode 100644 wrapper/Ada/client.gpr
joakim@joakim-N8xEJEK:/wolfssl/wrapper/Ada$ git status
På grenen ada
inget att checka in, arbetskatalogen ren
joakim@joakim-N8xEJEK:/wolfssl/wrapper/Ada$ git push origin ada
Username for 'https://github.com': joakim-strandberg
Password for 'https://joakim-strandberg@github.com':
remote: Permission to wolfSSL/wolfssl.git denied to joakim-strandberg.
fatal: kan inte komma åt "https://github.com/wolfSSL/wolfssl/": The requested URL returned error: 403
joakim@joakim-N8xEJEK:/wolfssl/wrapper/Ada$

To get the source code locally on my computer I followed the instructions at: https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/reviewing-changes-in-pull-requests/checking-out-pull-requests-locally

git clone https://github.com/wolfSSL/wolfssl
cd wolfssl/
git fetch origin pull/6605/head:ada
git checkout ada

Will be away from keyboard for a couple of hours and will try again later.

[dgarske]

@joakim-strandberg can you expand this section and update with latest steps? Perhaps also add some information about Ada and advantages for using?

[joakim-strandberg]

Sure!

[JacobBarthelmeh]

Thanks @joakim-strandberg works good. Not seeing the contributor documents in our internal tracker that we need in place yet though to merge. I'll be following up on that internally.