IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL

We motivate our analysis using two variations of a double-free vulnerability (listed as CWE-415 in the MITRE database²²2https://cwe.mitre.org/data/definitions/415.html). A double-free error occurs when a program calls free twice with the same argument. This may cause two later calls to malloc to return the same pointer, potentially giving an attacker control over the data written to memory.

The occurrence of the double-free vulnerability is straightforward to see in Listing 1, but of course, in a real program, the vulnerability may be much more difficult to identify. Listing 2 presents an alternative program that contains two occurrences of free(p) with no intervening malloc. However, Listing 2 does not contain a double-free vulnerability since the true branch returns from the method call before the second free(p) is executed.

The focus of our work is to analyse such programs without relying on any high-level language semantics. Instead, we aim to develop a technique for reasoning about programs (e.g., those in Listings 1 and 2) at a lower level of abstraction by first compiling the programs then, lifting the resulting binaries to an intermediate representation (BIL). Although such analysis contains more detail, the analysis reflects the behaviour of the actual executable, thus is more accurate (e.g., does not require any additional compiler correctness assumptions).

Our overall workflow is given in Figure 2, where the dashed steps represent existing work. The first step to proving properties about our example program is to use BAP to generate a BIL representation of a binary executable (see Figure 2). For our example program in Listings 1 and 2, the BIL equivalent (expressed in BIR format) are given in Listings 3 and 4, respectively. BIR (Binary Intermediate Representation) is a structured refinement of BIL that significantly enhances human readability by presenting sequences of BIL as a single instruction. Take for example the BIR instruction call @free with return 18 on line 16 in Listings 3 and 4. This represents two BIL statements, a jump to the address of the symbol “free”, and the assignment of the return value 18 to the return pointer. Note that IsaBIL takes as input BAP’s abstract data type format (see §​ 4), which we refer to as ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$, as opposed to the human-readable forms shown in Listings 3 and 4. This makes the BIL instructions simpler to parse when generating the corresponding Isabelle/HOL object (discussed in more detail below).

Extensions to Isabelle/HOL’s logic [15, 5, 26, 18] often make use of Isabelle/HOL’s locale system [27, 3], which provides convenient modules for building parametric theories. Locales are aimed at supporting the use of local assumptions and definitions for collections of similar theories, defined in terms of fixed variables and definitions. We refer to the fixed variables as parameters which must satisfy the local assumptions. For a locale $ℒ$, we give its definition as $ℒ=(p_1,p_2,\mathrm{\dots })$ where $p_1,p_2$ are the parameters of the locale. Each parameter may be any type derived from a set or a relation. From these variables, assumptions and definitions we can derive general theorems within the context of a locale. These theorems can be exported to the current proof context by instantiation, in which we provide values to one or all of the parameters and verify the fixed assumptions of these parameters. This effectively gives us the general theorems contained within each locale for free for a specific instantiation. Locales can be extended through inheritance or interpretation, enabling reusability and specialisation by introducing and refining a locale’s parameters. Inheritance operates hierarchically, directly propagating the context of a parent locale to a child locale. This transfer includes general theorems, assumptions, definitions and fixed variables. Interpretation is compositional, associating a locale or definition with another locale. During interpretation, the assumptions of the parent locale must be satisfied as part of the mapping process. A locale that interprets another locale is referred to as a sublocale, denoted $ℒ\subseteq {ℒ}^{\prime }$, where locale ${ℒ}^{\prime }$ is the parent of $ℒ$. For IsaBIL, they provide a uniform system for representing both the program, and the underlying reasoning framework.

The overall structure of the IsaBIL development is given in Figure 2, and comprises four main parts (which highlight our four main contributions). Overall, we have: (1) a locale (see §​ 4), representing a complete formalisation of the BIL specification from §​ 3, (2) a set of locales (see §​ 5) that encode Hoare Logic (to verify correctness) and Incorrectness Logic (as developed by O’Hearn), (3) a locale (see §​ 6.1) that combines formalisation of the BIL specification with (in)correctness logics, (4) a set of locales (see §​ 6.4) that apply the resulting verification framework to prove correctness of a number of examples from the literature and (5) a set of locales (see §​ 7.2 and 7.3) that demonstrate scalability of the approach. In particular, §​ 7.2 demonstrates the use of subroutines to enable one to focus on key functions of interest, even when starting with large BIL files (> 100k LoC). Then §​ 7.3 describes how verified subroutines can be used as subcomponents to prove (in)correctness of a larger system.

Our framework is highly flexible and extensible. For instance, the BIL_inference locale combines the BIL_specification and inference_rules locales. In case one wishes to change the specification (for a different operational semantics), or use a different set of inference rules (to perform a type of analysis), one can simply change the specification and/or inference rule locales. Similarly, a locale can be extended with additional semantic features: our proofs extend the BIL_inference locale with an allocation locale (that models memory allocation) and a find_symbol locale (that tracks a symbol table) to enable reasoning about different program features.

Our encoding of BIL (§​ 4) is the first full mechanisation of BIL in Isabelle/HOL. This mechanisation is a standalone contribution and can be used by others outside of our reasoning framework. Our encoding uncovers some inconsistencies in the official specification, which are addressed by the mechanisation (see §​ 3). Moreover, given that BIL is an intermediate language for many different architectures, future versions could be further optimised to a particular architecture. As an example, we present optimisations for RISC-V (see §​ 6.2.3), which is the architecture that we focus on.

To maximise flexibility, we provide an encoding of the inference rules parameterised by an operational semantics, i.e., an instance of the correctness and incorrectness rules can be generated for any operational semantics. This instance automatically inherits all of the rules of Hoare and Incorrectness logic that we prove generically in the correctness and incorrectness locales (§​ 5).

The BIL semantics from §​ 4 and the inference rules from §​ 5 are combined to form a new locale, BIL_inference, which provides facilities to verify BIL programs. Then, as discussed above, to verify particular types of examples, we extend the locales with models of allocation and symbols to verify particular sets of examples. These proofs represent the first proofs of both correctness and incorrectness for BIL programs in Isabelle/HOL. As we shall see in §​ 3, the BIL semantics is highly detailed, with the reductions related to even single load command potentially splitting into a large number of small-step transitions. This has the potential to increase the verification complexity making the proofs of even small programs intractable. To address this, we use BIL’s big-step semantics (§​ 6.1) and introduce a number of high-level lemmas that allow one to discharge such proofs generically. These lemmas are reusable across all of the examples that we verify.

Our proofs cover key examples from the JSF coding standards [32] and the CWE database³³3https://cwe.mitre.org/data/definitions/415.html. This task is greatly simplified using IsaBIL’s parser, written in Isabelle/ML [50], that automatically generates a locale corresponding to a BIL program written in ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ format. Note that Isabelle isolates Isabelle/ML programming, and hence our parser cannot interfere with soundness of Isabelle’s core logic engine. The generated locale is then combined with BIL_inference to provide a context in which (in)correctness proofs can be carried out.

The basic syntax of BIL programs is given in Figure 3.

BIL’s type system facilitates the need for typing rules to ensure type correctness. At the lowest level, the rules ensure that types are correctly defined with the predicate $t\text{is ok}$. The type of variables must be tracked during symbolic execution to ensure that they do not change and only values of the correct type can be assigned. This is achieved via a typing context, defined as $\mathrm{\Gamma }::=va{r}^{\ast }$, where type correctness of $\mathrm{\Gamma }$ is expressed by overloading the predicate $\mathrm{\Gamma }\text{is ok}$. The rules for $t\text{is ok}$ and $\mathrm{\Gamma }\text{is ok}$ are given below:

These are extended to expressions, then to the level of statements (see [8] for details). As part of our formalisation, we discover a missing typing rule for empty sequences, which would otherwise be needed to ensure the sequencing rules are type correct. We have created a pull request in the BAP repositories for this issue (see https://github.com/BinaryAnalysisPlatform/bap/pull/1588), which has now been merged.

Expression evaluation requires the repeated application of small-step semantics rules until the expression is reduced to a value. An expression step in BIL is formally expressed with the $\mathrm{\Delta }⊢e\mathrm{⤳}{e}^{\prime }$, where multiple steps can be reduced using the reflexive transitive closure $\mathrm{\Delta }⊢e{\mathrm{⤳}}^{\ast }{e}^{\prime }$. Recall that loads and stores occur at the expression level, and are sensitive to endian orderings. We provide the load rules here, and refer the interested reader to the BIL manual [8] for further details.

A store instruction (semantics not shown) targets a single unit of addressable memory, typically 8-bits in size. When a storage operation exceeds this size, it is converted into a sequence of 8-bit stores, organised in big-endian order. The reduction rules for load operations is given in Figure 4. First, all sub-expressions of a memory object are reduced to values using the rules load_step_addr and load_step_mem. Then, the resulting object is recursively deconstructed using the load_word_el and load_word_be rules, depending on the endian. This process continues until one of load_byte, load_un_mem or load_un_addr is used. load_byte reduces the expression to the value, $v^{\prime }$, when the memory object is a storage of an immediate (known) value, $w$. load_un_mem and load_un_addr both reduce the expression to an unknown value when the memory or address being loaded is unknown, respectively.

In this section, we describe the operational semantics for evaluating statements. We also provide a correction to the sequencing rule from the manual [4]. Although each statement induces local control flow, in BIL, they are assumed to execute to completion in a single step.

The semantics of a statement is defined by $(\mathrm{\Delta },pc)⊢seq\mathrm{⤳}({\mathrm{\Delta }}^{\prime },p{c}^{\prime })$, which executes the $bil$ statement $seq$ from the variable store $\mathrm{\Delta }$ to generate a new variable store ${\mathrm{\Delta }}^{\prime }$ and program counter $p{c}^{\prime }$. The move statement (see below) modifies $\mathrm{\Delta }$ by generating a new variable binding, and jmp (not shown) affects program counter.

Example rules for move (aka assignment) and if_true (for branching on a true guard are given below). In the move rule, the given expression $e$ is evaluated to a value using the big-step semantics, and the value for the given variable $var$ is updated in the variable state. In the if_true rule, the guard is evaluated (to $true$) then the statement $se{q}_1$ is executed. The sequencing rules describe execution of a list of statements to completion. The sequencing rules in manual [4] do not provide a means to reduce multiple statements in a single transition⁴⁴4We have created a Git pull request in the BAP repositories for this issue (https://github.com/BinaryAnalysisPlatform/bil/pull/12. .

A machine instruction in BIL is represented by a named tuple, $insn=⦇\text{addr},\text{size},\text{code}⦈$ (implemented later as an Isabelle record). Here addr, refers to the instruction’s address in memory; size, the size of the instruction; and code, the semantics of the program represented by BIL statements. Instructions operate over the BIL machine state, $(\mathrm{\Delta },pc,mem)$, where $\mathrm{\Delta }$ is the variable store, $pc$ is the program counter and $mem$ is a variable that denotes the memory. To decode the current instruction from a machine state, we assume an uninterpreted $\mapsto$ function, referred to as the decode predicate, which maps a machine state, $(\mathrm{\Delta },pc,mem)$, to the corresponding instruction, $⦇\text{addr},\text{size},\text{code}⦈$. The BIL step relation $(\mathrm{\Delta },pc,mem)\mathrm{⤳}({\mathrm{\Delta }}^{\prime },p{c}^{\prime },me{m}^{\prime })$ defines the execution of a single BIL statement:

IsaBIL’s BIL_specification locale (see Figure 2) provides a complete mechanisation of BIL’s syntax and semantics⁵⁵5As outlined in §​ 3 and provided in full in [21].. We encode BIL’s operational rules (§​ 3.5) as Isabelle’s built-in inductive predicates, which allow one to formalise the structure of the syntax from Figure 3.

The BIL_specification = $(\mapsto )$ locale provides a single parameter: the decode predicate ($\mapsto$), which will be uniquely instantiated for each binary that we wish to verify.

​We provide rules for both introduction (which are used to introduce compound statements such as if-then-else to the proof goal) as well as elimination (which are used to eliminate compound statements from the proof assumptions) directly within the BIL_specification locale. For example, introduction and elimination rules for the step_prog rule in §​ 3.5 which formalises a single step of the program are given below:

We prove introduction and elimination lemmas in this way for all of the rules in the official BIL specification [6] with respect to our changes (§​ 3). In total, the BIL_specification locale consists of over 500 lemmas and rules.

Recall that our workflow (Figure 2) proceeds by Step 1: compiling the given program; Step 2: feeding the resulting assembly into BAP to generate the corresponding ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$; and Step 3: using IsaBIL to automatically generate an Isabelle/HOL locale for the given ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ input. Note that if a binary is distributed without source code, then Step 1 could be skipped and the given assembly could be fed directly into BAP to generate the ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$.

The locale for a program prog is generated using IsaBIL’s translation tool, which is written in Isabelle/ML and is invoked using the custom Isabelle/HOL commands BIL or BIL_file for inline or external BIL in ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ format, respectively. Both commands take as an input, a name for the locale and either a BIL string (for BIL) or a filename (for BIL_file). Within this locale, we automatically generate a decode predicate, ${\mapsto }_{\text{prog}}$, that maps each machine state $(\mathrm{\Delta },pc,mem)$ to an instruction.

Note that, internally, Isabelle maintains the ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ format, however, we choose to represent it using class locales [50, 3, 41] to maintain human-readable syntax. For instance, without these syntax classes, expressing a direct jump to the fixed program address 3076 would require writing RAX := Val(Imm(Word(3076,64))). By instantiating the word syntax ($nat::sz$, see Figure 3), we can simplify the expression to the syntax RAX := (3076 :: 64).

In addition to ${\mapsto }_{\text{prog}}$, a program’s locale defines Step 1: an address set, $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}:\mathbb{P}(word)$ (defining the set of addresses that have corresponding instructions) and Step 2: a symbol table, $\mathrm{𝚜𝚢𝚖}\mathrm{\_}\mathrm{𝚝𝚊𝚋𝚕𝚎}:\mathrm{𝑠𝑡𝑟𝑖𝑛𝑔}\to word$ (mapping the binary’s symbols, e.g. main, memcpy, free, as string literals to raw addresses).

Both $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}$ and $\mathrm{𝚜𝚢𝚖}\mathrm{\_}\mathrm{𝚝𝚊𝚋𝚕𝚎}$ capture additional information about a binary that can be used later in a proof. For example, the $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}$ is useful for determining whether the program counter points to a valid address and is particularly important for validating the correctness of indirect jumps. Many binary proofs verify that execution from some entry point, such as the main function, is either correct or incorrect with respect to some property. Symbols typically represent entry points to functions and although the address of an entrypoint may differ between binaries, the symbol will remain constant. Hence, referring to positions within the binary using symbol names, stored in the $\mathrm{𝚜𝚢𝚖}\mathrm{\_}\mathrm{𝚝𝚊𝚋𝚕𝚎}$ rather than program addresses, is often more convenient. Further details regarding the extraction of the $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}$ and $\mathrm{𝚜𝚢𝚖}\mathrm{\_}\mathrm{𝚝𝚊𝚋𝚕𝚎}$ from a binary can be found in §​ 6.3.

