We’ve been working to improve usability for SAW, our tool for verification of C and Java programs. The primary way that users interact with SAW is its specification and scripting language. In order to make SAW as accessible as possible, Python can now be used as that language for SAW! We’ve built an example to demonstrate that new capability, performing verification of part of the C implementation of the Signal Protocol. In particular, we identify the conditions under which a Signal Protocol message will be successfully authenticated as a SAW specification.

The Python SAW client

SAW can be controlled from Python through the saw-client library on PyPI. There’s nothing magic about Python that makes this work—it controls SAW through a JSON-RPC API, as demonstrated in an earlier post. The saw-client library has come a long way since then, and the library now offers a high-level interface that takes care of the RPC-related details behind the scenes.

Besides Python, SAW also has an alternative scripting language called SAWScript. While SAWScript is capable of writing the same proofs as Python, it’s not without its drawbacks. SAWScript is a custom language, so it imposes a barrier to entry for those trying to learn SAW for the first time. Moreover, SAWScript has basically nothing in the way of external libraries. If you want to do something in SAWScript that the standard library doesn’t provide, you will have to figure out how to implement it yourself.

On the other hand, Python is a widely used language that will be familiar to many more people from the get-go. It also has a rich ecosystem of libraries and tooling through PyPI. Even if Python isn’t your favorite programming language, we encourage you to give saw-client a try. If nothing else, the code in saw-client can serve as inspiration for how to implement a similar client in a different language.

A basic spec in saw-client

Let’s see how saw-client can be used to write specifications for real-world C code. Our case study is libsignal-protocol-c. This library contains a C implementation of the Signal Protocol, a cryptographic protocol used to encrypt instant messages, voice calls, and video calls. This protocol is used in the Signal messenger application, after which it is named, but it is also supported in other applications such as WhatsApp, Facebook Messenger, and Skype.

If you are more interested in a high-level description of what SAW is able to prove about libsignal-protocol-c, feel free to skip to the Future Directions section.

To start, let’s take a look at a key data structure used in libsignal-protocol-c, the signal_buffer:

struct signal_buffer {
    size_t len;
    uint8_t data[];
};

A signal_buffer is an array of bytes (data) where the length is equal to len. Any time you send a message using libsignal-protocol-c, a signal_buffer will lie at the heart of the message.

If we want to have confidence that libsignal-protocol-c is working as advertised, we will need to verify that the contents of a message’s signal_buffer match what is expected. The library checks whether two signal_buffers match up by way of the signal_constant_memcmp function:

int signal_constant_memcmp(const void *s1, const void *s2, size_t n)
{
    size_t i;
    const unsigned char *c1 = (const unsigned char *) s1;
    const unsigned char *c2 = (const unsigned char *) s2;
    unsigned char result = 0;

    for (i = 0; i < n; i++) {
        result |= c1[i] ^ c2[i];
    }

    return result;
}

Intuitively, signal_constant_memcmp checks if the contents of two signal_buffers’ byte arrays are the same. If they are the same, the function will return 0. If they are not the same, they will return a value indicating the bytes in which the contents of the arrays differ.

With that said, it might not be obvious at first glance that this function returns 0 if the arrays are the same. After all, there is a fair amount of bit-twiddling going on, and it’s possible that someone made a mistake when writing the bit-manipulating code. We can verify this code’s correctness by checking it against a specification written in saw-client. The specification will look broadly like this:

from saw_client.llvm import *

class ConstantMemcmpEqualSpec(Contract):
    def specification(self) -> None:
        _1

        self.execute_func(_2)

        _3

The Contract class characterizes SAW specifications by way of the specification method. To write your own specification, you simply create a subclass of Contract and override the specification method as shown above. Each specification has three parts:

• Preconditions (_1), which indicate the assumptions to make before invoking the function being verified.
• The arguments to pass to the function being verified (_2).
• Postconditions (_3), which indicate the things that must be checked after invoking the function being verified.

With this vocabulary in mind, we can turn our intuition of how signal_constant_memcmp works into a SAW specification:

class ConstantMemcmpEqualSpec(Contract):
    n: int

    def __init__(self, n: int):
        super().__init__()
        self.n = n

    def specification(self) -> None:
        s1  = self.fresh_var(array_ty(self.n, i8), "s1")
        s1p = self.alloc(array_ty(self.n, i8), points_to = s1)
        s2  = self.fresh_var(array_ty(self.n, i8), "s2")
        s2p = self.alloc(array_ty(self.n, i8), points_to = s2)
        self.precondition(cryptol(f"{s1.name()} == {s2.name()}"))

        self.execute_func(s1p, s2p, cryptol(f"{self.n} : [64]"))

        self.returns(cryptol("0 : [32]"))

The preconditions are that there are two byte arrays (s1p and s2p) whose contents (s1 and s2) are the same. The call to self.precondition(…) in particular is what ensures that the contents are the same. The argument to self.precondition(…) is written in Cryptol, a DSL for specifying cryptographic code. This particular Cryptol expression is rather simple, as it only performs an equality check, but we will see more complicated Cryptol examples later.

