WEBVTT

00:00.000 --> 00:09.680
I'm assuming it's chosen because he was on kind of vanity project or just because they

00:09.680 --> 00:11.640
catered like it.

00:11.640 --> 00:17.140
With this, I want to answer to this with the idea that, no, I'm glad it's interesting,

00:17.140 --> 00:19.440
especially because he uses a say that.

00:19.440 --> 00:24.560
And maybe if I can convince you, maybe you guys should try it too for your next

00:24.560 --> 00:26.680
projects.

00:26.680 --> 00:31.480
So, first of all, I know that most people will be familiar with I don't have already.

00:31.480 --> 00:35.760
I've done several talks about it, but I want to cover it with my bases.

00:35.760 --> 00:40.280
I know that it's a positive compatible, partially formally verified cano.

00:40.280 --> 00:41.960
It's hard real time capable.

00:41.960 --> 00:49.800
This means that it has strict scheduling guarantees that it makes its best effort to accomplish.

00:49.800 --> 00:52.880
And it's almost 100% ADA and Sparkle.

00:52.880 --> 00:57.680
I see almost 100% because a semi-operating system requires some assembly code.

00:57.680 --> 01:03.160
It has some C code as well for things like an AML interpreter,

01:03.160 --> 01:09.760
because there is an extreme workload and all the libraries that do that for the space handwritten in C.

01:09.760 --> 01:15.120
And it's free as you're free to use in the GPL with three license.

01:15.120 --> 01:18.880
One makes ironclad special, it's mostly three things.

01:18.880 --> 01:24.560
It's mandatory access control, the real-time guarantees that I mentioned,

01:24.560 --> 01:29.520
which are done without compromising general purpose computing.

01:29.520 --> 01:33.280
And the pragmatic form of verification you see in Spark.

01:33.280 --> 01:37.200
I won't talk much about the first two points,

01:37.200 --> 01:40.320
because it's mostly an ADA token, if you can't afford to talk much about it.

01:40.320 --> 01:45.440
This is them internals, when it's mostly about language stuff.

01:46.320 --> 01:49.520
But I do have for the resources that I will talk about at the end.

01:49.520 --> 01:51.520
If you guys want to check them out.

01:54.000 --> 01:56.640
Lastly, talking about the project, I don't play this only, I care no.

01:56.640 --> 02:00.400
Those of you that work with Linux distributions must be familiar with this.

02:00.400 --> 02:03.840
I don't play this is the same distribution method.

02:03.840 --> 02:08.720
I don't play this only, I want to mix it with new tools,

02:08.800 --> 02:12.400
XORG, AliveC, to make a complete system.

02:13.680 --> 02:16.800
They made distribution, I don't plan, not the only one,

02:16.800 --> 02:22.400
but the main and open source one is GULAR, which is the one that is trying this presentation right now.

02:23.120 --> 02:30.320
Which is a mix of XORG, no user space tools, and the MVC, which is made by the Maraghan project.

02:33.280 --> 02:35.280
So where was it actually for I don't plan?

02:36.240 --> 02:38.160
It's a mix of three things mostly.

02:38.160 --> 02:41.040
It's the form verification of Spark.

02:42.000 --> 02:46.720
The fact that I don't have quite interesting set of challenges,

02:46.720 --> 02:49.280
we felt them better development and having to mix form

02:49.280 --> 02:52.960
really far enough for my verified code, that ADA approach is best.

02:54.000 --> 02:57.920
And the fact that the specifications and tools are fully open source.

03:00.080 --> 03:03.120
Before being an ADA developer, I was mostly a CD developer, and it's

03:03.120 --> 03:06.000
yes, so nice to be able to have all the specifications, yes,

03:06.000 --> 03:08.880
the reach of your hands is the high-to-play harness of euros for

03:10.080 --> 03:11.040
a specification.

03:13.840 --> 03:17.280
So going into why form verification is so important for I don't plan.

03:17.280 --> 03:19.920
What I mentioned the three things that make a run class special,

03:19.920 --> 03:23.680
it's really not that true that the three things have the same weight.

03:24.240 --> 03:28.960
When we talk about form verification, form verification is a foundation for everything else that we build on the kernel.

03:29.680 --> 03:34.640
Form verification basically allows us to guarantee that we don't have runtime errors,

03:34.640 --> 03:38.800
and check the conditions that we set up on the code.

03:38.800 --> 03:41.600
And with that we can verify that actually mandatory access control,

03:41.600 --> 03:45.440
that's what we want, that the real-time guarantees are accomplished that we want.

03:46.160 --> 03:50.640
And it just gives us this full set of tools that we can use to accomplish this.

03:50.640 --> 03:52.640
That wouldn't be possible with form verification.

