We have to deal with undecidable problems when reasoning about data trees using Mso-D or Sdtas, and this is unavoidable if we want to *(a)* handle trees with data from infinite domains, and *(b)* relate data from different nodes. These two features make Sdtas *Turing-powerful* since they can encode executions of two-counter machines. A similar argument holds for the satisfiability problem of Mso-D, since we can write a formula that allows us to relate data in consecutive nodes. By prohibiting the propagation of unbounded information between nodes, the decidability of relevant decision problems can be recovered (see [11,12] for an account on this). However, these features are both essential to deal with data structures such as Bsts, Rbts, AVL trees, Heaps, etc.

A way to cope with undecidability is to encode the executions of an Sdta as a system of CHCs (*Constrained Horn Clauses*) or, equivalently, as a CLP (*Constraint Logic Program*) [26], and solve the system using efficient off-theshelf tools. Systems of CHCs correspond to a restricted class of first-order logic, and are a versatile formalism for representing and solving a variety of program verification or model checking problems, including those regarding sequential, concurrent, and functional programs. Efficient algorithms have been proposed for solving systems of CHCs, often leveraging or generalizing techniques developed in the context of automatic program verification [2,21,22]. As a result, CHCs are often used as an intermediate representation in a variety of verification and synthesis tools [6,18,20,23,25,27,29,35]. Here, we follow a similar approach to solve the emptiness problem for Sdtas, and this offers several advantages. First, it provides a separation of concerns, allowing users of our framework to focus only on aspects related to the tree data structure at hand, while giving CHC solver developers a clean framework that can be instantiated using various model checking algorithms and specialized decision procedures. Furthermore, by expressing CHCs in the standard SMT-LIB language, one can take advantage of different CHC engines, whose performance keeps improving year-over-year, as witnessed by the *competition on constrained Horn clauses* CHC-COMP [19].

As a third contribution, we show several results linking the Mso-D satisfiability problem to the emptiness of Sdtas, and thus to the problem of solving a CHC system. A fundamental theorem for the class of regular (word or tree) languages states that a language is regular if and only if it is Mso-definable, i.e., definable by a closed formula (i.e., a sentence) of standard Mso [4,5,14,15,39,41]. Here, we show that if we allow Mso-D data predicates to talk only about the data of a single node, the satisfiability problem can be reduced to the emptiness of Sdtas. Furthermore, both decision problems are decidable in this case [11]. Moreover, we identify a larger undecidable syntactical fragment of Mso-D where the above reduction can still be performed. Namely, we give an effective reduction when the Mso-D formula is of the form ∃*x*∀*y* . ϕ(*x*, *y*), where ϕ can contain additional quantifiers and each data constraint in ϕ is either unary, or accesses the data in a bounded neighborhood of the nodes referred to by *x* and at most one of the variables of *y*. We show that this fragment is very expressive as it allows us to characterize a variety of tree data structures from the literature, solve certain infinite-state games, and handle many other potential applications.

As a fourth and final contribution, we have implemented the reduction for the syntactic Mso-D fragment described above in a prototype tool that combines an Mso decision procedure over trees (Mona [28]) with a CHC engine (of the SMT solver Z3 [24,36]). Using this tool we have conducted several experiments to demonstrate the effectiveness and the practicality of our approach.

*Organization of the Paper.* The rest of the paper is organized as follows. Section 2 defines data trees, while Sect. 3 introduces the Mso-D logic. Section 4 deals with the definition of Sdtas, and Sect. 5 shows that the emptiness problem for Sdtas is undecidable in general but can be solved by off-the-shelf CHC engines. Section 6 shows a reduction from the Mso-D satisfiability problem to the emptiness of Sdtas, for the Mso-D fragment ∃*x*∀*y* . ϕ(*x*, *y*). Section 7 describes our prototype implementation and summarises our experimental evaluation. Related work and concluding remarks can be found in Sect. 8 and 9, respectively.

#### **2 Data Trees**

Here we formally define *data trees*. We deal with trees that are finite in size and labeled with data from possibly infinite domains. We consider only binary trees (i.e., trees of arity 2) to keep notation to a minimum. However, the methods and approaches presented in the paper apply to any class of trees of fixed arity.

We will use N to denote the set of all natural numbers, Z to stand for the set of integers, and B to represent the set {0, 1}. For a number n ∈ N, we write [n] to denote the interval {1,...,n}.

**Words.** An *alphabet* is a finite set of *symbols*. A *word* w over an alphabet Σ is a finite (possibly empty) sequence w = a1a2 ...an where ai ∈ Σ for i ∈ [n]. We denote with |w| the *length* of the sequence of symbols forming w. The *empty word*, denoted by , is the word formed by no symbol. We denote the set of all words over Σ by Σ∗. A *language* L over Σ is any subset of Σ∗. A *prefix* (resp. *suffix*) of a word w is either , or any sequence a1 ...aj (resp., aj ...an), for some j ∈ [n]. Given two words a = a1a2 ...an and b = b1b2 ...bm, their *concatenation* denoted ab, is the word a1a2 ...anb1b2 ...bm. Given a word w ∈ Σ∗ and a language L ⊆ Σ∗, we define *Ext*(w, L) as the language of all words w such that ww is a word in L, i.e., *Ext*(w, L) = {w | ww ∈ L}.

**Trees.** A *binary tree* T, or simply a *tree*, is a finite and prefix-closed subset of {0, 1}∗. We call the elements of T *nodes*, and the node identified by the *root* of T. The *edge relation* is defined implicitly: for d ∈ {0, 1}, if v and vd are both nodes of T, then (v, vd) is an *edge* of T. Further, if d is 0 (resp., 1) we say that vd is the *left* (resp., *right*) *child* of v, and v is the *parent* of vd. A *leaf* is a node with no children, while an *internal node* is a node that is not a leaf. The *height* of T is maxt∈T |t|. The *sub-tree* of T rooted at a given node t ∈ T is *Ext*(t, T). Further, *Ext*(t, T) is a *left* (resp., *right*) *sub-tree* of t if t = t 0 (resp., t = t 1), for some t ∈ T. The k-th *level* of a tree T consists of the sequence of all t ∈ T, with |t| = k, sorted in ascending lexicographic order. Further, the k-th *level* of T is filled *left to right* if it is a prefix of the k-th *level* of {0, 1}∗.

**Data Signatures.** Data signatures are like structured data types (a.k.a. *records*) in programming languages: a *data signature* S is a set of pairs {*id*i : *type*i}i=1...n. Common types of interest include bounded or unbounded integers (denoted by int and Z, resp.), floating point rationals and real numbers (float and R), the Boolean type B and the bit vectors of length k. If a signature contains a single field whose type is a finite alphabet Σ, we call that signature an *enumeration*. An *evaluation* ν of a data signature S is a map that associates each field name *id* in S with a value of the corresponding type, denoted by ν.*id*. We denote by L(S) the set of all evaluations of S, also called the *language* of S.

**Data Trees.** A *data tree* with data signature S, or an S-*tree*, is a pair (T,λ) where T is a tree and λ is a labelling function that maps each node t ∈ T into an evaluation of S, i.e., λ(t) ∈ L(S). Another way of looking at data trees is to think of them as a traditional tree data structure where the data λ(t) associated with each node t is structured. Thus, to simplify the notation when λ is clear from the context, we adopt a C-like notation to refer to the value of fields associated with tree nodes: if t is a tree node and *id* is a field of S, we write t.*id* as a shorthand for λ(t).*id*. If the data signature is an enumeration, we recover the traditional notion of Σ-labelled tree.

Many data structures from the literature can be seen as data trees. Below we give a high-level description of well-known data structures [9]. In addition to using them for motivating purposes, we will also use them as running examples.

*Example 1 (Binary Search Trees).* A Bst is a binary tree where each node stores a key taken from a totally ordered set, with the property that the key stored in each internal node is greater than or equal to all the keys stored in the node's left subtree, and smaller than those in its right subtree. Thus, an appropriate signature for data trees representing Bsts is {*val* : Z}.

*Example 2 (Red-black Trees).* An Rbt is a binary tree where each internal node stores a numerical value, satisfying the binary search tree property. The leaves do not contain keys or data and they represent a NIL pointer. Each node has a color (red or black), and the following properties hold: *(i)* every leaf is black, *(ii)* if a node is red then both its children are black, and *(iii)* every path from a given node to a descendent leaf contains the same number of black nodes.

Note that while the color is a piece of information stored in the node, the *black height* can instead be computed on demand. Thus, the signature for data trees representing Rbts may be {*val* : Z, *is black* : B}.

*Example 3 (Max-Heap).* A Max-Heap is a binary tree where each node stores a key taken from a totally ordered set, say Z, and can be described as an Stree (T,λ) where S is a data signature consisting of a single integer field, say {*key* : Z}, that obeys the following two constraints: (i) (*shape property*) T is almost complete, i.e., all its levels are complete, except the last one, that is filled from left to right; and (ii) (*heap property*) the value stored in each node is greater than or equal to the values stored in the node's children.

#### **3 Monadic Second-Order Logic with Data**

In this section, we introduce our Mso-D logic to express properties of data trees. We define Mso-D by extending the standard Monadic Second-Order logic on (enumeration) trees (a.k.a. Mso) with constraints on the Data.

Data constraints are formulas in first-order logic (Fol) with equality (here we use standard Fol syntax and semantics [34]). However, since data trees may involve different data types, we will consider formulas with many-sorted signatures as opposed to the classical unsorted version. Specifically, we deal with formulas of a many-sorted first-order theory D with sorts *data*1,..., *data*n. For each *data*i, we allow a theory D*datai* whose function symbols have type *data*n i → *data*i and whose relation symbols have type *data*m i → B, for some n and m. For example, each of these theories can be the theory of *arithmetic*, *reals*, *arrays*, etc. From now on, we may refer to D as the *data theory* of Mso-D.

We also introduce a finite set of *connecting function symbols*, denoted F, which we use to extend the Mso component of our logic with data. Let *nodes* be the sort of the Mso component. Then, each f ∈ F is an uninterpreted function symbol with type *nodes* → *data*i, for some i ∈ [n]. These functions allow us to model fields that we associate with each node in the tree. In particular, we say that f ∈ F models a field of an S-tree if f is also the name of a field in S. Otherwise, f may serve the purpose of endowing tree nodes with extra data fields without these being present in the labels of the data tree. This is a very useful feature for characterizing tree data structures, e.g., we can use *bh* ∈ F to logically characterize the *black height* of nodes in Rbts, even if that information is not part of the data signature of Rbts.

We are now ready to formally define the syntax of Mso-D over S-trees with data theory D and connecting functions F. We fix countable sets of propositional variables (denoted by p), first-order node variables (denoted by x, y, etc.), and node-set variables (denoted by X, Y, etc.). We assume that D includes relation symbols Drel. We also assume that the symbols in D, the variable names, and the symbols in F do not overlap. Since D is imported in Mso-D unchanged we do not report its definition here. The remaining components of the syntax of Mso-D(D, F, S) are defined by the following grammar:

$$\begin{aligned} \text{Node terms: } & t \stackrel{\text{def}}{=} x \mid t. left \mid t. right\\ \text{Formulas: } & \varphi \stackrel{\text{def}}{=} p \mid t\_1 = t\_2 \mid t \in X \mid \exists x. \,\varphi \mid \exists X. \,\varphi \mid \neg \varphi \mid \varphi \land \varphi\\ & \mid r(f\_1(t\_1), \dots, f\_k(t\_k)) \qquad r \in \mathcal{D}^{\text{rel}}, f\_1, \dots, f\_k \in \mathcal{F} \end{aligned}$$

where r and f1,...,fk are well-typed, i.e., there is an index i such that the type of r is *data*k i , and for every j ∈ [k], fj has type *nodes* → *data*i. We denote the set of all variables occurring in ϕ by *Var* (ϕ).

An *interpretation* of a formula ϕ is a pair (T λ,I), where T λ is an S-tree (T,λ), and I interprets the remaining symbols of the logic. We interpret the D-component of our theory as we would interpret D in isolation. Assume that D is the chosen interpretation of D, with underlying universes Di for sort *data*i. Also, I maps each function symbol f in F with type *nodes* → *data*i to a concrete function I(f) : T → Di. Moreover, if f is also the name of a field in S, then we require that I(f) coincides with the value of the field f in each node of the tree, i.e., I(f)(v) = λ(v).f, for every v ∈ T. The satisfaction relation depends also on D, but we omit it here because we consider it fixed.

We interpret the variables in *Var* (ϕ) by mapping each of them into a subset of nodes of T with the following properties: (i) first-order variables are assigned singletons, and (ii) propositional variables are assigned either all nodes (encoding *true*) or no node at all (encoding *false*). For a set of nodes S ⊆ T and a (first- or second-order) variable α ∈ *Var* (ϕ), we denote by I[S/α] the function that maps α to S, and agrees with I on all the other variables. Node terms are interpreted as follows:

$$\mathbb{I}(t) = \begin{cases} \mathbb{I}(x) & \text{if } t = x \\ \mathbb{I}(s)0 & \text{if } t = s.left \text{ and } \mathbb{I}(s)0 \in T \\ \mathbb{I}(s)1 & \text{if } t = s.right \text{ and } \mathbb{I}(s)1 \in T \\ \mathbb{I}(s) & \text{otherwise.} \end{cases}$$

Notice that the .*left* and .*right* operators *stutter* on leaves, that is, for all leaves v it holds v = v.*left* = v.*right*.