BIL_inference interfaces with the BIL_specification and inference_rules locales (see Figure 2) and is later extended with instances of state models (e.g., allocation and find_symbol) to enable verification of generated BIL programs. Therefore, it is one of IsaBIL’s most complex components.

Our first task is to define a big-step relation, $\underset{BIL}{\overset{}{\Rightarrow }}$, required by inference_rules, using the BIL step relation, $(\mathrm{\Delta },pc,mem)\mathrm{⤳}({\mathrm{\Delta }}^{\prime },p{c}^{\prime },me{m}^{\prime })$, defined in §​ 3.5. One option for defining $\underset{BIL}{\overset{}{\Rightarrow }}$ is to simply take the transitive closure of $\mathrm{⤳}$. However, this would mean that the pre/postconditions that we define in our example would be predicates over the full variable store $\mathrm{\Delta }$, which is heavy-handed.

An alternative (which is the approach we take) is to define another transition relation $\underset{BIL}{\overset{}{\to }}$ that abstracts $\mathrm{⤳}$, and define $\underset{BIL}{\overset{}{\Rightarrow }}$ as the transitive closure of $\underset{BIL}{\overset{}{\to }}$. As we shall see, this vastly increases the flexibility of our approach, which becomes (1) extensible, since $\underset{BIL}{\overset{}{\to }}$ can be used to cover additional program features such as memory allocation (see §​ 6.4.1), and (2) more efficient since the components of $\mathrm{\Delta }$ that are not needed for the proof can be ignored.Thus, assuming $𝒞=(\mathrm{\Delta },pc,mem)$, we have:

