[MUSIC]
>> Next up, I sat down with
a few Microsoft engineering researchers to learn
how software engineering research
accelerates how we develop our services at Microsoft,
and how you can use these tools yourself. Take a look.
>> Software engineering research plays
an important role in how the tools we use to build
software are created and it can have
a major impact on the future of programming.
Today, I'm joined by three software engineers,
all from Microsoft Research, Pantazis, Patrice,
and Nick, to talk about some of the projects they're
working on that will impact the future of testing,
debugging, and even securing software.
I'm going to start with you, Pantazis.
Now you're working on something called Project Coyote and
this is making the process of
doing concurrency testing easier.
Can you tell us a little bit about Project Coyote?
>> Yeah, of course. Thank you.
Basically, concurrency bugs are hard to catch,
but can cause serious issues
if they manifest in production.
Today, most developers write unit and stress tests.
But this can be flaky in the presence of
concurrency because each time you run the test,
it can produce different results.
Coyote help suppress exactly this problem.
It is an open-source tool for
unit testing concurrency subcode.
It allows you to test, for example,
what happens when your service receives
two requests at the same time.
Another cool thing is that Coyote takes full control of
your program's concurrent execution
and can run the test again and again,
providing very high co-variates of
concurrent behaviors that you could not otherwise get.
Coyote can also fully reproduce any bug that it finds.
Today, several teams in Azure
are using Coyote for testing their services.
They have reported higher coding velocity
and much fewer bugs in production.
For some of them, it has
redefined the way they think about testing.
Now that Coyote is open source,
we hope that everyone finds it helpful.
You can just download it as a NuGet package in
your sub-project and you're good to go.
We also have a website hosted on
GitHub with a lot of documentation,
tutorials, and samples to help you get started.
>> I love it, that's so cool.
People can go to the GitHub link, they can get started,
they can start to run this
on their own code and it'll help
make the process of doing
these concurrency tests much more efficient.
>> Exactly, yes.
Basically what was happening is that traditionally
today developers have been
using techniques such as stress-testing.
These techniques, they often left
a program to run for a very long time,
and this really relies on pure luck for
the conditions to be right and the bug to happen.
Even if you know techniques
like stress testing to find the bug,
how do you really debug it?
You don't have the ability to reproduce it,
which makes debugging frustrating and time-consuming.
We're trying to solve this with Coyote.
Basically, you can focus back on unit testing.
Because Coyote uses intelligent exploration strategies
to find these concurrency bugs,
you can even do that in very
simple scenarios with us giving,
for example, two concurrent requests.
You don't need to write or to spawn thousands of them.
Instead, you can just write simple test,
and you get fully producable test which
makes debugging so much easier.
>> We've got a link on
the screen for people to go to learn more.
It is open-source. Pantazis, thank
you so much. This is so cool.
I'm going to move over to Patrice
who has been working on a project that
will make it easier to test Cloud services and APIs.
This is known as Project RESTler.
Patrice, talk to me a little
bit about what Project RESTler is.
RESTler is a testing tool to find bugs in Cloud services.
Most Cloud services are
accessible through so-called REST APIs,
and most REST APIs are described as
specification languages such as the open API format.
RESTler is a tool that takes
as input REST API specification
in the open API format and then it
automatically generates and executes test from
that specification in order to find
bugs in the Cloud services behind that API.
With RESTler, you do not need a test suite
or prerecorded API traffic to start.
RESTler automatically generate API traffic from
scratch directly from an open API specification.
Then it will automatically generate lots of requests,
some well-formed requests and
some badly formed requests in order to
try to trigger bugs in
the Cloud services behind these APIs.
That's what fuzzing means.
It means to take well-formed requests and slightly
modifying them with noise in order
to see if the service under test can handle these errors.
With RESTler we found hundreds of bugs
in Microsoft Cloud Services and in open source services.
>> When we were talking earlier,
you told me RESTler has been used
internally at Microsoft for quite some time,
but you open sourced it six months ago.
What can you tell me about
the feedback that you've received
since it went open source?
>> Yes. The feedback has been great.
There's lot of interest out there.
Just to give you an idea,
we started the project RESTler about
four years ago inside Microsoft Research.
About two years ago we had
a workable prototype that we
started to deploy inside Microsoft.
We found lots of bugs,
it was very successful.
Then we published some research papers.
Then we decided to open source it because we had
lots of requests from outside
Microsoft asking us, "Oh, that's great.
But could we have access to this tool because we are
developing our own Cloud services outside Microsoft,
on top of Azure, etc.,
and it would be great if we
could have access to that tool."
That's why we decided to open source
RESTler about six months ago.
It's available on GitHub and
I invite everyone to give it a try.
>> That link's on
the screen for people to go check that out.
But you should definitely check this out,
especially if you're using something that uses
the open API standard and you're using Azure services.
We're talking about testing,
but sometimes the surface area
of the large codebase can make that,
frankly, impossible to find all the bugs.
What if we could guarantee that the code
that we write is what it says it is?
This is the basic idea,
I think, behind Project Everest.
I'm going over to Nick now to talk to us
about Project Everest and
what it means. How are you, Nick?
>> Great, Christina. Yeah, you got it
right. Thanks for these questions.
While testing software is really important,
there are scenarios where you want
higher assurance than what testing can give you.
For example, where human lives are at stake or where
the cost of a bug is just unacceptable.
In Project Everest, what we've been
looking at is how to prove
mathematically the software is bug-free by construction.
Now, you may have
heard about software verification before
and it's always been thought
of as being a bit futuristic.
But we made a lot of progress,
and now in several domains,
ranging from things like cryptographic protocols to
virtualization components that are
used to secure the Azure platform,
we can actually and we are deploying code
that is formally proven to be correct and secure.
>> When you're actually writing the code,
you're getting that assurance that this is secure.
It is what it says it is.
Or when you're receiving, I guess,
a piece of information that it
is what it says that it is; is that correct?
>> That's right. Yeah. We have
a new programming language called
F* that supports something
that we call proof-oriented programming.
It allows you to write a program together with
the proof that the program
does what you intend for it to do.
That proof is mathematically
checked as it's a theorem about your code.
For instance, in Hyper-V,
in its network virtualization components,
we're using a tool called EverParse
built on top of F*.
EverParse is a code generator that
produces formally proven parsers for
binary formats
from a class of binary formats where you can
specify these formats declaratively and
EverParse will generate proven code for you.
What we've been doing is taking the code
that EverParse produces and integrating it
with the network virtualization components
to ensure that every network packet that passes through
the system is first validated by
this piece of formally proven code to ensure,
for instance, that a whole class of bugs due to
improper input validation are
just ruled out by construction.
>> We've got a link where people can get
more information about this. This is so cool.
I could talk to all three of
you about the research you're
doing for hours, frankly. I would love to sometime.
Nick, Patrice, Pantazis,
thank you so much for joining me.
All three of you have also been participating in
a video series that Microsoft Research
is doing called Tech Minutes.
We actually have a little bit of
a sneak peek. Check this out.
>> We had to actually rethink the entire AI stack.
>> What is reinforcement learning?
Let's look at an interactive demo.
>> Online code is now open source.
[MUSIC]