(light music)
- Let's say you're building a simple piece of software,
like an arithmetic calculator.
The way people build it today
is that they implement a piece of software
that's got the functionality of a calculator,
and then they have a separate team of people
who either manually or using automated tools,
feed this calculator a bunch of inputs.
And they try this for some time
and check that you get the right results.
They have some confidence
that this calculator is working correctly,
and then typically you just ship it.
But if you really want the assurance
that this calculator is going to answer correctly
on all possible inputs,
this is not a way to get that level of assurance
because the space of potential inputs to this calculator
is astronomically large.
And if you're trying to build a piece of software
for a domain where getting things right is really important,
for instance if there're human lives at stake
or if the financial cost of an error
is really, really large, you may want a degree of certainty
that is greater than what can be given to you by testing.
And in this kind of domain, what we advocate
is to approach the problem of developing software
similarly to how you would approach the problem
with proving theorems in mathematics.
So, let's say you want some certainty about Pythagoras's theorem.
We certainly don't go around drawing a bunch of triangles,
right triangles and doing measurements
and checking if Pythagoras's theorem is true.
You can conclude that Pythagoras's theorem is true
about any right triangle
without ever drawing any single right triangle.
So, this is what we want to do with software.
We want to give you assurance about a piece of software,
that it correctly computes its results,
or it never leaks secrets, or it never crashes.
We want to give them, these assurances,
to you mathematically as theorems
without ever needing to actually run your software.
So that's what high assurance software is about.
My name's Nikhil Swamy, I'm a researcher at the RiSE group
in Microsoft Research, Redmond.
RiSE is a team that's been working on various aspects
of software engineering and programming languages
and high assurance software for several decades.
In the last five years or so,
we have a project called Project Everest
that involves researchers
from multiple Microsoft research labs,
as well as several academic institutions,
where we're looking at building tools and techniques
that allow you to prove software correct
and secure at scale.
This endeavor of trying to build formally verified software
has been a goal
of many computer scientists for several decades.
But in the last, say 10 to 15 years,
the community has made a lot of progress in building tools
that scale to verifying and
doing proofs about nontrivial pieces of software.
So, for instance, as part of Project Everest,
every day, multiple times a day,
every time we push to our repository,
we are doing formal proofs about a code base
that is currently greater than about 600,000 lines of code.
This is a scale at which maybe even just 5, 10 years ago,
this was unthinkable
that you could get software verification to scale
to this extent.
What I'm showing you here is a demo
in a programming language called F* (F Star).
So, F* is the main programming language
in Project Everest.
It's a language that me and others have been developing
for the last, almost a decade at this point.
And it's a programming language that allows you
to write programs and proofs together,
proofs about the programs that you're writing
intertwined with the programs themselves.
So, here's a demo where it's going to show you
how you can use F* to write a program,
to copy one array of bytes to another.
This is my first attempt, I have
a function called copy0 (copy zero).
It takes two arguments, source and dest,
which are buffers of bytes.
And I'm going to try to copy a byte,
just for starters, just one byte from source to dest.
And it's complaining here.
It gives me a squiggle over the zero
saying, "Hey, something's wrong here."
And if I go and look at the error that it's pointing me to,
it's saying I'm trying to index a buffer, an array,
and it's unable to prove that the value that I gave it,
the index that I gave it at that point
is within bounds with that array.
So, this is a common problem that happens
when you're trying to write low-level code,
that you may be indexing arrays out of bounds.
And every time you do that, an out of bounds array access
can lead to essentially a buffer overflow
and can lead to a number of correctness
and security problems.
So, F* notices this and says, something's wrong here,
you may have a buffer overflow, try again.
So, here's my second attempt.
I'm going to protect my access of this buffer
with a runtime check
to show that zero is strictly less
than the length of the buffer.
Meaning the buffer has to have
at least one element if I'm going to read it's zero.
So, here again, I've got a complaint saying,
well, it's now pointing to the dot
and it says, something's wrong here.
And if I go and see what's wrong here,
it's saying, well, I was unable to prove
that when you're trying to index this buffer
that this buffer is actually currently live.
So, what this is trying to say is that,
maybe in this particular context,
you're trying to read from a buffer
and read from a piece of memory that has already been freed.
And this is going to protect against errors,
like use after free, which can also be both a correctness
and a security concern.
So, here's my third attempt at copying one byte,
this time I have a precondition,
I've enhanced my specification,
and this is kind of where F* is somehow a bit unique.
You can write these specifications that say,
in order to call this function copy2,
the caller must prove that the source
and the destination buffers are live in the initial state
when calling this program with this procedure.
And as a result, once you call this procedure,
this procedure promises
that it will only modify the destination buffer.
And if I do this, F* is happy
and the whole thing highlighted in this light blue color,
which says that F* has successfully verified
this piece of code.
So, this was just copying one byte.
What I want to do of course
is to copy the entire buffer over from source to dest.
And to do that, I can, for instance,
write a recursive procedure, copy3,
that is going to iterate over the buffer
from the current position to len.
And it's going to, at each stage,
copy the current byte, and then recurse.
And I can do this and F* is happy about this.
It says, this is also safe to run under this precondition,
that both the source and the dest buffer are live.
But I would like to do more than just prove it's safe,
I would actually like to prove
that this piece of code is correct.
So, this is my final attempt at proving this.
And here, what I've done is to say,
well, in addition to proving
that the source and dest buffers are live,
the caller needs to prove
that the source and dest buffer do not overlap.
And if I add that as a precondition,
then I've struck an indeed proof that this function ends
by modifying only the destination buffer
and ensuring that the source and destination buffers
are equal all the way from zero to their len,
which is my intention of writing.
Now that I've written this piece of code in F*
and proven it correct, I can now say, let's start to compile it.
And you can ask F* to compile this thing to C,
and what you get out of it is, here's copy4 in C.
All the specifications
that we wrote about it in F* have gone,
they don't impose any runtime cost.
What I get in C is what you would expect, and sometimes
you get a straight transcription
of the computational content of this procedure
that's just doing a check of the iteration
to make sure that the current position is still in bounds.
A copy of one byte, and then a recursive call
to copy the remaining bytes.
So, that's a really simple demo,
trying to show you
how you can prove a piece of code correct in F*
and get out of it a C code,
but you don't pay any runtime cost
for the verification that you did at the source level.
We use F* at scale to verify
a number of large systems ranging from things
like verifying cryptography in the Linux kernel
to even third party companies,
financial technology companies
using F* to write their core trading
and specification algorithms.
So, as you saw, perhaps from my demo of memcopy,
doing these kinds of proofs in F*
can actually be quite challenging.
So, one thing we've been doing recently
is focusing on specific domains
where we can give you automation
so that we can do proofs almost entirely automatically
without the user having to intervene at all.
And one such domain
which we think is really important, is parsing.
So, it's often the case that when you're writing a program,
the program has to receive some inputs
that can be controlled by an adversary.
So, what's really important in this kind of system
is to ensure that when you're receiving untrusted inputs,
that you correctly validate and parse those inputs.
We have a tool called EverParse.
That is a tool that allows you
to generate formally verified parsers
from input formats that are specified declaratively
in a syntax that resembles the syntax
of C data type structures and unions.
And let me give you a little bit of a demo of that.
So, here's a data format, a classic data format,
the format of TCP headers.
The interesting thing about this format,
it has a number of variable length structures in it,
and parsing these variable length structures
can actually be quite hard,
even for something as classic as TCP headers.
For instance, for code that's been in the Linux TCP IP stack
for 20 years or more,
memory safety bugs have been found and patched
as recently as 2019 in parsing of TCP options.
So, making sure that you get parsers
for these kinds of variable length formats,
making sure that you get it correctly is an important task
and EverParse can help you with that.
So, the way you can specify this message format in EverParse
is by using a language of C structures and unions.
So, here's a struct for the TCP header
in EverParse's input language.
And it allow you to... it's an enhancement of C structures
where you can parametrize the instructors
with semantic constraints and parameters
that describe the caller's environment.
So, the caller can say, "I expect a TCP segment
to fit in a buffer whose length is segment length,
and that buffer must contain these structures in it,
a source port, a destination port, and so on,
which look just like C structure definitions."
But what EverParse lets you do
is to augment these definitions with semantic constraints.
For instance, that the data offset
must point to some regional memory
that follows the TCP options
that are at the end of this project.
And the options themselves are a variable length array
whose size is described by some arithmetic expression
that's computed from the data offset in scope.
So, you write a declarative spec like this
about your data format,
and then you push a button,
you ask EverParse to say, compile this TCP.3d file.
3d is the input language of EverParse.
And what EverParse does is, it translates a TCP.3d to F*,
does a proof in F*, and then from it
produces a piece of C code whose signature looks like this.
It's a function called TCP check header,
where if you give it a pointer to an array of bytes,
starting at base and containing at least len bytes,
it will check that there is a well formatted TCP header
whose length fits in this parameter,
in segment length, in that byte.
And we have a formal proof
that if this function returns true,
then in fact you have a valid TCP header
stored in those bytes.
And in all other cases it will return false.
And that's a mathematical theorem about this piece of code.
So, once you get this piece of code,
which you didn't have to do any proof about it,
all the proofs were done automatically,
what's left for you to do is to integrate this one call
that can validate the TCP header
into your existing C program.
And we've been using this inside Microsoft,
in particular, inside Hyper-V
and in the network virtualization components.
So, input validation is a really big problem
in software today.
By some counts, it's the third most common
software security vulnerability
and it plagues software of all flavors, in some sense.
We develop our code in the open on GitHub,
including F*, EverParse, and have
a high assurance crypto library.
We have lots of papers about our work in several blog posts,
including a recent one about applying EverParse to Hyper-V.
Do check it out and get in touch.
We'd love to hear from you.