Steel (Outline)

Steel is:

• a "refined" concurrent separation logic

• shallowly embedded within F*'s depend type theory

• with verification condition generation and proofs partially automated by tactics and SMT

• interoperable with Low*, an existing Hoare logic in F* for stateful programs

What is a "refined" concurrent separation logic

At the core of a separation logic, is a Hoare triple of the form

{ P } c { Q }

where P and Q are from an algebra of separation logic assertions.

In Steel's refined CSL, we refine Hoare triples to a quintuple of the form:

{ P | Phi } c { Q | Psi }

where Phi and Psi are classical heap predicates. The quintuple is read:

When owning the resources P an initial state s0 satsifying Phi s0, the computation c diverges or returns a result x and final state s1 that provides resources Q x and satisfies Psi s0 x s1.

The decomposition of pre- and post-conditions into separation logic asserts (P, Q) and classical heap refinements (Phi, Psi), provides a natural way to decompose the construction verification conditions and their proofs. Namely, the separation logic parts are handled by tactics and unification-based type inference; whereas the heap refinements are handled by a classical, weakest precondition calculus and SMT.

In analogy with the refinement type checking, a successful form of SMT-assisted lightweight verification, refined CSL uses a mixture of syntax-directed typechecking, tactics, and inference to achieve a convenient form of specification and verification for concurrent programs with shared state.

Refined CSL allows specifications that have a mixed flavor separation logic and classical Hoare logic, e.g., As a small initial flavor, one can write

{ ptr x | fun x -> s0.[x] <> 0 } x := 1 / !x { ptr x | fun s0 _ s1 -> s1.[x] == 1 / s0.[x] }

i.e., the refinements can refer directly to the initial and final states, avoiding the need for ghost variables or existentials.

We aim to make a case that this hybrid style of specification and verification, mixing separation and classical heap refinments, strikes a good balance between expressiveness and automation.

Three prongs of Steel

1. Semantics

We have a semantics accounting for:

• generic state
• generic algebra of resources
• generic frameable actions
• the frame rule
• the par rule
• specifications indexed both by resources and resource refinement WPs
• value locks
• storable locks

A striking element of the semantics is its simplicity and genericity

• It is built within a dependent type theory by providing a computational model for a free monad structure for stateful, parallel computations.

• By making use of an existing theory of monotonic state, we show how to give a semantics for value-based locks and storable locks, while avoiding technicalities like step-indexing.

• The semantics can be instantiated with many different memory models and flavors of heap assertions, i.e., making it suitable as basis for several varieties of separation logics.

Being shallowly embedded in F*, Steel inherits all the abstraction facilities of the host language, e.g., type abstraction, dependent types, recursive predicates, fixpoints, ...

We provide two instantiations of the semantics:

a. Using a simple flat heap model and separation logic a la Reynolds with connectives including

 - p -pi-> v        Points to assertions with fractional permission pi
 - P * Q
 - P -* Q
 - P \/ Q
 - P /\ Q
 - exists x. P
 - forall x. P

b. We adapt an existing region-based memory model that has already been used extensively in Low* and instantiate our semantics with it. We discuss in Section 4, how this allows us to interoperate between Steel and Low* in a verifiable way.

2. VC generation and solving

Using F*'s effect system, in particular its new support for "layered effects", we package the semantics from (1) into a new computation type in F* embodying the refined CSL quintuple described earlier. The computation type, RCST for "refined concurrent state", has the form:

RCST (result : Type)
     (expects  ( p   : hprop ))
     (provides ( q   : result -> hprop ))
     (requires ( phi : mem p -> prop ))
     (ensures  ( psi : mem p -> result -> mem q -> prop ))

where

• hprop is the type of separation logic assertions,
• mem p is the type of memory that validated p

(Note, internally, this we combine phi and psi into a single WP-index, though we do not surface that to programmers)

RCST computations can be composed using combinators for

• returning pure values
• sequential composition
• branching composition
• parallel composition

with combinators capturing the expected typing rules for each of these constructs. Each combinator is also indexed in a manner that allows computing the weakest precondition of a computation, following (an improvement of) an existing methodology in F* based on Dijkstra monads.

Further, and most importantly, the central frame rule of CSL is also provided in Steel as a combinator. Applications of the frame rule are automated through the use of a tactic that combines a type-inference strategy based on a simple, forward symbolic analysis, combined with a tactic for canonicalizing terms in a commutative monoid.

frame is the main combinator in Steel to manipulate the * connective. We also provide combinators for manipulating the other connectives, e.g., or, exists etc.

Once a program is typechecked, its frames inferred, etc. what's left is a classical verification condition that we feed to an SMT solver for proof.

3. Steel in action

We evaluate Steel's refined CSL by using it to verify several programs of varying complexity.

Swap

Pointers with read/write permissions

Arrays and array splitting with read/write permission

Rust-style mutable borrows with magic wand

Singly linked lists in two styles

• Using exists
• Using explicit witnesses

Doubly linked lists

Schorr-Waite algorithm on graphs

Concurrent merge sort on arrays

Producer-consumers in a concurrent ring buffer

4. Connection to Low*

Being a framework for a variety of separation logics, we instantiate our semantics with Low*'s HyperStack memory model, and show how it can be used to interoperate with existing verified code in Low*.

Our instantiation shows how Low*'s specification style of dynamic frames can be accommodated within a fragment of Steel rCSL.

We evaluate this by verifying the following programs:

• ChaCha20 and Poly1305, a cryptographic algorithms in HACL*, verified in Steel but interoperating with existing Low* libraries.

• A secure file transfer application, programmed and verified in Steel but making use of the verified EverCrypt library in Low* for its cryptographic needs.

• A concurrent TLS terminator application programmed in Steel but built on top of a verified implementation of the TLS-1.3 handshake in Low*.

A work plan

In dependence order (concurrent tasks are given the same label)

a. Settle on a basic instantiation of type of hprops for the semantics, i.e., 1 (a). Express it as a target interface on top of a basic heap like structure.

b. Assume a layered effect for RCST, combinators for return, bind, ..., frame, or, exists, wand, par, locks, etc.

c. Enhance the ParDivWP semantics to provide a model for those assumes

c. Tactics:

• Provide an instance of the canon tactics to run with hprops
• Compile the canon tactics natively so that they run efficiently
• Compile the symbolic execution frame inference to run it efficiently
• Other tactics? E.g., for the other connectives?

d. Start writing some programs from Section 3 and iterate to iron out glitches, potentially revising a, b, c, d.

e. Provide an instance of the heap signature in (a) using HyperStack, building on this summer's work.

e. Write more sample programs from Section 3

e. Consider writing a custom front end to automate some of the tedium from the examples

f. Write sample programs from Section 4