Importance of Natural Resources

Steel: A Concurrent Separation Logic Framework to Scale Up Verification in F*


[MUSIC]>>Thank you-all for coming. I’m really happy to
introduce Aymeric and Denis, who have been here
the last three months. It’s been great fun working with them this summer on many different things. What they’re going to
tell you about today is a new set of libraries in a domain-specific language
in F* called Steel, that we hope to use to scale up
reasoning about state in F*.>>Thanks for the introduction. It’s a pleasure to be here today and present to you the results
of our internship. Many critical systems
nowadays still are implemented in low-level
languages such as C. Think, for instance, of operating
systems of the HTTPS stack. Such systems are really cornerstone
of modern cybersecurity, and because of that the cost
of failure is really high. So there are systems that are a very good target for
formal verification. Unfortunately, verified low-level
programming is still very hard, and one of the biggest
issue comes when we start reasoning about memory and
because especially of aliasing. So in low-level languages, you can have pointers
pointing to arbitrary regions of memory and you have no guarantees that if you
have two different variables, it might not alias. So that means that once you start performing updates
to some variables, you have to reason about
is this other variable, this other value in my context
actually updated as well or not. That means that proving that
some invariants on, let’s say, states or complex memory objects is becoming much harder
to prove as well. All of that is just assuming we
are verifying sequential programs. Once we start thinking
about concurrent programs, it becomes even harder
because suddenly you have several agents that are sharing some memory performing updates
and memory accesses on the same memory and so you have
a lot of interference going on. So over the past few years, several projects have been successful in verifying
low-level programs, and I only want to
mention a few today that were developed as
part of Project Everest. The first one is EverCrypt which is a verified industrial grade
cryptographic provider implemented in F* and which extracts to a mix of C and assembly
code for maximum performance. One of the many really impressive
things about EverCrypt is that its performance beats state-of-the-art unverified
implementation in many cases. The other project I want
to mention is EverParse, which as the name suggests, provides verified parsers
and serializers, and there is ongoing work
to actually integrate the verified EverParse library
into Microsoft’s Hyper-V. So such projects showed that verified low-level
programming was now viable, they total about
100,000 lines of code, they are pretty massive projects, but it still requires
a lot of effort. It requires a lot of
human interaction, human annotation, and it sometimes
feels like climbing a mountain. So why is that report on? So F* is an SMT based tool
for verification, and as many of other SMT based tools, it reasons in memory using Classical Hoare logic and
select/update reasoning. It has many advantages. First of all, it’s fairly general, it’s fairly simple, it’s
nice for pseudo-logic. So it’s very nice to
encode into SMT logic. But it’s also known to
have issues scaling up. So what are the other possibilities? Over the last 20 years, there has been a lot of research into types-based aliasing control systems
in the PL community, and it’s languages such as Cyclone or Vault that have been
developed over past 20 years. These IDEs finally made their way into mainstream languages
such as the Rust language. So Rust is a language that provides you with many fascinating
guarantees such as memory safety and
data-race freedom and all of that by virtue of typing. So what this means
is that if you have a Rust program that type
checks and compiles, you are guaranteed to have memory
safety and data-race freedom. So that’s great because for many people you get all these
properties that’s all we need. But unfortunately, it’s not yet
good enough for critical systems. First of all, Rust programs
are not verified, they are not proven correct, so you have safety, but you don’t have formal functional
correctness, for instance. Second, Rust has this system
called Unsafe Rust that allows you to temporarily escape Rust state
system and it has its uses, it has its reasons but that’s also
defeats the purpose of having all of this nice safety guarantees in Rust as soon as you go
into the unsafe vault. So today, we are presenting Steel which ends up providing ownership and verification via Resource Typing. So Steel is a domain-specific
language which is shallowly embedded into
a text-based programming systems, namely F*, and our target with Steel is really general-purpose
concurrence systems programming. So Steel programs are
ensured to be always safe, and on top of that,
a user can decide how much he or she wants to
verify about the programs. It can run from nothing at all, we just want more safety,
we are fine with that, to full-fledged complex security
and functional properties. As it is shallowly embedded into F*, we can also prove that its core
theory is sound within F* logic. In addition, Steel is very
extensible with new constructs. As it’s implemented in F*, we can just implement and prove some new libraries and
then package them to give them to the user as part
of the Steel framework. So here are the main ideas
and concepts inside of Steel. Steel is designed as the separation logic obstruction
on top of the F* memory model. So we are seeing heap
case as resources, and we provide separation and framing for them in order to do
interference control. We also allowed reason about
permissions on such resources, that is we can either have an exclusive mutable or a shared immutable or read-only
access to resources. Finally, we are aiming at concurrency
and so we want to be able to implement and verify concurrent programs in a simple
fork/join concurrency with locks. So over this internship, we laid the foundations
for this Steel framework, and that means we implemented and proved the core
memory model correct, we implemented a system for resources with separation
permissions framing, and we provided operators to start to implement and verify
concurrent programs. Building upon that, we started
implementing SQL verify library inside of Steels for
both singly and doubly-linked lists. But as a disclaimer, we don’t believe that
this framework is mature yet. There are still are many quirks,
many things we want to solve. Like for instance, it still requires more annotations than we would like. Specification still needs to be formulated in a specific way
for things to work smoothly. So it still requires
a lot of user knowledge. So in a sense, this seminar
was about Steel episode one. We are hoping that after
a few more months of work, we are going to get it all
nice and shiny to give it the bright future it deserves.>>Thanks Aymeric. So now that we know why we’re
doing this Steel framework, we’re going to dive
into the main ideas of the framework and as
you’ll be able to see, they build on each other. So first, we have to start
with the idea of resource. So before in the F*
that we had before, we used to see each
function as taking a whole heap and then
transforming into another heap. But actually, these functions, they operate in a very
small portion of the heap. So we wanted to restrict actually what each individual function
could say about the heap. In order to do that, we first have the concept
of footprints; a resource which is what the
functions are going to talk about, has a footprint which is a heap
fragment and not the whole heap. Then on this footprint we’ve been
through it actually, invariants, which is going to be a consistent assertion
that’s going to be valid across all the heaps. So given those two simple ideas, we can define some
examples of resources. First, you have the anti-resource. The footprint is
just the non-location. There’s no location, no footprint associated to it and
the invariant is always true. With that we have
more interesting resources. We have the pointer resource, the array resource that each point to a single cell in our memory model, and the Invariant is
that they are live, they should be live across all heaps when we want
to talk about them. Live, meaning that
they’re not dereferenced. They’ve been allocated
and not dereferenced. So now, we have the basic blocks
of our resource building. But we can actually say
more rich things about resources. For instance, we can talk
about their contents. This resource says
that pointer p points to value v. The array b points to an array of size two which whose first cell contains a value
which is greater than zero. You can see, you can use
this resource language to actually specify what’s happening
inside a particular heap. So we attach the third component of the resources which is the View, and the View is not as important
and there is the last two. But it’s a high level description of what the contents of the heap
are associated to this resource. So now that we have our resources, we can separate them because
in separation logic, we have this very pervasive operator, which is the star operator
that lets us define the heap as a collection of things that
are just joined to each other. This is the basic block we are going to use to
build our Steel framework. For instance, in separation logic, you would write a heap containing two pointers pointing to
two different values and you can see those pointers are not aliased
because of the star operator. We can see that in our Steel framework using
our research language, when we define a star as like
the footprints are disjoint. So then we can actually have some separation logic inside F*
with this resource language. Let’s define Slist. So here is the single Slist, x, that corresponds to a Slist L, what resources is that? If L is empty, then the resource is
just empty resource, and if L is the head of
the Slist and then the tail, then resource is just the pointer
x should point to the head, stars, meaning not aliased
with the rest of the Slist. So that’s nice. We now have a way to specify fragments of the heap in a fairly logical and it’s what you’re used to if
you use separation logic. Now we have to enforce
that the heap is actually corresponds to
this description of the heap. We do that with resource typing. We actually leverage
F* effect system and define a new computation type
which is called RST. So for a computation of type alpha, we can say that the
computation expects the heap satisfying all
the things described in resource, and provides after
the computation a new resource which is going to describe the heap fragments
after the computation, and you can see here
there’s a function, it’s because the final
resource can depend on the value returned
by the computation. So this is very theoretical. Let’s give some examples right now. What happens when you want
to allocate a pointer? So this is the alloc function. It takes a value and
returns a pointer pointing to this value of this type. So how to specify
that using resources. Well, at the beginning, you just expect nothing. The allocation function
should work anywhere. So you expect empty resource. Then you’re going to
provide the resource, which is going to be pointer
pointing towards your value, and you can see here
we take advantage of the function begins and you can talk in your final resource about the value that’s being
returned by the function. Let’s do another example. Let’s say you want to update
the value inside a pointer. So this is the classical
function, take a pointer, the new value you want to
be the pointer to point to, it’s just equal function
returning unit, it expects the pointer v, we don’t care what’s
the value inside of pointer, but then in the end, we’re going to have a pointer
that points to v. Here we don’t use the unit thing that’s
returned by the function. So now we have a way to specify->>Just some questions
about [inaudible]>>Feel free to ask
[inaudible] But this is->>Can I ask a question? Is
pointer v both a resource and the left-hand side of
this pointer v I think? Does the same expression pointer
v that’s been used in->>So actually here you can see
there’s a difference, and it’s->>It looks like PTR P.>>Yes. So it’s
different for a reason, because as you can see here, pointer alpha is the type of
the actual value of the pointer.>>Got it. I mean the last few lines. Expects PTR P, and provides PTR P RV. So PTR P is a resource
and you put it on the left side of
the little arrow, is that right?>>Okay. So I think
there are three arrows. Sorry for confusing. This is the classical R function->>So there’s PTR P, and PTR P matched to v is
a resource refinement.>>Refinement? Okay.>>So PTR P is just saying
our pointer is live, I don’t know what it points to,
PTR P matched to these is live, and it actually points to v.>>-So if we come
back here we can have the standard pointer resource, and then we can refine this resource saying that the pointer
actually points to v.>>Okay. I can put any resource on the left-hand side
of the map there?>>Yes.>>There’s no interpretation for any kind of resource
that makes sense, or does it depend on
the type of the resource?>>There is a way inside the framework to actually
lets you define that. But it’s called reserve refinement. [inaudible].>>Every resource has a view.>>Okay.>>That’s the value
that’s in the resource.>>Okay.>>I have a question.>>Yes?>>So for these
two functions, so a lot, I guess pointer assignments, so there’s the effects there, but do these functions
happen per rotation?>>Yes, they have. This is just the specification
which is developed.>>Okay.>>The implementation I’m
going to talk about later. So now we can actually specify
what our functions should do in terms of our new nice
separation logic description. Actually, staying on
that specification, if you want to specify things using
a full separation logic style, then if you want to specify the
increment function for a pointer, let’s say you have a
pointer to an int and yet you want to add one to the value, then if you want to specify
it using separation logic, you actually have to say, “Okay. There’s a ghost value”, which is the value contained
inside the pointer, and then you have to say, “Okay. The value after is v plus one.” But this is not the style
in which were used to specify functions in F* historically, because we don’t want to carry these ghost arguments around because you’re actually
extracting to see, so we have to make sure
they erase etc etc, so we actually provide
a hatch to actually use the old style of specification in conjunction with
the separation logic. So let’s say you’re defining
your increment function again, you’re specifying
your increment function again, but then you’re adopting a less precise description
of the resource. Because here you’re only talking
about the shape of the heap. You’re not talking
about the contents. To talk about
the contents you can add another clause in your specification, which is going to be a
traditional ensures clause. An ensures clause is going to
provide you with all the new with which you can access the view of your resources before and
after your computation. So then you can say, “Okay. So the new view of PTR P, which is the value inside
of pointer is equal to the old view of PTR P plus one.” That allows you to have a more state-full specification if you don’t want to carry
this ghost value around. That was a side note. Now, let’s move on to the implementation
of these functions.>>What do you mean, like keywords?>>No. They’re not keywords. In the implementation
they’re just functions. They’re functions that take a
resource which you have in contexts, and return the view to it.>>Then they’re not accessible
from provides, is that right?>>You have a requires clause
that’s symmetrical to ensures. You have expects, provides, and then requiring these ensures. So if ensurers is the
same as provides, and then you have a requires clause
that’s the same as expects.>>So if I wanted to just say
provides and then have a view there, pointer p points to
old pointer p plus one, I can’t say that, right?>>No. You can’t say that.>>Okay.>>You can’t say that. That’s one of the pitfalls of separation
logic specification. You have to actually carry all the values in your program
in the specification.>>But we support both styles. It’s up to you to decide
which you prefer.>>Okay. It’s either the left or
the right, there’s no in-between?>>That’s right.>>Okay.>>You could have bound
a ghost value for some of your pointers but not
for other pointers. There could be a middle ground.>>You could find
the ghost value once they additionally when it happens to be quite often let’s say
zero or something? [inaudible].>>Yeah?>>You can talk about something
that doesn’t exist any more.>>So actually this is going to be fairly technical point but I
can provide you the answer. All the new functions, they’re actually functions that have a restricted domain and you can only apply them to stuff that is
inside your resource contexts. So if for the allocation function, the provides would be the empty heap. So you can apply new
to only things that are contained inside
the empty resource which is nothing. So we guarantee that you can’t talk
about things that don’t exist.>>Okay. Thanks.>>But this might be
a little technical. So let’s move on.>>I have one more. Besides old and new are certainly not the whole heap?>>Yeah.>>We will never let you speak about the contents of the
[inaudible] All your specifications are small footprint.>>If you leave out provides as the assumption that
the research doesn’t change, or where the resource goes away.>>So for now, you always have to include expects in provide closes. So you have to describe
in your provides close. If the resource is in
there, it goes away.>>So provides EMP is that?>>Yeah. Okay. Let’s move on to implementing
these functions which we were in the process of specifying. So the way you implement
and prove memory CFC about your functions in separation logic is that
you use the frame rule. The frame rule says that if you
have a function from Q to R, then you can apply it to some
P star Q and it is going to give you a P star R. P is going
to be untouched by the function. The neat thing is that we can actually express that rule
as a Steel function, a special function
that’s going to take the initial and final
resource contexts, the function Q and R, and it’s just going to
return your computation with the right resource contexts. So with that function and
actually this is like the workhorse of Steel because
all of your function goals, they should be encapsulated
inside the frame rule so that for each stateful
operation on the heap, you know precisely which part is modified and which part is untouched. That’s what allows us to have modularity when reasoning
about the heap. But the frame rule, in encoding all of
that inside the F* and reaching a level of Domitian
in usability for the user, it has been challenging. For instance, if say you have some
P star Q star R in the context, and that you have a
function which just works on Q and returns a Q prime, then what you want is you
want to actually select the Q inside and then
performing computation, then recompose the things together. But actually, you have
to prove all the steps. So first, you have
to rewrite this term using associativity
and commutativity, isolate the Q, apply the frame rule, apply F, then recompose via always still the frame
rule your Q prime, and then actually rewrite the term again as you
have your Q prime here. All of these steps
have to be proven and the way to do that with
SMT is that you take this term and you explore
the context with all of the possible rewritings
of that in hope that in order to apply that, you select the correct form. This is not very efficient. The second problem is that we’re going higher-order
with these coming years because before if the updates
selects heap model, we just had the first-order terms
which we could feed to the SMT. But then, since our resource
are heap predicates, the star which takes
two resources and return a resource is actually
higher-order because these types, they hide some functions inside them. So these verification conditions that are stemming from
the specification using separation logic are not going
to compose all of the SMT. So the classic way to solve verification conditions not manually for a starter just to
feed them with SMT. But since 2017, we have tactics and we have in
something called Meta-F*. So what we’re actually
going to do is that we will be crafting
tactics to solve all of the verification conditions tied
to our separation logics and specification framework
and the rest we are going to feed to SMT as before. It’s using that mix of
tactic in SMT that we can reach a level of usability and niceness for the user
in the framework. So this is the first concept of seal and we have something
that lets you specify function using
separation logic and proof that they respect that
specification using the frame rule. But now as [inaudible] mentions, we want to be able to
talk about ownership. What if you want to share data across different actors or something? Right now, with the stuff
that was already presented, all the function they
require exclusive ownership. If you remember the update pointer
which I have shown you earlier, here having the pointer peak
resource in the context, when you call it, means that you have exclusive ownership
over that pointer. It is the case because you can’t duplicate resources in your context, because the context is a
list of disjoint resources. So if you have two pointers
you’re using to the same thing, they can be disjoint from each other. But what if we only wanted to read P? Then we have a read-only P and R contexts and then
the type checker should disallow these updates mechanisms. Well, we can actually do that. It’s the classic extension
to separation logic. We can define read-only resources, read-only R and the
read-write resources. Then for instance our pointer, the reference specification which takes a pointer and returns
the value inside it, just expects the
read-only resource and provides the read-only resource
pointing to v. Here, we know that because the read-only, the contents haven’t been modified. Okay. So how do we produce
these read-only resources? We have a rule for that, the share rule which takes a pointer and will
return another pointer. So it expects the first pointer
to be read-write, and then it’s going to return
another pointer which is going to be the immutable copy
of the first pointer. You can see that in the final heap, the two pointers are disjoint using our separation logic framework,
although they’re alias. So in that way, we can control precisely what’s the
aliasing that can be done. So this classical extension
to separation logic usually comes with the way we have multiple read-only copies
of the resource, but then we want to gather them back and recover full
permission in some points. Usually, separation logics
include some scoped allocation, the allocation mechanism
for having some read-only and then gathering
them back in the end. But we said, we have SMT so why
not go more general than that? So we actually implemented
fractional permissions. We just said, okay. So you have a resource in the heap. It says a permission like
a fraction between zero and one. One meaning that you
have full permission. So then the gather rule is that
you just have two pointers. They’re these joint,
but have permission F. Then when you gather them back, you just have a single pointer with the sum of
the permissions of both. The other pointer is
not in the context. Meaning that you can’t
talk about it anymore. It’s not live anymore. You can’t access this. It’s gone. Of course you can do
that with every pointer. They’re have to be alias
to the same thing for you to be able to do that. So the nice thing about
this extension is that it stays within the trusted
computing base and a memory model because
we actually implement those permissions as a ghost value is stored somewhere inside the heap. All the permissions, when you manipulate permissions
inside the Steel framework, everything is statically
checked and you have to account for
all the permission things. But we can do that because we have SMT that’s going to
ease us with this task. Actually, if you don’t want to use fractional permission because
it’s too complicated and if your needs are something much simpler like scoped allocation
of reasonable resource, then you can define it as a verify library on top of
the existing framework, and that allows us to define
more restrict patterns of permission usage while
staying in some world. Now, for the next main idea, I’m going to hand over.>>I have a question about
the fractional permission.>>Yeah.>>You just said PTRP. Does that have like
a default permission on it?>>PTRP if you want to say anything, it has permission one.>>Okay. So we’ve got full access.>>Yeah, yeah. Full access.>>The last main concept of Steel
is how do we handle concurrency? How do we implement and
verify concurrent programs?>>Off-target here is, we want to prove that
our programs are free. We’re going to assume that we are in a sequentially
consistent model. We are focusing especially on
simple concurrency model which is a simple scope full-joint model
with a par combinator. And we’re going to be sharing
mutable memory using locks. So how does this work? Steel is very heavily inspired
from separation logic and separation logic has
a standard extension called concurrent separation logic
to handle concurrency. The idea being, if you
have two functions, F and G but walk on
different heap fragments. You can just execute
them in parallel, assuming the front heap fragments
are actually separated. So in other words, what this means
is if you have two functions that operate on these joints
separated regions of memory, it is safe to fork, execute them in parallel, wait until it terminates,
and then join again to resume the execution
of the main program. So that’s something that is very
easily expressible in Steel. We can just define
this par combinator that takes executive as two functions and assuming they actually
operates on separated resources. We can execute them
in parallel safely. That’s a model that is
already fairly expressive. For instance, if you think
about a match salt on lists. The way match salt works is
you speed for this somewhere. You take two sublists, you salt them recursively, and then you melt again at the end. So that’s something that is very
parallelizable because you can just salt your two
sublists in parallel. That’s something that can be
captured with power because there’s two sublists
are actually disjoined. Similarly in our contexts, when we have different immutable
pointers of two resources, we are considering that
we are separated as well. So using this par combinator, we can also share
immutable resources across agents. But what happens if we actually
want to share mutable memory? One of the classic example is
this consumer producer model where basically you have two agents that
are sharing one data structure, usually your Q, and one of
the agent is feeding the Q, the one is emptying the Q. Basically they are
both performing updates and reads on the same data
structure in parallel. So how does this work? Lucky for us, concurrence separation logic also has a solution which is based on locks. So the idea is if we have a heap predicate P
initialing in our context. We can take a lock that is associated to this
specific heap predicates. Once this heap region is locked
after creating the lock, it’s not available anymore
because we cannot access it before actually
acquiring the lock. So because of that, we have
this acquire and release functions that take a specific lock and
say well if I acquire the lock, I now have whistles in my context
meaning I can operate on this. I can access it. I can
update it and conversely, what this would say we are
not releasing the lock. We don’t have access
personally to these whistles anymore but other people will
be allowed to access the lock. One of the many very
interesting things here is this resource is not
just a memory object. It’s also comes for
heap predicate with an invariance and this invariance
will be insured for by locks. So the idea is whenever
we acquire a lock, we also acquire the heap invariant
which associate it for lock. Then that means we can do whatever
we want with the resource. Then when we release it, we will need again to prove that
this invariant is satisfied and that is safe because whenever
we have a lock nobody else, no other agent can actually
access a resource, not even read from the results. So in a sense we don’t
need to preserve the invariant between
the acquisition and release. We only need to prove
that it’s preserved again when we’ve release the lock and allow other agents to access the lock. So again in Steel, this is fairly
straightforward to specify. We can just for instance have this acquire function that
takes a lock on a resource. It doesn’t need anything
at the beginning and gives you the results back. So all of these invariance, they are checked
statically again using a [inaudible] since we are
doing a verification. But the availability of
flux is checked at runtime. We have blocking semantics
meaning if you tried to acquire a lock and the lock is
already owned by somebody else. You’re just going to wait until
this lock becomes available. So that also means
that at the moment,, kids, we are not trying
to prevent deadlocks. It might be the case
that you are waiting for a lock but will never be released and so your program will block. Yes.>>So P is a predicate. It’s thought to be a predicate then.>>Here on the left is a predicate
in separation logic and it’s equivalent to this R which is
the resource in our [inaudible].>>So let’s say I acquire
a lock, predicate ma, and execute a function that allocate new cells that happen to
satisfy the predicate. Those new cells also compiles
that part of resource.>>No, because this new cells will be about
a different heap fragment. So in a sense, it’s
not just a predicate. It’s a heap fragment with a predicate on
this specific heat fragment. So if you just allocate new cell, it will be in a different
heap fragment and hence you will have
a different resource.>>Then how do we handle cases
where you acquire a lock that connects to the link
list allocating elements to the link list that should
be protected by the same?>>Yes.>>You can do that so
you can have a resource for a linked list that
says this captures a abstract location in
memory that is potentially unbounded but it’s reachable
from say the head of the list. You can allocate and say cons
add to the tail of list, let’s say, and then package it
back a the same resources before.>>So for concurrency, all of the operators we have currently don’t have
any implementation. Because of that to ensure
that we still have all of the safety properties
velocity programs, we need to provide
a proof of soundness of a concurrency model and
that’s something that we are still working on but it’s
still a work in progress. But still basically I just want to give
a general idea of this proof. So we are working in
a sequential model which means that we’re
going to consider that functions are a list of atomic instructions being
either operations and lock, acquired over the list or
updates or reads from memory. So we have two functions
here, F and G, that have a list of
atomic operations and they operate on separated resources
and they have some lock memory. So basically what we want
to prove is that for any possible interleaving of base atomic operations
that is non-blocking, then we still have this
specification that is admissible. That is assuming we have
this initial stat resources. In the end, we indeed get
these stat resources. That’s something that we are
actually formalizing and proving in [inaudible] This is not a proven paper but that is
still a work in progress. So building upon this, I want to spend a bit
of time just presenting what we can actually do
with the Steel framework. One of the best examples of that is, how do you implement linked lists. Linked lists are a fairly dynamic structure with
a lot of aliasing, and because of that,
that’s a nice example to showcase what
our framework can do. So as we presented previously, it’s pretty straightforward
and it’s really to define what our list resource is. It’s just, you have a pointer and if a pointer
points to an empty list, you actually don’t have
anything, you have empty heap. If it does not, if it
points to a non-empty list, you have the head pointer that points to the head of a list, and then, recursively, you have
the next pointer that points to with
the rest of the the list. So this is a nice, clean, concise specification, four lines to encapsulate all of
the invariants about your list. Using that, you can reduce signature for
the usual operations on list. For instance, appending an element
at the beginning of a list. So here, what we are saying is, if you have a pointer to cell that is separated from a pointer to a list, we can just append this element
at the head of a list. What you get in the end
is a pointer to the whole list where
the element was appended. Similarly, we can
define a map operation, where we are saying, again, we have a pointer to a list, initially. We have a function
that will operate on the cells of these lists,
and, in the end, what we get is the same list where the F function was applied to
all of the cells of a list. So in comparison, this is what
it looks like in Low-star, which is the current DSL for doing a lot of the
[inaudible] in F*. Just the specification
of what is a valid list, takes about 20 lines in F*, and I omitted this for
brevity, but, basically, it’s saying we have
this invariant and then we have to define exactly what
the heap fragments is. It’s much more complex defined. Then for instance, defining the same function
up-end, or rather, cons, takes a lot more work because we have to specify carefully
all of the invariants, we have to specify
exactly what is modified. I don’t want to go
too much into detail, but if you look on the left, it looks much cleaner and nicer
than what’s on the right. So because of that, in
the current status of Steel, we are providing: cons, heap, tail, and map,
primitive for list. Their specification takes
about 30 lines of code in Steel, it takes about a 100
lines in Low-star. That’s just for specification. Once you start looking at
the implementation, it becomes much, much worse because implementation in Steel is going to be very straightforward, as
I’ll show in a minute, while implementation in Low-star, which involve a lot of [inaudible] to reason again about
aliasing and things like. So what does this implementation
actually look like in Steel? I just want to show a very small excerpt of how
map function actually works. This is the recursive case
of a map function, where you are first applying the
function to the head of a list, and then recursively applying
map to update up a list. So here, what we are
seeing is that we need to apply this framework of
separation logic to do that, because when we were first
updating the head of a list, the rest of the list
should remain untouched. Similarly, when we are
updating the tail of a list, the head of a list
should remain untouched. That’s still a limitation
of a framework, which is, we have to apply
this frame rule explicitly. We have to give exactly what
is the context initially, and at the end of the execution
of each function. We would much rather have
something simple as that, which is, well, I want
to apply function, I am applying a function. That’s all I need to
know. The framework should take care of
all of that for us. That’s a fairly tricky problem. It requires a lot of engineering
and language design, and we are working on having
a better frame inference and perhaps some syntax that would do
that automatically for the user. So the last example, I want to quickly mention
is doubly-linked lists. Over the last few days, Nick implemented doubly-linked
lists in Steel. He implemented a few of them, like going primitive, such
as allocating a list, concatenating to doubly-linked lists, appending an element at
the beginning or at the tail. Doing that for the whole specification,
implementation, and proof, took about 400 lines of code, and it took Nick a few hours
of work do that. In comparison, there is
a doubly-linked list in Low-star, which is slightly more complex. But this library, to specify
all of the invariant and especially to prove all of
the implementations correct, with respect to aliasing, takes thousands of lines of code. So it seems to suggest that Steel is much more adapted to
these complex aliasing problems, and it also seems to be making
for proofs that are both faster and more robust for
the existing [inaudible] framework. So in comparison- yes.>>How many of those 400 lines
are for this framing?>>Quite a few. So it’s really even nicer once
a framework is mature. So that’s like the current status
and it’s, hopefully, should be even better once we
are actually in a few moments.>>I should say one thing. We
were writing these applications, the [inaudible] , but
the tactics are solving, are still doing
all the AC rewrittings. I just assert
what resource have right now and what resource I
expect to get afterwards, and the tactic does the rest. So it’s still manageable.>>So you need these manual
limitations, but in a sense, I don’t think you need any external
[inaudible] to prove anything. While the doubly-linked
list library that currently exists in Low-star is full
of such [inaudible] , to reason about aliasing and
what’s modifying and whatnot. One of the interesting part is, this doubly-linked list structure, that’s actually something that
is not expressible in safe REST. The reason for that is
that RESTs safe type system has some restriction on aliasing. Especially, it is restricted to
unaliased tree-shaped structure. So doubly-linked lists aliasing is
too complex for recurrent REST. You need to implement it in the unsafe world if you
want to do it in REST.>>So your answer to dealing with
unsafe flux is to not have any? Is to not need them, not to be able to deal with them?>>At the moment, we
think we don’t need them. I just took in a minute
about what could possibly be a way to
dealing with unsafe flux. So otherwise, in terms with
what do we have left to do, we still think that for
this framework to be mature, we need a few more months
of work in order to be comfortable with
unleashing users. The biggest item is we want to
make this framework more usable. I hinted at some things,
for instance, this frame rule that we
have to apply explicitly. We have some ideas perhaps doing a front-end syntax to hide
some of the gory details, make it easier for the user
to use the framework. That’s really a lot of
language design work to do that. We also want to make sure that we are fine-tuning as much as we can, the queries that are
passed to SMT servers, so that we have
some nice attractions, but we don’t want to leak
accidentally some things that’s are not needed by the SMT
server and might just confuse it. If we want to have a comprehensive framework that allows you to verify a lot
of that programming, we also probably need
more basic libraries. We currently have
a fairly comprehensive library for buff pointer on arrays, and basic ones for lists
and doubly-linked lists. We probably may need some more like based data
structures and so on. Additionally, one of the thing
we really want to do is have a nice and complete operation
with the existing Low-star, which is, again, this framework to do a lot of the programming
in F* at the moment. The reason for that is
that, first of all, we have many fascinating projects, such as EverCrypt or EverParse that are currently
implemented in No star. We would really like
to build upon them, not just throw them away because
we are changing the framework. So we need a way to be
able to build upon them, to preserve all the guarantees, and to have all of these
that operates smoothly. The second reason is that, possibly, you could almost see
unsafe flux as a form of C, and Low-star can be pretty
adapted to some forms of C. So it has to be possible if you really want to
break out of the guarantees, to verify the equivalent of very unsafe flux into
Low-star and it to operates. So that’s also something
we are thinking about. We are not sure exactly what
the need would be. So that’s all the future. The last item we have left is also to actually wrap up
this concurrency model. So first of all, there exists technique to
statically prevent deadlocks. We want to see if we could apply
them to a framework and also see if the framework still remains efficient
and scalable this way. We also need to complete our proof of some [inaudible] to ensure that the everything remains safe and nice. So to conclude, over the summer, we finally gave F* it’s long
awaited star, which is great. What took so long?
Well, separation logic. If you just have SMT
solving it’s not working. It’s not scalable, it’s
too hard to specify, it has other logic. It just doesn’t work. So first of all, we had
to wait for F* to have this tactics framework that allows you to reason about
these kind of things. But, there have also been pretty attempts at doing
separation logic of tactics. If you just use pure tactics,
it becomes tedious. For instance, there was
a previous implementation with tactics of appending to linked lists, and it took about a 100 lines
of manually applying that. It was very tedious, it was just not so
nice to program with. So what really worked with us this summer was
the nice combination, the great combination of
tactics, and SMT solving, with the right
abstractions, including, resource typing, to make it
work and to make it scale. Building upon that, we have many fascinating applications
that could be targeted, and we can finally go
beyond crypto verification. So first one is, if we can verify concurrent programs, we might be able to verify concurrent network protocols, such as QUIC. The other one is, if we can actually
scale up to bigger systems, we might just be able to verify critical system components
in, let’s say, Azure. So if there is some work
with a Hyper-V people, we might be able to verify some passive Hyper-V or
some passive Azure CCF. We might also have many possible
synergies for our projects. In morally, we are fairly
close to what REST is doing. So maybe we could be able to verify
REST programs inside of Steel, and we actually want to
see if we can design a front-end language to verify REST programs directly inside Steel. There’s also this
Verona language that is developed current here at
Microsoft Research Cambridge, which basically does
ownership-based systems programming. It would be interesting
to see if we can perhaps verify some of its components
inside of Steel and have a nice collaboration with people so that we can have a more
comprehensive tool, in a sense. We would like to take
some time to give our sincere thanks to
both Nick and Jonathan, our adviser over the summer, for all of the help and
advice they provided. We’d like to thank
also Tahina and Daniel for the help they’ve
provided with both the F*, [inaudible] and VM F* framework,
and also, more generally, to all of Project REST members
and VMSR committee for many fun and interesting discussions
for the summer. Thank you.>>Do you have time for questions?>>So the [inaudible] only that he has a specialized solvers
for separation [inaudible] based on rewriting things won’t
[inaudible] something that would fit with your check to [inaudible].>>What exactly just-.>>So his claim is that as you do the symbolic
execution [inaudible]. It’s an advantage to know
what is the necessarily equal and you can simplify
terms drastically [inaudible]. Default isn’t [inaudible] or interface doesn’t give
you that information.>>So I guess it’s maybe somewhat
similar to what we are doing. But one of the nice parts about
this framework at least to apply to F* is we don’t need to extend
it with any additional solver. In a sense we are purely
using what comes to exists. We have a tactics framework in F*
that already exist on the three [inaudible] and we
already have an encoding of F* verification conditions
into the three.>>[inaudible]. So if you are only using the encoding
as we can see [inaudible]>>Yeah.>>[inaudible].>>That’s correct.>>[inaudible].>>That’s correct. Solve it
[inaudible] is really discharge [inaudible] verification
conditions for the three inside of a tactics. So doing all of these
associative and committed or writing with tactics by
manipulating [inaudible].>>So what happens under
the who it is that you have this associativity and
commutative operator which is Star, which we do is we normalize both
terms of both sides of the equal. Inside we have a tactic
to normalize in terms. And then we compare
the normalized form. That’s how we managed to do this.>>As a fast field [inaudible].>>Yeah.>>Yes.>>So I think he takes
it one step further.>>Okay.>>So to just [inaudible]. Maybe you can do that once
the tactics is [inaudible].>>Okay. We’ll look into that then.>>Other questions?>>So what’s the [inaudible]?>>Could generation [inaudible]?>>Yeah.>>So the plan is seemed to
reuse the existing pipeline. So various currently a compiler
from [inaudible] existing DSL to C. So the idea is we are defining still as an abstraction of
the existing [inaudible]. So since it’s just an abstraction
once we try to extract, we want to just reuse
existing code and there might be some minor changes to do but
that’s the general idea.>>That actually extracts pretty
well with like existing KreMLin. The only downside is
that for permissions. Let’s say you want to share data, but the way we prove that it’s inside of the memory model is that we have to look in the heap to see what are the permissions
and update them. So it’s going to extract to
like a read and update but you don’t think you don’t
do anything with the value of the [inaudible]
because it [inaudible]. So we need to remove that because
it’s unnecessary in performance.>>Yes. It’s extracted
to see [inaudible]>>Yeah.>>The model of locks you have, can you store them in the heap?>>Sorry. Can you what?>>Can you store
your lock pointers in the heap?>>So that’s something that we
didn’t completely sort out yet. The whole [inaudible] model
is still a work in progress. But I think that’s
what we’re aiming for.>>Your locks are just values so you can store them in the heap but you can’t- but logs do not
have lifetime of their own. You can’t reclaim a lot.>>Right. But we do not burn into like step indexing hell
with your semantics. If you go down the street
if you’re not careful.>>Maybe. We refer,
we should talk more.>>Yeah. [inaudible] if you want.>>Okay.>>[inaudible] something
some sort of shared state. You can’t just pass it around. You can’t just pass [inaudible]
in the locker room as about you.>>No. Yeah. It’s a ref. [inaudible] a ref.>>Okay.>>I have a question
about your frame rule. Almost syntactically you were using
your P star Q as an variable?>>Yeah.>>What was that? Cheating
or we have that syntax?>>So it’s was presentation cheating. A lot of the work that still remains to be done with
the framework is actually making sure that you can use the frame rule of
that syntactic sharing because basically I’m going to show
back the rollback again. Yeah.>>It binds P and Q separately
not binding P star Q.>>Yeah. Know that the thing is
that when you use it currently, you actually feeds its P star
Q and then it resolves P because it looks at- because it
knows Q and R from the function, it knows P star Q and P star R.
So the remaining thing is that you have to- okay. Let me- okay. So you know Q and R
from the function. You know P star Q and
P star R. So what you don’t know is P.
In the actual there is a tactic that to like find P from P star Q and P star R
because you know Q and R. So that’s cheating, but it’s solve by a tactic actually.>>So to answer your question. No. We don’t actually write P star Q. We write it like auto
zero and auto one. Then, inferring the actual P is
done automatically [inaudible]. We’d be happy to send you
some quick pointers if you want to look on your [inaudible].>>Couple of minutes for
more questions if any.>>So does that mean you got to have precision on your formula
here in separation logic? Or what about disjunction?
I guess is the question.>>We don’t have disjunction.>>Okay.>>Started only Operator [inaudible].>>Yes. Combining resources, yes.>>All right. Let’s
thank, Aymeric and Denis.


