digamma.ai

Ilia Zaichuk, proof engineer at Digamma.ai

You’ve probably heard of Signal, right? It’s that messaging app that doesn’t suck. Okay, it might not have all the fancy features that some other apps have, but at least with Signal, you’re not handing over your private chats to the likes of Mark Zuckerberg or the NSA.

Now, I’m not here to get you to use Signal or to tell you it’s the ultimate secure messaging app. Actually, I’m here to say it could be even more secure! Sure, it’s good enough for sharing cute pics of your pup, but it’s not quite ready for something as important as, say, nuclear codes.

The thing is, Signal is built on some seriously strong math, using algorithms that claim to offer top-notch security and privacy for users. If these algorithms are implemented right, they should be pretty solid. But that’s the big question – is Signal’s code as trustworthy as the math it’s based on?

Luckily, there’s a way to find out. There are techniques that can actually prove, mathematically speaking, that Signal’s algorithms, protocols, and code are on point, making it super secure. These techniques are called formal verification. But before we dive into how that works, let’s take a closer look at what Signal promises in terms of security.

Recently a zero-day exploit (CVE-2021-31440) was found in the Linux kernel eBPF module. We will show how this bug could have been discovered and prevented using formal verification. A relatively simple logical error caused this bug, but it is easy to overlook and could lead to grave security implications. The bugs like this are difficult to find via exhaustive testing as the space of value combinations you need to test to stumble on it is relatively big. The typical way to find these bugs is by expert code reviews. Formal verification is offering another way to prevent or find bugs like this. Instead of spending the expert’s time pouring over the code looking for potential bugs, the specification is created, formally stating what the code is supposed to do. Then, using a proof assistant, a proof is developed that the given implementation satisfies this specification. If this proof is successful, it provides a bullet-proof guarantee that the code is correct wrt spec. Sometimes, as we will see in this example, the correctness could not be proved, which indicates that the implementation contains a bug. In this example, we will:

1. Write a formal specification.
2. Try to prove correctness for the buggy version of the code.
3. Prove the correctness of the patched version of the code.