The arguments to the function are the two byte arrays along with their length (self.n), which is first converted into a Cryptol expression so that SAW can reason about it. Finally, the postcondition is that the function returns 0, again as a Cryptol expression.

Once that scaffolding is in place, we can actually check that signal_constant_memcmp matches the specification we wrote:

mod = llvm_load_module("libsignal-protocol-c.bc") # An LLVM bitcode file
array_len = 42 # Pick whichever length you want to check
llvm_verify(mod, "signal_constant_memcmp", 
ConstantMemcmpEqualSpec(array_len))

If all goes well, we can run this code in Python and see the following result:

✅  Verified: lemma_ConstantMemcmpEqualSpec (defined at signal_protocol.py:122)

Hooray! SAW verified the correctness of signal_constant_memcmp, and what’s more, we never needed to mention anything about the bit-twiddling inside of the function—SAW is powerful enough to reason about this automatically. Note, however, that ConstantMemcmpEqualSpec only specifies what happens when the byte arrays are equal. If we wanted to characterize what happens when the byte arrays are not equal, we would need a slightly more sophisticated spec.

One additional thing to note is that there is some amount of repetition in the code above, as we call self.fresh_var() followed by self.alloc() twice. Fortunately, the use of Python makes abstracting out this pattern cheap and cheerful:

def ptr_to_fresh(spec: Contract, ty: LLVMType,
                 name: str) -> Tuple[FreshVar, SetupVal]:
    var = spec.fresh_var(ty, name)
    ptr = spec.alloc(ty, points_to = var)
    return (var, ptr)

class ConstantMemcmpEqualSpec(Contract):
    ...

    def specification(self) -> None:
        (s1, s1p) = ptr_to_fresh(self, array_ty(self.n, i8), "s1")
        (s2, s2p) = ptr_to_fresh(self, array_ty(self.n, i8), "s2")
        ...

Verifying code involving HMAC

There’s much more to libsignal-protocol-c than just storing messages—it also has to send and receive them. Moreover, it needs to encrypt messages so that they can only be read by the intended receiver, lest private communication be vulnerable to interception by third parties.

One key step in encrypting a message is attaching a message authentication code (MAC), which can be used to verify that the contents of a message have not been changed after it was sent. In particular, libsignal-protocol-c uses HMAC, a type of MAC that is computed using a cryptographic hash function.

The precise details of how HMAC works are beyond the scope of this post, and luckily, we don’t need to know the details precisely in order to write SAW specifications related to HMAC. Instead, we can abstract away the details using uninterpreted functions. To start, let’s define some Cryptol functions that outline the skeleton of how HMAC works:

hmac_init : {n} [n][8] -> HMACContext
hmac_init = undefined

hmac_update : {n} [n][8] -> HMACContext -> HMACContext
hmac_update = undefined

hmac_final : HMACContext -> [SIGNAL_MESSAGE_MAC_LENGTH][8]
hmac_final = undefined

These will be the uninterpreted functions we use to specify HMAC-related code in libsignal-protocol-c. The basic idea is that given a cryptographic key as input, hmac_init will produce an HMACContext. This HMACContext will be updated multiple times with hmac_update using the data from the first argument. Lastly, hmac_final will turn the HMACContext into a signal_buffer that is sufficiently long to store the MAC.

The definition of HMACContext depends on which cryptographic hash function is used in conjunction with HMAC. libsignal-protocol-c is parameterized over the hash functions it uses, so one could plug and play OpenSSL, Common Crypto, or another suitable library.

Because these functions will appear uninterpreted, SAW will not evaluate them during verification. As a result, the implementations of these functions are unimportant. We have chosen undefined for the sake of convenience, but any other implementation would suffice.

With these functions defined, we can link them up to the corresponding C functions in the library itself. For example, here is an abridged specification for the signal_hmac_sha256_init C function:

class SignalHmacSha256InitSpec(Contract):
    key_len: int

    def specification(self) -> None:
        hmac_context_ptr = self.alloc(...)
        (key_data, key)  = ptr_to_fresh(self, array_ty(self.key_len, i8),
                                        "key_data")
   	 
        self.execute_func(..., hmac_context_ptr, key,
                          cryptol(f"{self.key_len} : [64]"))

        init = f"hmac_init`{{ {self.key_len} }} {key_data.name()}"
        dummy_hmac_context = self.alloc(..., points_to = cryptol(init))
        self.points_to(hmac_context_ptr, dummy_hmac_context)
        self.returns(cryptol("0 : [32]"))


key_len = 32
init_spec = llvm_assume(mod, "signal_hmac_sha256_init",
                        SignalHmacSha256InitSpec(key_len))

Don’t worry about understanding every line of code here. The most important part is the last line, which uses llvm_assume instead of llvm_verify. The llvm_assume function allows SAW to use a specification without actually simulating it—in effect, treating it like an axiom. This allows us to tie the behavior of signal_hmac_sha256_init to the uninterpreted hmac_init function in the spec’s postconditions.