03:52.640 --> 03:59.360
And when it comes to other languages, really, the competition is not that close in terms of form verification.

04:00.400 --> 04:05.520
C++ family languages have robust standards, even though you have to pay for them.

04:06.560 --> 04:07.440
It is where it is.

04:07.440 --> 04:12.640
And good open source tool change, DCC client, all the biggest tools had all C-centric.

04:13.280 --> 04:18.720
The problem though is that it has no language surface safety facilities, which makes form verification of CX extremely hard.

04:19.280 --> 04:26.960
I'll see form verifiers are either obscure, non-existent, or you have to pay 20,000 euros a month to use them,

04:27.680 --> 04:29.680
with big problem.

04:32.240 --> 04:35.600
When it comes to RAS, there are big options that everyone just knows me.

04:35.600 --> 04:37.360
Well, why did you not do I don't claim RAS?

04:38.000 --> 04:40.000
It has a really good community and force code.

04:40.000 --> 04:43.760
So it's just in that I really wish that we had in a really good strong force code.

04:44.480 --> 04:46.240
And it has a really good public image.

04:46.320 --> 04:51.920
When you mentioned RAS, people already think about safety, people already think about these things,

04:51.920 --> 04:57.520
that they don't really think about as much when you mentioned it, just because it's not as much in the spotlight.

04:58.960 --> 05:02.720
The main point is with RAS, though, is the very backbone standards.

05:02.720 --> 05:09.600
I see very bones because ferocene exists, but really it's not a RAS specification.

05:10.160 --> 05:15.760
It's basically a separate project that just very fizeset of tools used for RAS.

05:16.320 --> 05:20.320
With our concrete specification, but it really does not reflect on RAS.

05:21.120 --> 05:25.040
The very first I very mature in previous talks, we heard about kami.

05:25.040 --> 05:29.440
I said, to that I have to add personally, I was not really that safe.

05:30.640 --> 05:34.720
Much in terms of the features that spark offers.

05:36.240 --> 05:38.720
I would also have to use RAS, then I will not develop on that point.

05:39.680 --> 05:44.960
And then you can say that, I know that we have all the logo with the coin.

05:44.960 --> 05:47.120
I just really like the balance, I'm sorry about that.

05:48.480 --> 05:51.120
It has really robust standards and really good open source tool chains.

05:52.240 --> 05:57.440
And spark really is state of the argument it comes to open source form of verification.

05:57.440 --> 06:00.560
The only problem that it has has to do is that it has a really thin community.

06:01.600 --> 06:03.920
And much of it is not centered on open source.

06:03.920 --> 06:09.920
I will not talk with you.

06:09.920 --> 06:14.320
I will not tell you all the stuff of how spark works after five talks talking about it.

06:16.000 --> 06:20.080
Basically, all the important stuff is that it has free and post-conditions.

06:20.080 --> 06:22.960
It has the whole control, check and flow.

06:22.960 --> 06:30.480
And for what I want to talk following this is that all of this has to be written.

06:30.640 --> 06:33.040
So I think that you have to go out of your way to do.

06:33.040 --> 06:37.440
And it takes a lot of effort, especially when we talk about operating system code.

06:37.440 --> 06:42.000
When you have a mix of formally, you find a formally verified code, hardware interaction.

06:42.960 --> 06:48.480
And all of this brings me to talk about how formalification in the terms of

06:48.480 --> 06:50.320
operating system codes is extremely hard.

06:51.360 --> 06:54.560
Those of you that are into the field will also know about SL4,

06:55.200 --> 06:59.920
which is a microchernal, similar in scope of verification to what I don't quite want to do.

07:00.080 --> 07:05.760
And the report that it takes around 20% years to verify 10,000 lines of C.

07:07.200 --> 07:09.680
For our case, it's a bit better because we use a data.

07:09.680 --> 07:13.040
It already puts us in a better position when it comes to formally verified and C.

07:13.600 --> 07:16.960
But still, the scope is much better with ironclad ironclad.

07:16.960 --> 07:19.920
It's a full-possious, cannot influence all-possious behavior.

07:19.920 --> 07:23.680
It's not a microchernal that only has to manage stock with win servers.

07:23.680 --> 07:30.160
So we do have to pick our battles if we want to finish.

07:30.160 --> 07:34.080
It's a good time in August, it's a form of verification before we go into retirement.

07:35.920 --> 07:39.840
Basically, how we start is that we start from the things that are closer to userland.

07:39.840 --> 07:44.320
That will be process management, matrices, continuity, and we work all the way back

07:45.360 --> 07:49.360
from higher to lower priority to the things that are closer to the hardware.

07:49.360 --> 07:53.120
That will be going from the scale of logic to internal kernel access.

07:54.640 --> 07:58.640
Thankfully, that helps us with Spark mode off.