Here, we assume $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}$ is the set of addresses that contain program instructions (see §​ 4.2), which will be later instantiated by a program’s locale. A program may take a step as long as the current program counter corresponds to a program instruction. Note that the precise state model (i.e., type of $\sigma$, ${\sigma }^{\prime }$ and $\tau$) that one uses in program_big_step and program_big_step_last will depend on the verification task at hand. If required, one could also take $\sigma =\mathrm{\Delta }$ allowing the proofs to inspect the full variable state (at a low level of abstraction).

Overall, we obtain a locale $\text{BIL\_inference}=(\mapsto ,\underset{BIL}{\overset{}{\to }},\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝})$. This locale extends the BIL_specification (from §​ 4) from which we inherit the decode predicate, $\mapsto$. Then, we use $\underset{BIL}{\overset{}{\to }}$ and $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}$ to define $\underset{BIL}{\overset{}{\Rightarrow }}$ as above. This allows us to interpret the inference_rules as sublocale, instantiating the parameter $\Rightarrow$ to $\underset{BIL}{\overset{}{\Rightarrow }}$.

Within BIL_inference, we can prove several rules of Hoare and Incorrectness logic in terms of the BIL semantics. These proofs are trivial at this level, but are nevertheless critical for proof automation since they can be used by all of our examples [21].

