Skip to content

Steel

Jump to bottom Edit New page
Denis Merigoux edited this page Aug 16, 2019 · 1 revision

Steel : a concurrent separation logic framework for scaling up verification in F*

The Steel framework is being implemented on the denismerigoux_steel branch.

Why Steel ?

Verifying Low* programs has turned out to be a quite popular activity across all major F* projects like Evercrypt, miTLS, Everparse, etc. The current memory model augmented with dynamic frames and the theory of modifies clauses allows you to get the work done. However, there are a number of pain points that really limit the scalability of Low*:

  • Because Z3 is pushed to its limits with high --z3rlimit, proofs are flaky and fixing that requires knowing wich lemma to call among the gigantic lemma supermarket of LowStar.Monotonic.Buffer.
  • If you don't want to use specific lemmas, the only solution is to split up functions into small bits and specify each bit separately. However the maximum number of stateful operations that you can put in one function, which seems to be around 8~10, is extremely low.
  • Specifying complex memory invariants, for instance for data structures, is extremely difficult (e.g. doubly-linked lists).

For all of these reasons, we decided to have a more principled way of specifying the shape of the heap and how it changes. That is where Steels arrives.

The concepts

A function specification in Low* usually looks like that:

val swap (x: pointer int) (y: pointer int) : ST unit
  (requires (fun h -> live x h /\ live y h /\ disjoint x y))
  (ensures (fun h0 _ h1 -> 
    modifies (x `loc_union` y) /\
    get h1 x = get h0 y /\ get h1 y = get h0 x
  ))

You can see that this specification has two parts : one describing the shape of the heap with live and modifies, and another describing what happens to the contents of the two pointers. You only need the heap shape part to specify memory safety, the rest concerns functional correctness. The initial goal of Steel was to separate those two parts of the specification, and handle the memory safety part in a automated and reliable way without clogging the SMT.

Resources

For that, we introduced a new way to specify how the heap is organized and how it changes. This new way is based on a new type, resource. resources are only meant to be a specification tool; they are never extracted. However they encapsulate everything you need to know about an object living on the heap:

  • a footprint, which is the loc it corresponds to;
  • an invariant, of type HS.mem -> prop, which should contain things like live that are true for all the lifespan of the object;
  • a view, which is the high-level Tot equivalent of your object (e.g. Seq.seq for arrays).

Resources are specifications that are built upon regular F* values that are passed around inside your programs. For instance if your function has a pointer argument p, then you can talk about the associated resource using ptr_resource p.

Let's try to use resources to describe the state of the heap at the beginning of our swap function. We have two pointers, x and y. The corresponding resources are ptr_resource x and ptr_resource y. However we want to say that x and y are disjoint. Steel has a nice operator for that: <*>. It is the separation logic star, with the same meaning. So here's the description of our heap before the swap function: ptr_resource x <*> ptr_resource y. This description is also valid for the heap after swap, since only the contents of the pointers changed.

The RST effect

Now that we can describe heaps using resources, let's specify functions using that mechanism. For that, just use the RST effect which has 5 indexes:

RST (a: Type) // Return type 
  (pre_resource: resource) // Heap before, decribed with a resource
  (post_resource: a -> resource) // Heap after, described with a resource
  (pre: rmem pre_resource -> prop) // Other preconditions
  (post: rmem pre_resource -> a -> rmem post_resource -> prop) // Other postconditions

Let's immediately take an example with our swap function:

val swap (x: pointer int) (y: pointer int) : RST unit
  (ptr_resource x <*> ptr_resource y)
  (fun _ -> ptr_resource x <*> ptr_resource y)
  (fun h0 -> True)
  (fun h0 _ h1 -> 
    get x h1 = get y h0 /\ get y h1 = get x h0
  )

Why five indexes ? The second and third indexes allows you to specify your function using separation logic, while the fourth and fifth have the same meaning as the old requires and ensures indexes of the ST effect. While you should be at least use separation logic to describe the shape of the heap, you can also encapsulate more information in the resource specification. The hsrefine combinator allows you to define, for instance, a pointer resource pointing to a specific value:

let points_to (#a: Type) (p: pointer a) (v: a) : resource = hsrefine (ptr_resource p) (fun h -> get p h == v)

This system allows you to choose between two styles of specification for your functions, ranging from completely functional to completely stateful.

The frame rule

When implementing functions, each call to a RST function should make clears what is the part of the resource context that is touched, and what part is untouched. For that, we use an equivalent of the frame rule of separation logic. For instance, if your resource context at some point in the function is ptr_resource x <*> ptr_resource y and that you want to allocate a new pointer, you should write:

...
let z = rst_frame 
  (ptr_resource x <*> ptr_resource y)
  (fun z -> ptr_resource x <*> ptr_resource y <*> ptr_resource z)
  (fun _ -> ptr_alloc 0ul)
in
...

By encapsulating all of the RST calls inside rst_frame, Steel is aware of the resource context at each point of the program and can effectively prove memory safety using separation logic.

Permissions

In Steel, the view of your resources also contains a ghost FStar.Real number representing the fractional permission that your resource owns over the heap object. These permissions are set up such that they are strictly positive if the heap object is live, and you need full permission (=1) to modify the contents of the objects on the heap. The libraries provide functions allowing you to manipulate your object's permissions. For instance, here is a simplified example from the array resource library (LowStar.RST.Array):

val share (#a:Type) (b:A.array a) : RST (A.array a)
  (array_resource b)
  (fun b' -> array_resource b <*> array_resource b')
  (fun _ -> True)
  (fun h0 b' h1 ->
    get_rperm b h1 == P.half_permission (get_rperm b h0) /\
    get_rperm b' h1  == P.half_permission (get_rperm b h0) /\
  )

share creates a new, disjoint resource that is a read-only copy of the original resource. Since it halves the permissions of both objects, you will not be able to modify the contents of the arrays. That is why we can consider them disjoint even though they alias the same heap object.

Concurrency

TODO: @afromherz

Usage of Steel

As of August 2019, Steel is only usable by expert users. For instance, you have to write the rst_frame call explicitely each time. Here is a todo-list for reaching a beta stage:

  • Steel: surface-language
  • More fine-tuning of SMT queries
  • Additional libraries
  • Complete interoperation with Low*
  • Concurrency: deadlock prevention
  • Concurrency: complete proof of soundness

Libraries

Here is the architecture of the libraries:

-----------------------  -------------
| LowStar.Permissions |  | FStar.MG2 |
-----------------------  -------------
           ↓               ↓        ↓
           -----------------     --------------------
           | LowStar.Array |     | LowStar.Resource |
           -----------------     --------------------
                   |                       ↓
                   |                ---------------
                   |                | LowStar.RST |
                   |                ---------------
                   ↓                ↓             ↓
                ---------------------     ---------------------
                | LowStar.RST.Array |     | LowStar.RST.Loops |
                ---------------------     ---------------------
                     ↓            ↓
   -----------------------     --------------------------
   | LowStar.RST.Pointer |  →  | LowStar.RST.LinkedList |
   -----------------------     --------------------------

Here is the typical header for a Steel module:

open LowStar.RST
module A = LowStar.RST.Array
module P = LowStar.Permissions
Add a custom footer
Add a custom sidebar
Clone this wiki locally