In this blog post, we describe how we at SandboxAQ, together with Cryspen, formally verified key components of Sandwich—an open-source, unified API that simplifies the use of cryptographic libraries for developers, enabling crypto-agility.

Formal methods have been used successfully to produce high-assurance implementations of cryptographic algorithms that have since been integrated into popular libraries like BoringSSL, NSS, and AWS LC. However, APIs of cryptographic libraries are often complex to use and can be error-prone. Sandwich tackles this problem.

Sandwich

Sandwich is a cryptographic meta-library that offers a unified and declarative API for cryptographic functions and protocols, such as TLS, with bindings to various cryptographic implementations, such as OpenSSL and BoringSSL. It supports multiple programming languages, including C/C++, Rust, Python, and Golang. Sandwich promises a hard-to-misuse API and allows swapping algorithms and cryptographic library providers without changing the code via support for user-defined configuration files.

Besides crypto-agility, Sandwich aims to support security teams by providing the necessary information about cryptographic inventory and compliance efforts. To accomplish this, Sandwich can be configured with a declarative policy format that checks the cryptographic implementations, including the cryptography libraries in use, their versions, and FIPS mode. It also checks cipher suites, key strength, and quantum-readiness. For example, users of Sandwich can configure TLS to use only algorithms with security greater than 256 bits.

Given Sandwich’s critical role in managing cryptographic implementations and securing data and systems, it’s important to trust its operation. Exhaustive testing is essential for establishing this trust, but its coverage may be limited since many scenarios will remain untested. Formal methods, tools, and techniques can help in this task.

Formal Methods - Overview

Formal methods aim at giving guarantees. These guarantees can include:

• memory safety: no out-of-bounds access or null pointer dereferences;
• absence of uncontrolled aborts: the program won’t end unexpectedly;
• functional correctness: the program does what it’s supposed to do.

We aim to reason about Sandwich’s Rust code, which already provides some memory guarantees, giving us a head start. To verify additional properties, we use Hax, a tool for high assurance translations of a large subset of Rust into formal languages such as F*, a general-purpose, proof-oriented programming language.

Using Hax, we can translate Sandwich’s Rust implementation into F* to prove that it does not terminate in an uncontrolled way and to specify and prove several security properties, which are discussed next.

Target Security Properties

One of the main advantages of Sandwich is that it handles the complexity and pitfalls of cryptographic library APIs. The goal is to make things simple and safe.

A good example is X.509 certificate verification in OpenSSL during a TLS connection. A 2012 paper, “The Most Dangerous Code in the World: Validating SSL Certificates in Non-Browser Software,” highlights these challenges. It notes that some validation errors are returned through the return variable, while others are stored in “internal verify result flags” — even when the function returns OK. Developers need to call SSL_get_verify_result() explicitly to catch all errors.

More recently, CVE-2024-12797 (published in February 2025) described a related vulnerability in OpenSSL. Handshakes with unauthenticated servers didn’t abort as expected due to the lack of a simple API. Clients that explicitly called SSL_get_verify_result() were not affected.

Since our central goal is to handle these cases securely, our target security properties are designed to reflect them. Specifically, the properties we aim to prove ensure that the configuration defined by a Sandwich user matches what Sandwich actually sets when interacting with the cryptographic library.

In this initial effort, we focused on the OpenSSL 3 version of Sandwich and defined the following security properties.

1. Safe TLS Protocol Versions

   • Policy conformance, no unintentional version downgrade
     • TLS 1.2 is only enabled if the application configures it

2. Safe TLS Ciphersuites

   • Policy conformance, no unintentional crypto downgrade
     • Only ciphersuites that are configured are enabled

3. Correct X.509 Certificate Validation

   • Safe Certificate Verification Mode

     • The configured verification mode matches the input configuration

   • Trusted certificates

     • Only certificates that are configured are trusted

   • Trusted peer names

     • Only names that are configured are allowed as subject alternative names

Together, these goals guarantee that the established TLS tunnel provides the level of authentication and confidentiality that is required by the input configuration.

Specifying and Verifying the Goals using Hax

Sandwich exposes an API where a user can provide a Configuration file to first create a tunnel Context and then use it to create a tunnel. The high-level functions in this API in turn call a series of inner functions that validate the input configuration and perform other checks before calling a series of functions in the OpenSSL API to create an OpenSSL connection context that can then be used to create new TLS connections (i.e. tunnels).

The security goals listed above can therefore be interpreted as requirements for the OpenSSL context, based on the Sandwich configuration. That is, the output OpenSSL context should satisfy the TLS version, TLS ciphersuite, and X.509 validation policies specified in the Sandwich Configuration.

To formally specify and verify these properties for the Sandwich codebase, we first used Hax to translate the source Rust code to a model in F*, where each Rust function becomes an F* function. We then annotate these functions with contracts that encode the security goals. The goals themselves rely on some auxiliary functions, written in Rust, that parse the input Configuration to obtain various elements.

Hax allows users to annotate each Rust function with a contract consisting of a pre-condition (a predicate on the inputs) and a post-condition (a predicate on the inputs and the output). After translation, these contracts become proof obligations for F*, which then ensures that for every call to a function, the inputs satisfy the pre-condition, and that the output satisfies the post-condition.

