This blog post details an example of how to use our hax toolchain for verifying the security of cryptographic protocol implementations written in Rust.

When building high-assurance software, we use different verification techniques with different goals.

One goal is to prove implementation correctness. In this case the code in question is proven to be free of panics, or that the optimizations that it uses preserve conformance to a higher-level mathematical specification. hax is well-suited to doing this type of verification, by extracting a model of the code in F*. A recent example of this approach is our verified implementation of ML-KEM (Kyber). You can read more details about the verification effort in a separate blog post.

Another flavor of verification is security verification, where we want to establish, beyond correctness, that a piece of code achieves specific properties even in the presence of an attacker. For example, we recently joined forces with Rolfe Schmidt and Charlie Jacomme to provide a protocol analysis of Signal’s new PQXDH post-quantum key agreement protocol. In this case, though we found no serious security issues, we made out a number of imprecisions and potential pitfalls in the original specification and Signal addressed these with a new version of the protocol specification. For the new specification we used the ProVerif and CryptoVerif protocol analysis tools to show among other results that security properties such as forward secrecy are preserved in the presence of a quantum attacker and that the protocol resists store-now-decrypt-later attacks.

The analysis of PQXDH was carried out in the traditional style, where a group of protocol verification experts diligently model a protocol by hand, based on its (more or less formal) specification.

Today we want to introduce you to a new way to carry out protocol analysis that allows protocol developers themselves to extract a model for security analysis directly from an existing Rust implementation of the protocol, using hax. Moreover, since hax already provides mature facilities for correctness verification of real world Rust code, it is now possible to perform both, correctness and security proofs, based on the same Rust code!

In the remainder of this post, we’ll give you a little tour of hax’s latest backend to the ProVerif protocol analyser. We’ll first give you some background on ProVerif and its capabilities, then we’ll show you how hax translates real Rust code into models for ProVerif, and finally we’ll talk about our first milestone for the ProVerif backend; a new analysis of the TLS 1.3 handshake based on a model extracted automatically from a real Rust implementation.

ProVerif & Symbolic verification

Before we get started, a little background on protocol analysis using ProVerif.

ProVerif is a protocol verification tool, which allows specifying a model of a protocol in a language called the Applied Pi-Calculus. It allows to analyse a large number of possible attackers on a protocol. Once the models are written, ProVerif is fully automated and will either prove the security in the given scenarios, or construct an attack. The Applied Pi-Calculus, used in ProVerif, considers processes which communicate with each other using channels. The messages that are communicated are considered purely symbolically, meaning that they are terms that are constructed and can be deconstructed. The protocol designer has to define constructors and destructors for the terms that make up the messages of the protocol, as well as define processes which model the participants of the protocol.

Extracting PV Models with hax

Consider the following, very simple example protocol between an initiator and a responder:

1. The initiator sends a message Ping that carries a string payload to the responder.
2. The responder replies with a message Pong that echoes the initial payload string.

In Rust, we can describe the messages and code to generate them as follows:

pub struct Ping {
    payload: String,
}

pub struct Pong {
    payload: String,
}

pub fn send_ping(payload: String) -> Ping {
    Ping { payload }
}

pub fn send_pong(received: Ping) -> Pong {
    Pong {
        payload: received.payload
    }
}

pub fn receive_pong(received: Pong) -> String {
    received.payload
}

Defining a struct for the message types is not required for this toy protocol, but will serve us to show how hax will translate message types for more complicated protocols.

Using hax to extract ProVerif from a Rust crate can work as easily as running

cargo hax into proverif

within the crate.

hax’s ProVerif backend will then translate the Rust code to a ProVerif model. By default, it does this roughly as follows:

• Data structures, such as structs and enums are translated to types in ProVerif. Each type get a constructor that allows ProVerif process to construct terms of that type, as well as deconstructors that allow processes to retrieve the terms that make what would be for example field values in Rust. The Ping struct from the above example is translated to the following ProVerif code:

  type ping_pong__t_Ping.
  
  fun ping_pong__t_Ping_to_bitstring(ping_pong__t_Ping)
    : bitstring [typeConverter].
  fun ping_pong__t_Ping_from_bitstring(bitstring)
    : ping_pong__t_Ping [typeConverter].
  const ping_pong__t_Ping_default_value: ping_pong__t_Ping.
  letfun ping_pong__t_Ping_default() =
       ping_pong__t_Ping_default_value.
  letfun ping_pong__t_Ping_err() =
       let x = construct_fail() in ping_pong__t_Ping_default_value.
  fun ping_pong__Ping_c(alloc__string__t_String)
    : ping_pong__t_Ping [data].
  reduc forall ping_pong__Ping_f_payload: alloc__string__t_String;
    accessor_ping_pong__Ping_f_payload(
      ping_pong__Ping_c(ping_pong__Ping_f_payload)
    ) = ping_pong__Ping_f_payload.
  

  The code above includes a number of automatically generated constructs, like the _to/from_bitstring, _default, or _err portions of the generated code. These are necessary to automatically model Rust language features, which are not available in ProVerif.

