s2n-tls has a wide variety of tests covering a wide variety of different functionality. This document serves as a "quick reference", providing an overview of all the testing that s2n-tls does and linking to additional documentation.
Is the internal functionality of s2n-tls correct?
These test the correctness of low-level s2n-tls functions. These functions are commonly private. We have unit tests for both the C library and the rust bindings.
The C unit tests are additionally run with the following sanitizers enabled
- Valgrind: used to detect memory errors
- Address Sanitizer (ASAN): used to detect memory errors
- Thread Sanitizer (TSAN): used to detect race conditions
Further information:
Is the functionality of s2n-tls correct and compatible with other implementations?
Our integration tests involve interoperation with other TLS implementations, because testing against another implementation improves confidence that s2n-tls has implemented the feature correctly and is compliant with relevant RFCs.
s2n-tls integration tests are run using our integrationv2 framework. Tests are implemented using "client" and "server" executables from various implementations like Openssl and Boringssl. The client and server interactions are coordinated with pytest.
Further information:
Fuzz Tests provide additional confidence in s2n-tls correctness by testing s2n-tls functionality under a wide variety of inputs.
s2n-tls fuzz tests use LibFuzzer as the fuzzing engine. Fuzzing is generally only applied to functions that take external input.
Further information:
s2n-tls includes a variety of formal methods which are used to prove that s2n-tls has certain behaviors.
CBMC verifies memory safety (which includes array bounds checks and checks for the safe use of pointers), checks for various further variants of undefined behavior, and user-specified assertions. C Bounded Model Checker
s2n-tls writes CBMC proofs for a number of sensitive or commonly used functions in the codebase.
Further information:
SAW verifies the correctness of code. More specifically, SAW can verify that some LLVM bitcode (compiled from C) matches the behavior of a cryptol specification. s2n-tls includes SAW proofs for its HMAC and DRBG implementations, as well as the TLS handshake state machine.
Further information:
Sidetrail verifies the absence of timing side-channels, and is implemented using the smack toolchain. Our SideTrail proofs cover a number of the record processing functions.
Further information:
ctverif is another tool that verifies the absence of timing side-channels and is also implemented using the smack toolchain. Our ctverif proofs verify that s2n_constant_time_equals and s2n_constant_time_copy_or_dont are both constant time.
Further information:
s2n-tls maintains a set of Rust criterion benchmarks to assess the performance of s2n-tls. The most commonly used benchmarks cover
- performance of handshakes
- performance of data transfer (bulk encryption)
But a number of other low-level benchmarks are also included.
Further information: