Coming up next, we've got a talk on ADA,
exploitation in the era of formal verification,
a peek at a new frontier with AdaCore Spark.
So please help me welcome to the stage, Alex and Adam.
Hello everyone, and welcome to the presentation
in the exploitation in the area of formal verification,
a peek at the new frontier with AdaCore Spark.
Some folks already approached us and asked
what is this picture here?
What you can see, the answer is pretty dumb
because there is no logic behind that.
It's just kind of visualization that in the,
any kind of the software, you might have a wrong path,
correct path, failed path, and some of the path
are just correctly, could be correctly verified.
Some of the path is just wrong or undefined behavior.
This picture looks cool, that's why we decided to use it,
but don't find any meanings here because there is not.
If you find, let me know, I'll be happy to listen.
So I don't wanna spend too much time on this slide.
My name is Adam Zabrotski, and together with Alex,
we have been doing some security research for some time
already, for a few decades to be honest.
And yeah, there is some private contact to us,
some short bio to us, and this research has been done
during our work at Nvidia.
Both of us work at Nvidia currently.
So yes, apparently this research which we're going
to present is not only the result of our, both of our,
work, but entire offensive security research team,
which I'm currently leading.
And big kudos also to Jared, Max, and Nikola,
which also are involved in this research.
And before we also move to the formal verification problem,
especially in the software, we need to speak a bit more
about software vulnerabilities, because this is what
the formal verified method's supposed to address.
And you cannot speak about the software vulnerabilities
without touching the problem of memory safety.
So just quick intro about memory safety, what it is,
and what is memory safety.
It's apparently a term used by security engineers
to describe a state of being protected from various bugs
related to memory access.
And of course there's a bunch of bugs who falls into
this category, including every type of overflow,
some memory, like on the stack, on the heap, on the global,
every piece of the memory which can be overflowed,
and kind of out of band read and write,
and invalid page, including null port of reference,
and kind of use after free, use after return,
use after scope, et cetera.
There's many types of use after bugs.
Also, any type of unutilized memory,
including wild pointers, or memory leaks, invalid free,
all of that, it's a memory safety issue.
But not all of the security vulnerabilities
are memory safety issues.
So some of them, like any type of the overflows,
integer overflows, arithmetic overflows,
are not memory safety issues.
Logical issues is also not memory safety issue.
Error handling race condition, there's a star,
because race condition on data access is type
of the memory safety issue, but in general it's not.
And there's a few more, but what is worth to mention
that even this is not a memory safety issues,
they often result in a memory safety issues.
So if you have any kind of integer overflow on the size
of how much data you want to copy,
it's not memory safety issues,
but when you start to copy the data,
then you will have a memory safety issue.
So why we even speak about memory safety,
because apparently memory safety errors
are today the biggest attack surface.
And I really mean it, it's the biggest software
type of the bugs.
And there's a few reasons behind that.
Some of them are easy to spot, like this one,
memory unsafe language has been chosen to use
to develop a core of the execution environment,
so every type of the operating system,
like Windows, Linux, Macintosh, are written
in memory unsafe language, like CRC++.
And the question is why?
Because at that time when this ecosystem has been developed,
we already have memory safe language,
which could give us opportunity to not have these bugs,
but we still develop them in the memory safe language.
There's a few reasons behind that, some of them,
because at that time, the hardware was not performed
as well as today, that was much slower,
and the code in the memory unsafe language was faster,
and also it gives developers a fine-grained control
over the memory address, where the code can be executed
with the attributes, and this is one of the reasons
why memory safe was chosen to develop these ecosystems.
Also, memory safety bugs are very well researched,
as everybody knows.
Some professional exploiters even developed
the exploitation framework to target
exploitative software stack.
I've seen by myself reverse engineers, one of the frameworks,
developed to exploit Windows kernel vulnerabilities.
You have a full framework, you just find the bug,
and expose primitive, like read, write,
and include into the framework,
and the entire exploitation process magically runs.
It bypasses a , it bypasses any modern mitigation,
so you just find the bug, plug in the framework,
run, and it's done.
So it's a very well researched idea,
and traditionally, memory researchers do automation
on focusing for memory safety bug detection.
They don't even need to understand what the software does.
We just take an open source project,
you recompile this with the various
code coverage instrumentation,
then you spin up code coverage-driven fuzzers,
and you just run it, and you have bugs.
And apparently, it's kind of not rare
that some researchers, they just pick up
most popular libraries without going into details
to analyze what the architecture it is.
Well, let's just fuzz it, let's find the bug,
and we have benefits, yes?
So it's not also a theory, because a big corporation
starting to struggle with this problem
more and more, and they can't ignore it anymore,
and they want to study a few cases,
and the biggest corporation who produce software
is apparently Microsoft.
And they also face this problem for ages,
and they make a few presentation about that,
which I want to recap here.
So in 2002, Microsoft created something
called trustworthy computing, TWC,
where they wanted to, they cannot ignore anymore
the security issues in their ecosystem,
because larger customers, like government agencies,
financial companies, starting to be impacted
by the security problems on the Windows,
and this is Microsoft products, so they cannot ignore it,
and they needed to do something on that.
So they created TWC, and they focused on the few areas,
and one of them was security,
and as the pillars of this initiative,
and they developed, as a direct indication of that,
a few interesting things, like TWC developed SDLC,
security development life cycles process,
to be able to make the quality of the code higher
from the beginning.
They also created MSLC,
which is Microsoft Security Response Center,
which treated security bugs differently than other bugs,
so they also know that this is something
which can impact the security of the ecosystem,
so they are also starting to fuzz by themselves
some of the software, they are also starting
to do bug hunting, they are also starting
to do exploit research, so they do a lot
of interesting stuff, and traditionally, in 2019,
they said, okay, we spent so much engineered effort,
we spent so much money on that, do we see improvements?
Do we see any benefits of all of that?
And in 2019, they analyzed the last 12 years
of all of the security cases reported to them,
and that's what they saw.
So this is slide from Microsoft itself.
As you can see, the type of the security bugs
which are reported to them are more or less
the same over the time.
In the 2006, around 70% of all of the security issues
was memory safety issues, and 2018,
we still see 70% of memory safety issues.
So does it mean nothing changes over the time?
Even of this years of investment?
It's not obviously because these slides show what changes so we see that the type of the memory safety issues
Which are reported are differently so in the beginning 2006 we see the quarter of the bugs are stuck over for vulnerabilities
While in the 2014 there is almost zero of them and the reason is not because this bug disappear
It just doesn't give a benefits for the attacker because the modern mitigation makes the exploitation of this bug sometimes impossible or very hard
But in the same time they saw the rise of other type of issues like use after free
This is this great
Box here. You can see the huge rise of them because there's no any mitigations on that
So it's much trivial to exploit and then they introduce mitigation and you can see that the amount of the bugs are shrinking
And now we can see there is a rise on the edge of this year
You can see the rise of yellow which is type of the confusion because there is no mitigation
So people move to that type of the attack so something changes but overall
70% of the bugs are memory safety issues and
Google case let's speak about that because it's slightly different
They wanted to avoid
The problem which Microsoft sets instead of patching bad software with adding new security layers
They wanted to make something differently so they design the Google Chrome in the security in mind
They have a high code quality
They constantly fast that since 2015 because they knew the bugs will be there
They wanted to catch them in-house as soon as possible and you know Google has power
So they fuzz it in the various platform. They use OSS fast platform
They use Google cloud platform, which essentially means they have essentially unlimited computer power
They also have dedicated team to improve virus mitigations and in 2020 they did exactly the same job
They analyzed all of the security issues
Since 2015 when they starting to fuzz what were reported to them with the high and critical severity and guess what happened
They end up in exactly the same place even they took different approach
roughly 70% of the bugs are memory safety issues and
half of these bugs are used after feedbacks and
Even more they knew that this box will be there
so they designed the google chrome in such a case that these bugs will be there they knew this they
heavily sandbox them and they make a warranty that one of the bugs is not enough to take over
of the host machine although this is a quote from their blog but we are reaching the limits
of sandboxing and site isolation and yeah that's pretty concerning and what about open source world
is open source world is different than corporation world and there's not many research in this area
although we found one interesting research done by universe technical university in darmstadt in
germany continental ag and intel apps which summarize it as we find no clear evidence that
the vulnerability rate of widely used software decreases over the time even in the popular stable
releases the fixings of the bugs does not seem to reduce the rate of the newly identified vulnerabilities
so it's not much better i guess so are we doomed is memory safety something who will be for
with us forever
that we cannot fix anything so apparently no people trying to approach this problem because
we understand it much more and we have various ways how to try to address that we have a new
mitigation push to the hardware like memory tagging who are physically in the hardware
trying to stop the memory safety issues from being exploited or even happens before it happens
at first time that's the memory tagging idea we also have ideas of creating a new architecture
of the memory like cherry architecture cherry architecture treats different in memory
so it's also will be redesigned the hardware and there is a different approach different path let's
rewrite all of our software in the formally verified languages or use the language which
has static method of proving that the memory safety doesn't exist so we have rust and people
starting to write the program in the rust but we have also the formal methods which is even stronger
which can formally prove that there is absence of memory safety issues and
there is absence of undefined behavior so past formal verification you must to be safe
and one of the language which gives the which is the most advanced of giving the
attributes of the former verified software is apparently at the core spark where alex
will speak more about now yeah let's revisit a few key points from our presentation last year
spark is a subset of other core language uh it's basically a programming language formally defined
including a set of analysis tools and this the real strength of this uh comes from this analysis
these are not proven at stack and a few more so uh one of the key features is that it's statically
provable and the proof is produced by this uh gnat proof tool so you have to run it after you
compile build your code so what can you achieve with this formal proof so this this tool can prove
that that the action can be done even if you want to do it let's see that
using the feature of the gnat proof tool
use the feature of the gnat proof tool
and check the data
and we're going to take a look at the gnat proof tool
and then we're going to check the data
You can just omit them, the compiler may omit them
and do not build.
That may give you some performance benefits.
Also, it can prove that there may not be runtime error.
So, everything runs in a well-defined state.
You will not have any errors that arise in runtime.
And you will have hard proofs, like formal verify.
So, also, AdaCore Spark is memory-safe language, like Rust,
but it also has a very strong typing system,
which is much stronger than Rust.
So, for example, you will not have arithmetic overflows,
integer overflows, or stuff like that.
And because of this, it traditionally is used in industries
such as automotive, IOT, Spark is safety-certified.
So, NVIDIA constantly use that
for build safety-certified code.
So, the key point is that you can build buggy code,
but the problems are detected by the tools used.
You really have to run them to see,
to actually verify that your code doesn't have any problems.
And tools are orthogonal to each other.
You have to run all of these tools,
because they detect different kinds of problems.
So, when we first approached the project written in Spark,
we thought about this attack surface that we can use.
So, obviously, no memory corruption bugs are there anymore
because it is memory safety language.
So, also, there are no pointers.
So, problems with pointers do not apply to Spark.
But, since 2019, Spark has a feature.
So, it's introduced the concept of pointers,
pretty much like Rust Borrow checking.
So, what about arithmetic security?
So, we have very strong typing systems.
So, that's why arithmetic issues also don't apply.
Our project was single-threaded,
so we didn't care about parallel execution,
but if you do care about it,
there is extension to Spark called ravenscar which we can use.
So, what is left is attack surface.
These are logic bugs and bad design.
Obviously, if you prove wrong things,
you can have correct proofs about wrong assumptions,
and you will have bugs in this case.
Yes, so, everything what Alex said, it's compelling.
It sounds compelling.
Apparently, you can have a buggy code.
You just must run all of the tools.
If you don't run them, you still have a bugs.
And the tools are orthogonal to itself,
so you must run all of them.
If you just pick some of them,
you will not have all of these benefits.
And most of the potential security issues
must be in the design issues or in the logical errors.
And bugs also can be introduced by the compiler itself,
which we can see later on this slide.
So, everything sounds very good.
Very compelling and pretty interesting, but benefits.
Do we really see benefits in the software
written in Spark or any formal verified language
compared to non-Spark code in memory and safe language?
And apparently, before we go there,
I just want to quickly say that what our team does,
because we did this evaluation,
so just to give you overview why we think
we are the good guys to do this comparison,
we essentially work as a third-party company
inside of the company.
We just take a product after they pass all of the checkbox,
and they said, okay, ship it.
It's secure.
Then we said, no, don't ship it.
Let's review something which is the most critical
and can input components.
So that's what we do.
And we, since 2020, we analyzed 17 very high product,
impact products, which it's not a small feature.
It's a huge product.
And 10 of them used the software written
in memory and safe language.
And four of them had the software written in Spark.
And what is important, that four of this project
was fully written in Spark.
There was not even a single line of code to read it.
It was written in the non-formally verified language.
And two of them was written in Spark,
and the Spark was the imposer and enforcer
of the security warranties of the software,
while inside there could be still software
written in the memory and safe language,
but they didn't change the security warranties
of the entire ecosystem, so it's fine to have it there.
So we get a closer look on them,
and we wanted to compare, do we really see the benefits?
And so first question, how do we compare them?
How do you compare them as an Apple to Apple,
not Apple to anything else, and have some kind
of bad impression about the quality of that?
So it's difficult, so what we did,
we just put the raw data of all of the project
which we reviewed.
We choose the one which could be compared.
We sort them out by the time frame of the review
which we spent analyzing the software.
We also put what is the total bug counts,
what is the percentage of the memory safety issue,
and what is the type of the software which we review.
And by sorting by the type,
we could be able somehow to compare,
because if the type of the software is the same,
we can more or less compare how do they behave
with the formal verified language.
So first project in Spark could be also,
not could, does not apply to this comparison,
because it's focused on the hardware modeling,
and we have nothing in the memory unsafe language
to compare with, so it was out of scope.
So we left with the free project in Spark
which you can compare.
So let's look at the first one.
This is operating system like software,
which we fully developed in Spark in the formal proof,
this operating system like software.
And also, we have in the memory unsafe language
another type of the software, also internally developed,
which was developed in C and C++.
And as you can see, we spent three weeks
in the memory unsafe language for the reviewing,
and six weeks, which is twice as long on Spark.
But we found only five, 10 bugs in Spark
while we spent twice as long
as reviewing the memory unsafe language.
And in the memory unsafe language,
we found 45 total bug counts.
It's a huge difference.
Additionally, as you can see,
there is almost 52% of the bugs,
53% of the bugs are memory safety issues
in the memory unsafe language, while in Spark, it's zero.
And another software, which is also good to compare,
is the Project Ford, the last project in the Spark,
which is a boot software, also written in Spark,
and we spent almost the same amount of the time
of reviewing as booting software
in the memory unsafe language.
And apparently, memory unsafe language boot software
was not written by us, not written by Nvidia,
it was written by an external company,
although it was using the Nvidia product,
so that's why we reviewed it.
And as you can see, we found around five bugs in the Spark,
and 17 bugs in the memory unsafe language.
Again, a huge difference.
If you look at the percentage of the memory safety,
it matches the industry standard,
65% are memory safety issue in memory safe language,
and zero percent in Spark.
The last project is pretty difficult, let's say,
because it's kind of hybrid project combining two different
other software.
It's a boot, it's a root of trust software,
and additionally, there is a functionality
of being resource management software.
And apparently in the memory unsafe language,
we have had two separate projects
doing exactly the same functionality.
So two of these project in the memory unsafe
combined together gives more or less the same functionality
and the same code size of the software written in Spark.
So we spend more or less the same amount of the time frame,
four weeks plus less than two weeks,
and five weeks in Spark, so more or less the same timeframe.
We found around four bugs.
40 bucks in the memory and safe language,
and 28 bucks in Spark.
Again, big benefits.
And so, in the recap, that's a conclusion
based on this average data.
Formally verified software can be free
from the memory safety problem.
There is a star, as you can see later.
There is still some room for abuse,
but in general, yes, it can be memory safe.
Formally verified software has much higher quality
because Spark apparently enforces a lot of attributes
like secure and strict coding practice,
strong typing system.
You need to correctly utilize any data,
otherwise before you use it,
you will be like killed by the compiler.
You cannot use it.
And also, what is worth to mention,
Spark is not a silver bullet.
You just see that you can apply
and all of your problem disappear.
It's a pretty heavy software, programming language,
so you cannot just sit down and write a code
like in the sea.
You write a function, you write another function, no.
You must be really sit down, think about the software,
design it properly, map any object,
and then when you have that,
then you can start writing,
starting to compile it,
compile them together, and then write the software.
So you need to keep this in mind.
Additionally, Spark can prove
that there is no dynamic checks cannot fail.
There is something called absent of runtime errors,
and depends on your level of assurance,
you might have warranty they will never appear,
so these checks might not be in the binary
because you don't need them anymore.
Also, it enables much more efficient security efforts
because at first, you will not see dummy bugs there
like we sometimes see in the memory safe software,
and something which is not verified or unprovable
is very clearly marked with the attributes,
so you just focus on this function,
what is unproved and what is unverified,
and focus there.
And there is also something called
speak condition, post condition, ghost code.
I don't want to go into details on that,
but essentially, you can clearly define the state
of the software in that specific point of time,
so you know what to expect from the software
and how to behave.
You just read that stuff,
and you know what is the purpose
of the specific software state machine.
And what also is worth to mention,
is that you don't have to worry about,
is that most of the bugs which we found in Spark
requires apparently very deep knowledge
and understanding of the software,
so in the end of the day,
the bugs which we found are very deep type of the bugs.
We have architecture issues, design issues,
and if you look from the statistical perspective,
when we do review the product in the memory safe language,
on average, in four weeks, we found around 40, 50 bugs,
while in Spark, we spent six weeks,
which is longer on average,
we found around five, 10 bugs,
which you can see there is a benefits
which you can see internally in our company.
So what is the real bugs?
What are the example of the bugs
which we are speaking about here?
So yeah, formal verified software can produce you
the software which is very strong,
but there is always but.
So let's look at this but in the Spark.
So first problem is a problem with the signature verification
which we found in one of the project.
So there was a function who calls,
let's say, verify public key,
and this verify public key has a specific checks.
If the software is configured to verify the signature,
then it's a bug.
Then it verifies the signature.
So what is this route of trust
for this functional verify signature?
Let's take closer look,
and you can see that this function get authentication
has apparently three states.
It's a state authentication known,
authentication RSA,
but there is also state authentication unknown.
But the function verify public key
never takes into account this third state.
So is this state even possible to appear?
Because if you have authentication RSA,
everything is fine.
Authentication known,
we don't need to verify, so it's okay.
What about authentication unknown?
And apparently the route of trust of authentication unknown,
it's coming from the register and the hardware,
and register occupied three bits.
But three bits gives you eight states, not two states.
So eight states apparently means that authentication unknown
will be assigned to six states of this hardware.
Not, so, and these states,
these six states are never taken into account
in the verify public key
because we only take into account verify known
and verify RSA.
So what happens?
You have authentication known.
Apparently the software will treat this in the same ways
as authentication known.
So in the out of eight states,
only one state enforces signature verification,
and seven states are handled
as there is no verification at all.
And again, prover will not be able to catch that
because it's a logical error.
It's a logical error how it's defined by the developer.
So this type of bugs you can still have here.
And this is a program mode compiler,
which Alex speak more about.
Yeah, one of the projects we reviewed,
had fault injection protection in scope.
So the code must incorporate some kind of mitigation
against fault protection to enable this fault mitigation.
So here you see a disassembly of the binary
that we analyzed.
We see some memory compare function
are implemented in a constant way
so that this is protected.
Constant time execution.
But at the same time,
you will see a single point of weakness,
which is definitely a bad thing
if you care about fault injections.
So what happened here?
We analyzed the source code
and saw that developers implemented everything correctly.
But for some reason,
compiler optimized out certain functions,
which weakened the protection.
So this was essentially a compiler problem.
And you only can see that in the binary.
So that's why you not only have to analyze your source code,
but the binaries.
Yes, and that's another interesting example of the issue.
It's not the one issue.
We found the very small issues here and there.
But then we realized when we combine them together,
we have a pretty serious security issues.
It's a problem with the auto-utilization,
problem with the absent of random error,
problem with the design and performance.
And then in the end, when we mix them together,
we found something interesting.
So first thing first,
Spark, of course, cannot prove the correctness
of some metadata coming from untrusted sources,
like from the external media, from the ROM.
Because how it can?
You don't know what's there.
But although if you want to prove such kind of software,
you can provide this knowledge to the prover
so the prover know what are the limits
or what are the bounds check of specific untrusted data.
And this is what the developer did here.
They essentially provide some manual verification
for specific contracts to help prover
prove what they wanted to be proved, essentially.
So what was verified there?
Essentially, they verified the maximum,
of the external media to not cross
through the out of band of the memory.
They also verify what the local buffer is,
what the minimum size is.
And also there is some other checks which are boring
so I didn't include there.
But there is also, you cannot start reading
from the beginning of the media
but from the offset of the media
so you also don't wanna go out of the media size.
So all of that is there.
And in short, all of this sanitization for the prover
allows you to read the data between X and Y.
Then they will pass the check
and the prover will be happy then.
And X apparently was some kind of small number,
let's say eight bytes.
And Y always warranties that you never go
outside of the media size.
So everything is fine, it's okay so far.
We just have some bands check
and the prover can prove it's okay.
And then what we saw, when we started to execute
further this function, they started to read
from external media some image
and this image had another header
inside which had different size
than the minimum size verified by the prover.
Because the minimum size of this header
was 512 bytes, not eight bytes.
Which essentially means that some portion of the data
if you read will be not really internalizing
the internal representation of the buffer
and internal states of the buffer based on this header
also won't be internalized because you just didn't read them
so you cannot pass them, et cetera, et cetera.
But because before you wanted to reference
any memory in Spark or you want to use any type system
in the Spark, you must internalize them
because otherwise you're not even
able to compile the software.
So what happens, I mean, prover will be unhappy
if you do that, and what happens then,
the developers force internalization
so they zero this memory, yes?
So it's fine, yes, you just zero the memory
which you don't use, so it's fine, yes?
So let's go forward.
What we see that somewhere in the middle later
on the stage execution, we see the function
who also tried to verify some pieces of the memory
from this second image which you read.
And this is pretty interesting function
because first thing first, they internalize
the entry point to be always success.
It should be fail, but they make it success.
So okay, that's the first red flag.
Second red flag, they said, okay, if you already verified
some part of the image, why you want to re-verify it again?
So if it's already verified, we have some local cache,
don't verify anymore, performance improvements,
and just go to exit and return success.
But there is also, as you can see, there is ID zero.
This ID zero is internal representation of the state
based on the header which you read in the second image,
and because you never fully read this image,
this ID was internalized by zero as an auto-intelization.
But apparently, this software, probably written
by different team, assumes that this ID
in the internal memory representation is zero.
You means there is some performance improvements
in internal state, so go out and never verify anything.
So in the end, because of this auto-intelization,
the zero was there, and you never verify the image.
And the RSA verification never happened, it's skipped.
Let's see another example of the bug.
So this one is a memory initialization code,
and you see that a developer, for some reason,
decided to make a certain piece of memory readable
for both super user mode and user mode.
So basically, there is a lack of memory isolation
between these two modes, but the problem was
that Spark didn't know the context of this code.
So it was a fine code, it compiled correctly,
but since there was no context,
Prover didn't catch any kind of issue with that.
So it's a logical error, we didn't want this memory
to be readable by both user and supervisor.
But since there was no good model of the hardware,
the Prover could not find this problem.
But it's possible to build such knowledge via ghost code,
but it's very difficult to do.
Another example of the issue is in this code
that performs initialization of the tasks,
during task switch, and you see that certain features
of the cache management have been enabled
to be accessible from the last privilege mode,
and also the cache is not invalidated on task switch.
So it gives a less privileged mode an ability
to perform side channel attacks.
Again, without a good hardware model,
the Prover could not catch that.
Yes, so essentially, if you write the software in Spark,
you also should care about the hardware model, everything,
otherwise the Prover might be blind.
So this knowledge is possible to be done, but it's difficult.
So that's another problem which we found.
It's pretty interesting.
So as I mentioned, we developed some specific operating
system in Spark, and this works on the top
of the custom RISC-V microprocessor
which we also developed in NVIDIA.
And this is a problem which we found in the shared memory.
I don't want to go into the details
how this entire operating system works,
because we can have another talk about that.
Although it's already public, it's nothing new that we
disclose here, and there's a talk made by Demarco Mitic
who fully goes over all of the details,
how this operating system software works within Spark.
In short, just to recap, this is architecture.
You have a hardware, hardware is sliced
by specific sub-portion of the hardware,
and this sub-portion of the hardware is being seen
as exclusive, independent hardware
for each of the software partition.
And the Spark code is here as a part
of the separation kernel, and the separation kernel essentially
enforces the limits of what the partition
can have access to or not.
And because it's formally proved and formally verified,
we have warranties that we didn't miss anything,
that what we divided and sliced,
it's exclusively only accessible
for that specific software partition.
So we can have multiple partitions,
and each of them have exclusive view
of some specific portion of the hardware,
and we prove there is no other way around than that.
So essentially, everything, when you verify it,
looks fine and looks okay, but then we
realize that from the performance reasons,
which of course makes sense,
if you have the shared libraries
used by two separate partition,
we do not want to lose the memory
and map the same shared library twice
in the different physical page, yes?
So you just share the same page.
So you have a shared page between the various partition
if they use exactly the same shared libraries.
And that's interesting because shared partition
not only include the text section,
but they also can include the data section.
And the data section could be read and write, yes?
So if it's read and write,
and depends on the shared library,
we might have interesting information there.
This interesting information might include
the global state of specific shared library,
which could be taken into account
in the logic of execution of the specific software
in the partition.
They also might have individualization data.
They also might have some control flow data.
They also might have, if it's written in the memory
and safe language, pointers.
And this is getting pretty interesting, yes?
So apparently, Spark and the prover
cannot know what you physically do
with the content of this shared library
inside of the partition.
Because how?
So essentially this opens the room for abuse
and depends, of course, what is in this shared memory
and what is in this shared library
and also what is in this shared global data.
So we found a few interesting bugs in our use cases
and we decided to develop a proof of concept exploit
against some of these shared libraries
in this operating system written in Spark.
And we wanted to show you how it works.
I'm not sure what will be the quality of the...
image here but let's try so this is apparently can I ask for a help some of
the goons because when I switch they doesn't switch to the video mode somehow
now we have okay apparently it worked so what we see here I'm not sure how much you can see
here but this is a software like a partition one what I was explaining before this is a in
the sea written partition one it's not very complicated as you can see here this is one
partition main and there is also top handler because if something screwed up we wanna you
know handle the exceptions
and what you can see in this partition one we just first we're trying to define the pointer
with specific others of the memory and so you can see the others of the memory is a shared buffer
this is a shared buffer which is visible in the partition one and partition two and this is the
others of the shared buffer a virtual others of course 1801 thousand so we define the pointer
here exactly to point somewhere in the middle of the shared library which is exactly in the
page where this shirt library is it's 18
410 essentially so it's inside of this point if we point somewhere inside of the shared
buffer which is visible in the both partition and then inside of the shared buffer we will
write some value and we write this value in the partition two there is definition where the stock
page is and the stack page is mapped and the virtual address 18 5000 so we write to the shared
buffer others of the stack that's all what we do in partition one and then we switch the partition
So that's what the entire software does.
This is the magic tool which we use internally
in the NVIDIA to be able to debug
or verify specific hardware, specific software.
So we run this magic software, let's say,
to be able to connect to the RISC-V engine.
We see, we reset RISC-V engine to be clear,
we check in the DMS clock, you see there is nothing there,
there's no messages, it's just clear state of the RISC-V.
And you can see it's clear state, but it's still running.
It's here, you see, it's not halted.
We still RISC-V is running.
So what we do now, we're trying to reflash the firmware
of the entire RISC-V engine in the GPU
to exactly have these two partition running together
under separation kernel software,
which is formerly verified, and so you can see,
after reflashing, there is some censorship
which we needed to put, but logic, I guess, is visible.
You can see that something happened,
and you see the core is started.
Everything is fine, and you can see
that RISC-V status is not halted
after reflashing of this new firmware, it's running.
But when you see the DMS, you see the partition two crashed,
and we have stack overflow,
and it's formally verified software,
and formally verified language,
and you can see, be able to do stack overflow.
That's interesting.
So let's check the specific page where we write.
So you can see, when we dump the software,
that the page of the stack page, it's a physical page,
which is only visible in the partition two,
it's not visible in the partition one,
we were managed from the partition one,
just put the pointer to the stack and overflow
the stack of the memory, which you don't even see
after the partition switch happens.
So you can see, it's exactly the address what we overflow.
So let's check again, this is the address of physical page,
and if you reset the engine, and you check again,
the DMS, you see it's nothing there,
so we are not faking, it's really running the firmware
which we designed to run.
And yes, and then again, verify the address, to be sure,
this is what we did, so you see in the partition one,
we only write the address of the physical page
where the stack will be mapped in the partition two,
which we don't see in the partition one,
and the address of the page physically matches.
So that's all what we did here,
and this exactly page is mapped as a stack.
So that's the proof that this is a stack page.
So yeah, we are here.
Fast forward.
So just to summarize everything,
at first we would like to thank NVIDIA
for developing such an amazing execution environment
that we can analyze,
we want to thank the security research team,
we want to thank the GPU software security team,
we want to thank the product security team,
and AdaCore for creating such a
brilliant language and everyone who was involved in this research and to summarize what we did
the use of the type safety language like formal verification can minimize the attack surface not
only for the memory safety issues but for other issues as well but it's not a silver bullet as
you can see here there is also other issues and we need to keep this in mind and also formally
verified software has a much higher quality thanks to the enforcement and also can prove that dynamic
checks cannot fail if you have assurance of silver plus and also it enables much more efficient
security efforts and in short most of the bugs which we saw requires like a deep knowledge and
deep understanding of the software and also hardware not only software you need to analyze
entire execution environment in the details and in as a result the bugs which we found it's a more
architectural box more design issues more deeper problems essentially and again in short just to
repeat again the
summary of the reviews like if you lose memory safe language we internally found around 40 50
bucks in average during the review in the time frame of four weeks in the memory safe language
we found only 5 10 even if you spent 50 percent more of the time of them on average and but the
bugs which you found is better quality of the bugs so that's all thanks
and we
could take some question i think we still have four minutes
on
so the
so the question is how many bugs in spark we found in nvidia when we analyzed the
software written in spark so in general we haven't seen any software where we did not find
the bugs that's what you can say so essentially every software which is written have some bugs
we haven't seen anyone without the box although
also it's
Worth to mention that the software which we write
usually it's huge in scale, it's complicated,
and we also have a custom hardware,
so this is very difficult to model,
so most of the bugs we found in this area.
How many of them, we cannot say the numbers,
but certainly it's significantly lower
than in the memory-safe language.
In memory-safe, sorry.
Thanks.