We can also use llvm_assume in similar ways to create specifications involving hmac_update and hmac_final. Once that is done, it is time to verify a very important MAC-related function: signal_message_verify_mac. In essence, this function takes a message as an argument, computes the MAC for the data inside of the message, and checks that it matches the MAC that is attached to the end of the message. If they match, we can be reasonably sure that the message was not modified while being sent to the receiver.

Explaining every detail of how signal_message_verify_mac works would be quite involved, so for the purposes of this post, we will only present the punchline: what should the contents of the message look like? The data inside of the message can be arbitrary, but the MAC at the end must have a very particular shape. That shape can be defined with a Python function:

def mk_hmac(serialized_len: int, serialized_data: FreshVar,
        	receiver_identity_key_data : FreshVar,
        	sender_identity_key_data: FreshVar,
        	mac_key_len: int, mac_key_data: FreshVar) -> SetupVal:
    sender_identity_buf = f"""
        [{DJB_TYPE}] # {sender_identity_key_data.name()}
            : [{DJB_KEY_LEN} + 1][8]
        """
    receiver_identity_buf = f"""
        [{DJB_TYPE}] # {receiver_identity_key_data.name()}
            : [{DJB_KEY_LEN} + 1][8]
        """
    hmac = f"""
        hmac_final
         (hmac_update`{{ {serialized_len} }} {serialized_data.name()}
          (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({receiver_identity_buf})
           (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({sender_identity_buf})
            (hmac_init`{{ {mac_key_len} }} {mac_key_data.name()}))))
        """
    return cryptol(hmac)

Whew, that’s quite hefty! Again, don’t try to understand every line of code here. The important part is that this first calls hmac_init, followed by multiple hmac_update calls, and topped off with an hmac_final call. This very closely corresponds to the intuitions we developed earlier for HMAC, so if SAW verifies that the MAC looks like this Cryptol expression, we can be confident that it is working as expected.

Next, we need to use this in a specification. Here is an excerpt of the specification for signal_message_verify_mac, which describes what a valid message should look like in its preconditions:

class SignalMessageVerifyMacSpec(Contract):
    serialized_len: int

    def specification(self) -> None:
        ...
        mac_index = 8 + self.serialized_len - SIGNAL_MESSAGE_MAC_LENGTH
        ser_len   = f"{self.serialized_len} : [64]"

        self.points_to(serialized[0], cryptol(ser_len))
        self.points_to(serialized[8], serialized_message_data)
        self.points_to(serialized[mac_index], mk_hmac(...))

        self.execute_func(...)

        self.returns(cryptol("1 : [32]"))

Here, serialized points to the signal_buffer for the overall message. We can use Python’s slice notation (e.g., serialized[0]) to describe the memory contained in different parts of the buffer. The first part contains self.serialized_len, the overall length of the message. Eight bytes after that is where serialized_message_data, the message data, is found. Finally, the very end of the buffer contains the MAC as computed by mk_hmac(…).

The rubber finally hits the road when we call llvm_verify in concert with this spec. This time, we have to pass some additional arguments. We need to explicitly indicate which assumptions we made earlier with llvm_assume by way of the lemmas argument. We also need to tell the SMT solver which functions should be treated as uninterpreted by way of the script argument:

uninterps = ["hmac_init", "hmac_update", "hmac_final"]
llvm_verify(mod, "signal_message_verify_mac",  SignalMessageVerifyMacSpec(...),
            lemmas=[init_spec, update_spec1, update_spec2, final_spec],
            script=ProofScript([z3(uninterps)]))

The result of all this work is a very, very satisfying green checkmark:

✅  Verified: lemma_SignalMessageVerifyMacSpec (defined at protocol.py:160)

Future directions

With saw-client, we were able to prove some interesting results about the code in libsignal-protocol-c. We were able to demonstrate that signal_message_verify_mac, the function which checks the integrity of a message sent using the Signal Protocol, works correctly when the last part of a message contains a proper message authentication code (MAC). Moreover, we characterized what the contents of the MAC should be relative to an abstract specification of cryptographic hash functions. 

There is so much more that could be done beyond what was shown in this post, however. While we verified a key property of the code which checks the integrity of messages, we did not go as far as demonstrating that messages sent over the wire pass this integrity check. We also avoided completely specifying the behavior of HMAC, although this would be possible to do—see this post for the full details.

Although saw-client can hold its own as a tool for writing proofs, there are some places where saw-client hasn’t quite reached parity with SAWScript. There are some SAW capabilities that saw-client doesn’t currently support, such as initializing global variables in specs. Moreover, there are some SAWScript idioms that don’t look quite as nice in saw-client, such as quasiquotation of Cryptol expressions. We believe these limitations can be overcome with more thought and implementation effort.

Going forward, we aim to make Python a first-class citizen when it comes to writing SAW proofs, and this work is a first step in that direction. If you want to take a closer look at the code presented in this post, you can find it at the saw-demos repo under the demos/signal-verification directory. We encourage you to try out saw-client yourself, and if you find anything that could be improved, don’t hesitate to file issues on the SAW issue tracker.