The *satisfaction relation* T λ,I |= ϕ is so defined.

$$\begin{array}{lll} T^{\lambda}, \mathbbm{1} \vDash p & \text{iff } \mathbb{I}(p) = T \\ T^{\lambda}, \mathbbm{1} \vDash t\_{1} = t\_{2} & \text{iff } \mathbb{I}(t\_{1}) = \mathbb{I}(t\_{2}) \\ T^{\lambda}, \mathbbm{1} \vDash t \in X & \text{iff } \mathbb{I}(t) \subseteq \mathbb{I}(X) \\ T^{\lambda}, \mathbbm{1} \vDash (f\_{1}(t\_{1}), \dotsc, f\_{k}(t\_{k})) \text{ iff } \mathbb{D}(r) (\mathbb{I}(f\_{1}) (\mathbb{I}(t\_{1})), \dotsc, \mathbb{I}(f\_{k}) (\mathbb{I}(t\_{k})) \text{ } \\ T^{\lambda}, \mathbbm{1} \vDash \varphi & \text{iff } T^{\lambda}, \mathbbm{1} \vDash \varphi \\ T^{\lambda}, \mathbbm{1} \vDash \varphi\_{2} & \text{iff } T^{\lambda}, \mathbbm{1} \vDash \varphi\_{1} \text{ and } T^{\lambda}, \mathbbm{1} \vDash \varphi\_{2} \\ T^{\lambda}, \mathbbm{1} \vDash \exists x. \varphi & \text{iff } \text{there exists } v \in T \text{ such that } T^{\lambda}, \mathbb{I}[\{v\}/x] = \varphi \\ T^{\lambda}, \mathbbm{1} \vDash \exists X. \varphi & \text{iff there exists } S \subseteq T \text{ such that } T^{\lambda}, \mathbb{I}[S/X] \mid \varphi \end{array}$$

We say that T λ *satisfies* ϕ, denoted T λ |= ϕ, if there is an interpretation I such that T λ,I |= ϕ. We define the language of trees satisfying an Mso-D sentence in the usual way. An Mso-D *sentence* is a formula with no free variables. We define the set of all S-trees T λ satisfying an Mso-D(D, F, S) sentence ϕ by L(ϕ), i.e., the set of all S-trees T λ such that T λ |= ϕ. A language of trees L is Mso-D(D, F, S) *definable* if there exists an Mso-D(D, F, S) sentence ϕ such that L = L(ϕ).

We recover standard Mso when S is an enumeration and D includes a unary relation ra for each a ∈ Σ, whose interpretation is {a}.

*Undecidability of the Satisfiability Problem.* The *satisfiability problem* for a given Mso-D(D, F, S) sentence ϕ asks whether L(ϕ) is empty. Let D be the theory of linear integer arithmetic. It is easy to model an execution of any given 2 counter machine using a unary data tree whose signature has two fields of type N to model the counters, and an enumeration field to keep track of the current instruction. Each machine configuration is represented by a node, and we can impose constraints in our logic so that two consecutive nodes in the tree model a machine transition. Likewise, we can also express the property of a halting computation in our logic. Thus, the satisfiability of the Mso-D logic is undecidable, even though the underlying data logic D is decidable. Of course, by choosing a finite domain for the interpretation of the underlying data logic, we regain decidability in that the problem matches that of the standard Mso.

**Examples.** We now show various examples to illustrate the expressiveness of Mso-D. We will use the usual predefined abbreviations to denote the remaining propositional connectives (ϕ1 ∨ ϕ2 and ϕ1 → ϕ2), the universal quantifier (∀α.ϕ def = ¬∃α .¬ϕ), x = y def = ¬(x = y), and the conditional expression (ϕ ? ϕ1 : ϕ2) def = (ϕ ∧ ϕ1) ∨ (¬ϕ ∧ ϕ2). Finally, the following standard Mso predicates will come in handy: *child*(x, y), *root*(x), *leaf* (x), and *path*(x, y).

*Example 4 (*Mso-D *Characterization of* Bst*s).* We define the characteristic property of Bsts on data trees with data signature {*val* : Z}. We first introduce the auxiliary predicate *path*l(x, y) (resp., *path*r(x, y)) with the meaning "y is in the left (resp., right) sub-tree of x". Using these predicates, we define the Mso-D sentence (1) that says that all values in the left sub-tree of a node x contain values that are smaller than the value in x, and similarly for the right sub-tree.

To demonstrate the use of connecting functions to model auxiliary node fields, we give an alternative way to characterize Bsts. We introduce two auxiliary connecting functions: *min* and *max* . We impose constraints to ensure that for each node x in the tree min(x) and max(x) are the minimum and maximum values of the sub-tree rooted in x, respectively. It is straightforward to see that we can impose the Bst property by relating the values in each node with *min* and *max* in their children as follows:

ψbst def = ∀x . - x = x.*left* ? *min*(x) = *min*(x.*left*) ∧ *max* (x.*left*) ≤ *val* (x) : *min*(x) = *val* (x) ∧ x = x.*right*? *max* (x) = *max* (x.*right*) ∧ *min*(x.*right*) > *val* (x) : *max* (x) = *val* (x) .

*Example 5 (*Mso-D *characterization of* Rbt*s).* We can also express the defining properties of red-black trees as follows:

$$\forall x. \left( \neg is.black(x) \right) \rightarrow \left( is.black(x.left) \land is.black(x.right) \right).$$

*(c) Every path from a node to a leaf contains the same number of black nodes.* We encode this property as the consistency of the black height data field *bh*:

$$\begin{split} \forall x. \forall y. \left( \left( \left\{ \begin{array}{l} is\\_label(x)\wedge\\_child(y,x) \right\} \rightarrow (bh(y) = bh(x) = 1) \end{array} \right\} \right) \\ \land \left( \left( \neg is\\_label(x)\wedge\\_child(y,x) \right) \rightarrow (bh(y) = bh(x)) \right) \\ \land \left( \left( \left\{ leaf(x) \wedge\\_child(x) \right\} \rightarrow bb(x) = 1 \right) \right) \\ \land \left( \left( \left\{ leaf(x) \wedge\neg is\\_black\_$$

*Extended Models.* Since we are going to build automata corresponding to formulas with free variables, it is convenient to encode the variable interpretation in the tree itself, by expanding the data signature with an extra Boolean flag for each free variable. The flag corresponding to a free variable will be set to 1 in the node(s) that belong to the interpretation of that variable. In detail, for a given interpretation (T λ,I), assume that *Var* (ϕ) = {α1,...,αn}, we can define an *extended tree* (T,λE) with data signature SE = S∪{a1,...,an : B}, where λE(u)(ai) = 1 iff u ∈ I(αi). Conversely, from an extended tree we can extract the corresponding variable interpretation. For such an extended tree we can write T λ*E* |= ϕ without mentioning I.

#### **4 Symbolic Data-Tree Automata**

In this section, we define a new class of tree automata called *Symbolic Data-Tree Automata*. They generalize traditional bottom-up finite tree automata as they work with data trees. Furthermore, they are symbolic because the alphabet and set of states are defined using evaluations of data signatures, and its transition function is defined through constraints1 involving states and alphabet.

**Definition 1** *(*Symbolic Data-Tree Automata*). A* symbolic data-tree automaton*, or* Sdta *for short,* A *is a tuple* (SΣ, SQ, ψF , ΨΔ) *where:*

ψ*lr* (ql, qr, σ, q), ψl(ql, σ, q), ψr(qr, σ, q), ψ*leaf* (σ, q),

*where* ql, qr*, and* q *are variables of type* SQ*, and* σ *is of type* SΣ*.*

A *accepts* SΣ*-trees. A tree* (T,λ) *is* accepted *by* A *if there is a total function* π : T → Q *such that for every node* t ∈ T *the following holds:*

*The* language *of* A*, denoted* L(A)*, is the class of all* SΣ*-trees accepted by* A*.*

We recover standard tree automata when both data signatures SΣ and SQ are enumerations. In that case, we call A an *enumeration tree automaton* and we denote it as (Σ, Q, F, Δ), where Σ = L(SΣ), Q = L(SQ), and so on.

1 We use the term *constraint* to denote a generic predicate *con*(x1,...,x*k*) in which the type of variable x*i* is some data signature S*i*. We deliberately leave the definition of the constraints unspecified, and specify them only when it is necessary to do so.

*Example 6* (*Symbolic Data-Tree Automaton for Max Heap*). We define an Sdta A*bmh* where L(A*bmh* ) is the set of all max heaps. The state data signature of A*bmh* is {h : N, f : B, *val* : N}. We use the h field to store the height of the sub-tree rooted in the node, the f field to store whether the sub-tree rooted in the node is complete with the last level completely filled, and *val* stores the node's data value. The transition data constraints are as follows:

$$\begin{split} \psi\_{\mathit{laf}}(\sigma,q) \stackrel{\scriptstyle \mathsf{at}}{=} q.h &= 1 \land q.f \land q.val = \sigma.val \\ \psi\_{\mathit{l}}(q\_{l},\sigma,q) \stackrel{\scriptstyle \mathsf{at}}{=} q.h &= 1 \land q.h = 2 \land \neg q.f \land \sigma.val \ge \sigma\_{l}.val \land q.val = \sigma.val \\ \psi\_{\mathit{lr}}(q\_{l},q\_{r},\sigma,q) \stackrel{\scriptstyle \mathsf{at}}{=} & \ (q.h-1 \le q\_{r}.h \le q.h) \land \ \{q.f \leftrightarrow (q.f \land q\_{r}.f \land q.h = q\_{r}.h)\} \\ & \qquad \land \left(\neg q.f \to (q\_{r}.h < q\_{l}.h \land q\_{r}.f)\right) \land \left(\neg q\_{r}.f \to (q\_{r}.h \land q\_{l}.f)\right) \\ & \qquad \land \ \sigma.val \ge q.val \land \sigma.val \ge q\_{r}.val \land q.val = \sigma.val. \end{split}$$

For each leaf, we set the height field h to 1, the field f to true, and copy the label of the node into the state field *val*. Note that all sub-trees of a complete tree are still complete trees. Thus, if a node has only the left child, this child must be a leaf, and we set the parent node's fields accordingly. A node with only the right child leads to a violation of the shape property, thus ψr(qr, σ, q) def = *false*. Finally, we consider the case where the node has both children. Here ψ*lr* constrains the fields of the state data signature to guarantee their invariants. Specifically, the first two lines enforce the shape property while the last line enforces the heap property and copies the value of the label into the state field *val*. To conclude, we define ψF as a tautology. However, if, for example, we wanted to accept only max heaps of height at least 100 we could have defined ψF (q) def = (q.h ≥ 100).

## **5 Solving the Emptiness Problem for** Sdta**s**

The *emptiness problem* for Sdtas consists in determining whether the tree language recognized by a given Sdta A is empty, i.e., whether L(A) is empty. We first prove that the emptiness problem for Sdtas is undecidable, and then show that it can be reduced to the satisfiability of a system of constrained Horn clauses (CHCs), for which increasingly efficient off-the-shelf semi-procedures exist.

It is well known that the emptiness problem for tree automata is decidable [8]. However, as explained for Mso-D in Sect. 3, as soon as the state data signature involves an unbounded data domain (such as integers or reals) and basic arithmetics (e.g., increment and test for zero), the emptiness problem becomes undecidable. Thus, we have the following.

#### **Theorem 1.** *The emptiness problem for* Sdta*s is undecidable.*

We cope with this negative result by providing a reduction to the satisfiability of a system of CHCs, when the transition constraints of the automaton are defined through quantifier-free first-order logic formulas.

**Constrained Horn Clauses.** We fix a set R of uninterpreted fixed-arity relation symbols, which represent the unknowns in the system. A *Constrained Horn Clause*, or CHC for short, is a formula of the form H ← C ∧B1 ∧···∧Bn where:

A finite set H of CHCs is a *system*, and it corresponds to the first-order formula obtained by putting all its CHCs in conjunction. We assume that the semantics of constraints is given a priori as a structure. A system H with relation symbols R is *satisfiable* if there is an interpretation to each predicate in R that makes all clauses in H valid.

It is a well-known result from constraint logic programming that every system of CHCs H has a unique minimal model that can be computed as the fixed-point of an operator derived by the clauses of H [16,26]. This property, which allows us to use a fixed-point semantics for CHC systems, to justify the correctness of the reduction defined below (i.e., Theorem 2).

**Reduction.** We give a linear time reduction from the emptiness problem for Sdtas to the satisfiability of systems of CHCs.  We map A into the CHC system HA formed by the CHCs shown on the right.

**Theorem 2** *(*Emptiness*). Let* A *be an* Sdta*. Then,* L(A) *is empty if and only if* HA *is satisfiable.*

#### **6 From Logic to Automata**

In this section, we describe a reduction from the satisfiability problem of Mso-D to the emptiness problem of Sdtas, when the Mso-D formula ϕ is a sentence in the following form:

$$\varphi = \exists x\_1, \dots, x\_n. \forall y\_1, \dots, y\_m. \theta,\tag{2}$$

where each data constraint of the formula θ, say r(f1(t1),...,fk(tk)), satisfies one of the following:

Notice that θ may contain other quantifiers, but the additional quantified variables can occur only inside unary data constraints. Moreover, it is easy to see that this fragment is closed under positive Boolean combinations (i.e., conjunctions and disjunctions).

This fragment strictly includes the Mso logic with data defined in [11] for data words, which only allows unary data constraints. Below we show that the added expressivity can be used to define and verify properties of a variety of data structures, including those from Examples 4 and 5, and infinite-state games.

In our reduction, we first construct a standard finite-state tree automaton over a finite alphabet (Sect. 6.1), which we then convert to an Sdta (Sect. 6.2).

#### **6.1 Building the Enumerated Tree Automaton**

The first step in our reduction from Mso-D to Sdtas is to convert the Mso-D formula ϕ of type (2) into a formula ϕ in standard Mso by *abstracting away* all data constraints. We distinguish two types of data constraints. *Global constraints* refer only to the data of the existentially quantified variables xi; on a given data tree, once the interpretation of those variables is chosen, each global constraint is either *true* or *false*: it is a global property of the tree. *Local constraints*, instead, additionally refer to a variable, say z, that is not one of {x1,...,xn}; even if the interpretation of {x1,...,xn} is fixed, the truth of such constraints depends on the interpretation of z. Accordingly, we replace each data constraint in θ, say r(f1(t1),...,fk(tk)), as follows:

Besides the above substitutions, in the resulting Mso formula we leave variables x1,...,xn free, so that the models of the formula will carry the interpretation of those variables as extra bits in the node labels (recall the discussion on extended models in Sect. 3). We thus obtain the following Mso formula:

$$
\varphi' \stackrel{\text{at}}{=} \forall y\_1, \dots, y\_m. \theta'. \tag{3}
$$

Since ϕ has no data constraints, we can take its data signature to be empty.

*Example 7.* Consider the formula ψbst from Example 4 that defines Bsts using auxiliary data *min* and *max* . Since it uses a single universal quantifier, it belongs to the syntactic fragment (2). For the sake of simplicity, consider a stronger formula ψ bst forcing internal nodes to have two children (a.k.a. a *full* Bst):

$$\psi\_{\text{bst}}' \stackrel{\text{def}}{=} \psi\_{\text{bst}} \land \forall y . full . tree(y), \quad \text{where}$$

$$full . tree(y) \stackrel{\text{def}}{=} \{\neg leaf(y) \to (y. left \ne y \land y. right \ne y)\}.$$

Now, consider the following true property of full Bsts: the successor of an internal node is the left-most leaf in its right sub-tree. The following formula states the opposite of that property:

ψsucc def = ∃x1, x2, x3 . *val*(x1) < *val*(x2) < *val*(x3) ∧ ¬*leaf* (x1) ∧ *leaf* (x3) ∧ *left only path*(x1.*right*, x3) .

It is easy to see that ψ bst ∧ ψsucc is equivalent to a formula ψ in our fragment: ∃x1, x2, x3 . ∀y . - *val* (x1) < *val* (x2) < *val* (x3) ∧ ¬*leaf* (x1) ∧ *leaf* (x3)

$$\begin{aligned} &\wedge \text{left\text{\textquotedblleft}} \text{only\textquotedblright}(x\_1.right) \text{right}(x\_3) \wedge \text{left\text{\textquotedblleft}} \text{left\text{\textquotedblleft}} (y) \\ &\wedge \left\{ y \neq y.left \text{\textquotedblleft} \text{\textquotedblright} \, \text{\textquotedblleft} \, \text{\textquotedblright}(y) = \min(y.left) \wedge \max(y.left) < \text{val}(y) < \text{val}(y) \, : \, \min(y) = \text{val}(y) \right\} \\ &\wedge \left\{ y \neq y.right \, \text{right} \, \text{?} \, \max(y) = \max(y.right) \wedge \min(y.right) > \text{val}(y) \, : \, \max(y) = \text{val}(y) \right\}. \end{aligned}$$

The conversion outlined above turns ψ into the following Mso formula:

$$\forall y. \left(p\_1 \land \neg \mathit{left}(x\_1) \land \mathit{left}(x\_3) \land \mathit{right}\mathit{right}.\right) \land \mathit{right}\mathit{right}.\mathtt{with}\left(x\_1.\mathit{right}, x\_3\right) \land \mathit{right}\mathit{left}.\mathtt{tree}(y)$$

$$\land \left(y \neq y.\mathit{left}?\,y \in C\_1:y \in C\_2\right) \land \left(y \neq y.\mathit{right}?\,y \in C\_3:y \in C\_4\right),$$

where proposition p1 corresponds to the global constraint *val*(x1) < *val*(x2) < *val*(x3), the second-order variable C1 corresponds to the local constraint *min*(y) = *min*(y.*left*) ∧ *max* (y.*left*) < *val*(y), and variables C2 – C4 correspond to the other data constraints in ψbst.

We now apply the standard Mso construction to ϕ , leading to a bottomup finite-state tree automaton Aϕ on the alphabet Σ = {0, 1}n+h+l , accepting all finite trees that represent interpretations satisfying ϕ . The alphabet is Σ because n + h + l is the total number of free variables in ϕ : n first-order variables xi, h propositional variables pi (corresponding to global constraints), and l second-order variables Ci (corresponding to local constraints). We recall the formal statement of this construction below, for more details see [40] and [8].

**Theorem 3.** *For all* Mso *formulas* ϕ *on the empty data signature, with free first-order variables* x1,...,xn*, propositional variables* p1,...,ph*, and secondorder variables* C1,...,Cl*, there is a deterministic bottom-up tree automaton on the alphabet* {0, 1}n+h+l *whose language consists of all extended trees* T *such that* T |= ϕ *.*

*Simplifying Assumptions.* To simplify the presentation of the following constructions, we make two simplifying assumptions. First, we assume that all terms appearing in data constraints are variables, and not composite terms like x.*left*.*right*. Dropping this assumption is technically simple and omitted due to space constraints. Second, we assume that all connecting functions f appearing in data constraints correspond to fields in S. Sentences that satisfy the second assumption have a unique interpretation I, because they have no free variables and the connecting functions must be interpreted as the functions extracting the corresponding field from each node. We discuss how to remove this restriction in Sect. 6.3.

We now establish a relation between Σ-trees accepted by Aϕ- , and data trees on the data signature S defined by ϕ. Denote by (a1,...,an, b1,...,bh, c1,...,cl) the generic element of Σ. Given a Σ-tree (T,σ) and a variable xi in ϕ , we define *node*(σ, xi) to be the unique node u ∈ T such that the ai component of σ(u) is 1. In words, the function *node* picks the position in the tree where the Σ-tree activates the bit ai.

**Definition 2.** *Consider an* Mso-D *sentence* ϕ *of the form* (2) *on the data signature* S*, and let* I *be its unique interpretation. We say that a* Σ*-tree* (T,σ) *and an* S*-tree* (T,λ) *are* consistent *iff for all nodes* u ∈ T *the following hold:*

*1. For all* i ∈ [h]*, let* r glb i f 1 i (α1 i ),...,fj*i* i (αj*i* i ) *be the global constraint from* ϕ *corresponding to the propositional variable* pi *from* ϕ *. Recall that under the simplifying assumptions each* αj i *is one of* x1,...,xn*, and each* fj i *is one of the names of the fields of* S*. Then,* σ(u)(bi)=1 *iff the following holds*

$$\mathbb{D}(r\_i^{\text{glb}}) \Big( \mathbb{I}(f\_i^1)(node(\sigma, \alpha\_i^1)), \dots, \mathbb{I}(f\_i^{j\_i})(node(\sigma, \alpha\_i^{j\_i})) \Big).$$

*2. For all* i ∈ [l]*, let* rloc i g1 i (β1 i ),...,gk*i* i (βk*i* i ), gi(zi) *be the local constraint from* ϕ *corresponding to the second-order variable* Ci *from* ϕ *. Recall that each* βj i *is one of* x1,...,xn*, and each* gj i *(as well as* gi*) is one of the names of the fields of* S*. Then,* σ(u)(ci)=1 *iff the following holds*

$$\mathbb{D}(r\_i^{\rm loc})\Big(\mathbb{I}(g\_i^1)(node(\sigma, \beta\_i^1)), \dots, \,\_r\mathbb{I}(g\_i^{k\_i})(node(\sigma, \beta\_i^{k\_i}))\,\,, \mathbb{I}(g\_i)(\lambda(u))\Big).$$

The following result states the fundamental relationship between ϕ and Aϕ-.

**Theorem 4.** *Let* ϕ *be an* Mso-D *sentence of the form* (2) *on the data signature* S*, and let* Aϕ *be the corresponding tree automaton described above. For all data trees* (T,λ) *with data signature* S*, the following are equivalent:*

#### **6.2 Building the Symbolic Data Tree Automaton**

We now convert the tree automaton from the previous section into an Sdta that accepts all and only the data trees satisfying the original Mso-D formula ϕ.

Intuitively, the Sdta mimics the behavior of the tree automaton, and in doing so, it enforces the data constraints contained in ϕ. The information about which constraints should be true and which should be false at every node is encoded in the alphabet Σ = {0, 1}n+h+l of the tree automaton. In detail, if (a1,...,an, b1,...,bh, c1,...,cl) is a generic symbol from the alphabet, the bi's encode the truth value of the global constraints, and the ci's encode the truth value of the local constraints. However, the *data* on which to evaluate those constraints comes from different sources. The global constraints are evaluated only on the *guessed* data for the existentially quantified variables x1,...,xn, whereas the local constraints also access the data of the current node.

Finally, the ai component of the alphabet encodes the actual position of each xi in the current tree (i.e., ai is 1 only in the node that is the interpretation of xi). So, when ai = 1 the symbolic automaton checks that the guessed data evaluation for xi corresponds to the data in the current node.

Let Aϕ- = (Σ, Q, F, Δ) be the tree automaton from Sect. 6.1, we now define the Sdta Aϕ = (S, SQ, ψF , ΨΔ). First, notice that the alphabet data signature S coincides with that of the original Mso-D formula. We then set the state data signature SQ to {*state* : Q}∪{*id*i : *type* | (*id* : *type*) ∈ S, i = 1 ...n}, i.e., SQ contains an enumerated data field representing the state of the tree automaton Aϕ- , and n copies of each data field in S. These copies are used to store the guessed data evaluations for the existentially quantified variables xi from (2). For a symbolic state q ∈ L(SQ) and i ∈ [n], we denote by q[xi] the i-th projection of q on S, i.e., the evaluation that assigns to each field *id* in S the value q.*id*i . The acceptance constraint ψF (q) is simply defined as q.*state* ∈ F.

Regarding the transition constraints ΨΔ, we will focus only on the case of nodes with two children, since the other cases are similar. Let (sl, sr, a, s) be a transition in Aϕ- , where a = (a1,...,an, b1,...,bh, c1,...,cl) ∈ Σ. We add the following implicant to the transition constraint ψ*lr* :

$$\begin{cases} \end{cases}\quad q\_l.state = s\_l \wedge q\_r.state = s\_r \wedge q.state = s\tag{4a}$$

$$\bigwedge\_{i \in [n]} \left( q[x\_i] = q[x\_i] \land q[x\_i] = q\_r[x\_i] \right) \quad \land \bigwedge\_{\{i \mid a\_i = 1\}} \left( q[x\_i] = \sigma \right) \tag{4b}$$

$$\wedge \bigwedge\_{i \in [h]} \left[ (b\_i = 1) \leftrightarrow \mathbb{D}(r\_i^{\text{glb}}) (q[\alpha\_i^1], f\_i^1, \dots, q[\alpha\_i^{j\_i}], f\_i^{j\_i}) \right] \tag{4c}$$

$$\begin{aligned} \{ \wedge \bigwedge\_{i \in [l]} \left[ (c\_i = 1) \leftrightarrow \mathbb{D}(r\_i^{\text{loc}}) (q[\beta\_i^1], g\_i^1, \dots, q[\beta\_i^{k\_i}], g\_i^{k\_i}, \sigma.g\_i) \right] \: \} \\ & \implies \quad \psi\_{lr}(q\_l, q\_r, \sigma, q) . \end{aligned} \tag{4d}$$

The above conjuncts can be explained as follows: (4a) mimics the state change in the discrete transition, the first part of (4b) states that the n copies of the data fields held by the symbolic automaton are uniform over the whole tree, the second part of (4b) additionally states that the i-th copy of the data fields coincides with the data σ in the unique node where the discrete automaton

**Fig. 1.** Architecture of the prototype implementation. Dashed transformations are performed manually, but could be automated by an Mso-D parser.

prescribes ai = 1, (4c) enforces the i-th global constraint r glb i in all nodes where the discrete automaton prescribes bi = 1, and finally (4d) enforces the local constraints when the ci component of the discrete alphabet is 1.

**Theorem 5.** *Let* ϕ *be an* Mso-D *sentence of the form* (2) *and let* Aϕ *be the corresponding* Sdta *described above. We have* L(ϕ) = L(Aϕ)*.*

#### **6.3 Supporting Auxiliary Data**

So far, we have assumed that all connecting function symbols f appearing in the data constraints correspond to fields in S. In other words, all data constraints refer to data fields that are present in the trees. However, our logic also supports connecting function symbols that do not correspond to fields in the data signature. In that case, the interpretation is free to assign any value to f(u), for each node u in the data tree. Thus, the Sdta Aϕ must accept a data tree if there exists an interpretation for those functions that satisfies the formula. To achieve this effect, let {fi}i=1...k be the set of connecting function symbols occurring in ϕ and not corresponding to data fields in S, where fi has type nodes → datai. Define the extended data signature

$$\mathcal{S}' = \mathcal{S} \cup \{ f\_i : data\_i \}\_{i=1\ldots k}.$$

We enrich the state data signature of Aϕ as follows:

$$\mathcal{S}^{Q} = \{ state : Q\} \cup \{ name^i : type \mid (name : type) \in \mathcal{S}', i = 0 \dots n\}.$$

Compared to the original definition from Sect. 6.2, we store an extra copy of the data fields, identified by index 0, representing the data in the current node. Moreover, all copies include the auxiliary data fields. It is straightforward to adapt the constraint ΨΔ from Sect. 6.2 to support such auxiliary data fields.

#### **7 Implementation and Experiments**

We implemented a prototype toolchain supporting our framework as shown in Fig. 1. Instead of developing an Mso-D parser, we provide an Mso formula already in the form (3), and supply the data constraints and the data signature for the formula in a separate file, directly in the SMT-LIB format. Next, we convert the Mso formula into an equivalent tree automaton, and in turn into a system of CHCs (as described in Sect. 5). We used Z3 v4.8.10 (64bit for Windows 10) [36] as the CHC solver, and Mona v1.4 [28] as the Mso-to-automata translator. The only new piece of code required by this implementation is the converter from the Mona tree automaton format to CHCs in the SMT-LIB language, which is a simple one-to-one textual transformation. For the experiments, we used a dedicated machine with 16 GB of physical memory and an AMD Ryzen 7 2700X clocked at 3.7 Ghz, running Windows 10.

#### **7.1 Proving Properties of Tree Data Structures**

Consider the property of full Bsts described in Example 7, namely that the successor of an internal node is the left-most leaf in its right subtree. We submitted to our tool the conjunction ψ bst ∧ ψsucc, which would be satisfied only by a full Bst where the successor of an internal node is *not* the left-most leaf in its right subtree (property Successor). Once the formula is converted into a system of CHCs, the SMT solver proves satisfiability of the system (and hence, unsatisfiability of the original formula) in less than a second.

**Table 1.** Mso-D satisfiability experiments (Sect. 7).

For Rbts, we consider the property that there exists an internal node whose black height is less than half of its height (property BlackHeight). Our approach can prove that this property is unsatisfiable on Rbts in less than a second. Both experiments are summarized in Table 1.

#### **7.2 Solving an Infinite-State Game**

Our approach can be used to solve certain infinite-state games, such as the Cinderella-Stepmother game [1,3]. In this software synthesis benchmark, two players share n buckets, each holding up to c units of water. The buckets are positioned in a circle and are initially empty. The game is played in a discrete sequence of turns: when it is Cinderella's turn, she can empty two adjacent buckets. When it is the Stepmother's turn, she can pour water into any subset of buckets, for a total of 1 unit of water. If any of the buckets overflows, Stepmother wins. If the game continues forever with no overflows, Cinderella wins. It can be described as an infinite-state turn-based two-player game of infinite duration with a safety objective (for Cinderella). Notice how not only the game state-space is infinite, but so are the moves available to Stepmother at each step.

Given values for the parameters n and c, we build an Mso-D formula ϕn,c that is satisfiable if and only if Stepmother wins the game with those parameters. The formula holds true on finite trees representing winning strategies of Stepmother. In other words, a tree that satisfies ϕ tracks all possible game plays where Stepmother pours water according to a specific deterministic plan and Cinderella takes all possible moves. Due to space constraints, further details on the encoding are deferred to an extended version of this paper.

In our experiments, we fixed the number of buckets n to 5 and checked the satisfiability of ϕ5,c for various values of the capacity c. In Table 1, we denote by Stepmother(c) the formula ϕ5,c. Bodlaender et al. [3], among their comprehensive analysis of this game, show that for n = 5, the minimum capacity for which Cinderella wins the game is c = 2 (see Table 1 in [3]). Their proof for this case is manual. Other cases were settled with the help of an SMT solver, using invariants based on non-trivial insights on the reasonable strategies of Stepmother. On the contrary, our encoding based on Mso-D employs only the rules of the game, with no further constraints on the players' moves.

Our setup successfully solves the game for various values of the capacity. The time needed by the SMT solver is very uneven, ranging from three minutes to a maximum of almost two hours for c = 2. That is explained by the fact that c = 2 is the hardest case for Cinderella to win the game. Therefore, proving that property requires building a complex winning strategy for Cinderella. Such strategy is embedded in the proof of unsatisfiability, and extracting it would be an interesting exercise beyond the scope of the present paper. When the capacity moves away from the critical threshold in either direction, the solving time visibly decreases.

#### **8 Related Work**

Our work is related to many works in the literature in different ways. In addition to the works already mentioned in the introduction, here we focus on those that seem to be closest to the results presented in this paper.

*Automata on Infinite Alphabets.* Symbolic finite automata (SFAs) [43] and symbolic tree automata (STAs) [42] replace the traditional finite alphabet by a decidable theory of unary predicates over a possibly infinite domain. They predicate over data words and trees, but they do not support storing, comparing, or combining data from different positions in the model, as that leads quickly to undecidability. Symbolic register automata [10] extend SFAs by storing data values in a set of registers. They retain decidability of the emptiness problem by only allowing equality comparisons between registers and input data.

Recently, Shimoda et al. [38] introduced *symbolic automatic relations* (SARs) as a formalism to verify properties of recursive data structures. While both Mso-D and SARs rely on CHCs as a backend, they differ in motivation and purpose. SARs aim at encoding specific properties of interest in a way that reduces the verification effort of the underlying CHC solver, whereas Mso-D is intended to provide a high-level language that can be compiled into CHCs.

*Decidable Logics with Data Extensions.* In [11], D'Antoni et al. design an extension of WS1S on finite data sequences where data can be examined with arbitrary predicates from a decidable theory, similarly to the capabilities of SFAs. They develop custom representations and algorithms to efficiently solve the satisfiability problem by reducing it to the emptiness of SFAs. Colcombet et al. [7] study a decidable fragment of Mso with data equality, called *rigidly guarded MSO*∼, where data equality constraints of the type *val*(x) = *val*(y) can only be checked on a single y-position for each x-position. Constraint LTL [13] is another decidable logic for infinite data words, where data in different positions can be compared for equality and for order. Segoufin [37] provides a wider, albeit slightly outdated, perspective on decidable data logics and automata.

*Logics for Automated Reasoning About Heap-Manipulating Programs.* Similarly to Mso-D, Strand [32] is a logic that combines Mso on tree-like graphs with the theory of integers. Although Strand has a fragment that admits a decidable and efficient decision procedure, it is not sufficiently expressive to state properties of classic data structures such as the balancedness of a tree. Also it does not allow solving the Cinderella-Stepmother game. Dryad logic [33] is a quantifierfree logic supporting recursion on trees, that is deliberately undecidable but admits a sound, incomplete, and terminating validity procedure, based on *natural* proofs [30]. Dryad recursive definitions could be expressed by our Sdtas that uses the theories of integers and integer (multi)sets; vice versa, proof techniques developed for Dryad could be used to check the emptiness of (some) Sdtas.

*Infinite-State Games.* Many infinite-state reachability games like the Cinderella game of Sect. 7.2 can be encoded in Mso-D, including all the reachability games used in the experiments performed by Farzan and Kincaid [17]. In that paper, the authors present a fully automated but incomplete approach for the (undecidable) class of *linear arithmetic games*. Our approach is incomparable to theirs: on the one hand, the approach proposed in Sect. 7.2 does not extend to all linear arithmetic games, because it assumes that one player has a bounded number of moves; on the other hand, we could easily handle games whose transition relations is not limited to linear arithmetic. Another related approach is presented by Beyene et al. [1], who reduce infinite-state games to CHCs extended with existential quantifiers. Such existential quantifiers are handled with the help of user-provided templates.

#### **9 Conclusions and Future Directions**

We presented Mso-D and Sdtas as extensions of Mso on trees and finite-state tree automata, respectively, for the purpose of reasoning about data trees. We have shown that these are versatile and powerful models for reasoning about relevant problems, outside the realm of classical automata theory. We believe that the key idea, namely separating the structural properties of interest from the data constraints, makes it easier to reason about challenging problems.

Several future directions are interesting. First, we may want to investigate theoretical questions about Sdtas, such as closure properties, and whether we can reduce classical automata decision problems to solving a system of CHCs. In addition, it will be interesting to identify more expressive Mso-D fragments that can be reduced to the emptiness of Sdtas.

Secondly, we believe that our results have applications to other areas in verification. We have conducted preliminary studies defining extensions of LTL with data (LTL-D) and, by using the framework developed in this paper and closure properties of Sdtas, obtained LTL-D model checking algorithms for (recursive) programs using scalar variables. Our approach is limited to finite runs only, so it will also be interesting to see how we can extend it to infinite trees and games.

Finally, (enumeration) trees can be used to encode executions of different classes of automata, such as concurrent pushdown automata or concurrent queue systems. It will be interesting to see if our approach can help lift the results of [31] to the corresponding class of concurrent programs.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Verified Erasure Correction in Coq with MathComp and VST**

Joshua M. Cohen(B) , Qinshi Wang , and Andrew W. Appel

Princeton University, Princeton, NJ 08544, USA<EMAIL_ADDRESS>
**Abstract.** Most methods of data transmission and storage are prone to errors, leading to data loss. Forward erasure correction (FEC) is a method to allow data to be recovered in the presence of errors by encoding the data with redundant parity information determined by an error-correcting code. There are dozens of classes of such codes, many based on sophisticated mathematics, making them difficult to verify using automated tools. In this paper, we present a formal, machine-checked proof of a C implementation of FEC based on Reed-Solomon coding. The C code has been actively used in network defenses for over 25 years, but the algorithm it implements was partially unpublished, and it uses certain optimizations whose correctness was unknown even to the code's authors. We use Coq's Mathematical Components library to prove the algorithm's correctness and the Verified Software Toolchain to prove that the C program correctly implements this algorithm, connecting both using a modular, wellencapsulated structure that could easily be used to verify a high-speed, hardware version of this FEC. This is the first end-to-end, formal proof of a real-world FEC implementation; we verified all previously unknown optimizations and found a latent bug in the code.

**Keywords:** Reed-Solomon coding · functional correctness verification · interactive theorem proving

#### **1 Introduction**

As part of a larger project of ensuring reliable networks, we are applying formal functional-correctness verification to network components: machine-checked proofs that C programs (and, eventually, P4 programs and FPGAs) satisfy their high-level functional specs. When attackers may gain access to the source code and analyze it for bugs and vulnerabilities, we want something stronger than software testing or conventional static analysis: we want a proof that the software works *no matter what input is provided, no matter how dastardly*. And we want a proof that the program works *correctly,* not merely that it does not crash.

One key to reliable networking is *forward erasure correction (FEC):* in a portion of the network in which packets are being lost, add extra parity packets that allow reconstruction of lost packets without retransmission. We use an FEC algorithm and C program that have been in active use for over 25 years. The program does many clever and not-so-clever things, and comments indicate that some parts are not fully trusted even by its original authors.

This FEC is a particularly intriguing target for verification because its highlevel correctness depends on fairly intricate mathematics—we must reason about polynomials, matrices, and finite fields. Meanwhile, the C implementation's correctness relies on C programming features and careful manipulation of pointers in memory. Thus, we need a tool that can reason at both of these levels. We use the Coq proof assistant, utilizing the Mathematical Components [10] (Math-Comp) library for the high-level reasoning and the Verified Software Toolchain [6] (VST) for the C program verification.1 Our VST specs are written using *separation logic*, in which we specify precisely what memory is read from and written to as well as all external effects (I/O, system calls, etc.). This gives us a blanket containment property: the C function is guaranteed to only interact with the outside world (memory, OS, etc.) in ways stated in the spec.

#### *Contributions*

#### **1.1 Forward Erasure Correction**

When transmitting data over a noisy channel, one can use an *error-correcting code*—adding generalized "parity" bits, sending the data across the channel, and then decoding to recover the data if any errors occurred; this technique is known as *forward error correction*. In an *erasure code*, the locations of the missing data are known to the decoder; this allows correction of more errors.

FEC is useful in any network where non-congestion-related packet loss is frequent and retransmission is infeasible or expensive. For instance, wireless networks are especially prone to packet loss due to interference or jamming. More generally,

1 Our Coq proofs and an appendix with expanded definitions, specs, and proofs can be found at github.com/verified-network-toolchain/Verified-FEC/tree/cav22.

errors in network devices due to firmware bugs, misconfiguration, or malware can lead to dropped packets. In these cases, retransmission with TCP is not desirable, because TCP will incorrectly interpret these losses as congestion, grinding the network to a halt. Similarly, applications such as video or audio streaming, often run over UDP, cannot handle retransmission without additional work; moreover, the latency of retransmitting is often too high. Thus, FEC continues to be important in ensuring network reliability.

The algorithm we consider is based on Reed-Solomon [24] coding; it groups the input bits into symbols representing elements of a finite field and interprets the data as a polynomial over this field. Reed-Solomon codes are particularly useful for correcting *burst* errors—errors that occur sequentially—since n + 1 consecutive bit errors can only affect at most 2 symbols of length n. Reed-Solomon decoders can be quite complex, both in theory and implementation; many mechanisms have been developed for this purpose. Nevertheless, these codes have been heavily used in applications such as CDs, DVDs, Blu-Ray disks, hard drives, and satellite communications [27].

In the early 1990's, there was a flurry of activity in Reed-Solomon erasure coding. McAuley described [18] and patented [19] a method for FEC based on Reed-Solomon coding for use in network transmission. Rabin [23] described an alternate technique for information dispersal, which was further developed by Preparata [22], Schwarz [25], and others, mainly for use in RAID storage systems; Plank [21] provides a tutorial and explanation. McAuley later wrote a C implementation of FEC for network packets based on this second technique with several further modifications. We will refer to the algorithm implemented by McAuley's C code as the Reed-Solomon Erasure (RSE) code.

Bellcore (now Peraton Labs) has employed this FEC algorithm (and implementation) successfully in numerous networking projects to support resilient communication, most recently in the DARPA EdgeCT program. McAuley's implementation includes many optimizations and modifications to the core algorithm, including some whose correctness was unknown to the code's authors (Sect. 5.2). It had one bug that we corrected (Sect. 6.6). We have produced a formal, machine-checked proof that this FEC implementation correctly recovers data in the presence of erasures—we proved the *algorithm* correct and proved that the *program* correctly implements it.

#### **1.2 Coq and VST**

We use the Coq interactive theorem prover, in which the user states and proves theorems in a higher-order dependently typed logic. These theorems are mechanically checked by the Coq kernel. Proofs can be (semi)automated by Coq's built-in tactics and by user-defined tactic programming.

Coq has been widely used in program verification and formalized mathematics. One particularly important verification effort is CompCert [15], an optimizing C compiler written and proved correct in Coq. That is, CompCert comes with a formal proof that the assembly code generated by the compiler preserves the semantics of the input C program.

VST is a program logic and set of proof automation tools that enables the verification of C programs in Coq. Using VST, one can write a specification for each C function, stating its preconditions (properties that must hold before the function is run) and postconditions (properties that must hold when the function finishes). These properties can involve both C-specific assertions (e.g., about the contents of memory) and arbitrary statements in Coq's logic. Then, using custom tactics and proof automation included with VST, the user can prove in Coq that the C function satisfies its specification.

VST's program logic is proved sound, with a machine-checked proof in Coq. When we prove that McAuley's RSE correctly reconstructs missing packets, the soundness proof guarantees that the assembly-language program generated by the CompCert C compiler really has that behavior. VST is formally proved sound for CompCert, but not for gcc or clang. VST is intended (and believed) to be sound for gcc/clang; its program logic has stricter rules than would be necessary only for soundness w.r.t. CompCert. For example, for signed integer arithmetic, where CompCert is (unfortunately) a refinement of C11 (CompCert wraps while C11 is u.b.), VST imposes the (more abstract) C11 spec. Thus, VST proofs about C programs also provide useful (though less foundational) assurance about programs compiled with other compilers.

While conventional separation logics have spatial conjuncts that are predicates just on memory resources, VST's separation logic has spatial conjunct predicates on both memory locations and the outside world, which one might affect by performing IO or making a system call [17, Section 3]. In our project, none of the VST funspecs mention the outside world in the precondition or postcondition; this means, like any Hoare triple in separation logic, that those functions can neither access nor modify that resource.

Proving that a C program satisfies a specification is quite challenging. We must prove low-level correctness properties (the program does not crash, all memory accesses are valid, etc.) and provide loop invariants and intermediate proofs to prove high-level properties (that the function satisfies its spec). Though VST's proof automation is able to hide some of this complexity, many parts must still be done manually. Dealing with heavily optimized C code that was never intended to be verified makes these tasks substantially more complicated.

Section 2 describes the RSE algorithm, which differs in several ways from the technique described by Rabin, Preparata, and Schwarz. Section 3 explains the different verification tasks, including defining a functional model of the algorithm and showing with VST that the C code implements this model. Section 4 describes the functional model, Sect. 5 discusses the verification of this functional model, including the proof that the algorithm correctly reconstructs missing packets, and Sect. 6 discusses the proofs about the C code. Section 7 and Sect. 8 give related and future work.

#### **2 The RSE Algorithm**

Like all Reed-Solomon codes, the algorithm treats input symbols as elements of a finite field and interprets the input sequence of words as the coefficients of a polynomial over this field. However, both the C implementation and the RSE algorithm are more naturally described using linear algebra and matrix operations.

Let D be the input data, which consists of k packets, each of length at most c bytes. If any packets are smaller, fill in the missing entries with zeroes so that D is a k × c matrix. Let h be the number of parity packets we wish to append. We will be able to reconstruct up to h total packet-drops.

Let k*max* and h*max* be (fixed) parameters such that k ≤ k*max* and h ≤ h*max*. Let n*max* = h*max* + k*max* (maximum number of packets per batch) and let F be a field such that |F| > n*max*.

#### **2.1 Initialization**

First, we generate a Vandermonde matrix of size h*max*×n*max*; that is, take n*max* distinct nonzero elements of F, denoted as α1, α2, ..., α*nmax* , and generate the following matrix:

$$V = \begin{pmatrix} 1 & 1 & \dots & 1 \\ \alpha\_1 & \alpha\_2 & \dots & \alpha\_{n\_{max}} \\ \alpha\_1^2 & \alpha\_2^2 & \dots & \alpha\_{n\_{max}}^2 \\ \vdots & \vdots & \vdots & \vdots \\ \alpha\_1^{h\_{max}-1} \alpha\_2^{h\_{max}-1} & \dots & \alpha\_{n\_{max}}^{h\_{max}-1} \end{pmatrix}$$

Then, we run Gaussian elimination (see Sect. 4.2) on this matrix to get the row-reduced form, which consists of the identity matrix followed by W, the h*max* × k*max weight matrix* :

$$V \xrightarrow{\text{Gaussian elimination}} \left[I\_{h\_{max} \times h\_{max}} \, \middle| \, W \right]$$

#### **2.2 Encoding**

The encoder receives as input the data D, a k×c matrix. Let W be the submatrix of W consisting of the first h rows and the first k columns. The encoder computes P = W D, an h × c matrix. These are the parity packets that are sent (along with the original data) to the receiver.

$$W = \begin{array}{c} \begin{array}{c} k \\ \cdot \\ \cdot \\ \cdot \\ \end{array} \end{array} \begin{array}{c} \begin{array}{c} k \\ \cdot \\ \cdot \\ \cdot \\ \cdot \\ \cdot \\ \end{array} \end{array} \dots \begin{array}{c} \begin{array}{c} \\ \\ \\ \\ \cdot \\ \cdot \\ \cdot \\ \cdot \\ \end{array} \dots \begin{array}{c} P = W'D \\ \cdot \\ \end{array} \tag{1}$$

#### **2.3 Decoding**

The decoder is significantly more complicated. However, if no packets are lost, the decoder simply returns the first k packets; only if packets are dropped does the following algorithm need to be invoked. To give some intuition, we will first present the decoder for a special case before giving the full algorithm.

Since this is an erasure code, we know the locations of the missing packets; we also require that the total number of missing packets is at most h.

For a special case, suppose that the last h data packets were lost and all parity packets were received. We can think of the original data D as a block matrix consisting of D1, the (k − h) × c matrix of the received data, and D2, the h × c matrix of the lost data. Similarly, we can split the h × k matrix W (from the encoder) into W 1, consisting of the first k −h columns of W , and W 2, consisting of the rest.

$$W = \begin{array}{c} \underbrace{k-h}\_{h} \\ \left[ \begin{array}{ccc} \overbrace{W\_1' & W\_2'}^{\prime} & \dots & \\ \vdots & \vdots & \ddots & \\ \end{array} \right] & D = \begin{array}{c} k-h \end{array} \Bigg[\overbrace{D\_1}^{c} \end{array} \Bigg[\overbrace{D\_1}^{c} \end{array}$$

$$P = W'D = W\_1'D\_1 + W\_2'D\_2$$

From this, the missing data D2 can be computed using P, D1, and the parts of W , all of which are known:

$$D\_2 = (W\_2')^{-1}(P - W\_1'D\_1) \tag{2}$$

The general case is similar, but we need to define the relevant submatrices more carefully. Let *xh* be the number of missing data packets. We must have received at least *xh* parity packets (or else the total number of missing packets is more than h). Let P be the submatrix of P consisting of the first *xh* received parity packets. This time, we let W 1 be the *xh* × (k − *xh*) submatrix of W whose rows consist of the locations of the *xh* found parity packets and whose columns consist of the k − *xh* locations of the received data. Let W 2 be the *xh* × *xh* submatrix of W whose rows consist of the locations of the *xh* found parities and whose columns consist of the locations of the missing data. Finally, D1 and D2 are still defined such that D1 contains the received rows and D2 contains the missing rows. This time, these rows need not be contiguous. These definitions reduce to the previous ones in the special case considered above.

By the definitions of the above submatrices, Eq. 2 still holds (except that we replace P with P ), so we can find the missing data D2 by computing (W 2)−1(P − W 1D1).

This decoder is only well defined if W 2 is invertible. W 2 is dynamically chosen based on the found parities and missing data, so we must show a stronger claim that any square submatrix up to size h × h of W is invertible. Proving this was the crucial step in the functional model verification, described in Sect. 5.1.

As noted in Sect. 1.1, this algorithm is a modified version of the technique described by Rabin, Preparata, Schwarz, and others. The main difference is the use of the static weight matrix in RSE; all the others assume that the Vandermonde matrix has dimensions h × (k + h) and exactly h packets are lost. Thus, their needed correctness property is weaker; it requires only that any h × h submatrix of W is invertible.

#### **3 Verification Structure**

The verification consists of two distinct tasks: we prove that the RSE algorithm is correct (i.e., the decoder recovers the original data in the presence of errors) and that the C program truly implements this algorithm. These two tasks are quite different; the first is purely mathematical and involves proofs about linear algebra, while the second involves implementation details and C-language verification conditions. To separate these tasks and make the proofs more modular, we define a *functional model*, a purely functional program written in Coq that implements the RSE algorithm. This functional model is inefficient but easy to reason about in Coq. Then we use VST to prove that the C program refines this functional model. Finally, we compose these two parts to produce a formal proof that the C implementation of this erasure code is correct.

Separating the functional specification and the VST proofs is a common paradigm; it has been used to verify SHA-256 hashing [4], HMAC-DRBG cryptographic random number generation [28], and floating-point numerical programming [5]. This approach provides a clear formal specification independent of any implementation; we can reuse the same functional model and its correctness proofs to verify another implementation of this algorithm (for instance, an FPGA version). It makes verification more flexible; we can prove further properties later simply by adding additional lemmas about the functional model. It makes the proofs shorter and clearer; we can tell which parts are needed for the core correctness proofs and which are implementation-specific. Finally, it permits a separation of expertise: the person who proves mathematical theorems about the functional model need not know anything about C programming or VST verification, and the person who proves C refinement in VST need not know why the functional model accomplishes the high-level goals.

Our functional model was written in Gallina, the functional programming language embedded in Coq, using the Mathematical Components (MathComp) library for formalized mathematics. MathComp contains definitions and theorems about groups, rings, fields, vector spaces, matrices, polynomials, graphs, and other mathematical objects.

In fact, we define two functional models—a high-level version uses Math-Comp's abstract and dependent types of matrices, polynomials, and the like, while a low-level version uses concrete types such as list (list byte), which VST can use to represent memory contents. Translating between these types is nontrivial (because of all the dependent types in MathComp), so we separate the type conversion proofs from both the high-level mathematical reasoning and the low-level VST refinement proof. This makes the proofs more modular and helps to improve the readability of the resulting formalization. The translation is largely mechanical and we expect that it could be automated; we focus on the high-level functional model and the VST refinement proofs.

#### **4 Functional Model**

#### **4.1 The Encoder and Decoder**

We translate Eq. 1 into the language of Coq/MathComp:

**Definition** encoder (h k c max h max n : nat) (Hh: h ≤max h) (Hk: k ≤max n) (weights : 'M[F] (max h, max n)) (input : 'M[F] (k, c)) := (mxsub (fun (x : 'I h) ⇒ widen ord Hh x) (fun (x : 'I k) ⇒ rev ord (widen ord Hk x)) weights) ∗m input.

'M[F] (x, y) denotes a matrix of size x × y over field F and ∗m denotes matrix multiplication. The type 'I n represents an ordinal, a natural number in the range [0, n−1]. The encoder takes in the parameters h, k, c, h*max*, and n*max* (all defined as in §2), the h*max* ×n*max* weight matrix, the k ×c data matrix, and proofs that h and k are bounded appropriately. mxsub creates a submatrix from an input matrix by selecting rows and columns via user-specified functions. widen ord is needed to handle some dependent type casting; it has no computational content and can be ignored. Finally, rev ord selects the "opposite" ordinal; for x : 'I k, rev ord x = k − x − 1. Therefore, this function selects the first h rows and the last k columns (in reverse order) of the weight matrix and multiplies this by the input. This differs from the algorithm in Sect. 2.2, which selects the first k columns. The overall algorithm's correctness is not affected as long as we choose the matrices W 1 and W 2 in the decoder to be consistent, but this change makes the model consistent with the C implementation (see Sect. 6.2).

The decoder (Eq. 2) can be similarly translated into MathComp; we omit the full definition, but note that we defined the decoder more generally than needed: it is defined over any field and over any Vandermonde matrix on distinct elements of that field.

#### **4.2 Gaussian Elimination**

Gaussian elimination, or row reduction, is a well known algorithm in linear algebra for solving systems of linear equations, finding matrix inverses, and calculating determinants. The C code includes an implementation of Gaussian elimination, used to row-reduce the Vandermonde matrix to produce the weight matrix and to invert W 2 in the decoder. Thus, we need to define a corresponding functional model.

Gaussian elimination proceeds by applying a sequence of elementary row operations—swapping two rows, multiplying a row by a scalar, and adding a scalar multiple of one row to another row—to a matrix until it is in row-echelon form, which for full-rank matrices (including all relevant matrices in this application) means that the left hand side becomes the identity matrix. Crucially, these row operations preserve invertibility because each corresponds to left multiplication by an (invertible) elementary matrix.

The order of the row operations may vary; Algorithm 1 describes one concrete implementation of Gaussian elimination (we use 0-indexing to be consistent with

#### Algorithm 1: Gaussian Elimination

```
On input A, an m × n matrix:
  r ← 0; c ← 0
  while r<m and c<n do
    if for all i such that r ≤ i<m, Ai,c = 0 then
      c ← c + 1
    else
      i ← the first index s.t. r ≤ i<m and Ai,c = 0
      Swap rows r and i
      For all 0 ≤ j<m, if Aj,c = 0, multiply row j by A−1
                                                         j,c
      For all 0 ≤ j<m, j = r, if Aj,c = 0, subtract row r from row j
      r ← r + 1; c ← c + 1
    end if
  end while
  for r = 0 to r = m − 1 do
    Let c be the index of the first nonzero entry in row r if one exists
    Multiply row r by A−1 r,c
  end for
```
MathComp). While translating this into MathComp is largely straightforward, it turns out that the C program does not actually implement Algorithm 1. Rather, rows are never swapped and at each iteration, all entries in column c must be nonzero.

The following excerpt from the C code, with the original comments, shows the error checks to ensure this condition. The code is mainly interesting for the error checks and comments, but we briefly detail how it works: the while guard value never changes; instead for current column k, the code iterates through rows w. The second conditional checks if matrix element (w, k) is nonzero for swapping (but returns an error because swapping is not implemented), while the first conditional breaks out of the loop with an error when w has reached the last row.

```
while (∗(q − k) == 0){ /∗ if zero ∗/
 if (++w == i max){
   return (FEC ERR TRANS FAILED); /∗ failed ∗/
 }
 if (∗(p + (w ∗ j max) + j max − 1 − k) != 0){
   /∗ swap rows ∗/
   return (FEC ERR TRANS SWAP NOT DONE); /∗ Not done yet! ∗/
 }
}
```
The "swap rows" and "Not done yet!" messages suggest that the authors intended to (eventually) implement the full algorithm. The error checks indicate that the authors were not sure if these errors could be triggered.

We will call this algorithm "Restricted" Gaussian elimination (Algorithm 2). Once again, defining this function in MathComp is not difficult, but proving that this limited form of Gaussian elimination suffices was a major part of the functional model verification (Sect. 5.2).

#### Algorithm 2: Restricted Gaussian Elimination

```
On input A, an m × n matrix:
  r ← 0
  while r<m do
    For all 0 ≤ j<m, if Aj,r = 0, return error
    For all 0 ≤ j<m, multiply row j by A−1
                                          j,r
    For all 0 ≤ j<m, j = r, subtract row r from row j
    r ← r + 1
  end while
  for r = 0 to r = m − 1 do
    Multiply row r by A−1 r,r
  end for
```
#### **4.3 Field Operations**

The encoder, decoder, and Gaussian elimination work over any field, but the C implementation uses the field GF(28), which we must define. Mathematically, this field is isomorphic to F2[x]/(1 + x2 + x3 + x4 + x8). That is, the elements of this field are polynomials of degree at most 7 with coefficients in F2 (the field of two elements), and all operations are performed modulo 1 + x2 + x3 + x4 + x8. The choice of F2 is important; it allows us to represent polynomials as sequences of bits. Since the polynomials are of degree at most 7, all field elements can be represented as bytes.

This field and its construction are well understood; while MathComp did not include the construction of finite fields via quotients, we were able to define and prove general results about primitive polynomials and the finite field's construction without much issue. Then, we can prove correct the method the C code uses to populate the lookup tables used to compute in this field (Sect. 6.4).

One difficulty in using this field is the difference between the polynomials we used to define the field and the bytes that we would like to represent as field elements. To avoid manually converting everywhere, we defined another field structure directly on the byte type and used Coq's Canonical Structures.

#### **5 Verifying the Functional Model**

#### **5.1 Decoder Correctness**

To prove the RSE algorithm correct, we need to prove that the decoder actually reconstructs the original packets. That is, if the data and parity packets that were marked as "received" are correct and there are at most h missing packets, then running the decoder on the received packets should recover the original data. We state this in Coq below:

**Theorem** decoder correct: ∀ (h xh : nat) (Hh: xh ≤h) (data : 'M[F] (k, c)) (input: 'M[F] (k, c)) (parities: 'M[F] (h, c)) (missing packets : seq 'I k) (found parities : seq 'I h) (Hhh: h ≤max h) (x h : 'I h), (∗ Only the rows in [missing packets] are incorrect ∗) (∀ (x: 'I k) (y: 'I c), x \notin missing packets → data x y = input x y) → (∗ All found parity packets were produced by the encoder ∗) (∀ (x: 'I h) (y: 'I c), x \**in** found parities → parities x y = (encoder Hhh k leq n weights data) x y) → (∗ We have xh unique missing packets and found parities ∗) uniq missing packets → uniq found parities → size missing packets = xh → size found parities = xh → (∗ Then, the decoder recovers the original data ∗) decoder xh input parities missing packets found parities Hhh x h = data.

This theorem is expressed entirely in terms of MathComp matrices and operations; it does not rely on the C implementation at all. Its proof requires two main tasks: showing that W 2 is invertible and proving that the sequence of operations in the decoder is sufficient to recover the original data. The second task is fairly straightforward; we compare the matrices elementwise. Thus, the main challenge comes from proving the invertibility of the submatrix W 2.

**Proving the Invertibility of** *W-* **2.** Recall that W 2 is a dynamically chosen submatrix of W, the right submatrix of the row-reduced Vandermonde matrix V . Therefore, we want to prove the following theorem (any submx unitmx):

**Theorem 1.** *Let* V *be an* m × n *row-reduced Vandermonde matrix on distinct elements. Let* m ≤ n *and* z ≤ min(m, n − m)*. Let* Y *be the submatrix of* V *formed by taking* z *rows of* V *and* z *of the last* (n − m) *columns of* V *. Then* Y *is invertible.*

Formally proving this theorem in Coq is quite complicated, partly because Math-Comp does not include many of the definitions and results that we need. Namely, we need to define and prove properties about row operations and Vandermonde matrices, including the following well-known property (vandermonde unitmx):

**Theorem 2.** *Let* V *be an* n × n *Vandermonde matrix on distinct nonzero elements. Then* V *is invertible.*

The proof relies on the fact that a degree n polynomial with n + 1 zeroes is identically zero, a fact already included in MathComp. This marks the only direct use of polynomial properties (other than in the finite field construction); the rest of the results are purely based on linear algebra.

Note that the only property we required of the weight matrix W was that every z × z submatrix is invertible. Row-reduced Vandermonde matrices satisfy this property, but any other matrix that satisfies this property could be used, and the encoding-decoding scheme would still be correct.

#### **5.2 Gaussian Elimination**

Proving full Gaussian elimination (Algorithm 1) correct is fairly standard (though nontrivial to formalize completely in Coq), since the algorithm is very well-understood.

The real challenge is to determine the conditions under which RGE (Algorithm 2) will return the same result as Algorithm 1. It is easy to see that if the error case is never reached, then the two algorithms are equivalent. But it is not at all obvious how to avoid triggering the error. Invertibility is a necessary but quite insufficient condition; for instance, the restricted algorithm fails on diagonal and triangular matrices. Therefore, we had two tasks: determine the class of matrices for which RGE works correctly and prove that the matrices used in the RSE algorithm are in this class.

For the first task, we needed to determine when certain elements will be zero or nonzero at a given step in Gaussian elimination. This is difficult, since the elements are constantly changing; instead, we transformed the condition into a statement about the invertibility of certain submatrices, since Gaussian elimination preserves invertibility.

During the rth step of Gaussian elimination (assuming no error was reached), the r × r upper-left submatrix is a diagonal matrix with nonzero elements along the diagonal; all other elements in the first r columns are zero. With this, we defined the submatrix C*r k* (for k<r) as the submatrix of A consisting of the first r rows and the first r + 1 columns except column k. Then, for k<r, A*k,r* = 0 exactly when C*r k* is invertible (we prove this by showing that the rows of C*r k* are linearly independent). We can do something similar for k ≥ r; this time we consider R*r k*, defined to be the submatrix of A consisting of the first r+1 columns and rows {0, 1,...r − 1, k}. Similarly, R*r k* is invertible iff A*k,r* = 0. We will say that A is *strongly invertible* if, for all 0 ≤ r<m, C*r k* is invertible for all k<r and R*r k* is invertible for all k ≥ r. Finally, we prove that RGE is equivalent to full Gaussian elimination iff input A is strongly invertible.

Note that this condition requires a particular set of m2 submatrices of the input m × n matrix to be invertible, quite a difficult condition to satisfy. However, in this application, Gaussian elimination is applied to only two kinds of matrices: the matrices W 2 in the decoder and a Vandermonde matrix on x*nmax*−2,...,x2, x, 1 (where x is the primitive element of the field). The strong invertibility of each ultimately follows from properties of Vandermonde matrices: the result for the first matrix follows from Theorem 1, while the result for the second is harder to show, but ultimately follows from repeated applications of Theorem 2 and use of the fact that the field elements are consecutive powers of the primitive element. With this, we proved the previously unknown result that RGE suffices for this application and that the errors shown in Sect. 4.2 are never reached.

## **6 Verifying the Implementation**

The C code consists of five primary functions with the following signatures:

// Populate the field lookup tables **void** fec generate math tables(**void**) // (Restricted) Gaussian elimination on the i max × j max matrix p **int** fec matrix transform(**unsigned char** ∗p, **unsigned char** i max, **unsigned char** j max) // Generate weight matrix (row−reduced Vandermonde matrix) **void** fec generate weights(**void**) // Encode the data by appending h parity packets to the k data packets in pdata. // plen is an array of the lengths of the data packets. // pstat is a flag, all are initially FEC FLAG KNOWN. **int** fec blk encode(**int** k, **int** h, **int** c, **unsigned char** ∗∗pdata, **int** ∗plen, **char** ∗pstat) // Decode the packets in pdata. The ith flag in pstat is FEC FLAG WANTED if // the ith packet is missing, otherwise FEC FLAG KNOWN **int** fec blk decode (**int** k, **int** c, **unsigned char** ∗∗pdata, **int** ∗plen, **char** ∗pstat)

Each of these functions has a corresponding VST specification. We first describe key implementation differences and verification challenges, then discuss the specs for selected functions in Sect. 6.4 and Sect. 6.5.

#### **6.1 Implementation Differences from Algorithm**

Broadly, the C code implements the RSE algorithm from Sect. 2 with the parameters k*max* = 127 and h*max* = 128 (as well as a bound of 16000 on c, but this does not affect the correctness). However, neither this algorithm nor the functional model precisely align with the C implementation. Instead, the implementation makes a few changes, and we must prove that these changes do not modify the algorithm's behavior:

– The code takes as input a sequence of variable-length packets, and we want to recover the original data once the decoder has finished. The RSE algorithm only describes how to generate the recovered packets, but the implementation has to put each packet pointer in its correct position in the packet array and ensure that the length for each packet is correct. The functional model includes filling in missing packets, but it uses matrices of uniform length.

#### **6.2 Implementation-Specific Verification Challenges**

Aside from differences between the algorithm and implementation, the C code, first written 25 years ago and last modified over 15 years ago, does several things that make it poorly suited to verification:

#### **6.3 VST Specifications**

A C specification in VST looks like:

DECLARE f WITH v PRE [ *param typs* ] PROP(p1) PARAMS(*params*) GLOBALS(*globs*) SEP(s1) POST [ *ret ty* ] PROP(p2) RETURN(*ret*) SEP(s2)

where f is the function name, *param typs* are the C function parameter types, *ret ty* is the C return type, *params* are the (symbolic) values of the function parameters, *globs* are the global variables, and *ret* is the (symbolic) return value. The entire PRE block represents the precondition, which must hold before the function is run. The POST block is the postcondition, which is true after the function finishes. *p1* and *p2* are propositions in Coq's logic, while *s1* and *s2* are propositions in separation logic—they describe the contents of memory. Finally, the variables v in the WITH clause are logical variables, abstract mathematical values to which the precondition and postcondition can refer.

#### **6.4 Verifying fec generate math tables**

The first C function is fec generate math tables, the function that generates the power, logarithm, and inverse tables for the field elements. This function, like the others, is interesting because of how it modifies memory, not because of what it returns; thus the interesting part of the VST spec is the SEP clause. The precondition's SEP clause says that the global array fec 2 index (the power table) initially stores fec n zeroes. In the postcondition, this global array now stores the Coq list byte pows, which we define as the powers of field element x (the ith entry contains x*i* ). We have similar Coq lists and pre- and post-conditions for the log table and inverse table.

Proving that the field table generation is correct is largely straightforward, given the field definitions described in Sect. 4.3. However, there were two main complications. The first comes from the method of populating the tables: compute x*i* for all 0 ≤ i < 256 by repeatedly multiplying the result by x in each iteration (this can be implemented efficiently as a bitwise shift left and an xor). The correctness of this method relies on the fact that the modulus polynomial is primitive (i.e., the smallest n such that the modulus polynomial divides x*n* − 1 is 255), and is not trivial to show in Coq.

Separately, although in the functional model we prove results for arbitrary fields and irreducible polynomials, here we need to show that several specific polynomials are irreducible and primitive (several field sizes are allowed by the code, although only one is used). Both of these conditions require showing that a polynomial is not divisible by a set of polynomials, so the easiest way to show this is by direct computation along with a proof that this computation is sufficient. However, MathComp polynomials are opaque and not computable (dividing two MathComp polynomials results in a hanging computation), so we needed to define concrete, computable polynomials and operations and relate them to their MathComp equivalents. Then, we can prove that the particular polynomials that the C code uses satisfy all needed properties.

#### **6.5 Verifying fec blk decode**

The function spec for fec blk decode is quite long; it consists of many tedious preconditions to ensure that the input packets are stored correctly in memory, that the length and packet status arrays correspond to the actual packets in memory, and that the various integer parameters are within their correct bounds. The list of preconditions is long; however, these functions are called by client functions that do packet-handling and buffer management, and the verification of *those* functions will check that they do indeed set up their inputs correctly (see Sect. 8).

We focus on a key part of the spec: the precondition's SEP clause includes the predicate iter sepcon arrays packet ptrs packets, which states that the Coq list packets is stored in memory at the given pointers. In the postcondition's SEP clause, this becomes iter sepcon arrays packet ptrs (decoder list k c packets parities stats lengths parbound). In other words, after the function is run, the contents of the packet memory are represented by the *low-level functional model* of the decoder (the version that uses concrete types that VST can understand rather than opaque MathComp types).

Our decoder correct theorem (Sect. 5.1) states that the *high-level functional model* correctly reconstructs the missing packets that were originally given to the encoder. Lemma decoder list correct lowers that result to the low-level functional model, using some injectivity results between the two models.

Thus, a client of the code can compose the VST spec and the correctness theorem to prove that, after fec blk decode is run, as long as the received packets and parities were correct, the missing data is recovered and the original data is now stored in memory (see Sect. 8).

#### **6.6 Implementation Bug**

While verifying fec matrix transform, we discovered a bug in the following code:

```
q = (p + (i ∗ j max) + j max − 1);
m=q − j max;
for (n = q; n > m; n−−) {
        //loop body
}
```
Here, i ranges from 0 to i max, and p is a pointer to the input matrix. The problem is, when i = 0, q points to p+j max − 1 and thus m points to p − 1. By the C standard and the semantics of CompCert C, the comparison n > m is undefined behavior. In fact, in C11, even the line q − j max is undefined behavior [12, Section 6.5.6, #8].

This may seem harmless, but 21st-century C compilers optimize under the assumption that the program does not exhibit undefined behavior. A compiler can assume that m=q − j max cannot be reached when i=0, and it may mangle the loop body "knowing" that i= 0 . This has caused problems for systems code [26], and the solution is to avoid writing C programs with undefined behavior.

Fortunately, VST's machine-checked proof of soundness makes it impossible to prove a C program correct that contains undefined behavior (unless ruled out by a function precondition). The loop test n > m cannot be verified in VST, since undefined behavior cannot be ruled out.

Without formal methods, this type of bug is quite difficult to find: it depends on subtle C semantics, today's static analyzers won't catch it,2 and testing cannot catch it until (in some future year) an optimizing C compiler gets more aggressive. VST provides blanket assurance against this entire class of errors.

Moreover, because VST uses separation logic, we specify exactly what effects the code is allowed to have. Thus, in principle, this kind of verification is 100% resistant to adversarial attacks that try and put exploits into code provided that those exploits can be defined as a functional property of the C code (such as which memory addresses it accesses, what system calls it makes, etc.). But our methods cannot defend against side-channel attacks.

#### **7 Related Work**

*Verification of Network Middleboxes.* Through several recent efforts, verification of network functions running in the dataplane has become increasingly feasible. Software dataplane verification [9] uses symbolic execution to prove certain lowlevel properties (such as memory safety) about programs written with Click, a popular framework for configuring routers and writing network functions. Gravel [31] uses symbolic execution and SMT solvers to verify many middlebox-specific properties of Click programs, including functional correctness. VigNAT [30] uses a mix of symbolic execution and proof checking to verify a Network Address Translation (NAT) implementation in C; this approach requires the use of a specialized data structure library and annotations on the C program but is quite automated overall. Vigor [29] builds on VigNAT to extend similar methods to more general network function verification. It uses a simpler but less expressive specification language, enabling fully automatic verification. Vigor and VigNAT use Verifast [13], a separation-logic-based tool for verifying C programs that is more automated than VST but is not connected to a proof assistant; this makes functional model proofs much more difficult.

These tools are considerably more automated than our work, but face significant restrictions on the type of code they can verify: none can verify code with

2 "Conceptually, this undefined-behavior optimization bug is possible to trigger with STACK's approach [26]. But, as for the current implementation of STACK, the answer is likely no, because it depends on LLVM to do loop unrolling/inlining . . . and I doubt LLVM would do either . . . ." (Xi Wang, e-mail of May 23, 2022).

arbitrary unbounded loops, pointer arithmetic, or use of complex data structures. More importantly, none could handle the mathematical reasoning needed to prove the correctness of the functional model and ensure that the FEC correctly reconstructs packets.

*Verification of Error-Correcting Codes.* Since error-correcting codes are both ubiquitous and quite complex to implement correctly, there has been a long line of research in formalizing various codes. Most of these efforts take the form of either automated hardware verification of digital circuits or recent efforts to create formalized libraries of error-correcting codes. We believe that our work is the first to connect a high-level, mathematical specification with an efficient implementation.

Error-correcting codes are hard to verify with automated methods such as model checking and BDDs because of the large state space and the complexity of the algorithms. Some recent efforts [8] have used automated hardware verification tools to verify (non-Reed-Solomon) ECCs, but they can handle very few bit errors. BLUEVERI [16] is a tool for verifying hardware implementations of finite field operations and was applied to Reed-Solomon codes. It can handle more errors (up to almost a dozen bits), but requires extensive manual effort and knowledge of hardware implementation details.

In a separate vein, several recently-developed libraries of formalized coding theory are similar to the functional model in our work, but are not connected to an efficient implementation. Most notably, Affeldt, Garrigue, and Saikawa have developed a Coq library for error-correcting codes, including Hamming and acyclic LDPC [1], Reed-Solomon [2], and BCH [3] codes. This library is built atop MathComp, and includes many theoretical results about each of these codes as well as specific encoders and decoders. Ideally, we would have liked to use this library as part of our functional model, but the implementation we verified differs significantly from standard Reed-Solomon coding, which corrects errors rather than erasures. Their library's Euclidean-algorithm-based decoding is extremely different from the decoder in RSE.

In Lean, a coding theory library called Cotoleta was developed and used to prove results about Levenshtein distance [14] and Hamming(7,4) codes [11]. Separately, Hamming(7,4) and 1 2 -rate convolutional codes were verified in the ACL2 theorem prover [20] with a particular focus on correcting memory errors; these codes were verified against a particular memory model. Both of these projects focused on verifying concrete-sized codes; thus they did not require the same level of abstraction or general mathematical reasoning as our work.

#### **8 Future Work**

In a real system, the encoder and decoder verified in this work are called by clients who handle receiving packets, assigning them to batches, and maintaining various data structures. We are currently working to verify a real-world version of such a system. This will permit a single, clean, end-to-end correctness result; right now, we have separate results for the decoder's correctness and the C program refinement which must be composed together. However, the specification of such a system introduces new challenges; it must reason about packet streams and network-specific features such as headers, timeouts, and packet reordering.

This C implementation of RSE has been useful in several projects at Bellcore/Telcordia/Peraton even though it cannot run at modern packet bit rates. We believe that a line-rate FPGA implementation of the finite-field matrixmultiply partial step is possible, and we are designing an API by which this could be controlled by a C program or a P4 program. Such an FPGA could be proved correct by a layered proof. The top layer would be our MathComp proof with no changes. The bottom layer could be proved using a Coq tool for hardware synthesis and functional-correctness verification, such as Kˆoika [7].

## **9 Conclusion**

We have presented an efficient, real-world C implementation of Reed-Solomon forward erasure correction that we formally verified using the Coq proof assistant and the Verified Software Toolchain. The code was verified with only minor changes; one macro was turned into a function for ease of verification and one bug that caused undefined behavior was fixed. While the code has been in use for over 25 years, the correctness of certain parts of the underlying algorithm, a modified form of Reed-Solomon erasure coding, were still ill-understood, including a very restricted form of Gaussian elimination. We were able to use Coq's Mathematical Components library to completely verify the correctness of this algorithm and VST to prove that the C code, with its various optimizations and modifications, correctly implements this algorithm. This demonstrates that tools like VST allow us to verify real-world, dusty-deck programs in C, even those whose correctness depends on a broad base of mathematics and those with numerous low-level optimizations. We believe this can be a viable approach to connect efficient low-level code with sophisticated high-level reasoning, enabling reliable software components for networks and other systems.

## **Appendix**

The appendix to this paper can be found in our git repo (see footnote 1) in doc/Appendix.pdf.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers**

Shenghao Yuan1(B) , Fr´ed´eric Besson1 , Jean-Pierre Talpin1 , Samuel Hym2, Koen Zandberg4, and Emmanuel Baccelli3,4

> 1 Inria, Rennes, France {shenghao.yuan,frederic.besson<EMAIL_ADDRESS>2 University of Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, 59000 Lille, France<EMAIL_ADDRESS>3 Freie Universit¨at Berlin, Berlin, Germany 4 Inria, Saclay, France<EMAIL_ADDRESS>
**Abstract.** RIOT is a micro-kernel dedicated to IoT applications that adopts eBPF (extended Berkeley Packet Filters) to implement so-called femto-containers. As micro-controllers rarely feature hardware memory protection, the isolation of eBPF virtual machines (VM) is critical to ensure system integrity against potentially malicious programs. This paper shows how to directly derive, within the Coq proof assistant, the verified C implementation of an eBPF virtual machine from a Gallina specification. Leveraging the formal semantics of the CompCert C compiler, we obtain an end-to-end theorem stating that the C code of our VM inherits the safety and security properties of the Gallina specification. Our refinement methodology ensures that the isolation property of the specification holds in the verified C implementation. Preliminary experiments demonstrate satisfying performance.

**Keywords:** Mechanized proof · Virtual machines · Fault isolation

#### **1 Introduction**

Hardware-enforced memory isolation (*e.g.,* Trustzone, Sanctum [6], Sancus [30]) is often not available on micro-controller units (MCU) which usually trade coarse-grain isolation for price and performance. To mitigate development variability and cost, common practices for MCU operating system design (RIOT [3], FreeRTOS, TinyOS, Fushia, and others [14]) advise to run all the device's code stack in a shared memory space, which can only be reasonably safe if that code can be trusted. While standard in safety-critical system design, such a trust requirement is oftentimes unsuitable for networked MCUs, where the extensibility of the OS kernel at runtime is an essential functionality. When system reconfiguration does not affect the entire network (via, *e.g.,* leader election), extensibility can easily be provided offline, by employing library OSs or unikernels [24], to reconfigure network endpoints independently (*e.g.,* cloud apps). Otherwise, the best solution is to load and execute system extensions (configurations, protocols, firewalls, etc.) as assembly-level Wasm [13] or Berkeley Packet Filters [25] scripts using an interpreter or a Just-In-Time (JIT) compiler on the target device.

*Femto-Containers.* RIOT adopts the extended Berkeley Packet Filters (eBPF) and tailors it to resource-constrained MCUs by implementing so-called femtocontainers: tiny virtual machine instances interpreting eBPF scripts. Compared to more expressive languages, like Wasm, experiments show that RIOT's eBPF implementation, rBPF, requires less memory [39]. The Linux kernel features an eBPF JIT compiler whose security depends on a sophisticated online verifier [29]. As an MCU architecture cannot host such a large verifier, executing JIT code would imply delegation of trust to a third-party, offline, verifier. The alternative is to rely on a defensive VM. Though a VM may be slower than a JIT, it can run untrusted, erroneous, adversary code in an open, and possibly hostile environment, and still isolate faults to protect its host's integrity.

*Approach and Goals.* This paper investigates an approach that trades high performance on low-power devices for defensive programming and low memory footprint. Our primary goal is to prevent faults that could compromise host devices and, by extension, force networked devices to reboot and resynchronize (*i.e.,* fault tolerance protocols). To maximize trust in the implementation of rBPF, our refinement methodology allows the verified extraction of C code directly from its mechanically proved definition in Gallina, the functional language embedded in the Coq proof assistant [4].

*Method.* To mechanically prove the correctness of an interpreter, a conventional approach consists in defining the reference semantics in a proof assistant and in showing that an executable optimized interpreter produces the same output. In this paper, our goal is to verify the interpreter of the virtual rBPF instruction set, implemented with the system programming language C. To this aim, we introduce a direct, end-to-end, validation workflow. The semantics of the source instruction set is directly defined by monadic functional terms in our proof assistant. We prove that this semantics enforces safety and security requirements regarding memory isolation and control-flow integrity. Then, C code is automatically derived from these monadic functional terms to implement the expected virtual machine. We prove that the extracted C code has the same stateful behavior as the monadic specification. Our method uses a monadic subset of Gallina of sufficient expressiveness to specify rBPF's semantics, supports the verified extraction of equivalent Clight [20] code, while provably implementing all required defensive runtime checks.

*Plan.* The rest of the paper is organized as follows. Section 2 states our contributions. Section 3 provides background on BPF and its variants, CompCert and the ∂x code extraction tool. Section 4 presents our workflow to formally refine monadic Gallina programs into C programs. Section 5 defines the proof model of our virtual machine: its semantics, consistency and isolation theorems. Section 6 refines the proof model of our femto-container into a synthesis model ready for code generation with CompCert. Section 7 proves the refinement between the synthesis and implementation models. Section 8 introduces our verified verifier which establishes the invariants needed by the VM. Section 9 case studies the performance of our generated VM implementation with respect to off-the-shelf RIOT femto-containers. Section 10 presents related works and Sect. 11 concludes.

#### **2 Contributions**

Implementing a fault-isolating virtual machine for MCUs faces two major challenges. One is to embed the VM inside the MCU's micro-kernel and, hence, to minimize its code size and execution environment. A second challenge is to minimize the verification gap between its proof model and the running code. We address these challenges and present the first end-to-end verification and synthesis of a full-scale, real-world, virtual machine for the BPF instruction set family: CertrBPF, an interpreter tailored to the hardware and resources constraints of MCU architectures running the RIOT operating system. CertrBPF employs a workflow of proof-oriented programming using the functional language Gallina embedded in the proof assistant Coq. The verified refinement and extraction of an executable C program is performed directly from its proof model. We report the successful integration of CertrBPF into the open source IoT operating system RIOT and the evaluation of its performance against micro-benchmarks.

*A Certified rBPF Interpreter.* CertrBPF is a verified model and implementation of rBPF in Coq. We formalize the syntax and semantics of all rBPF instructions, implement a formal model of its interpreter (femto-container), complete the proof of critical properties of our model, and extract and verify CompCert C code from this formalization. This method allows us to obtain a fully verified virtual machine. Not only is the Gallina specification of the VM proved kernel- and memory-isolated using the proof assistant, but the direct interpretation of its intended semantics as CompCert C code is, itself, verified correct. This yields a fully verified binary program of maximum security and minimal memory footprint and reduced the Trusted Computing Base (TCB): CertrBPF, a memory-efficient kernel-level virtual machine that isolates runtime software faults using defensive code and does not necessitate offline verification.

*End-to-End Proof Workflow.* An obvious choice is to use the existing Coq extraction mechanism to compile the Gallina model into OCaml. The downside of this approach is that Coq extraction has to be trusted. Moreover the OCaml runtime needs to be trimmed down to fit space requirements of our target architecture and also becomes part of the TCB. Our ambition is instead to minimize the verification gap and provide an end-to-end security proof linking our Gallina model to, bare-metal, extracted C code. Our intended TCB is hence restricted to the Coq type-checker, the C semantics of the CompCert compiler and a pretty-printer for the generated C Abstract Syntax Tree (AST).

To reach this goal, our starting point is a model of the rBPF semantics written in Gallina. We use this proof model to certify that all the memory accesses are valid and isolated to dedicated memory areas, thus ensuring isolation. From this proof model, we then derive a synthesis model of which we extract an executable version in Clight, that we finally prove to perform the same state transitions.

*Systems Integration and Micro-benchmarks.* We integrate CertrBPF as a drop-in replacement of the current, non-verified, rBPF interpreter in the RIOT operating system. We then comparatively evaluate the performance of CertrBPF integrated in RIOT, running on various 32-bit micro-controller architectures. Our benchmarks demonstrate that, in practice, CertrBPF not just gains security, but reduces memory footprint as well as execution time.

## **3 Background**

This section describes essential features of rBPF, of the CompCert compiler, and of the ∂x code generation tool, that are required by our refinement methodology.

*BPF, eBPF and rBPF.* Originally, the purpose of Berkeley Packet Filters [25] (BPF) was network packet filtering. The Linux community extended it to provide ways to run custom in-kernel VM code, hooked into various subsystems, for varieties of purposes beyond packet filtering [10]. eBPF was then ported to microcontrollers, yielding RIOT's specification: rBPF [38]. Just as eBPF, rBPF is designed as a 64-bit register-based VM, using fixed-size 64-bit instructions and a reduced instruction set architecture. rBPF uses a fixed-size stack (512 bytes) and defines no heap interaction, which limits the VM memory overhead in RAM. The rBPF specification, however, does not define special registers or interrupts for flow control, nor support virtual memory: the host device's memory is accessed directly and only guarded using permissions.

*The CompCert Verified Compiler.* CompCert [18] is a C compiler that is both programmed and proved correct using the Coq proof assistant. The compiler is structured into passes using several intermediate languages. Each intermediate language is equipped with a formal semantics and each pass is proved to preserve the observational behavior of programs.

*The Clight Intermediate Language.* Clight [20] is a pivotal language which condenses the essential features of C using a minimal syntax. The Verified Software Toolchain (VST) [2] verifies C programs at the Clight level that are obtained by the clightgen tool. Though we do not reuse the proof infrastructure of VST, we are reusing clightgen in order to get a Clight syntax from a C program.

*CompCert Values and Memory Model* [19,20]. The memory model and the representation of values are shared across all the intermediate languages of CompCert.  The undefined value *Vundef* represents an unspecified value and is not, strictly speaking, an undefined behavior. Yet, as most of the C operators are strict in *Vundef* , and because branching over *Vundef* or de-referencing *Vundef* are undefined behaviors, our proofs will ensure the absence of *Vundef* . CompCert values also include floating-point numbers; they play no role in the current development. CompCert's memory consists of a collection of separate arrays. Each array has a fixed size determined at allocation time and is identified by an uninterpreted block b ∈ *block*. The memory provides an API for loading values from memory and storing values in memory. Operations are parameterised by a memory chunk k which specifies how many bytes should be written or read and how to interpret bytes as a value v ∈ *val*.

For instance, the memory chunk *Mint32* specifies a 32-bit value and *Mint64* a 64-bit value. The function *load* kmbo takes a memory chunk k, a memory m, a block b and an offset o. Upon success, it returns a value v obtained from the memory by reading bytes from the block b starting at index o. Similarly, the function *store* kmbov takes a memory chunk k, a memory m, a block b, an offset o and a value v. Upon success, it returns an updated memory m which is identical to m except that the block b contains the value v encoded into bytes according to the chunk k starting at offset o. The isolation properties offered by CompCert memory regions are worth mentioning: *load* and *store* operations fail (return None) for invalid offsets o and invalid permissions.

*The* ∂x *tool.* ∂x emerged from the toolchain used to design and verify the Pip proto-kernel [15]. Its aim was to allow writing most of Pip's source code in Gallina in a style as close to C as possible. ∂x extracts C code from a Gallina source program in the form of a CompCert C AST. The goal of ∂x is to provide C programmers with readily reviewable code and thus avoid misunderstanding between those working on C/assembly modules (that access hardware) and those working on Coq modules (the code and proofs). To achieve this, ∂x handles a C-like subset of Gallina. The functions that are to be converted to C rely on a monad to represent the side effects of the computation, such as modifications to the CPU state. Yet ∂x does not mandate a particular monad for code extraction.

∂x *'s Workflow.* ∂x proceeds in two steps. First, given a list of Gallina functions, or whole modules, it generates an intermediate representation (IR) for the subset of Gallina it can handle. The second step is to translate this IR into a CompCert C AST. Since Coq has no built-in reflection mechanism, the first step is written in Elpi [8], using the Coq-Elpi plugin [37]. That step can also process external functions (appearing as extern in the extracted C code) to support separate compilation with CompCert. In order to obtain an actual C file, ∂x also provides a small OCaml function that binds the extracted C AST to CompCert's C pretty-printer. Even though the ∂x language is a small subset of Gallina, it inherits much expressivity from the use of Coq types to manipulate values. For example, we can use bounded integers (*i.e.,* the dependent pair of an integer with the proof that it is within some given range), that can be faithfully and efficiently represented as a single int in C. To this end, ∂x expects a configuration mapping Coq types to C.

∂x *Memory Management.* A major design choice in the C-like subset of Gallina used by ∂x is memory management: its generated code executes without garbage collection. This affects the Coq types that can actually be used in ∂x: recursive inductive types, such as lists, cannot automatically be converted. However, this Gallina subset is particularly relevant to programs in which one wants to precisely control memory management and decide how to represent data structures in memory. This is typically the case of an operating system or, in our case, the rBPF virtual machine.

## **4 A Workflow for End-to-End Verification in Coq**

This section gives an overview of our methodology to derive a verified C implementation from a Gallina specification. In the following sections, the methodology will be instantiated to derive the C implementation of a fault-isolating rBPF virtual machine and its verifier. Our approach provides an end-to-end correctness proof, within the Coq proof assistant, that reduces the hurdle of reasoning directly over the C code.

As shown in Fig. 1, the original rBPF C implementation is first formalized by a proof model in Gallina, and the verification of expected properties (*e.g.,* safety) is performed within the Coq proof assistant. This specification is then refined into an optimized (and equivalent) synthesis model ready for C-code extraction.

**Fig. 1.** End-to-end verification and synthesis workflow

The refinement and optimization principle employed by our method consists of deriving a C-ready implementation, in Gallina, that is as close as possible to the expected target C code. This principle allows to i) prove optimizations correct, ii) improve the performance of the extracted code and, iii) facilitate review and validation of extracted code with the system designers. From the C-ready Gallina implementation, we leverage ∂x to automatically generate C code and verify it: i) the generated C code is first parsed as a CompCert Clight model by the clightgen tool of VST and ii) it is proved to refine the source Gallina model in Coq using translation validation. Because ∂x generates C code in a syntax-directed manner, a minimal *Clightlogic* is designed to facilitate the refinement proof. The rest of the section explains these different steps in details.

*Proof-Oriented Specification.* Our specification takes the form of an executable abstract machine in monadic form. It uses the standard option-state monad M.

M a state := state → **option**(a × state) returnM : a → M a state := λa.λst.**Some**(a, st) bindM : M a state → (a → M b state) → M b state := λA.f.λs.**match** A s **with** | **None** ⇒ **None** | **Some**(x, s ) ⇒ (f x) s

In the remainder, we write ∅ for **None** and x for **Some** x.

The monad threads the state along computations to model its in-place update. The safety property of the machine is implemented as an inline monitor: any violation leads to an unrecoverable error, *i.e.,* the unique error represented by ∅. One step of the machine has the following signature:

*step* : M r state

where r is the type of the result. The *step* function implements a defensive semantics, checking the absence of error, dynamically. For our rBPF interpreter (see Sect. 5), the absence of error ensures that the rBPF code only performs valid instructions. In particular, all memory accesses are restricted to a sandbox specified as a list of memory regions. Function *step* is part of the TCB and, therefore, a mis-specification could result, after refinement, in an invalid computation. The purpose of the error state is to specify state transitions that would escape the scope of the safety property and, therefore, shall never be reachable from a well-formed state st ∈ *wf* ⊆ P(state). We require well-formedness to be an inductive property of the *step* function.

**Theorem 1 (Well-formedness).** *The step function preserves well-formedness.*

$$\forall st, st', r.\ st \in wf \land step\ st = \lfloor (r, st') \rfloor \Rightarrow st' \in wf$$

We also require that well-formedness is a sufficient condition to prevent the absence of error and, therefore, the safety of computations.

**Theorem 2 (Safety).** *The step function is safe,* i.e., *a well-formed state never leads to an error.*

$$\forall st. \ st \in wf \Rightarrow step \ st \neq \emptyset$$

*C-Ready Implementation.* Our methodology consists in refining the step function into an interpreter step∂x complying with the requirements of ∂x. As ∂x performs syntax-directed code generation, the efficiency of the extracted code crucially depends on step∂x. In order to preserve the absence of errors, we need a simulation relation between the step and step∂x functions. A direct consequence of the simulation thoerem is that step∂x never raises an error.

**Theorem 3 (Simulation).** *Given simulation relations* Rs ⊆ state × state *and* Rr ⊆ r × r *, the function* step∂x *simulates the function* step*.*

$$\forall s\_1, s\_1', s\_2, r. (s\_1, s\_2) \in Rs \land step \ s\_1 = \lfloor r, s\_1' \rfloor \Rightarrow \exists s\_2', r'. \bigwedge \begin{cases} step\_{\partial x} \ s\_2 = \lfloor r', s\_2' \rfloor \\ (s\_1', s\_2') \in Rs \\ (r, r') \in Rs \end{cases}$$

*Translation Validation of C Code.* The next stage consists in refining the step∂x function into a Clight program by relying on ∂x to get a C program and on the clightgen tool to get a Clight stepC program (see Sect. 6). As this pass is not trusted, we require the following translation validation theorem.

**Theorem 4 (Translation Validation).** *Given a simulation relation* Rs ⊆ state × val × mem *and a relation* Rr ⊆ res × val*, the Clight code* stepC *refines the function* step∂x*:*

$$\forall r, s, s', v, k, m. (s, v, m) \in Rs \Rightarrow step\_{\partial x} \; s = \lfloor (r, s') \rfloor \Rightarrow \exists m', r'. Call state (step\_C, [v], k, m) \rightarrow^{\*t} ReturnState(r', call.cont(k), m') \land (s', v, m') \in Rs \land (r, r') \in Rr$$