Instruction set architectures (ISAs), despite their large scale, are inherently finite, and compilers employ common patterns for optimization. Additionally, developers leverage reusable components such as functions and gadgets to perform common tasks. Consequently, binaries often exhibit a significant degree of repetition. Once identified, this repetition can be verified without the need for human input. IsaBIL exploits this repetition to alleviate the burden associated with proof construction and verification. In this section, we outline the proof automation techniques employed by IsaBIL.

A key component of our IsaBIL framework is a verified BIL parser that transpiles ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ programs into an Isabelle/HOL locale to enable verification.

Parsing occurs in two distinct phases. The first phase involves the translation of ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ into ${\text{BIL}}_{\text{ML}}$, a format suitable for manipulation within Isabelle/ML. This intermediate step enables analysis tasks in Isabelle/ML, such as calculating the size of instructions. The second phase involves translating ${\text{BIL}}_{\text{ML}}$ into an Isabelle/HOL representation, which is the starting point for verification. Parsing can be invoked directly on a ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ string with BIL or alternately on a file containing ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ with BIL_file. An overview of the parsing process is given in Figure 7.

During the first phase, the parser iterates over the instructions in a ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ input. It captures and stores all program addresses in $\mathrm{𝚊𝚍𝚍𝚛}\mathrm{\_}\mathrm{𝚜𝚎𝚝}$. Moreover, the parser associates symbols with a program address in $\mathrm{𝚜𝚢𝚖}\mathrm{\_}\mathrm{𝚝𝚊𝚋𝚕𝚎}$. Since the syntax of ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ resembles a tree structure, it is intuitive to convert it into an Abstract Syntax Tree (AST) using a lexer. This AST is processed by a Recursive Descent Parser (RDP), which traverses each node in the tree depth-first, matching the node’s value to a corresponding parsing function. For example, if the parser encounters a Var node, it will attempt to parse the first child as a string and the second child as a BIL type. This process transforms the input into ${\text{BIL}}_{\text{ML}}$, a structured data type closely resembling ${\text{BIL}}_{\mathrm{𝖠𝖣𝖳}}$ which can be manipulated within Isabelle/ML.

