|
| 1 | +# VeriFast for Rust |
| 2 | + |
| 3 | +[VeriFast](https://github.com/verifast/verifast) is a tool for verifying the |
| 4 | +absence of [undefined |
| 5 | +behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html) |
| 6 | +in single-threaded or multithreaded Rust programs that use `unsafe` blocks, and |
| 7 | +for verifying |
| 8 | +[soundness](https://doc.rust-lang.org/nomicon/working-with-unsafe.html) of Rust |
| 9 | +crates/modules that use `unsafe` blocks. VeriFast performs *modular |
| 10 | +verification*: it verifies one function at a time; during the verification of |
| 11 | +one function, if that function calls another function, VeriFast uses the |
| 12 | +callee's *specification*, not its implementation, to reason about the call. |
| 13 | +VeriFast verifies each function against its specification: it verifies that, if |
| 14 | +started in a state that satisfies the precondition, the function does not have |
| 15 | +undefined behavior and any state in which it returns satisfies the |
| 16 | +postcondition. |
| 17 | + |
| 18 | +Besides requiring that the user annotate each function with a precondition and |
| 19 | +a postcondition, VeriFast also requires that the user annotate each loop with a |
| 20 | +loop invariant. This enables its modular symbolic execution algorithm to |
| 21 | +perform only a single symbolic execution of the loop's body to cover all |
| 22 | +possible real executions of the loop. Furthermore, the use of function |
| 23 | +specifications means a single symbolic execution of a function covers all |
| 24 | +possible real executions, even if the function is recursive. In summary, these |
| 25 | +annotations enable VeriFast to perform unbounded verification (i.e. of |
| 26 | +arbitrarily long, including infinitely long, executions) in finite time. |
| 27 | + |
| 28 | +VeriFast function specifications and loop invariants are expressed in a form of |
| 29 | +[*separation logic*](https://en.wikipedia.org/wiki/Separation_logic), and it |
| 30 | +performs symbolic execution using a separation logic-based representation of |
| 31 | +memory. Separation logic addresses the problem of *aliasing*, which is that in |
| 32 | +programs involving pointers or references, different expressions can denote the |
| 33 | +same variable. By enabling assertions to express exclusive *ownership* of |
| 34 | +memory regions, separation logic enables concise specifications, proper |
| 35 | +information hiding, and efficient verification for pointer-manipulating |
| 36 | +programs. |
| 37 | + |
| 38 | +## Verifying `unsafe` functions |
| 39 | + |
| 40 | +Consider, for example, the function `Node::reverse_in_place` below that reverses the |
| 41 | +given linked list in-place and returns a pointer to the first node (which |
| 42 | +was the originally the last node). |
| 43 | + |
| 44 | +```rust |
| 45 | +struct Node { |
| 46 | + next: *mut Node, |
| 47 | +} |
| 48 | + |
| 49 | +/*@ |
| 50 | +
|
| 51 | +pred Nodes(n: *mut Node; nodes: list<*mut Node>) = |
| 52 | + if n == 0 { |
| 53 | + nodes == nil |
| 54 | + } else { |
| 55 | + (*n).next |-> ?next &*& Nodes(next, ?nodes0) &*& nodes == cons(n, nodes0) |
| 56 | + }; |
| 57 | +
|
| 58 | +@*/ |
| 59 | + |
| 60 | +impl Node { |
| 61 | + |
| 62 | + unsafe fn reverse_in_place(mut n: *mut Node) -> *mut Node |
| 63 | + //@ req Nodes(n, ?nodes); |
| 64 | + //@ ens Nodes(result, reverse(nodes)); |
| 65 | + //@ on_unwind_ens false; |
| 66 | + { |
| 67 | + let mut m = std::ptr::null_mut(); |
| 68 | + loop { |
| 69 | + //@ inv Nodes(n, ?n_nodes) &*& Nodes(m, ?m_nodes) &*& reverse(nodes) == append(reverse(n_nodes), m_nodes); |
| 70 | + //@ open Nodes(n, _); |
| 71 | + if n.is_null() { |
| 72 | + return m; |
| 73 | + } |
| 74 | + let k = (*n).next; |
| 75 | + //@ append_assoc(reverse(tail(n_nodes)), [n], m_nodes); |
| 76 | + (*n).next = m; |
| 77 | + m = n; |
| 78 | + n = k; |
| 79 | + } |
| 80 | + } |
| 81 | + |
| 82 | +} |
| 83 | +``` |
| 84 | + |
| 85 | +VeriFast interprets comments of the form `/*@ ... @*/` or `//@ ...` as VeriFast annotations. This example illustrates four types of annotations: |
| 86 | +- Three *specification clause annotations* specify the function's precondition, postcondition, and unwind postcondition, respectively. The function never unwinds, so its |
| 87 | + unwind postcondition is `false`. |
| 88 | +- The precondition and postcondition are specified in terms of the separation logic predicate `Nodes`, defined in a *ghost declaration annotation*. This predicate |
| 89 | + recursively defines the memory footprint of the linked list starting at a given node `n` and associates it with a mathematical list `nodes` of node locations. |
| 90 | + The separating conjunction `&*&` implies that the first node of the linked list is *separate* from the remainder of the linked list. It follows that mutating the first node does not affect |
| 91 | + the remainder of the linked list. The *variable pattern* `?next` binds logical variable `next` to the value of field `(*n).next`; its scope extends to the end of the assertion. |
| 92 | + If a logical variable is introduced in a precondition, its scope includes the postcondition. |
| 93 | +- At the start of the loop body, a *block annotation* specifies the loop invariant, expressing that `n` and `m` point to disjoint linked lists and expressing the relationship between their contents and that of the original linked list. |
| 94 | +- *Ghost command annotations* provide hints needed for the symbolic execution algorithm to succeed. `open Nodes(n, _)` unfolds the `Nodes` predicate application whose first argument equals `n`. `append_assoc` invokes a library *lemma* expressing the associativity of the `append` operation on mathematical lists. |
| 95 | + |
| 96 | +The generic mathematical datatype `list` is defined in file [`list.rsspec`](https://github.com/verifast/verifast/blob/master/bin/rust/list.rsspec), part of VeriFast's *prelude*, as follows: |
| 97 | +``` |
| 98 | +inductive list<t> = nil | cons(t, list<t>); |
| 99 | +``` |
| 100 | +A list of `t` values is either empty, denoted by *constructor* `nil`, or nonempty, with first element (or *head*) `v` and remainder (or *tail*) `vs`, denoted by `cons(v, vs)`. |
| 101 | + |
| 102 | +Mathematical functions `append` and `reverse` are defined in the same file as follows: |
| 103 | +``` |
| 104 | +fix append<t>(xs: list<t>, ys: list<t>) -> list<t> { |
| 105 | + match xs { |
| 106 | + nil => ys, |
| 107 | + cons(x, xs0) => cons(x, append(xs0, ys)) |
| 108 | + } |
| 109 | +} |
| 110 | +
|
| 111 | +fix reverse<t>(xs: list<t>) -> list<t> { |
| 112 | + match xs { |
| 113 | + nil => nil, |
| 114 | + cons(x, xs0) => append(reverse(xs0), cons(x, nil)) |
| 115 | + } |
| 116 | +} |
| 117 | +``` |
| 118 | +Lemma `append_assoc` is declared (but not proven) in the same file. Here is a proof: |
| 119 | +``` |
| 120 | +lem append_assoc<t>(xs: list<t>, ys: list<t>, zs: list<t>) |
| 121 | + req true; |
| 122 | + ens append(append(xs, ys), zs) == append(xs, append(ys, zs)); |
| 123 | +{ |
| 124 | + match xs { |
| 125 | + nil => {} |
| 126 | + cons(x, xs0) => { |
| 127 | + append_assoc(xs0, ys, zs); |
| 128 | + } |
| 129 | + } |
| 130 | +} |
| 131 | +``` |
| 132 | +A lemma is like a regular Rust function, except that it is declared inside an annotation. VeriFast checks that it has no side effects and that it terminates. |
| 133 | + |
| 134 | +## Verifying safe abstractions |
| 135 | + |
| 136 | +Consider the following broken implementation of [`std::mem::replace`](https://doc.rust-lang.org/std/mem/fn.replace.html): |
| 137 | +```rust |
| 138 | +fn replace<T>(dest: &mut T, src: T) -> T { |
| 139 | + unsafe { |
| 140 | + let result = (dest as *mut T).read(); |
| 141 | + (dest as *mut T).write(src); |
| 142 | + (dest as *mut T).read() // should be `result` |
| 143 | + } |
| 144 | +} |
| 145 | +``` |
| 146 | +The Rust compiler accepts it just fine, but VeriFast complains that it cannot prove that when this function returns, the ownership of the value pointed to by `dest` is *separate* from the ownership of the return value. If we replace the final line by `result`, VeriFast accepts the code. |
| 147 | + |
| 148 | +For a function not marked as `unsafe`, VeriFast generates a specification expressing that the function is *semantically well-typed* per [RustBelt](https://research.ralfj.de/thesis.html)'s definition of what Rust's types mean in separation logic. If no specification clause annotations are provided for the function, VeriFast verifies the function against the generated specification; otherwise, VeriFast first verifies that the provided specification implies the generated one, and then verifies the function against the provided specification. |
| 149 | + |
| 150 | +The generated specification for `replace` is as follows: |
| 151 | +```rust |
| 152 | +fn replace<T>(dest: &mut T, src: T) -> T |
| 153 | +//@ req thread_token(?_t) &*& *dest |-> ?dest0 &*& <T>.own(_t, dest0) &*& <T>.own(_t, src) &*& _t == currentThread; |
| 154 | +//@ ens thread_token(_t) &*& *dest |-> ?dest1 &*& <T>.own(_t, dest1) &*& <T>.own(_t, result); |
| 155 | +``` |
| 156 | +`<T>.own(t, v)` expresses ownership of the T value `v` accessible to thread `t` (in case T is not [Send](https://doc.rust-lang.org/nomicon/send-and-sync.html)). |
| 157 | +`thread_token(t)` represents permission to open *nonatomic invariants* and *nonatomic borrows* at thread `t`; these contain resources shared in a non-thread-safe way at thread `t`. |
| 158 | + |
| 159 | +For more information on how to verify safe abstractions in VeriFast, see the relevant [chapter](https://verifast.github.io/verifast/rust-reference/non-unsafe-funcs.html) in the VeriFast for Rust Reference and the [examples](https://github.com/verifast/verifast/tree/master/tests/rust/safe_abstraction) (in `tests/rust/safe_abstraction` in the VeriFast binary distributions). (See [`testsuite.mysh`](https://github.com/verifast/verifast/blob/master/tests/rust/testsuite.mysh) to learn the command line to use to verify a particular example.) |
| 160 | + |
| 161 | +## Running VeriFast |
| 162 | + |
| 163 | +To run VeriFast, download a binary distribution for your platform, either the |
| 164 | +[nightly build](https://github.com/verifast/verifast/releases/tag/nightly) or |
| 165 | +the [latest named |
| 166 | +release](https://github.com/verifast/verifast/releases/latest). Extract the |
| 167 | +archive to any folder on your computer. (On Macs, first [remove the quarantine |
| 168 | +bit](https://github.com/verifast/verifast?tab=readme-ov-file#binaries).) Then, |
| 169 | +either use the VeriFast IDE at `bin/vfide`, the command-line tool at |
| 170 | +`bin/verifast`, or the [VSCode |
| 171 | +extension](https://marketplace.visualstudio.com/items?itemName=VeriFast.verifast). |
| 172 | +In the IDE, open a file and press F5 to verify it. VeriFast will then either |
| 173 | +report "0 errors found" or show a debugger-like GUI that allows you to step |
| 174 | +through the failed symbolic execution path and inspect the symbolic state at |
| 175 | +each step. If verification succeeds, choose Show execution tree to see the tree |
| 176 | +of symbolic execution paths traversed for each function that was verified. |
| 177 | + |
| 178 | +In the IDE, the Verify menu allows you to postpone dealing with certain |
| 179 | +complexities of the verification task. Specifically, you can tell VeriFast to |
| 180 | +ignore unwind paths, ignore arithmetic overflow, and treat shared reference |
| 181 | +creation like raw pointer creation (which ignores the complexities of Rust's |
| 182 | +[pointer aliasing |
| 183 | +rules](https://marketplace.visualstudio.com/items?itemName=VeriFast.verifast)). |
| 184 | +(Many of the other options are only relevant when verifying C programs and have |
| 185 | +no effect when verifying Rust programs.) All of these options can also be |
| 186 | +specified on the command line. |
0 commit comments