Today, advanced logics are often formulated as variations on the theme of
“higher-order concurrent separation
logic.” One of these, Verifiable C, is the
foundation of Appel’s Verified Software
Toolchain,
1 and includes an expressive
higher-order logic supporting recursive
predicates. Iris29 encompasses reasoning about fine-grained concurrency and
even relaxed memory, based on different instantiations of a single generic
model. Iris has been used to provide
a foundation of the type system of the
Rust programming language,
28 which
is very natural when you consider that
ownership transfer is one of the central
ideas in Rust.
Technically, these works are based on
“non-standard models” of SL, different
from the heaplet model but instances of
Pym’s resource semantics as in Figure
2; see Pym et al.
36 There are many such
models, including ones incorporating
read and other permissions,
7 auxiliary
state,
39 time,
39 protocols,
29 and others.
Abstract SL13 showed how general program logic could be defined based on
these models, and the works just mentioned and others showed that some of
them had surprising ramifications.
Fictional separation and views
worked to reimagine fundamental concepts. The programs being proven go
beyond the loosely connected processes
that CSL was originally designed for.
Significant new theoretical insights and
soundness arguments were needed to
justify the program-proof rules supporting the fine-grained concurrency examples.
17 This led to a flowering of interest
and new ideas which is still in progress.
A recent survey on CSL provides many
more references in addition to those
mentioned here.
9
Directions in
Mechanized Reasoning
SL spawned new approaches to verification tools. In order to provide a taste
of where the field has gone, we present
a sampling of practical achievements;
that is, we focus on the end points rather than the (important) advancements
along the way that helped get there.
Further references to the literature, including discussion on intermediate advances, may be found in the appendix
( https://bit.ly/2CQD9CU).
Mostly automatic verification. Small-
foot,
2 from Calcagno, Berdine, and
O’Hearn, was the first SL verification
tool. Given procedure pre/post specs,
loop invariants and invariants governing
lock usage, Smallfoot attempts to con-
struct a proof. For the pointer-transfer-
ring buffer, given a buffer invariant and
pre/post specs for put and get it can
verify memory safety and race freedom.
Smallfoot used a decidable fragment
of SL dubbed “symbolic heap,” formu-lae of the form B ∧ H where H is a separating conjunction of heap facts and B
is a Boolean assertion over non-heap
data. The format was chosen to make
in-place symbolic execution efficient.
Smallfoot’s heap facts were restricted
to points-to assertions, linked lists and
trees. Subsequent works extended symbolic heaps in numerous directions,
covering more inductive definitions as
well as arrays and arithmetic; see appendix ( https://bit.ly/2CQD9CU).
Some of the most substantial automatic verifications done with SL have
been carried out with the VeriFast tool of
Jacobs and colleagues. VeriFast employs
a symbolic execution engine like Smallfoot, but integrates a dedicated SL theorem prover with a classical SMT solver
for non-heap data. A paper reports on
the verification of several industrial case
studies, including Java Card programs
and device drivers written in C;
35 see VeriFast’s GitHub site for these and many
other examples ( https://github.com/
verifast/verifast).
Interactive verification. In an automatic verifier like Smallfoot, the proof
construction is automatic, given the
pre/post annotations plus invariants.
In interactive verification the human
helps guide the proof search, commonly using a proof assistant such
as Coq, HOL4, or Isabelle. Interactive
verification can often prove stronger
properties than automatic verifiers,
but the cost is higher.
Interactive verifiers have been used
to prove small, intricate algorithms. A
recent paper reports on the verification
of low-level concurrent algorithms including a CAS-lock, a ticketed lock, a GC
allocator, and a non-blocking stack.
39 An
emphasis is placed on reusability; for instance, the stack uses the GC allocator,
which in turn uses a lock, but the stack
uses the spec of the allocator and the
allocator uses the spec rather than the
implementation of a lock.
The verifiable C logic1 has been
used to prove crypto code. For example,
OpenSSL’s HMAC authentication code,
comprising 134 lines of C, was proven
using 2,832 lines of Coq.
4
A larger example is the FSCQ file system.
14 The code and the proof are both
done in Coq, taking up 31k lines of
proof+code. This compares to 3k lines of
C for a related unverified file system. Although the initial effort, which included
development of a program logic framework in Coq, took several person years,
experiments show incremental, lower
cost when modifying code+proof.
A commercial example concerns
key modules of a preemptive OS kernel, the μC/OS-II.
41 Modules verified
include the scheduler, interrupt handlers, and message queues. 1.3k lines
of C were proven using 216k lines of
Coq. It took four person years to develop the framework, one-person year
to prove the first module, and then the
remaining modules, around 900 lines
of C, took six person-months.
Automatic program analysis. With a
verification-oriented program analysis
the annotations that a human would
supply to a mostly automatic verifier
like Smallfoot—invariants and pre/post
specs—are inferred. A tool will be able
to prove weaker properties when the human is not supplying annotations, but
can more easily be deployed broadly to
many programmers.
Program analysis with SL has received a great deal of attention. At first,
analysis was formulated for simple
linked lists,
20 and progressively researchers moved on to more involved
data structures. A practical high point
in this line of work was the verification
of pointer safety in Linux and Windows device drivers up to 10k LOC by
the SpaceInvader program analyzer.
43
SpaceInvader was an academic tool;
its sibling, SLAyer,
3 developed in parallel at Microsoft, was used internally
to find 10s of memory safety errors in
Windows device drivers. SpaceInvader
and SLAyer were able to analyze complex, linear data structures: for example, oneWindows driver manipulated
five-cyclic doubly linked lists sharing a
common header node, three of which
had acyclic sublists.
Like much research in verification-oriented program analysis these techniques worked in a whole-program
fashion: you start from main() or