The second phase defines a locale within the current proof context with a fixed decode predicate. For each ${\text{BIL}}_{\text{ML}}$ instruction, an assumption is added to the locale, stating how a program with any variable state and memory, but with the instructions program address, decodes to an Isabelle/HOL representation of said instruction. To obtain the Isabelle/HOL representation, an RDP translator recursively converts each ${\text{BIL}}_{\text{ML}}$ instruction to Isabelle/HOL terms defined in the BIL_specification locale (see §​ 4).

The first phase of the parser harnesses Isabelle/HOL’s code generation, where specifications for both the lexer and parser were defined within Isabelle/HOL and subsequently translated into ML. ${\text{BIL}}_{\text{ML}}$ for example, is a direct ML representation of the BIL specification from the IsaBIL framework. Using code reflection, we import the generated ML code back into Isabelle/HOL as a plugin. Consequently, the lexer and parser are formally verified under the Isabelle/HOL framework. In contrast, the second phase employs non-code-generated ML. This decision stems from its necessity to interface with Isabelle/HOL’s core ML library, which cannot be achieved via code-generated ML. To bridge this gap, we introduce a minimal layer of unverified ML code that lifts the BIL representation obtained from the verified parser into Isabelle/HOL’s proof system. Below, as an example, we present a snippet of the translation code responsible for converting ${\text{BIL}}_{\text{ML}}$’s binary operations to IsaBIL’s binary operations:

Note that Isabelle isolates Isabelle/ML programming, and hence our parser cannot interfere with the soundness of Isabelle’s core logic engine.

The majority of the development consists of general tactics and lemmas which can be reused across multiple developments. We give the number of lemmas for each component in Table 2.

