WEBVTT 00:00.000 --> 00:24.880 So, hello everyone, I'm Christian, even though I go in the internet as strictso, and I wanted to talk to 00:24.880 --> 00:31.720 today about my experience developing devices for Ironclad, using ADA. 00:31.720 --> 00:36.040 The agenda for this talk is going to be short and concise, going to be what is Ironclad. 00:36.040 --> 00:41.040 We will see that chosen for the kernel, the reasons why I chose it, and how I apply this 00:41.040 --> 00:45.880 on device drivers with examples, but most of all, what I wanted to do with this talk is 00:45.880 --> 00:51.000 give our counter argument to the idea that has spread on the internet, and what Ironclad 00:51.000 --> 00:57.280 is like it's like lived effects in it, which is part of Corbwood, which are projects 00:57.280 --> 01:03.680 that take spaces that are usually occupied by price made in C or C++, and people approach 01:03.680 --> 01:08.440 projects like this with the idea of, the price is interesting, but sadly they are written 01:08.440 --> 01:09.440 in ADA. 01:09.440 --> 01:14.280 I'm assuming chosen because it was some kind of vanity project, or just because they gave it 01:14.280 --> 01:20.760 or liked it, with this I want to answer to this, with the idea that, no, Ironclad 01:20.760 --> 01:26.360 is interesting, especially because it uses ADA, and maybe if I can convince you, maybe 01:26.360 --> 01:31.000 you guys should try it for your next projects. 01:31.000 --> 01:36.280 So first of all, I know that most people will be familiar with Ironclad already, I've done 01:36.280 --> 01:39.640 several talks about it, but I want to cover it with my bases. 01:39.640 --> 01:44.680 Ironclad supports this compatible, but surely for my verified kernel. 01:44.680 --> 01:49.640 It's hard real time capable, this means that it has strict scheduling guarantees that it 01:49.640 --> 01:57.800 makes it's best effort to accomplish, and it's almost 100% ADA and Sparkle, I see almost 01:57.800 --> 02:02.800 100% because a similar operating system requires some assembly code, it has some 02:02.800 --> 02:10.520 C code as well for things like an AML interpreter, because there is an extreme workload 02:10.520 --> 02:15.240 and all the libraries that do that for the space handwritten in C, and it's free as in 02:15.560 --> 02:20.120 the GPL with three license. 02:20.120 --> 02:27.000 One makes Ironclad special, it's mostly three things, it's mandatory access control, the 02:27.000 --> 02:32.600 real-time guarantees that I mentioned, which are done without compromising general purpose 02:32.600 --> 02:37.720 computing, and the pragmatic form of verification you see in Spark. 02:37.720 --> 02:43.240 I want to talk much about the first two points, because it's mostly an ADA token, if you 02:43.320 --> 02:48.440 offer to talking much about the operating system in Ternos, when it's mostly about language 02:48.440 --> 02:54.440 stuff, but I do have for the resources that I will talk about at the end, if you guys want to 02:54.440 --> 02:57.240 check them out. 02:58.440 --> 03:02.280 Lastly, talking about the project, Ironclad is only a kernel, those of you that work with 03:02.280 --> 03:08.280 Linux distributions must be familiar with this, Ironclad uses the same distribution method, 03:08.280 --> 03:13.080 I don't know why it's only a kernel, I want it to mix it with new tools, 03:13.080 --> 03:16.760 XORG, I'll leave say, to make a complete system. 03:18.040 --> 03:23.400 The main distribution, I don't plan, not the only one, but the main and open source one is 03:23.400 --> 03:29.800 Glower, which is the one that is trying this presentation right now, which is a mix of XORG, 03:29.800 --> 03:34.680 no user space tools, and the MVC, which is made by the MNG project. 03:35.240 --> 03:43.240 So, we will see that chosen for Ironclad, it's a mix of three things mostly, it's the 03:43.240 --> 03:51.160 form verification of Spark, the fact that Ironclad has quite interesting set of challenges, 03:51.160 --> 03:54.040 with all the embedded development, and having to mix for one of the very far, 03:54.040 --> 03:59.960 I don't know, for a very, very wide code, that ADA approach is best, and the fact that the 03:59.960 --> 04:05.720 specifications and two genes are fully open source, before being an ADA developer, 04:05.720 --> 04:10.040 I was mostly a CD developer, and it's, yes, so nice to be able to have all the specifications, 04:10.040 --> 04:15.400 yes, the reach of your hands is the high to pay hundreds of euros for a specification. 04:18.280 --> 04:21.640 So, going into wide form verification is so important for Ironclad, 04:21.640 --> 04:26.200 what I mentioned, the three things that make Ironclad special, it's really not that true, 04:26.200 --> 04:29.960 that the three things have the same weight. When we talk about form verification, 04:29.960 --> 04:33.320 form verification is a foundation for everything else that we build on the kernel. 04:34.040 --> 04:39.000 Form verification basically allows us to guarantee that we don't have runtime errors, 04:39.000 --> 04:44.600 and check the conditions that we set up on the code, and with that we can verify that 04:44.600 --> 04:48.280 actually mandatory access control, that's what we want, that the real-time guarantees are 04:48.280 --> 04:54.440 accomplished that we want, and it just gives us this full set of tools that we can use to accomplish 04:55.080 --> 05:00.600 that wouldn't be possible with a form verification. When it comes to other languages, 05:00.600 --> 05:03.800 really the competition is not that close in terms of form verification. 05:04.840 --> 05:09.800 Cc++ family languages have robust standards, even though you have to pay for them, 05:11.000 --> 05:16.040 it is where it is, and good opportunity to start a change, GCC client, all the biggest tools 05:16.040 --> 05:20.520 are all systemic. The problem though is that it has no language surface safety facilities, 05:20.600 --> 05:27.160 which makes form verification of Cx extremely hard. I'll see form verifiers are either of 05:27.160 --> 05:34.040 skewer, non-existent, or you have to pay 20,000 euros a month to use them, with big problem. 05:36.600 --> 05:40.360 When it comes to rest, there are big options that everyone just knows me. Well, 05:40.360 --> 05:44.360 why did you not do viral client rest? It has a really good community and force code. 05:44.360 --> 05:48.200 So it's just in that really which that we have in a really good strong force code. 05:48.920 --> 05:53.720 And it has a really good public image. When you mention rest, people already think about 05:54.440 --> 05:58.920 safety, people already think about these things that they don't really think about as much 05:58.920 --> 06:04.520 when you mention it, just because it's not as much in the spotlight. The main point is we 06:04.520 --> 06:09.960 rest, though, is the very backbone standards. I see bare bones because ferros in excess, but 06:10.920 --> 06:18.600 really is not a rest. Specification is basically a separate project that just very 06:18.600 --> 06:24.680 fastest set of tools is for rest, with a concrete specification, but it really does not reflect on rest. 06:25.480 --> 06:29.960 And the very first, I'm very mature. In previous talks, we heard about kami. I said, 06:29.960 --> 06:38.360 to that I have that personally, I was not really that safe. Much in terms of the features that 06:38.440 --> 06:43.080 spark offers. I would also have to use rest and I will not develop on that point. 06:46.520 --> 06:49.880 Then you can say that, I know that we have all the logo with the coin. I just 06:49.880 --> 06:54.360 really like the balance, I'm sorry about that. It has really robust and that's a really good 06:54.360 --> 07:00.600 open source tool change. And spark really is state of the argument it comes to open source 07:00.600 --> 07:04.120 form of verification. The only problem that it has has to do is that it has a really 07:04.120 --> 07:14.840 thing community. And much of it is not centered on open source. I will not talk with you. I will not 07:14.840 --> 07:21.160 tell you all the stuff about how spark works after five talks talking about it. But basically 07:21.160 --> 07:26.440 all the important stuff is that it has three and post conditions, it has the whole control, 07:26.440 --> 07:32.440 check and flow. And for what I want to talk following this is that all of this has to be 07:34.280 --> 07:39.080 written. So I think that you have to go out of your way to do. And it takes a lot of effort, especially 07:39.080 --> 07:44.120 when we talk about operating system code, where you have a mix of form of refinery, form of 07:44.120 --> 07:50.120 verify code, hardware, interaction. And all of this brings me to talk about how 07:51.240 --> 07:56.360 form of verification in the terms of operating system code is extremely hard. Those of you that 07:56.360 --> 08:02.760 are into the field, we also know about SL4, which is a microcarnal, similar in scope of verification 08:02.760 --> 08:09.640 to what item code wants to do. And the report that it takes around 20% years to verify 10,000 lines 08:09.640 --> 08:15.720 of C. For an case of it better, because we just say that, it already puts us in a better position, 08:15.720 --> 08:20.920 when it comes to form of a very fine density. But still, the scope is much better with ironclad 08:20.920 --> 08:25.160 ironclad, it's a full-possious, cannot influence all-possious behavior, it's not a microcarnal, 08:25.160 --> 08:33.800 that only has to manage stock between servers. So, we do have to pick our battles, if we want to 08:33.800 --> 08:38.440 finish, put ironclad in a good state of form of verification before we go into retirement. 08:40.360 --> 08:44.200 Basically, how we start is that we start from the things that are closer to userland, 08:44.200 --> 08:48.760 that will be process management, matrices, continuity, and we work all the way back 08:49.720 --> 08:54.840 from higher to lower priority to the things that are closer to the hardware. That will be 08:54.840 --> 09:02.520 going from the scale of logic to internal kernel access. Thankfully, that helps with Spark mode 09:02.520 --> 09:06.920 off, that let's say to me, it makes, I'm very tired, I'm all used, I'm very tired. 09:09.160 --> 09:16.040 Specifications, I make some much them into being able to delegate a bit of the work for later. 09:16.040 --> 09:23.640 And we expose safe interfaces for unsafe code. But there is more to it than Spark. 09:25.400 --> 09:30.920 Hardware developers are, initially this set of slides where hardware developers are 09:30.920 --> 09:34.440 say this, I was told that I should not be putting that for them, 09:35.800 --> 09:43.240 presentation, so we just left it that silly. This is a part of a HCI, which is the protocol used for 09:43.240 --> 09:49.560 Satan, similar this access. You will notice that I don't know how well it will translate from afar, 09:49.560 --> 09:55.480 but has several fields that are like three for bits, it's a whole mismatch of types only, 09:55.480 --> 10:01.480 the name of saving space. But language is struggle a lot to represent this. See, for example, 10:01.480 --> 10:09.400 you have to use bit fields, bit fields that are, I'm in field for issues regarding NDNs, 10:09.480 --> 10:15.000 for issues regarding the encircness to use, this solution is not really ideal. 10:17.800 --> 10:25.000 Last step has no way to represent this. This is a great created by a user that 10:25.000 --> 10:29.560 represents this behavior, but again, this is not meant by the risk community, it has no way 10:29.560 --> 10:36.760 on the specification of rest or frozen to do this. And you still have problems of type safety, 10:36.760 --> 10:43.400 like you're reducing there are use size, which is 64 bit type to four bits, it's just a mess in terms 10:43.400 --> 10:50.600 of type safety. In the meantime, the ADA just handles it perfectly, you can define your 10:50.600 --> 10:57.720 types with your own bit lengths, you can compose them using record representations, 10:57.720 --> 11:03.400 and it just handles all of this flawlessly without the pain that the other languages have. 11:06.760 --> 11:13.000 With that as well, we come to ADA runtime, which I think is the biggest reason as to why ADA does 11:13.000 --> 11:22.200 better to operate existing work is when compared with other languages. When we think about about 11:22.200 --> 11:28.440 language runtime, most of them we think about monolithic blocks, where we cannot negotiate anything 11:28.440 --> 11:32.680 with the language. But it goes to it, although we have the whole set of restrictions that let's 11:32.760 --> 11:37.240 speak and choose what we want to the runtime to be able to do an implement. So if you want to 11:37.240 --> 11:42.680 operate it, use the runtime in a stage where you know how memory allocation yet, you can just disable 11:42.680 --> 11:49.400 that for the time being or disable the whole floating point subsystem for the whole kernel as we do 11:49.400 --> 11:57.400 for performance reasons. And truly this is one of the best things when it comes to adaptation of 11:57.400 --> 12:05.800 ADA into weird conditions, weird runtime. Without I wanted to come to the presentation, 12:05.800 --> 12:10.200 if you guys want to follow progress of the project, check the source code, download your 12:10.200 --> 12:17.400 distribution for testing. You can go to ironclad.nong new.org and I would like to thank these 12:17.400 --> 12:21.640 organizations, the free server foundation, either core and the limit good loader, which is a 12:21.880 --> 12:27.080 loader that uses that color uses along with the internet foundation for giving us funding and resources 12:27.080 --> 12:32.920 to continue the project. And I would also like to thank these people as well. 12:52.520 --> 12:58.840 Oh, yeah. Well, I guess that I could also do a little showcase of the operating system. So all of this 12:58.840 --> 13:07.800 is glow art itself. It features terminus, file managers, it just was the 13:07.800 --> 13:15.320 data. Pay the lucky data as soon as the reality crashes. 13:15.320 --> 13:20.600 Well, this one. Yeah, any questions? 13:24.600 --> 13:27.400 Well, you, well, you, I do a question. I will just reboot it. 13:27.400 --> 13:42.840 Okay. Go ahead. So we have, we know of the question was, if whether we know how many people 13:42.840 --> 13:47.800 are using the operating system, we are aware of distributions that are made by 13:48.600 --> 13:53.720 all the people for their own uses, some of the internal testing at companies. So there are some 13:53.800 --> 13:58.040 hobbies, do you sense how well they use the operating system? But we don't have really 13:58.040 --> 14:04.760 cannabis, we don't have any kind of telemetry that let's not know how it does. Any other questions? 14:11.800 --> 14:19.640 So the question was whether we selected any specific hardware for the, I didn't hear 14:19.640 --> 14:22.920 well, the last part was for the implementation of the operating system or for the, 14:26.920 --> 14:31.320 for the source of time, for the source of time. Okay. So the person architecture, 14:31.320 --> 14:37.640 I don't have supposed to architecture, six, six, six and three, five. For X36, we use the HPEAT 14:37.640 --> 14:49.400 as well as the LAPIC Interattimer, the HPEAT for high precision timekeeping, for 14:49.400 --> 14:56.120 things like counter calibration and the LAPIC, we use it for day to day tasks, like checking 14:56.120 --> 15:03.320 intervals. And for for risk five, the port is not far enough yet to what I can give a comfortable 15:03.320 --> 15:18.760 answer. Any other questions? But I will try this. I will definitely try. 15:20.040 --> 15:29.480 Uh, it's actually really, I was joking with, with another project. Where is it? 15:29.480 --> 15:30.760 Race at perfectly fine. 15:40.680 --> 15:41.640 Yes, we're going to take a bit. 15:49.400 --> 16:01.960 Okay, there we go. So this is glad, uh, shame that the introduction had to be, to the actual 16:01.960 --> 16:07.800 features had to be with, uh, the display manager crashing, but this is it. It's running 16:07.800 --> 16:15.640 XOR has its, has its own file managers, uh, that would be the files for the slides that I used, 16:15.960 --> 16:20.680 uh, it also has its own applications, uh, that are ported from other Linux distributions, 16:20.680 --> 16:29.880 like calculators, clean shooters, features, also a few games that I will run GLX gears by popular demand. 16:32.520 --> 16:33.160 Those they are. 16:33.400 --> 16:35.400 Thank you. 16:37.720 --> 16:42.760 Also, features features soliter as well, along with other games. 16:44.760 --> 16:50.760 Has again, terminal regulators where you can do the typical Linux ritual of the in a new 16:50.760 --> 16:57.560 fetch, uh, that's it. It's just a fully featured general purpose operating system. 17:03.400 --> 17:14.680 Yeah. Wow, that's, extremely lucky. Yeah, it did. You read. It's fine. I think I didn't 17:14.680 --> 17:20.280 various months ago, for us. It's fine. It's better. It's better. It's better, so, well, yeah, well, yeah.