All right, welcome everyone, great to see many people.
I'm Jo from the KLurvin University in Belgium.
Professor there and joining me for this talk later is Skobb, who started a PhD with us.
And during his Marsity, this is the work with me on this project.
I want to talk a bit about today.
So this dev room kind of has a long history.
And in one of the first editions, this was not called confidential computing, right?
It was called trusted execution.
And so what I want to talk about today is trust.
And I really like this XKCD image.
And when we talk about trust, because it shows very visually
that in computer systems, trust is very much a vertical thing, right?
You can see how if something goes wrong here at the bottom of the stack, the whole thing falls down, right?
And we are engineers, we all know this way too well.
But if you really want to think more about trust and this idea that you depend on
the operating system and compile it and so, I very much recommend to have a look at the
monitoring of our lecture of Kantonson.
Kantonson, I think you all know him, developer of Unix,
inventor of the B programming language, the preceded C.
And it's very nice, he had a talk, it's also nice little paper, it's only a couple of pages.
There are really things about what happens if you start implementing back doors and malicious codes
in lower layers of the system stack, let's say, in compilers in this case.
And he concludes somewhere at the end of this couple of pages.
It's written in a very accessible style.
So he says, the moral is obvious.
You can trust codes that you did not totally create yourself.
And I think he asked after that, especially if it's written by people like me.
And so this, I think is something to really think about and that I will repeat a couple of times later on in the dark.
So if you kid code yourself and it's not too big, you might have a reasonable twist, at least,
not in terms of books, but at least in terms of, let's say, back doors.
I think that's also very much the spirit of trusted execution.
So if we go from reflections on trusting trust and the tiering of art lecture to reflections on trusting trusted execution environments,
you all know these pictures being shown a couple of times today.
The idea, of course, of trusted execution of confidential computing is to put big,
of the stacks like the operating system outside of the trusted computing space, which that's,
we can, we can embed trust directly in the process of the end of the end of the end.
And if you look at the picture, a lot of the research that the community as a whole has been doing,
but also our group in learn, is trying to look at these two green boxes.
And on the one hand, you have a trusted processor.
We all know that's not perfect.
There's been a number of high impact attacks, some of them we did in the past, like the foreshadow attack,
that show if things go wrong in the CPU, in the microarchitecture, the whole thing falls down again.
That's not what I want to talk about today, if you want to talk about that,
confine me in the hallway, super exciting stuff.
But what I want to talk about today is the inverse side of that, namely,
what do we put inside that, what I call an angliff now, but it could also be a CVM, a confidential, virtual machine.
What do you put inside the tris bounty?
As of today, it's not perfect, it also has bugs.
And in this respect, I think we've all seen in this confidential computing devroom, as well,
a shift over the more recent years from this original idea of confidential computing or artistic execution,
which was very small containers, typically, isolated to level of a function call,
and the original idea of aesthetics, towards what the industry is now adopting on the large scale.
Actually, it has been vastly covered in the last talk.
So let's go back.
Well, I want to do today is not talk about VMs, maybe a nice hardware discussion,
but I want to talk a bit more about this original idea of small interfaces.
And if you look at sjits, which was the most ambitious today,
I'm maybe partially at fault for that, but sjits has gotten a lot of bad publicity, right?
And Intel needs to do something with that.
So one of the things they did is to try to sell that, and to some extent, as fair,
and they say, Intel sjits is the most researched and battle tested to such execution environment.
That's a good marketing, I think.
But they also say something very interesting here.
It has the smallest attack surface within the system.
In the case of course, in a confidential VM, you put your several million lines of code,
Linux kernel in there, and in sjits, the ideas, we write small good things, right?
And that's true support.
So that's the idea, the star eyes here are always fine.
Okay, okay, that's what, when we also started 2011, we were on board with that idea.
But then the reality hits, right?
And the reality is, we now have a vast, quite big open source ecosystem to develop into a zig-saint
place.
And again, I'm very much aware, there is a lot there.
But I'm going to look at the projects that try to build the enclaves in the most minimal way.
And those are not language integration and likely open systems,
but those are what we call software development kits, right?
So they allow you to write an enclaving C.
And there's two of those in production today.
You have the one from Intel, the Intel SDK, and you have the one from Microsoft,
essentially, the open enclave SDK.
And so what we did together with Corban, Corban in the T.S.
Let's first just try to map out the landscape.
How big are these things?
And you see just a simple slow count here.
And we were talking, maybe not about million lines of codes,
like in Linux, but you're talking about hundreds of thousands of lines of code.
And this is already, let's say very kindly,
because if you measure in the root directory, it's much more,
because they have all these git modules.
And for some reason, they have the whole Google portal buff in there.
So it's bad, right?
But take away here is, you want to isolate a small secret.
It's like, like, say, this little apple here.
And you want to package it in an enclave container.
And instead of putting it in a nice little box,
that you can reason about you put it in a big trip, right?
And that's what we are doing, that's what least questionable.
Right?
That's bad, because software is buggy.
And in some of the past research, we also showed out,
this is practically part of when we did a first on analysis.
We've done many since, also automated tools.
But this shows that these hundreds of thousands of lines of code
have film abilities.
And again, I'm coming back to my friend here,
Kentomsson, who says, yeah, this again shows you can trust
these hundreds and thousands of lines of code.
And you cannot reasonably check them out, right?
Okay, maybe open source and that's great.
I have fun going through all these hundreds of thousands of lines of code.
And so the idea for this project is,
can we do better?
Can we maybe build anchors,
that we can totally, like, where we write all of the code
that goes in there, literally all of the code,
and then maybe we can trust them.
That's the idea.
Okay, and that's the topic of today.
I started thinking about that long ago,
and one of the things you need to do, of course,
when you want to make anchors,
a zig-sync place in this case, is to talk to the hardware,
and you talk to the hardware typically to the operating system.
And so, many of you will know the Linux control,
now this has upstream support for SVX,
it took a lot of effort and wooden tiers,
but we now have this slash Jeff slash a zig-sync place.
And so, what I wanted to do is,
okay, can I talk to that drive directly,
to create anchors for me?
And I looked to turn it out,
and I don't have to do that from sketch,
because there was already some support in the Linux kernel,
in the form of the what they call self-test,
super, super, yeah,
super, super, super tricky of the kernel directory.
We're essentially doing a bunch of small tests,
and they had some sort of testing left there,
and I looked at the interesting, right?
You just have a C file, and an assembly file,
you're remdored through something like GCC,
typically GCC, you might also want to use client,
and then you'll get an ELF file,
and they have a very small C file,
or something, that basically talks to the driver.
And they use stats in Linux explicitly,
because they wanted to test their driver infrastructure
without pulling in these hundreds of thousands of lines of code.
Okay, so I thought that's great, let's use that,
and start at looking a bit at that,
and this is actually part of the project
that Martin mentioned earlier in the open IP,
and he talked that we have this in both infrastructure,
in both execution infrastructure,
and so one of the projects we did there,
in this Pandora project, find the paper here,
is to check small enclaves,
and I checked this test, self-test enclaves,
and it was full of bugs, right?
It's quite bad because some of that was even,
like, to some extent, used in production by Intel.
Okay, so you'll find bugs,
the next thing you do is you try to fix them,
so I talked to the Linux kernel developers,
and what you see here is that Dave Hansel,
made any of the x and the 6,
and one of the maintenance of the x and the 6 subsystem,
let's put that look, I see,
or you have a point, but I don't want to have this in the kernel,
and it's that there is a gap,
and it would be wise to close this gap,
but take it basically in a fork,
and that's where this bargex project was born.
I forked off this code from the Linux kernel,
and started sort of making that into a self-contained framework
to build in place.
Okay, looks basically like this,
and we have the same idea here,
that you have basically an assembly file.
If you want to see file,
you don't even have to do that.
And if you want, there is some,
to sort of library that the code will talk a bit about.
But the basic idea is,
you render into a very small inklet,
and then there is an interest at runtime functionality
that, that, then talks to the drive.
The cool thing is,
this is all packaged these days in a build route,
file system,
so you basically have a super small VM that runs,
and that,
only dependency has the upstream kernel drive,
which is supposed to be forward and backward,
compatible, right?
So it should be fine if you build a bargex,
and claim if you don't touch it in maybe ten years,
hopefully if the hardware is there,
you might be able to run it.
And Barry, in mind,
these are super small inklet,
and we're talking really about a couple of pages.
Typically one code page,
plus than the architectural pages you need,
like the threat control structure in the safe state area.
Okay, so here you see a screenshot of this build route container,
and you basically see,
you can just operate them,
you can interact with them like,
like normal C programs essentially,
and you even get some asky art for free.
And another thing I did,
already, is to integrate this with the SX step,
attack framework,
and some of you will notice,
if you're researching attacks on SX,
like we do,
which means that you can do all kinds of rapid prototyping,
of smaller attacks,
and maybe also make them long-term available,
without pulling in these dependencies
from the SDK that are very fragile.
So that's the story of,
of what you can do with Barry's Jix,
from perhaps a research site,
but Cobra also works in his master's thesis
on trying to make something real,
and I'll hand over to him to explain a lot of bits.
All right, so,
everybody says the proof of the pudding is in the eating,
so that's what I did.
I built a prototype,
and in this prototype,
I ported Hackelstar,
which is a high assurance cryptographic library.
It has been formally verified in F-star,
and so, just as a proof of concept,
we made that work in our bare SX and cliff SDK.
So an application with a C file,
and you have some buffer,
you want to, for example,
calculate the hash,
and that can be done entirely inside the enclave.
What did I do?
This bridge code that is needed between the application,
and the enclave is automatically generated.
As it's really error prone,
you can trust on yourself to write it.
It has to be done by something,
someone really small or smart or by iterated.
So, this iterated tool also has a lot of dependencies,
and I fulfill these dependencies with caution,
and with care.
So, I implemented, from F-artos,
a heap implementation with this really bare bones,
a really minimal,
that can be really,
it's trustworthy,
and I also implemented some small ellipse.
So, what does this all mean from a performance point of view?
If we look at the Y-axis,
you see the amount of code lines of code,
so the actual line count of the trusted code,
and for our project bare G-axis,
you can see that's only limited to a really, really tiny amount,
and especially if we look at the binary size,
we're below a usual page.
So, that's astonishingly minimal.
Right there.
So, if we look at it from the application included,
you can see that's really, really small runtime that we have to trust,
and again, the runtime that we have is really trustworthy from F-artos.
And so, again, this application part is also really massive,
but higher assurance because it has been formally verified.
If we look at the performance,
because we also want performance,
we don't just want security,
you can see on the Y-axis,
the CPU cycles that are needed to perform certain calculations,
so we have the bare bones return,
and clip that immediately returns upon entering,
and now we have the H-Mac calculation and the authenticated encryption.
The lightly marked area is the area
that is absolutely minimal for an angle to perform.
So, if that's the theoretical limit that we can achieve,
and you can see that with the bare SGX return,
and clip super duper close,
and also perform a lot of the state-of-the-art production as the case.
And then, maybe zoom in,
because the CPU cycle count as a bit perturbed,
the actual instruction is really large to enter the enclave.
So, if we only look at the instructions that are executed with SGX steps,
where we can interrupt the enclave step by step instruction by instruction,
you can see that for the really bare bones and clip,
we only have 29 instructions,
which is, as we would say, bare minimum.
So, to conclude,
the reality is right now that's Intel SGX,
the Intel SGX is quite large,
and as we want to say, it's really bloated.
It is a large text surface,
and again, our trusted computing base is massive,
actually the goal, or the dream that we would try to avoid,
and keep a minimal TCP is a bit lost.
So, what we introduce is a small box with a small apple,
bare SGX, where it's truly minimal trust,
and where you can actually know all the code that's inside,
and know what we are using.
There's tons of use cases,
for example, formal verification,
but you can think about, like, your set with a prototyping,
or the long-term packaging, anything is possible.
So, one last thing, it's all open source.
You can scan the QR code or access the link.
As you can see, I recently joined this training at Research Group.
It's a fun place, and it's a nice working environment,
so if you're interested,
just also link down below for that.
And if there are any questions, happy to answer.
Thank you.
So, very interesting work.
I really like the score.
If you see between as a script, and to this,
I'm not a fan of moving towards the VM,
which is really going up all the spirit that we had as a community.
So, I really appreciate this work.
And one question specifically in hand,
is about the formal verification use case that you mentioned here.
If you can calibrate how you think that use case of this work,
or are you saying that is a potential future work,
someone can calibrate it,
and heckle star was already by and of star, right?
Right.
So, what is the key,
because formal verification,
and you can use that risk, maybe.
So, quickly repeating the question,
what other parts do you consider to be formally verified,
or are you thinking about?
So, we have some projects ongoing right now
to formally verified the iterator bridge code
that has been generated.
And that would already cover a lot.
The T-lip C that I wrote is also really minimal.
So, it's a mamm copy and a mamm set, for example,
that's basically it.
And I'm also the heap implementation
from free articles is also left behind.
But there's also been some rumors about people wanting to formally verify that.
So, that's a bit the state that we are currently interested.
Just to replace, like it's not going to be used,
it's kind of some future work that you are planning
that some parts which are not really identified,
you can verify, right?
Is it correct?
Yeah.
Maybe, wait.
If I unclip and I just hold it.
So, the question,
your follow-up question was,
whether this is future work or not.
So, I think,
So, when I say use, or when we say use cases,
the idea is that formal verification and enclaves
go very well together, right?
Because we have security critical code,
typically that is relatively small size.
The problem is, if you take something like Hackelstar
and you just put it in an enclave with tooling that we have today,
you would add 200,000,
of very verified lines of code, right?
And we've also had some prior work, for instance,
Martin, on doing attacks on Hackelstar in an embedded context
where there was some bridge code that was in verified,
that then invalidated the nice F-star security proofs.
And the idea is to fold on the one hand,
can we minimize that code?
That's what we have today, that's what the code will build.
And you see here, the code is minimal.
But the immediate future work with B,
can we also get security guarantees,
formal security guarantees, for that minimal code.
So this is now in the scope of being small enough to formally verify
at a moment.
And that's a spectrum of things.
One of the things we are doing already is to simply execute it.
That does not give you a strong security guarantees,
perhaps, as something like F-star.
But we also have other work, for instance,
to do more sound verification at a C language level
with a two-called wayfast.
But so the idea is to create, to engineer something
that is in the scope of formal verification.
Yes, by all means, I think we should do that.
I would like to create something like barricade, barricade,
barricade, barricade, and so on.
I think in terms of VMB's architecture,
as we can probably use the systems engineering work
from the last decade, some micro kernels and nano kernels
and all that, right?
Also, if you were interested in that, maybe,
so we don't have it yet.
But if you're interested in that,
I have a look at either NX, which is a small form scratch
represented in a time, or Tom Domans,
a first-time talk from last year, called Mushroom, right?
Which also has a think-similar spirit of,
can we build something from scratch,
not just run a play in Linux in there?