We use pre-conditions on the OpenSSL functions to specify safety conditions. For example: OpenSSL should only be configured with data coming from the user’s configuration. We use postconditions on the high-level Sandwich API to specify functional guarantees. For example: if the API function does not return an error, then some OpenSSL configuration operations must have been performed.

Here is how we specify the safe TLS version security goal:

#[requires(user_configured(configuration) &&
    min_tls_version_of_config(configuration) == version)]
fn set_minimum_tls_version(&self, version: TlsVersion) -> Result<()> {..}

requires is the keyword for Hax pre-conditions, so this pre-condition says that the OpenSSL function for setting the minimal TLS protocol version can only be called with a certain version if the user passed in a certain configuration in which this version was supported. In other words, with this precondition, we ask F* to verify that for all calls to set_minimum_tls_version, the version that is passed in the input is the same as the version specified by the user in the configuration. This relies on the specification function min_tls_version_of_config that specifies how this version can be extracted from the configuration:

fn min_tls_version_of_config(config: Configuration)  -> TlsVersion {
  match config.opts.clone() {
    Some(Client(ClientOptions{
      Some(Tls(TLSClientOptions {common_options,..})), ..})) => 
        if common_options.tls12.is_some() {
		  TlsVersion::Tls12
        } else {
          TlsVersion::Tls13
        },
        _ -> {
          TlsVersion::Tls13
        }
  }

Now let’s have a look at a functional property, ensuring that if the tunnel creation function from the top-level sandwich API returns no error, then OpenSSL has been configured with the right verify_mode. We specify this as a postcondition on the top-level function. Here is the top-level one:

#[hax_lib::ensures(|result| 
  if result.is_ok() {
    if let verify_mode_of_config(configuration) ==
       Some(verify_mode) {
      set_verify_mode_called(verify_mode)
    }
  }
)]
pub(crate) fn try_from(configuration: &pb_api::Configuration) {..}

The post-condition uses set_verify_mode_called which can only be obtained from the postcondition on the OpenSSL function:

#[hax_lib::ensures(|_| set_verify_mode_called(verify_mode))]
fn set_verify_mode(&self, verify_mode: VerifyMode){..}

Together, those two post-conditions enforce that if the top-level function succeeds, then somewhere deep inside the function, it has called set_verify_mode, and it has called it with the correct verify_mode (as computed from the configuration by the specification function verify_mode_of_config).

Once these specifications are written into the Rust code and translated to F*, the F* typechecker is able to automatically prove that they hold using the SMT solver Z3. The user does not need to write any proofs explicitly by hand, but they do need to annotate all the functions that are used, between the high-level Sandwich API and the low-level OpenSSL API, with pre- and post-conditions to aid F* in completing the proof. Indeed, F* is then able to prove all our security properties in a few seconds.

A key feature of Hax that aids us in this proof is that it slices the source code so that only the relevant code needs to be annotated and verified; none of the functions that are unused in this code path need to be specified, extracted, or verified. The total lines of code we process here is around 1500, resulting in about 2500 lines of F*.

Improving the Tools - the first step

To achieve our goal of formally proving the security properties discussed above, we had to extend the tools. Specifically, Sandwich helped identify many programming language features that were not supported by Hax. Next, we briefly present some of the key improvements to Hax that enabled the translation of Sandwich’s Rust implementation to F*.

Control-flow

Hax did not support several complex control-flow sequences. For instance, using return statements inside nested if or match statements was not allowed, and similar restrictions existed in the context of loops. Translating from Rust (imperative) to F* (functional) involves reworking the control flow while preserving semantics.

We extended Hax to inline certain statements in specific branches. This applies to if and match statements — our transformation adds an else branch if necessary and inlines the subsequent statements in each branch. We also introduced a transformation for loops, even when they contain return, break, or continue statements. This is achieved by introducing a monadic encoding of the loop, with the accumulator carrying information about whether it produces a return value for the whole function or not. For more details on this subject, check the “Control flow rewriting without monads including inside loops” section on Cryspen’s blog post about Hax.

Cyclic Dependencies

Another extension was to support cyclic dependencies between modules (for example, two modules that call functions from each other). In Rust, modules act as namespaces, and there are no acyclicity constraints at the module level. However, it is common for verification backends, including F*, to require acyclicity.

We solved this by moving items that create cycles into a single common module (which we call bundle) and then importing them back to their modules of origin. Graph algorithms helped us identify which items needed to be moved. Then, some rewriting was required to ensure all names inside the bundle point to the correct location.

Interface Extraction

As a final highlight, we improved the Hax frontend to handle interface extraction better. With this recent breakthrough, the Hax frontend now successfully extracts to F* more than 99% of the top 600 Rust crates, including protobuf, a widely deployed serialization library used in Sandwich. This result brings us one step closer to achieving our goal of including formal methods in our software development pipeline.

Conclusions

In this blog post, we described our efforts to formally verify the critical components of Sandwich. A major highlight is that we successfully verified that, in the context of establishing a Sandwich-configured TLS connection using OpenSSL 3, X.509 certificates are correctly validated.

A significant part of this effort was dedicated to improving the tools, which is essential for making formal methods more practical and scalable in this and similar contexts. These improvements not only strengthened the security guarantees of Sandwich but also laid the groundwork for applying these tools to similar contexts.

Our work demonstrated that formal verification can be integrated into real-world software development, improving security and developer confidence.