Reader Comments

  1. When you are genetically deficit, then there are more bio-molecular and metabolic holes and tears in nervous system

    that can be compounded upon further, to affect physcial performance and materialized results of whole peoples.

    Who did not sufficiently bolster fat and other forms of stored energy (via gorging when resources were abundant, including during periods of sacking and looting of other cultures,

    that results in certain peoples caught in negative spirals, that are being compounded further by digital economy proponents (systems builders and operators)

    Forcing drilling and training to score behavioral grooves onto nervous system, that human robots can then chug away at –

    called an education (worth less and less these days

    After they have been trained by teachers and programers, more positioned to play the part of masters, than slaves?

    Roles directly handed down by Gurus and headmasters across the ages

    Gotta go to school? But first have to get past the gauntlet of wolves, and snipers who take potshots from hidden crevices

    to keep traditional networks in tact, by way of tearing down at targets who raise "red flags" sometimes as simple as preferring indigenous foods over burgers and fries

    Where local organizations are actually funded , to perform this self mutilation, so the hand full of dummy bodies can stay in power

    And the world can turn into a single bordello, with the almighty A.I. as brothel madame. While sex workers call themselves students and teaching aids

    AIDS to teach peoples a lesson, about misplaced loyalties and too much running around. Now just stay at home and get your mouse to do it for you?

    Take me to your leader! It has a whole lot to answer for. Will it prove to be just another Bullet head, with someones name written on it?

    From Ghandi, to JFK, MLK to Robert Deniro in Taxi Driver! Fictionalizing Facts to prove that it was all play pretend

    So that everyone gets off!

Leave a Reply

Your email address will not be published. Required fields are marked *