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:

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

The tools we will be using:

- The Coq proof assistant. It provides a formal language to write mathematical definitions, executable algorithms, and theorems and an environment for the interactive development of machine-checked proofs.
- Verified Software Toolchain (VST) is a tool for stating specifications and proving theorems about code written in C. Combined with the verified C compiler, CompCert one gets unprecedented end-to-end correctness guarantees.

The affected function is **reg_combine_64_into_32**.

static void __reg_combine_64_into_32(struct bpf_reg_state *reg) { __mark_reg32_unbounded(reg); if (__reg64_bound_s32(reg->smin_value) && __reg64_bound_s32(reg->smax_value)) { //(1)reg->s32_min_value = (s32)reg->smin_value; reg->s32_max_value = (s32)reg->smax_value; } if (__reg64_bound_u32(reg->umin_value)) //(2)reg->u32_min_value = (u32)reg->umin_value; if (__reg64_bound_u32(reg->umax_value)) //(3)reg->u32_max_value = (u32)reg->umax_value; __reg_deduce_bounds(reg); __reg_bound_offset(reg); __update_reg_bounds(reg); }

The function uses the known bounds on a 64-bit register (**smin_value**, **smax_value**) to infer bounds for the register’s lower 32 bits (**s32_min_value**, **s32_max_value**).

First, the bounds are set to minimal and maximal signed and unsigned values, respectively (**S32MIN**, **S32MAX**, etc.) using **__mark_reg32_unbounded**.

Then in (1), after checking whether **smin_value** and **smax_value** are within 32-bit bounds,
the register’s allowed min and max values are updated accordingly.

`if (__reg64_bound_s32(reg->smin_value) && __reg64_bound_s32(reg->smax_value)) { // `**(1)**
reg->s32_min_value = (s32)reg->smin_value;
reg->s32_max_value = (s32)reg->smax_value;

The bug is in lines (2) and (3), where the checks are performed separately, which leads to a case when the minimum value is updated, but the maximal is not, and the bounds are inferred incorrectly.

if (__reg64_bound_u32(reg->umin_value)) //(2)reg->u32_min_value = (u32)reg->umin_value; if (__reg64_bound_u32(reg->umax_value)) //(3)reg->u32_max_value = (u32)reg->umax_value;

To see the problem, assume that **reg->umin_value = 1** and **reg->umax_value = (1 << 32)**. Then the 32-bit minimum bound will be set to 1 after the check-in (2). Since (3) is false, the maximum bound will not be updated. Hence, the inferred bounds are incorrect since the lower 32 bits of **umax_value** are 0. Check out a detailed description of the bug and how it is exploited here.

The proposed fix is to replace (2) and (3) with one check as in (1) so that **u32_min_value** and **u32_max_value** are updated simultaneously.

static void __reg_combine_64_into_32(struct bpf_reg_state *reg) { __mark_reg32_unbounded(reg); if (__reg64_bound_s32(reg->smin_value) && __reg64_bound_s32(reg->smax_value)) { reg->s32_min_value = (s32)reg->smin_value; reg->s32_max_value = (s32)reg->smax_value; }- if (__reg64_bound_u32(reg->umin_value))+ if (__reg64_bound_u32(reg->umin_value) && + __reg64_bound_u32(reg->umax_value)) {reg->u32_min_value = (u32)reg->umin_value;- if (__reg64_bound_u32(reg->umax_value))reg->u32_max_value = (u32)reg->umax_value;+ }

With this fix, in the problematic case, the bounds won’t be updated, and **u32_max_value** will stay **U32MIN**. In Coq, we can prove that bounds will always be updated correctly. First, we formulate what property is needed to prevent such problems, and this will be our specification. In English, it is simply “*either both u32_min_value and u32_max_value values are updated, or neither*“. We formalize this statement in logic in the following way:

(s32_min_value =int64_to_32(smin_value64)⋀s32_max_value =int64_to_32(smax_value64)⋁s32_min_value = S32Min⋀s32_max_value = S32Max)⋀(u32_min_value =int64_to_32(umin_value64)⋀u32_max_value =int64_to_32(umax_value64)⋁u32_min_value = U32Min⋀u32_max_value = U32Max)

We prove that **__reg_combine_64_into_32** corresponds to this specification in Coq using VST. We show that after executing the function, (a) and (b) are true. More precisely, we prove a Hoare logic triple **PRE { C } POST**, where the precondition **PRE** states that input to the function is any **reg** struct,** C** is an abstract representation of the C program in Coq **f__reg_combine_64_into_32,** and the postcondition states that values stored in **reg** after execution are correct.

PRE := reg C:= f__reg_combine_64_into_32 POST := (reg -> s32_min_value = (int64_to_32 smin_value64) ⋀ reg -> s32_max_value = (int64_to_32 smax_value64)) ⋁ (reg -> s32_min_value = S32Min ⋀ reg -> s32_max_value = S32Max); (reg -> u32_min_value = (int64_to_32 umin_value64) ⋀ reg -> u32_max_value = (int64_to_32 umax_value64)) ⋁ (reg -> u32_min_value = U32Min ⋀ reg -> u32_max_value = U32Max)

The proof is done by so-called forward simulation: we start with the precondition (which is empty in our case) and prove that the postcondition is true once we reach the last statement of the program. The proof is 71 lines long, which may seem a lot for such a short program, but it is conceptually simple and ⅓ of the proof are verbose intermediate VST specifications that correspond to one step in the proof.

We can see that in the buggy version, the proof doesn’t go through, and we are left with statements that cannot be proven. This is indicative of a bug in the program. Examining the cases in the proof script leading to unprovable goals allows one to identify counterexamples or narrow down the cases helping to locate the exact bug location in the source code. For example, we have the following unprovable goal:

int64_to_32(umin_value64) =int64_to_32(umin_value64)⋀U32MAX =int64_to_32(umax_value64)⋁int64_to_32(umin_value64) = U32MIN⋀U32Max = U32MAX

It corresponds to the bug described above: **32****umin_value ** was updated to **umin_value64** and **32****umax_value ** was not updated and stayed **U32MAX**.

Hence, formal verification can both help find bugs and exploits or prove that there is none.

For the full specification and proof, see this GitHub repository.

If you want to bulletproof your code, please reach out to us at hello@digamma.ai. Digamma could assess your system and determine parts of it that could benefit from formal verification. We would help you to create a formal specification of a feature defining safety, security, and reliability constraints, as well as functional correctness guarantees. And then, we can mathematically prove it and verify your code.