Today we at wolfSSL (https://www.wolfssl.com/) are happy to announce the availability of an Ada/SPARK binding that enables Ada applications to use post-quantum TLS 1.3 encryption through the wolfSSL embedded SSL/TLS library. The wolfSSL library is thread safe by design. Multiple threads can enter the library simultaneously without creating conflicts because wolfSSL avoids global data, static data, and the sharing of objects. When objects are used in the API the wolfSSL library provides opaque pointers to objects whose contents is only known internally by the wolfSSL library. This library interface design makes it easy to make bindings to other programming languages and at the same time enables the contents of the objects used internally to be highly configurable.

Having these bindings opens the door to obtaining FIPS 140-3 and DO-178C certifications for Ada and SPARK applications that use TLS for their encrypted communications and also makes them quantum-safe.

Examples

The Ada/SPARK bindings and examples can be found on GitHub here: https://github.com/wolfSSL/wolfssl/tree/master/wrapper/Ada

The examples demonstrate a TLS v1.3 server and client using the WolfSSL Ada binding and SPARK programming language. The implementation is cross-platform and compiles on Linux, Mac OS X and Windows.

The source code for the WolfSSL library Ada package is in the wolfssl.ads and wolfssl.adb files.

Security

The WolfSSL Ada binding avoids usage of the Secondary 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 (http://gcc.gnu.org/onlinedocs/gnat_rm/Stack-Scrubbing.html). 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 for Ada code that handles data that should be scrubbed.

Portability

The WolfSSL Ada binding has been developed with maximum portability in mind.

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.

SPARK

These Ada bindings can also be used in SPARK applications (a subset of the Ada language suitable for 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.

The result of the analysis is in the README.md and included below:

What is DO-178C?

DO-178C, Software Considerations in Airborne Systems and Equipment Certification is the primary document by which the certification authorities such as FAA (The Federal Aviation Administration in the United States), EASA (The European Union Aviation Safety Agency) and Transport Canada approve all commercial software-based aerospace systems.

What is FIPS 140-3

FIPS 140-3 is an incremental advancement of FIPS 140-2, which now standardizes on the ISO 19790:2012 and ISO 24759:2017 specifications.

Historically, ISO 19790 was based on FIPS 140-2, but has continued to advance since that time.

FIPS 140-3 will now point back to ISO 19790 for security requirements.

Keeping FIPS 140-3 as a separate standard will still allow NIST (The National Institute of Standards and Technology) to mandate additional requirements on top of what the ISO standard contains when needed.

Federal agencies in the United States purchasing cryptographic-based security systems must confirm an associated FIPS 140-2 or 140-3 certificate exists.

Contact us at facts@wolfssl.com with any questions, comments, or suggestions.