So, hello everyone, I'm Christian, even though I go in the internet as strictso, and I wanted to talk to
today about my experience developing devices for Ironclad, using ADA.
The agenda for this talk is going to be short and concise, going to be what is Ironclad.
We will see that chosen for the kernel, the reasons why I chose it, and how I apply this
on device drivers with examples, but most of all, what I wanted to do with this talk is
give our counter argument to the idea that has spread on the internet, and what Ironclad
is like it's like lived effects in it, which is part of Corbwood, which are projects
that take spaces that are usually occupied by price made in C or C++, and people approach
projects like this with the idea of, the price is interesting, but sadly they are written
in ADA.
I'm assuming chosen because it was some kind of vanity project, or just because they gave it
or liked it, with this I want to answer to this, with the idea that, no, Ironclad
is interesting, especially because it uses ADA, and maybe if I can convince you, maybe
you guys should try it for your next projects.
So first of all, I know that most people will be familiar with Ironclad already, I've done
several talks about it, but I want to cover it with my bases.
Ironclad supports this compatible, but surely for my verified kernel.
It's hard real time capable, this means that it has strict scheduling guarantees that it
makes it's best effort to accomplish, and it's almost 100% ADA and Sparkle, I see almost
100% because a similar operating system requires some assembly code, it has some
C code as well for things like an AML interpreter, because there is an extreme workload
and all the libraries that do that for the space handwritten in C, and it's free as in
the GPL with three license.
One makes Ironclad special, it's mostly three things, it's mandatory access control, the
real-time guarantees that I mentioned, which are done without compromising general purpose
computing, and the pragmatic form of verification you see in Spark.
I want to talk much about the first two points, because it's mostly an ADA token, if you
offer to talking much about the operating system in Ternos, when it's mostly about language
stuff, but I do have for the resources that I will talk about at the end, if you guys want to
check them out.
Lastly, talking about the project, Ironclad is only a kernel, those of you that work with
Linux distributions must be familiar with this, Ironclad uses the same distribution method,
I don't know why it's only a kernel, I want it to mix it with new tools,
XORG, I'll leave say, to make a complete system.
The main distribution, I don't plan, not the only one, but the main and open source one is
Glower, which is the one that is trying this presentation right now, which is a mix of XORG,
no user space tools, and the MVC, which is made by the MNG project.
So, we will see that chosen for Ironclad, it's a mix of three things mostly, it's the
form verification of Spark, the fact that Ironclad has quite interesting set of challenges,
with all the embedded development, and having to mix for one of the very far,
I don't know, for a very, very wide code, that ADA approach is best, and the fact that the
specifications and two genes are fully open source, before being an ADA developer,
I was mostly a CD developer, and it's, yes, so nice to be able to have all the specifications,
yes, the reach of your hands is the high to pay hundreds of euros for a specification.
So, going into wide form verification is so important for Ironclad,
what I mentioned, the three things that make Ironclad special, it's really not that true,
that the three things have the same weight. When we talk about form verification,
form verification is a foundation for everything else that we build on the kernel.
Form verification basically allows us to guarantee that we don't have runtime errors,
and check the conditions that we set up on the code, and with that we can verify that
actually mandatory access control, that's what we want, that the real-time guarantees are
accomplished that we want, and it just gives us this full set of tools that we can use to accomplish
that wouldn't be possible with a form verification. When it comes to other languages,
really the competition is not that close in terms of form verification.
Cc++ family languages have robust standards, even though you have to pay for them,
it is where it is, and good opportunity to start a change, GCC client, all the biggest tools
are all systemic. The problem though is that it has no language surface safety facilities,
which makes form verification of Cx extremely hard. I'll see form verifiers are either of
skewer, non-existent, or you have to pay 20,000 euros a month to use them, with big problem.
When it comes to rest, there are big options that everyone just knows me. Well,
why did you not do viral client rest? It has a really good community and force code.
So it's just in that really which that we have in a really good strong force code.
And it has a really good public image. When you mention rest, people already think about
safety, people already think about these things that they don't really think about as much
when you mention it, just because it's not as much in the spotlight. The main point is we
rest, though, is the very backbone standards. I see bare bones because ferros in excess, but
really is not a rest. Specification is basically a separate project that just very
fastest set of tools is for rest, with a concrete specification, but it really does not reflect on rest.
And the very first, I'm very mature. In previous talks, we heard about kami. I said,
to that I have that personally, I was not really that safe. Much in terms of the features that
spark offers. I would also have to use rest and I will not develop on that point.
Then you can say that, I know that we have all the logo with the coin. I just
really like the balance, I'm sorry about that. It has really robust and that's a really good
open source tool change. And spark really is state of the argument it comes to open source
form of verification. The only problem that it has has to do is that it has a really
thing community. And much of it is not centered on open source. I will not talk with you. I will not
tell you all the stuff about how spark works after five talks talking about it. But basically
all the important stuff is that it has three and post conditions, it has the whole control,
check and flow. And for what I want to talk following this is that all of this has to be
written. So I think that you have to go out of your way to do. And it takes a lot of effort, especially
when we talk about operating system code, where you have a mix of form of refinery, form of
verify code, hardware, interaction. And all of this brings me to talk about how
form of verification in the terms of operating system code is extremely hard. Those of you that
are into the field, we also know about SL4, which is a microcarnal, similar in scope of verification
to what item code wants to do. And the report that it takes around 20% years to verify 10,000 lines
of C. For an case of it better, because we just say that, it already puts us in a better position,
when it comes to form of a very fine density. But still, the scope is much better with ironclad
ironclad, it's a full-possious, cannot influence all-possious behavior, it's not a microcarnal,
that only has to manage stock between servers. So, we do have to pick our battles, if we want to
finish, put ironclad in a good state of form of verification before we go into retirement.
Basically, how we start is that we start from the things that are closer to userland,
that will be process management, matrices, continuity, and we work all the way back
from higher to lower priority to the things that are closer to the hardware. That will be
going from the scale of logic to internal kernel access. Thankfully, that helps with Spark mode
off, that let's say to me, it makes, I'm very tired, I'm all used, I'm very tired.
Specifications, I make some much them into being able to delegate a bit of the work for later.
And we expose safe interfaces for unsafe code. But there is more to it than Spark.
Hardware developers are, initially this set of slides where hardware developers are
say this, I was told that I should not be putting that for them,
presentation, so we just left it that silly. This is a part of a HCI, which is the protocol used for
Satan, similar this access. You will notice that I don't know how well it will translate from afar,
but has several fields that are like three for bits, it's a whole mismatch of types only,
the name of saving space. But language is struggle a lot to represent this. See, for example,
you have to use bit fields, bit fields that are, I'm in field for issues regarding NDNs,
for issues regarding the encircness to use, this solution is not really ideal.
Last step has no way to represent this. This is a great created by a user that
represents this behavior, but again, this is not meant by the risk community, it has no way
on the specification of rest or frozen to do this. And you still have problems of type safety,
like you're reducing there are use size, which is 64 bit type to four bits, it's just a mess in terms
of type safety. In the meantime, the ADA just handles it perfectly, you can define your
types with your own bit lengths, you can compose them using record representations,
and it just handles all of this flawlessly without the pain that the other languages have.
With that as well, we come to ADA runtime, which I think is the biggest reason as to why ADA does
better to operate existing work is when compared with other languages. When we think about about
language runtime, most of them we think about monolithic blocks, where we cannot negotiate anything
with the language. But it goes to it, although we have the whole set of restrictions that let's
speak and choose what we want to the runtime to be able to do an implement. So if you want to
operate it, use the runtime in a stage where you know how memory allocation yet, you can just disable
that for the time being or disable the whole floating point subsystem for the whole kernel as we do
for performance reasons. And truly this is one of the best things when it comes to adaptation of
ADA into weird conditions, weird runtime. Without I wanted to come to the presentation,
if you guys want to follow progress of the project, check the source code, download your
distribution for testing. You can go to ironclad.nong new.org and I would like to thank these
organizations, the free server foundation, either core and the limit good loader, which is a
loader that uses that color uses along with the internet foundation for giving us funding and resources
to continue the project. And I would also like to thank these people as well.
Oh, yeah. Well, I guess that I could also do a little showcase of the operating system. So all of this
is glow art itself. It features terminus, file managers, it just was the
data. Pay the lucky data as soon as the reality crashes.
Well, this one. Yeah, any questions?
Well, you, well, you, I do a question. I will just reboot it.
Okay. Go ahead. So we have, we know of the question was, if whether we know how many people
are using the operating system, we are aware of distributions that are made by
all the people for their own uses, some of the internal testing at companies. So there are some
hobbies, do you sense how well they use the operating system? But we don't have really
cannabis, we don't have any kind of telemetry that let's not know how it does. Any other questions?
So the question was whether we selected any specific hardware for the, I didn't hear
well, the last part was for the implementation of the operating system or for the,
for the source of time, for the source of time. Okay. So the person architecture,
I don't have supposed to architecture, six, six, six and three, five. For X36, we use the HPEAT
as well as the LAPIC Interattimer, the HPEAT for high precision timekeeping, for
things like counter calibration and the LAPIC, we use it for day to day tasks, like checking
intervals. And for for risk five, the port is not far enough yet to what I can give a comfortable
answer. Any other questions? But I will try this. I will definitely try.
Uh, it's actually really, I was joking with, with another project. Where is it?
Race at perfectly fine.
Yes, we're going to take a bit.
Okay, there we go. So this is glad, uh, shame that the introduction had to be, to the actual
features had to be with, uh, the display manager crashing, but this is it. It's running
XOR has its, has its own file managers, uh, that would be the files for the slides that I used,
uh, it also has its own applications, uh, that are ported from other Linux distributions,
like calculators, clean shooters, features, also a few games that I will run GLX gears by popular demand.
Those they are.
Thank you.
Also, features features soliter as well, along with other games.
Has again, terminal regulators where you can do the typical Linux ritual of the in a new
fetch, uh, that's it. It's just a fully featured general purpose operating system.
Yeah. Wow, that's, extremely lucky. Yeah, it did. You read. It's fine. I think I didn't
various months ago, for us. It's fine. It's better. It's better. It's better, so, well, yeah, well, yeah.