• Rust functions (fn) are translated to process macros – parts of ProVerif processes, which can be called like functions. These make use of the constructors and deconstructors that were generated for the crate’s data structures. The above message handling functions are thus translated as follows to ProVerif:

  letfun ping_pong__receive_pong(received : ping_pong__t_Pong) =
       let ping_pong__Pong_c(payload) = received in
       payload.
  
  letfun ping_pong__send_ping(payload : alloc__string__t_String) =
       ping_pong__Ping_c(payload).
  
  letfun ping_pong__send_pong(received : ping_pong__t_Ping) =
       let ping_pong__Ping_c(payload) = received in
       ping_pong__Pong_c(payload).
  

Now we need to manually define top-level processes for the protocol participants using the extracted macros and type translations.

let Initiator(input: alloc__string__t_String) = 
    let ping = ping_pong__send_ping(input) in
    out(c, ping);
    in(c, pong: ping_pong__t_Pong);
    let output = ping_pong__receive_pong(pong) in
    0.

let Responder() = 
    in(c, ping: ping_pong__t_Ping);
    let pong = ping_pong__send_pong(ping) in
    out(c, pong);
    0.

process
    new input: alloc__string__t_String;
    Initiator(input) | Responder

We compose the Initiator and Responder processes to run an instance of the initiator with a “fresh” input in parallel with an instance of the responder.

If this were a protocol with security goals we could now start asking ProVerif about its trace properties. For example, is it correct that if the initiator receives a Pong message with a certain payload, it must have sent that same payload before in a Ping message?

Verifying TLS 1.3 with hax and PV

Now with an idea of the hax-ProVerif workflow, let’s talk about our first major milestone for the ProVerif backend. Earlier this year we used hax-ProVerif to extract and verify a model from Bertie, our minimal implementation of TLS 1.3 at Cryspen.

More specifically, we let hax extract a model of the TLS 1.3 handshake protocol:

The figure above shows the idealized message flow of the handshake protocol and the names of the Rust functions that generate the exchanged messages in the form of HandshakeData structs, for example to initiate a session with a server a client will eventually call tls13handshake::client_init to obtain a HandshakeData struct which contains the ClientHello message, including the client’s key share. In the full TLS 1.3 protocol, that handshake data type is then encoded as a TLS record for sending over the wire. For our security modelling of the handshake protocol, we abstract away the encoding and decoding of handshake data structures, as well as record encryption.

(A concurrent analysis of Bertie using the F* backend focused especially on correctness of these parts that were abstracted away in the protocol security analysis.)

In a model that allows the attacker to perform long term key compromise attacks on the server, we could show that Bertie’s implementation of the handshake achieves server authentication. This means that every time a client concludes a handshake session with its desired counterpart server, the server must have also concluded a session with the client, unless either the server’s certificate private key or a pre-shared key from a previous protocol session had been compromised. Either of which would allow an attacker to mislead the client into finishing the handshake with an attacker controlled counterpart instead.

Additionally, we can show that an authenticated session guarantees session key confidentiality. Session key confidentially says that the derived session key is never revealed to an attacker.

All in all, we extracted a model of about 4500 lines of ProVerif code from around 900 lines of Rust code implementing the handshake, and the additional code for setting up top-level processes and formulating security queries comes in at around 500 lines of ProVerif code.

Conclusion

While the successful extraction of the TLS 1.3 handshake from the Bertie crate is a great first milestone for hax-PV, this is just a starting point and there are rough edges that should be smoothed out in time.

• Keen-eyed readers of the above example extraction will have noticed, for example, that it’s not self-contained, indeed it references a type alloc__string__t_String, which is supposed to be the ProVerif name for the Rust String type. For this type, and anything else that is not defined in your crate (this includes the Rust core library) we have to provide pre-defined, in the case of core types, or handwritten abstractions that model the desired behaviour in ProVerif. Expanding the set of general-purpose models for core types that can be automatically included in the extraction is one major goal going forward, as is improving the ergonomics of providing hand-written extensions to the extracted model when that is necessary.
• Another part that currently has to be manually modeled is top-level processes and security analysis queries. We envision that in the future hax-PV will at least be able to automatically extract a generic top-level process and perhaps certain types of security queries (e.g. secrecy of parts of the party state), given lightweight annotation of the Rust sources. This would make obtaining basic protocol analysis results much easier to achieve for non-experts in ProVerif and protocol modelling.
• We’re also looking into improving the readability of the extracted model. It’s crucial that security analysts can understand the extracted model, so a reasonable style for the generated code is essential, especially if the model grows to thousands of lines of code.

If you have a favorite protocol that would benefit from security analysis using ProVerif and it is implemented in the ever-growing subset of Rust that is supported by hax, let’s chat about it!