I'm assuming it's chosen because he was on kind of vanity project or just because they
catered like it.
With this, I want to answer to this with the idea that, no, I'm glad it's interesting,
especially because he uses a say that.
And maybe if I can convince you, maybe you guys should try it too for your next
projects.
So, first of all, I know that most people will be familiar with I don't have already.
I've done several talks about it, but I want to cover it with my bases.
I know that it's a positive compatible, partially formally verified cano.
It's hard real time capable.
This means that it has strict scheduling guarantees that it makes its best effort to accomplish.
And it's almost 100% ADA and Sparkle.
I see almost 100% because a semi-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 you're free to use 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 won't talk much about the first two points,
because it's mostly an ADA token, if you can't afford to talk much about it.
This is them internals, 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, I don't play this only, I care no.
Those of you that work with Linux distributions must be familiar with this.
I don't play this is the same distribution method.
I don't play this only, I want to mix it with new tools,
XORG, AliveC, to make a complete system.
They made distribution, I don't plan, not the only one,
but the main and open source one is GULAR, 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 Maraghan project.
So where was it actually for I don't plan?
It's a mix of three things mostly.
It's the form verification of Spark.
The fact that I don't have quite interesting set of challenges,
we felt them better development and having to mix form
really far enough for my verified code, that ADA approach is best.
And the fact that the specifications and tools 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-play harness of euros for
a specification.
So going into why form verification is so important for I don't plan.
What I mentioned the three things that make a run class 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 this.
That wouldn't be possible with form verification.
And when it comes to other languages, really, the competition is not that close in terms of form verification.
C++ family languages have robust standards, even though you have to pay for them.
It is where it is.
And good open source tool change, DCC client, all the biggest tools had all C-centric.
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 obscure, non-existent, or you have to pay 20,000 euros a month to use them,
with big problem.
When it comes to RAS, there are big options that everyone just knows me.
Well, why did you not do I don't claim RAS?
It has a really good community and force code.
So it's just in that I really wish that we had in a really good strong force code.
And it has a really good public image.
When you mentioned RAS, people already think about safety, people already think about these things,
that they don't really think about as much when you mentioned it, just because it's not as much in the spotlight.
The main point is with RAS, though, is the very backbone standards.
I see very bones because ferocene exists, but really it's not a RAS specification.
It's basically a separate project that just very fizeset of tools used for RAS.
With our concrete specification, but it really does not reflect on RAS.
The very first I very mature in previous talks, we heard about kami.
I said, to that I have to add personally, I was not really that safe.
Much in terms of the features that spark offers.
I would also have to use RAS, then I will not develop on that point.
And 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 standards and really good open source tool chains.
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 thin 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 of how spark works after five talks talking about it.
Basically, all the important stuff is that it has free 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.
When you have a mix of formally, you find a formally verified code, hardware interaction.
And all of this brings me to talk about how formalification in the terms of
operating system codes is extremely hard.
Those of you that are into the field will also know about SL4,
which is a microchernal, similar in scope of verification to what I don't quite want to do.
And the report that it takes around 20% years to verify 10,000 lines of C.
For our case, it's a bit better because we use a data.
It already puts us in a better position when it comes to formally verified and C.
But still, the scope is much better with ironclad ironclad.
It's a full-possious, cannot influence all-possious behavior.
It's not a microchernal that only has to manage stock with win servers.
So we do have to pick our battles if we want to finish.
It's a good time in August, it's a 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 us with Spark mode off.
That makes a modified data module, a modified specifications.
That makes a much to be able to delegate a bit of the work for later.
And we are supposed to save interfaces for and save code.
But there is more to it than Spark.
Hardware developers are initially these set of slides where hardware developers are
sadists. I was told that I should not be putting that for them
presentation, so we just left it at silly.
This is a part of a HCI, which is the protocol used for Satan, similar disk access.
You will notice, and I don't know how will 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 bitfills, bitfills that are
a mine field for issues regarding NDNs,
for issues regarding the crankiness to use.
This solution is not really ideal.
Rust still up 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 Rust community.
It has no way on the specification of Rust or ferros into do this.
And you still have problems of type safety, like you're reducing the
use size, which is a 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 bitlinks.
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 when compared with other languages.
When we think about language runtime, most of them we think about monolithic blocks,
where we cannot negotiate anything with the language.
When it comes to it, although we have the whole set of restrictions,
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
don't have 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
where conditions we run times.
Without I wanted to come to the presentation.
If you guys want to follow progress of the project,
check the source code, download your own distribution for testing.
You can go to ironclad.nongo.org.
And I would like to thank these organizations,
the free software foundation is at core and the limit of good loader,
which is a good loader that uses that color uses,
along with the internet foundation for giving us funding at resources to continue the project.
And I would also like to thank these people, as well.
Do you think you might have a memory to view it?
Yeah, and then they can start.
Hmm?
I guess I have a more memory to view it like you are into any video.
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 pretty unlucky datation of serenity crashes.
Well, this one, yeah, any questions?
Hmm?
Well, you, well, you, I do a question.
I will just reboot the real thing.
Go ahead.
Do you know how many people are into your operating system?
So we know of the question was,
how 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 that companies.
So there are some hobbies, these are several,
they're used to operating system.
But we don't have really cannabis, we don't have any kind of telemetry
that let's not know about that.
Any other questions?
What is the source of time, the user director's question
out there for the source of time?
So the question was whether we selected any specific hardware
for the, I didn't hear the, well, the last part was
for the implementation of the operating system,
or for the source of time, for the source of time.
So the person architecture, I don't have supposed to architecture,
six, six, six, and three, five.
For X-X-X, we use the H-Pet as well as the LAPIC
internal timer.
LH-Pet for high precision time keeping,
for things like counter calibration,
and the LAPIC we use it for day to day tasks,
like checking intervals.
And 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.
It's actually really, I was joking with another project,
where is it, it's perfectly fine.
Yes, I'm going to take a bit.
OK, terrible.
So this is Gluar, I assume that the introduction
had to be to the actual features had to be with the display manager
crashing.
But they say that it's running XOR has its own file
managers that would be the files for the slides that I used.
It also has its own applications that are
ported from other Linux distributions,
like calculators, screenshots, features, also a few games that I will run
in GLX gears by popular demand.
Those they are.
APPLAUSE
Those are features, features solider as well,
along with other games.
Has, again, terminal regulators where you can do
the typical Linux ritual of doing a near-fetch.
That's it, it's just a fully-fetched, general purpose operating system.
APPLAUSE
I think you can do it.
Yeah, I think you can do it.
Wow, that's extremely lucky.
Yeah, it did.
You're right.
It's fine.
I think I need to buy some stuff for us.
It's fine.
It needs to be fast, hopefully.
It's better to support, yeah.
Well, let me go see ya.
OK, thank you very much.
APPLAUSE