07:58.640 --> 08:05.520
That makes a modified data module, a modified specifications.

08:05.520 --> 08:11.520
That makes a much to be able to delegate a bit of the work for later.

08:11.520 --> 08:16.560
And we are supposed to save interfaces for and save code.

08:17.840 --> 08:19.360
But there is more to it than Spark.

08:19.920 --> 08:26.480
Hardware developers are initially these set of slides where hardware developers are

08:26.480 --> 08:30.080
sadists. I was told that I should not be putting that for them

08:31.440 --> 08:33.520
presentation, so we just left it at silly.

08:34.560 --> 08:41.280
This is a part of a HCI, which is the protocol used for Satan, similar disk access.

08:41.920 --> 08:45.280
You will notice, and I don't know how will it will translate from afar, but

08:45.920 --> 08:48.800
has several fields that are like three for bits.

08:48.800 --> 08:52.320
It's a whole mismatch of types, only the name of saving space.

08:54.080 --> 08:56.320
But language is struggle a lot to represent this.

08:56.320 --> 08:59.280
See, for example, you have to use bitfills, bitfills that are

09:00.960 --> 09:05.040
a mine field for issues regarding NDNs,

09:05.040 --> 09:07.040
for issues regarding the crankiness to use.

09:08.240 --> 09:10.640
This solution is not really ideal.

09:10.960 --> 09:16.720
Rust still up has no way to represent this.

09:18.640 --> 09:21.440
This is a great created by a user that represents this behavior.

09:21.440 --> 09:24.160
But again, this is not meant by the Rust community.

09:24.160 --> 09:29.200
It has no way on the specification of Rust or ferros into do this.

09:30.080 --> 09:34.000
And you still have problems of type safety, like you're reducing the

09:34.960 --> 09:37.920
use size, which is a 64-bit type to four bits.

09:37.920 --> 09:39.680
It's just a mess in terms of type safety.

09:42.880 --> 09:45.360
In the meantime, the ADA just handles it perfectly.

09:45.360 --> 09:48.960
You can define your types with your own bitlinks.

09:48.960 --> 09:53.280
You can compose them using record representations,

09:53.280 --> 09:59.040
and it just handles all of this flawlessly without the pain that the other languages have.

09:59.920 --> 10:04.640
With that, as well, we come to ADA runtime,

10:04.640 --> 10:11.440
which I think is the biggest reason as to why ADA does better to operate

10:11.440 --> 10:14.720
existing work when compared with other languages.

10:15.440 --> 10:22.480
When we think about language runtime, most of them we think about monolithic blocks,

10:22.480 --> 10:25.040
where we cannot negotiate anything with the language.

10:25.040 --> 10:27.920
When it comes to it, although we have the whole set of restrictions,

10:28.000 --> 10:31.280
let's speak and choose what we want to the runtime to be able to do an implement.

10:32.000 --> 10:35.440
So if you want to operate it, use the runtime in a stage where you

10:35.440 --> 10:39.200
don't have memory allocation yet, you can just disable that for the time being,

10:39.200 --> 10:44.560
or disable the whole floating point subsystem for the whole kernel,

10:44.560 --> 10:46.320
as we do for performance reasons.

10:48.560 --> 10:54.320
And truly, this is one of the best things when it comes to adaptation of ADA into

10:54.320 --> 10:56.000
where conditions we run times.

10:59.360 --> 11:01.520
Without I wanted to come to the presentation.

11:01.520 --> 11:04.560
If you guys want to follow progress of the project,

11:04.560 --> 11:07.360
check the source code, download your own distribution for testing.

11:07.360 --> 11:09.360
You can go to ironclad.nongo.org.

11:10.960 --> 11:14.400
And I would like to thank these organizations,

11:14.400 --> 11:16.960
the free software foundation is at core and the limit of good loader,

11:16.960 --> 11:19.200
which is a good loader that uses that color uses,

11:19.200 --> 11:23.680
along with the internet foundation for giving us funding at resources to continue the project.

11:24.720 --> 11:28.480
And I would also like to thank these people, as well.

11:39.760 --> 11:41.760
Do you think you might have a memory to view it?

11:41.760 --> 11:43.920
Yeah, and then they can start.

11:43.920 --> 11:44.560
Hmm?

11:44.560 --> 11:47.920
I guess I have a more memory to view it like you are into any video.

11:47.920 --> 11:49.120
Oh, yeah.

11:49.120 --> 11:52.720
Well, I guess that I could also do a little showcase of the operating system.

11:53.680 --> 11:56.960
So all of this is glow art itself.

11:56.960 --> 12:00.720
It features terminus, file managers,

12:00.720 --> 12:08.720
it just was the pretty unlucky datation of serenity crashes.

12:11.040 --> 12:13.680
Well, this one, yeah, any questions?

