Thank you.
Yes.
Thank you.
So I will start with a quick summary and also a motivation for this project.
So yeah, as you all may well be aware, like any larger project, the box in the Linux
certifier.
And there are existing solutions to this.
For example, the fuzzling has found a lot of box and some were resolved using formal verification.
And also there are hardware-based approaches to kind of put the program into another
sandbox inside the kernel.
But unfortunately, these all either involves runtime overheads to some extent or they are
where you hard and complicated to implement.
So they take time to cover the whole verifier.
And in this talk, I'm going to talk about an alternative idea to solving this problem
using layouts using a layout security approach.
So basically the idea was that you verify the program twice once maybe in user space,
for example, using prevail or based on the Rust compiler compiler.
And then in the kernel, you verify it again.
And if there are box in any of those algorithms, you hope that the box in one algorithm
are caught by the other algorithm.
And I did two case studies, one based on the Rust compiler and one based on prevail.
And unfortunately, you're found that this kind of design doesn't really work, at least
to me, it appears it is still exploitable, even though writing exploits certainly sometimes
becomes smaller tedious.
So sticking to the rough-based design, here's how it would look in detail.
So we get the source code from some untrusted Rust program.
And we compile this using a modified Rust compiler.
I will get to the modifications you would have to make in a second.
And then this generates some byte code, which in theory should already be safe, because
you restricted the Rust compiler and also the libraries the programs used in a way such
that this program can only do memory safe and type safe behavior.
And then you verify that again using the Linux verifier, and hopefully you get even safe
a byte code.
And so the implementations of the two verifiers should obviously be as different as possible
because then it is you are more unlikely to have the same bug.
If you have code we use between the verifiers, then you could end up with the same bug
in the two systems.
And the obvious benefits are that you basically have no runtime overheads, you just have
a verification time overheads, and you can reuse existing tools and libraries, so it's relatively
easy to implement.
And the two case studies are, and so one based on the Rust compiler already talked about the
other design would be based on pvail, and prevail already verifies ppf object files, so you
can directly feed those into the prevail verifier and then do a second pass with the Linux
verifier.
And in my analysis, I focused on the changes you would have to make to those systems
to make this kind of approach work, whether there are any bugs in those systems, so in the
prevail verifier and the Rust compiler, and whether the resulting layer verification approach
would be exploitable.
So first, looking at the Rust based design in more detail, so I previously thought about
that we have to make some changes to the Rust compiler, and likely we also have some kind
of trusted Rust library which can be used by the ppf program, so this would, for example,
allow the program to call bpf helpers in a safe way, and then this produces the bytecode
which can be verified by Linux.
So regarding changes, we would have to make to the Rust compiler, and you obviously have
to disable unsafe, but there's also a bunch of other features, for example, there are
procedure macros in the Rust compiler, which basically allow you to rewrite the whole program
source code to something else.
This also has to be disabled, and in the appendix, I also look at a few other features, for
example, ppf and some other, for example, unions, they also would likely allow you to introduce
unsound behavior or there will that relative in you and therefore likely background.
Another thing where the Rust compiler currently for short is termination checks, these are
obviously not needed for user space applications, so it doesn't provide those, and you could
likely implement something like this using procedural macros, but a more exhaustive check would
likely be better put into the compiler directly.
So these are the compiler related changes you would have to make, and second, and there's
also a bunch of changes that would have to be made to the Rust library that is used
by the bpf program, and so there's already a Rust library which allows you to write
bpf code in Rust, that's IA, also in the next talk, so you could likely extend this, and
looking at the examples I've looked at, you can already write where we complex programs
only using save code, and the places where they still use unsafe at least to me looked,
as if they could be likely easily removed using more interfaces.
Another thing is a problem in the Rust standard library, and also how safety is commonly
perceived in Rust is that it does not guarantee non-static destructors, so that's the reason
people commonly refer to Rust as not guaranteeing memory safety, however this could be changed,
I believe, so it was basically a design decision that was made for the Rust standard library
in 1.0 of the Rust compiler, but in the compiler I think it's not half-coded, so it's
only something, it's basically a definition of what safety means for the Rust standard library,
and it's not built into Rust. Yeah, so this concludes the changes you would have to make
to the Rust compiler, and now looking at the box in the compiler that would likely be relevant
to such a design, so all the compiler box reported, so the last one is the issue, so there's
roughly 10,000 issues open, around 4,000 bucks, and there are two kinds of bucks which are
relevant to such a system. First, you have arbitrary code execution, but the someone can
write a Rust program which can take over the compiler, they can obviously generate any ebps,
but they want to generate, and this can then be some exploit for the ebps verify.
However, at least I've not found any reports of our repository code execution box for the Rust
compiler directly, however there are 104 compiler crashes reported, and these indicate that there's
some kind of memory unsafe to the compiler that could probably lead to our repository code execution
down the line, or it doesn't seem that anybody tried to exploit those for our repository code execution,
they exist further potential for hardening, for example, memory sanitizers, I think they are
usually not applied to the compiler, and the second kind of box is an unsoundless box, of course,
or you basically have safe code, and it produces an unsafe binary, so it's basically at
back in the checks from Rust that for safe Rust, and they are around 100 of those open,
so that's already much better than the 4000 box overall, and then the following I will assume that
basically there are unfoundless box and assume that there are no arbitrary code execution
box, and I analyzed whether the system would be exploitable if we make this assumption.
Unfortunately, it appears to be exploitable, so the two box I have looked at as an example
are a Rust unsoundless, unsoundless issue, which is called implied bounds on nested references,
plus variance equals a sound as whole, and this is apparently relatively complex to fix because
they basically decided to redesign a whole part of the compiler to fix it, and that also explains
why it takes so much time. The other box I looked at was a Linux or a firebox, a TVE from 2022,
and that's basically a case where a pointer arithmetic is correct incorrectly.
So looking at the unsoundless box, there's proof of concepts online where you can look at how
you can exploit this unsoundless box in the verify, and it basically gives you a function,
you don't have to read this code, I just want to show it that it's a lot of code,
it basically gives you a function that allows you to cast one type into another type.
So this then basically gives you an unsave task primitive, which can be compared using only
safe code. And the idea to then build an exploit for this layered approach is to basically use this
unsoundless box for type unsave, if you have type unsave, you can, for example, cast a scalar
into a pointer, and this gives you a out of funds pointer, and the harder part of the exploit
is then finding a Rust program that generates the unsave EBPF bytecode that is also misbite
verify. So that's basically this compilation. And it takes some times, but you can certainly do it.
So you can use this transmute primitive to construct the out of bounds pointer, and the interesting
thing here is maybe that all this code I just showed you in Rust gets compiled basically down to a
single, register silent in the EBPF bytecode, because the compiler does the optimizations,
and therefore the EBPF verify has no way of kind of double checking whether the Rust compiler
did any error here. When you have optimizations, you don't want in the bytecode you can
avoid them using data dependencies. What is a little bit more tedious is to get the register usage
in the exploit right, because the Rust compiler doesn't really care whether it's at a
it adds a scarlet to a pointer or the other way around, and this can get more tedious to kind of
make it do the right thing, but yeah it's possible. And you can find the proof of concept in the
GitHub repo. Yeah, so this concludes the part on the Rust compiler, and I also looked into the
prevailed EBPF verify, and the good news is first it looks like it does not reuse any
kernel code, which should also be the case as it uses the MIT license. So if there are any bugs in
the prevail verify, which I will assume they are likely to be different from the bugs in the Linux
verify. There are currently around four the issues open. One is a one is tagged as a bug that
would be potentially relevant for this kind of thing, but I did not look into it specifically
I just assumed that there is some bytecode, which is incorrectly analyzed by the prevailed verify,
and then asked whether it can be exploited. As so the ideas we have two functions. One is
incorrectly abstracted by the Linux verify, one is incorrectly abstracted by prevailed, and we now
will try to combine these functions, and then kind of use the result of this combination to
construct a hidden out of bounds read all right, which is then native kernel exploit. And unfortunately
such a combination exists, and it's also very simple actually. So you basically, you assume
at one and at two are some complex sequences of bytecode, which are incorrectly abstracted by one
of the verifiers, and you see that both for air one and air two, at least one of the verifiers
still matches the actual execution, or ever if you of course, and these results together you
basically have a result, which where none of the verifiers is correct anymore, and then in the second
part you can basically just use this incorrectly track register to construct an out of bounds
point and use it. So this concludes my talk. Unfortunately, layer verification seems to have limited
potential. You can usually combine the exploits, it roughly doubles the exploitation effort,
because you need one exploit for one system and one for the other, and then you have to combine those.
Of course, marks in the runtime, for example, the helpers, but in any case, not be covered by it.
The effort, at least for a rest, it seems to be a little bit more tedious, however, I also
not look at whether there are any reliable tools, which give you a rest program for a certain
ebbed bytecode. I'm not sure if something like this exists. For prevail, it's certainly very easy,
because you can just use the generic consumption. Thank you very much, and I'm happy to take questions.
Yes? For the rest of the exploits, what you're not doing, technically, right, unsafe,
or a very code that is equitable, we have to intentionally make the exploit out of it.
Yes, the question is whether you have to make the exploit happen intentionally. Yes, that's the case for sure.
So I think, I guess someone stumbled upon this issue in the rest compile at some point by mistake,
I guess, or maybe through fuzzling or something like that, but it's very complex code, and I guess
you would never kind of write this kind of unsafe, safe code by mistake.
But it's like if you build a ebbed program, assuming you've done everything correctly according
to the rest centers and the compiler said, somebody else can't exploit your ebbed code. Or is that possible?
You mean that there are memory safety box in the ebbed program?
Would there be? I think if you do not make a mistake on purpose, it would be like, yeah, I think.
Yes?
More like the background for this topic, what's the extent behind using graphs to write ebbed over
So why we do that?
I think the question is better as we do for the next talk, but we can also talk offline.