All of the sublocales and inherited locales can reuse the proofs of the higher-level (more abstract) locales. Thus, for instance, the 594 lemmas of the BIL_specification locale are applicable to BIL_inference and all of the examples, which improves re-usability. The RISC-V optimisations help improve performance and are reusable across all examples. The theories for double_free_* and find_symbol are general and apply to all corresponding examples. Finally, each example comprises a step lemma for each line of code. Using the earlier optimisations, solving them is trivial and only requires running the automated tactics.

To motivate IsaBIL, we employ a combination of correctness and incorrectness proofs, focusing on illustrative examples frequently referenced in BAP literature [8]. These examples represent patterns commonly found within much larger programs/libraries.

We cross compile cURL 7.50.3 for RISC-V on Linux using the GNU RISC-V compiler with the default options. We modify the source code for read_data by adding the noinline attribute, which ensures the function is not inlined. Note that noinline is not a requirement for verification, but facilitates compositional reasoning (see §​ 7.3).

Using the generated BIL directly creates a scalability challenge. The assembly corresponding to version 7.50.3 contains 63,592 RISC-V instructions, which equates to 127,023 LoC in BIL with 63,592 BIL instructions. Naively generating the corresponding IsaBIL locales (see §​ 6.3) takes approximately 14 minutes, which is impractical for verification. Of this, the lexer takes 4s, the parser takes 2s and the translator takes approximately 13 minutes. The wait time in the translator arises from instantiating the Isabelle/HOL locale in the proof context, an operation which cannot be avoided.

​​To address this, we extend the BIL_file command with a new option, with_subroutines, to focus only on the subroutines of interest (and their dependencies). For example, to generate the IsaBIL locale for read_data in version 7.50.3, we use the following command:

where “…” contains functions that read_data calls (e.g., ntohl). Running BIL_file now takes only 6s, with 131 instructions to verify. We next show how we detect this vulnerability in version 7.50.3 using an incorrectness proof.

read_data contains a double-free vulnerability. However, unlike our prior example (§​ 6.4.1), the vulnerability arises from a reallocation of memory. Thus, we first describe the construction of a reallocation locale, which reuses components from the allocation locale. Then, we prove the incorrectness of the read_data function in version 7.50.3.

The proof in Figure 9 covers the read_data subroutine in the cURL library. However, this subroutine is an internal function (i.e. not defined in a header file), making the vulnerability difficult to exploit directly in practice. Nevertheless, as shown in the call graph in Figure 11, there is a path from an external function (defined in a header file), namely Curl_sec_login, to read_data. That is, a call to Curl_sec_login includes a call to choose_mech, which in turn includes a call to sec_recv, which itself calls read_data. As such, the vulnerability in read_data could potentially be exploited by a call to Curl_sec_login.

Note that this may not always be the case, as freeing the data buffer pointer is left up to the caller, not the callee, and thus further incorrect behaviour to by caller (in this case a function above read_data in the call graph) could rectify this vulnerability by forgetting to call free, or perhaps reallocating the pointer again before freeing it. Thus, we should aim to establish that each of these methods are (in)correct formally.

We do this in a compositional fashion through proof reuse: we reuse the (in)correctness specifications we prove at lower levels of the call graph in higher levels. For instance, when proving that sec_recv is (in)correct, we reuse the specification of read_data in Theorem 7 as a lemma. Indeed, this is precisely why we used the noinline attribute when compiling read_data: this allows us to reuse its specification; otherwise each call to read_data would be inlined, preventing us from proof reuse.

In Theorem 8 below, we prove incorrectness specifications for the ${\mathrm{𝑆𝑅}}_{\mathrm{7.50.3}}$, ${\mathrm{𝐶𝑀}}_{\mathrm{7.50.3}}$ and ${\mathrm{𝐶𝑆𝐿}}_{\mathrm{7.50.3}}$ functions, showing that each of these functions do indeed exhibit a double-free vulnerability. Our proof is compositional in that the proof for each function reuses the specification of the function below it, as discussed above (e.g. the proof of ${\mathrm{𝑆𝑅}}_{\mathrm{7.50.3}}$ reuses the incorrectness specification of read_data in Theorem 7 as a lemma).

Theorem 8 demonstrates a scalable proof for the incorrectness specifications of the functions in Figure 11. We can apply similar techniques to verify their corresponding correctness specifications for version 7.51.0; we have elided these proofs as they are similar.