12:14.160 --> 12:16.160
Hmm?

12:20.160 --> 12:22.160
Well, you, well, you, I do a question.

12:22.160 --> 12:24.160
I will just reboot the real thing.

12:26.720 --> 12:28.240
Go ahead.

12:28.240 --> 12:32.640
Do you know how many people are into your operating system?

12:32.640 --> 12:36.240
So we know of the question was,

12:36.240 --> 12:40.080
how if whether we know how many people are using the operating system,

12:40.560 --> 12:44.800
we are aware of distributions that are made by all the people

12:44.800 --> 12:48.640
for their own uses, some of the internal testing that companies.

12:48.640 --> 12:50.640
So there are some hobbies, these are several,

12:50.640 --> 12:53.040
they're used to operating system.

12:53.040 --> 12:55.520
But we don't have really cannabis, we don't have any kind of telemetry

12:55.520 --> 12:56.960
that let's not know about that.

12:59.760 --> 13:01.600
Any other questions?

13:01.600 --> 13:05.280
What is the source of time, the user director's question

13:05.280 --> 13:07.520
out there for the source of time?

13:07.520 --> 13:13.200
So the question was whether we selected any specific hardware

13:13.200 --> 13:16.240
for the, I didn't hear the, well, the last part was

13:16.240 --> 13:18.000
for the implementation of the operating system,

13:18.000 --> 13:25.200
or for the source of time, for the source of time.

13:25.200 --> 13:28.640
So the person architecture, I don't have supposed to architecture,

13:28.640 --> 13:31.200
six, six, six, and three, five.

13:31.200 --> 13:34.560
For X-X-X, we use the H-Pet as well as the LAPIC

13:34.560 --> 13:37.520
internal timer.

13:37.520 --> 13:44.800
LH-Pet for high precision time keeping,

13:44.800 --> 13:47.360
for things like counter calibration,

13:47.360 --> 13:51.200
and the LAPIC we use it for day to day tasks,

13:51.200 --> 13:53.520
like checking intervals.

13:53.520 --> 13:58.240
And for risk five, the port is not far enough yet to what I can give

13:58.240 --> 14:02.000
a comfortable answer.

14:02.000 --> 14:03.840
Any other questions?

14:08.560 --> 14:13.520
But I will try this.

14:13.520 --> 14:18.640
I will definitely try.

14:18.640 --> 14:24.640
It's actually really, I was joking with another project,

14:24.640 --> 14:28.080
where is it, it's perfectly fine.

14:28.080 --> 14:50.480
Yes, I'm going to take a bit.

14:50.480 --> 14:52.240
OK, terrible.

14:52.240 --> 14:56.080
So this is Gluar, I assume that the introduction

14:56.080 --> 15:00.960
had to be to the actual features had to be with the display manager

15:00.960 --> 15:01.600
crashing.

15:01.600 --> 15:06.240
But they say that it's running XOR has its own file

15:06.240 --> 15:11.840
managers that would be the files for the slides that I used.

15:11.840 --> 15:14.640
It also has its own applications that are

15:14.640 --> 15:16.400
ported from other Linux distributions,

15:16.400 --> 15:23.680
like calculators, screenshots, features, also a few games that I will run

15:23.680 --> 15:28.160
in GLX gears by popular demand.

15:28.160 --> 15:30.000
Those they are.

15:30.000 --> 15:33.360
APPLAUSE

15:33.360 --> 15:37.200
Those are features, features solider as well,

15:37.200 --> 15:40.400
along with other games.

15:40.400 --> 15:43.680
Has, again, terminal regulators where you can do

15:43.680 --> 15:49.920
the typical Linux ritual of doing a near-fetch.

15:49.920 --> 15:53.600
That's it, it's just a fully-fetched, general purpose operating system.

15:53.600 --> 15:55.440
APPLAUSE

15:55.440 --> 15:57.440
APPLAUSE

15:57.440 --> 15:58.960
I think you can do it.

15:58.960 --> 16:01.440
Yeah, I think you can do it.

16:01.440 --> 16:04.480
Wow, that's extremely lucky.

16:04.480 --> 16:06.400
Yeah, it did.

16:06.400 --> 16:08.800
You're right.

16:08.800 --> 16:09.760
It's fine.

16:09.760 --> 16:11.840
I think I need to buy some stuff for us.

16:11.840 --> 16:12.400
It's fine.

16:12.400 --> 16:13.760
It needs to be fast, hopefully.

16:13.760 --> 16:15.280
It's better to support, yeah.

16:15.280 --> 16:17.280
Well, let me go see ya.

16:17.280 --> 16:19.280
OK, thank you very much.

16:19.840 --> 16:21.840
APPLAUSE

16:26.640 --> 16:29.120
APPLAUSE