Gernot Heiser | SeL4: Formal Proofs for Real-World Cybersecurity

10:38AM Oct 19, 2021

Speakers:

Keywords:

seo

hardware

security

people

kernel

attacks

system

scale

proof

systems

proofs

terms

capability

problem

technology

operating system

functional correctness

model

software

build

Thank you for joining everyone. And welcome to foresight intelligent preparation group. Granted, I really can't tell you how long and how much and this group has looked forward and welcome to welcoming because whenever someone is asking me about concrete things that are implementable today, that could build Intelligent Systems of voluntary cooperation in something that would just something that this group is interested in, then something that comes to mind is SEO for and in this group, and in the company book draft, we will go from the premise that any desirable future will we be rely on computer security at every level, from hardware to operating system to software, all the way to the user interface. And, you know, it's essential for a variety of things, including de risking cooperation, but also preventing essential attacks for from automated autom automated webinars, mobile technologies, and so forth, things that we all discussed you in the past. So I think SEO boys, we need like a key, if you wish, for making sure that all of these technologies, amble well, and so we're really, really excited to have you here today. I'm very, very excited also to talk about perhaps I'm failing time, even how ncfr I will start with a regime attack with such a good rating that attackers couldn't even make progress on hearing out how to how to make progress on attacking so far. So thank you so much, everyone, for joining. And we look really much very much forward to presentation and to this session afterwards. So thanks.

Alright, so the SEO for microkernel is it's really about mathematically proving properties of a real world software system, in particular security relevant fonts. So what is SEO for? It's an open source, high assurance, high performance operating system microfil. So, kernel means it's the part of the software that runs in the most privileged mode of the hardware. And that implies if it gets compromised, and everything else is compromised, because the kernel there's no no protection against what the kernel that's operating system microkernel, meaning it's the core of an operating system. So you build an operating system on top of this grid. It's high performance, whoops, I claim it's the world's fastest microkernel. There's some partial evidence of that another complete proof. And it's high assurance. And this is really what what is SEO for is famous for in that it's the world, the operating system kernel with the most comprehensive mathematical vision story. And the cool thing, of course, is it's open source. So it's really available on the GitHub. And that doesn't apply only to the kernel itself to the code. But also the the proofs everything is open source. And such as 04 is arguably the most trustworthy foundation for building safety or security critical systems. And this is happening increasingly so people are deploying and CFO already in deployment or working on products that are going to be deployed across a very large range of domains, including automotive, which is presently apparently the holdest. area. avionics, space defense depends of causes where it's your hole was initially employed, mostly people deployed because they are the most security paranoid, IoT, industrial automation, everything. So it's, it's really taking off unnecessary, particularly the automotive sector. And we have this SEO Foundation, which was created the and a half ago, and it had a very strong influx of automotive companies this year, generally, companies operating on autonomous driving cars. And it seems like that's going to be the next big thing. In terms of performance. I said, there's a partial proof in the sense that there's some independent comparisons of performance only against open source systems. These are latency numbers. So smallest good and done by researchers in China, and we had nothing to do with they wrote several papers on using extra hardware support for improving microkernel performance. And they in the cause of that big comparison of SEO for performance against two other microkernels fiasco and Google circle. And you can see from these tables with between a factor of two and 10 pasta. So I and and I know that the non open source or many of the non open source systems, the performance is closer to that of Zircon than that of SEO work. And so I unashamedly make this claim. It's the world's fastest like brutal, and you can find the sources there. But what's important to understand is a microkernel is not an operating system. It's the Cool have an operating system. So in a microkernel based system, you have the TV, operating system services, which is includes storage systems, subsystems, networking, etc. General Resource Management. This is all contained in user level processes that are running side by side with the native applications. So from the kernel point of view, there's no principal difference between an application running on the system and an operating system service. They're all running at user mode unprotected by isolate isolated by the kernel enforce protection boundaries. And the kernels main job is really to switch between those domains, but also enable communication between them. And you can have virtual machines running legacy stacks. In most deployments of SEO for, we see that there's at least one virtual machine running a Linux Operating guest operating system to support the legacy stack and the critical bits running native on CFO.

And one of the not by far not unique characteristics, but the critical characteristic of SEO for is that it has a capability based access control. So capabilities are a abstraction for the managing access rights to objects, you can think of a capability like a key unboxer particular object, and security oriented operating system designs, general use capabilities. And of course, Mark Miller is part of your team. And he is one of the people who've been working in capability based systems for a very long time. So I assume the idea is familiar. And so what that means in ncfr, in particular is that any components that run off the on top of the SEO for microkernel can only communicate in any way if there is an explicit channel provided by that is access by capability. So if you have the capability to such a channel, then you can communicate and otherwise you cannot. So two components that do not have such a capability autolyzed channel are incapable of communicating. And this is called the key to the really strong isolate, not only isolation, but also the ability to enforce system wide security policies in SEO. in a way that's not possible in a system like Linux, for example, even even if the Linux was correct, there are free and safe which of course, it is not. So no communication on this explicitly authorized. That's a classical property of capability systems. But in ACL force case, it comes with the visual strengths that we know that the kernel by a mathematical proof, we know that the kernel will prevent complications if it's not explicitly authorized. And that gets me to what really defines SEO for its mathematical proof story. So SEO for is implemented in the C language. It's about 10,000 lines of code. And besides the C implementation, there is an abstract model. So that there is a description of the functionality of the kernel in a in a mathematical logic. And what we now i have is this proof of functional correctness, which means that the C implementation is a correct implementation of this abstract model. So in that very strict sense, the C, the implementation of the kernel is bug free with respect to this mathematical model of its functionality. And that's the thing that really made SEO famous It was the first time this was done for any operating system. This correct complete function correct the spirit from a mathematical model to the seed stage. That itself is a very powerful property because you know that the SEO implementation is correct against the more it still leaves you at the mercy of the compiler. And compilers themselves are complex species that are full of bugs. GCC for example, which we routinely use is probably a million lines of code all up it said also despite the proximity, and there is a risk of the compiler will introduce bugs in the compiled binary. And so we have various the proof that the C is correctly translated into the binary and by transitivity, we now know that the binary code which is the thing that actually executes on the silicon, Is this correct translation of the abstract all correct implementation of the abstract model. And I got my thinking out of order so that this comments that by now, the origin of functional correctness group was done 12 years ago. By now there's a few other operating system kernels with functional correctness proofs, they generally in the toy category, there's only one I'm aware of that sort of real world capable. The other side academic toys. But finally, what to me surprising the none of these are capability that is so sad, of course, you're still the only verified operating system kernel with capability based access control. And therefore this ability to reason about secure new foods meant in terms of security policies, etc.

And in particular, the least privileged properties are that every component on this given the access rights, it really needs to know more. Okay, so we have this proof chain from the abstract model down to the binary. That is extremely powerful, because it means you can do all through the reasoning at the level of the abstract model, which is much easier to reason about Dinah seep and the patient. But it by itself, it doesn't guarantee that the abstract model has right properties. And for that, we have through the proof chain on set of proofs from the high level security properties of confidentiality, integrity availabilities. So we have proofs that the colonel as represented by the abstract model is able to enforce the security properties. And again, this is before transitivity, we know that this property holds holds for the actual binary that executes on the silicon. Now, all of these proofs are machine checked. Generally using attractive theorem proving except their binary correctness proof is a tool chain, automated. And that's really important, because the, as I said earlier, the same limitations about 10,000 lines of code. The original functional correctness proof done on ARM v six posesses, was about 180,000 lines of proof script. And that just shows you that if those who have pen and paper groups, they would be completely worthless, because they would be more bugs in the proofs and in the code itself. Only by having these proofs machine checked down in this directive theorem, proving framework which does not allow you to make incorrect proofs. Does this all make sense. And by now this proof, the complete proof base we have for ACL core is well above 1 million lines of proof script. When we originated the functional correctness verse, it was considered the second largest proof ever done. It might be the largest by now, but it's certainly by far the largest maintained proof phase over an evolving system so far has changed a lot in 12 years, since we did the original verification, we keep evolving the kernel, because there is ongoing research to improve it to broaden its applicability. And while we're doing this, we follow we keep following with the verification, things are not allowed to be committed against into mainline, if they change, they break the proofs. So the proofs are being kept updated. And it does there's no other system of similar complexity in terms of proofs that has been evolving in such a fashion. There's a number of limitations still, then even after 12 years, we haven't verified the boot code of the kernel. And this is partially because the it's boring, it's batshit. As they say, in Australia. There's there's no, there's nothing interested it's just mind boggling engineering work. We've kept sort of students, best team members working on it in the background, but it's not complete. So someone would have to actually put money on the table to really compete that it's not a big deal to it's just yeah, we needed funded. And there's a few details that are not model to the same degree of faithfulness. So there's, there's some rather abstract models about the memory management unit and acacias in the system that are not done tied down to the instruction set architecture yet. Some of that has been is in principle, fixed or not in practice. There was a PhD thesis recently that explained how to do the formalization of the translation loop about sulfur, so the MMU so that could be integrated with his work. At the moment, we don't have funding or time for. And the we have the complete story for 32 bit ARM processors. For RISC five, we are close to having the complete proof story this is likely to happen later this year. And x86, which has type the functional correctness. And I forgot to put on this list multi core we have a high performance multi code limitation but no verification. So there is still work to be done.

The question is, so what does this really mean? So one is that, okay, we prove this functional correctness, that big kernel behaviors fully captured by the abstract model. And that means any further properties can be proved at the level of the abstract model. And that's a huge improvement because this is in the math, right mathematical logic, where it's much easier to work with. And in particular, explicitly, or implicitly, pretty much all the general attacks on operating systems are provably impossible in SEO for so there's never going to be an assertion failure in the verified kernel is the kernel provably doesn't be reference null pointers or initialized variables. No, I would have found access. So you can't run any stack smashing attacks on SEO for sidebar, it will never run out of resources, because it's called the verified resource management model. You can't fool it into doing stupid things by giving misformed inputs etc. So basically, the whole range of the typical attack vectors against operating systems are categorically impossible in SEO. So that's not. And it really important for us at the beginning, when we started this project, we did not want to use an academic toys people have been misleading in a way the world by doing verification on academic examples, and then pretending the scales and it didn't in the end, we wanted to build and verify a system that was capable for real world deployment right from the beginning, that was my target. And it worked. So it is already deployed primarily in defense systems in the real world. So this is a example of a secure communication device which people can't plug into a laptop that's deployed in various multiple armed forces. And it's approved for use hot dog secure, are classified as up to a classification secret. In terms of the SEO for microkernel, the redwoods scale to top secret but the packaging would have to be much more tamper proof or top secret device. There's this military cross domain destiel composite data that connects to networks of different classification that can be overlaid onto a single screen that's going into commercialization. Now, there is this device which is about to be deployed in a remote power generation station, which is designed for protecting critical infrastructure from cyber attacks. These are a number of products that I know of, and that I can talk about that are out there. And besides that, there's many more, which is your voice being signed into. And one important point about the real world usability was what we learned from the DARPA DARPA hackers program, where we worked with

project partners in the US on securing real world systems and the important thing there existing real world systems. So this is basically proving incorrect, the long held belief that the system has to be designed for security from the start. And it's impossible to retrofit security into the we disprove that in the heavens program. So what we did there, and as I said, most of the work was done by all of our collaboration partners. We worked with autonomous system both here craft as well as ground vehicles, and for each week had a research vehicle and a military vehicle. So the research vehicle for the autonomous aircraft was this off the shelf drone, where which basically we picked the airframe and replaced everything else. So this was a true green field design. And the land vehicle was this GVR board, which is the US Army, robotics reference platform. And they are we could basically play with completely replace everything. We wanted and write a lot of new code. So this was for developing the technology. And then there were the military vehicles. And these were vehicles that already existed. So they the area one is this unmanned littlebird, which is a standard helicopter airframe, which fully converted for autonomous flight. And that was already flying autonomously. And the on the ride, you have these US Army trucks, they are running around Detroit for ovilus. They also existing system and we retrofitted them for security. And the scary thing, even though these are military vehicles, the red team DARPA, hired as part of the project took about two weeks to completely compromised this military helicopter and be working with our partners. And they said the work was mostly non power partners, because the systems that export controls, we weren't even allowed to look at the code. So we can could only instruct them what to do. They retrofitted these systems to put them on to SEO for extract the critical components into protected sandboxes on SEO for leaving a lot of the legacy code and Linux virtual machines. And in the end, the the hackers couldn't compromise the systems anymore. We the red team was in April, he cabled to break the OB, we even gave them root access on one of the Linux virtual machines on the system. So they weren't on the platform had complete control over this Linux system, could plant fog bombs where they were they wanted, they could not affect the operation of the rest of the system. So that was a incredible success story that was playing way better than we had expected initially. So you can check us out. Seo four is not yet done. I indicated some of the holes that we still have insurance story. But there's still a lot of ongoing research and my own behind adding a little bit of that. One is that this is a success on the alpha program, where SEO for in the whole formal methods framework is being integrated in a repeatable system engineering poses. So these are avionics systems builders that they have, they have established processes and tool chains, etc. And the project partners in the davon case program are integrating Uc ofour and other formal methods into this standard engineering tool chains with the idea of scaling it to really develop knob scale, real world systems. So this is a very applied research, I would say. And then there is time protection, which is a principled approach for preventing climate change. So timing channels have been a are now pretty much mainstream started by the specter attacks, where they can compromise security in systems leading to loss of disclose of encryption keys, etc. With timing protection, tough with time protection, we are building abstractions, operating system abstractions, and tying them to hardware improvements that will allow to provably make timing channels impossible. And we already have working prototypes on that we have hardware improvements that show that this can the necessary changes to the hardware have minimal and no overhead both in terms of chip space as well as performance and runtime that allows us to actually do that and we're working on a formal proof that's on a conforming system, we can eliminate these tiny channels completely.

We're also working on making the verification scale. At the moment, this is still a fairly expensive engineering process. Our estimates show that verification of a system like ACL for is about a factor of two to three more expensive than sort of classical industrials standard quality assurance, we want to reduce that cost to park in which case of course it makes no sense to produce and verified software. And the key there is have the right high level languages that are suitable for implementing low level code. But use automate a lot of the assurance and the newest product project we're working on is what we call it back to the future. In the 80s people have really tried to build Complete operating systems with a high assurance or ideally proof that they enforce a security policy and all these projects have failed to various degree. We believe it's time to restart that based on SEO pool and build the prototype of a really general purpose operating system where we can prove that it enforces the system wide security policy. So in summary, with SEO four, we have shown that mathematical proof techniques really scale to real world software. And that's, to me the the most amazing outcome of the whole SEO project. We have shown that provable security for well designed system is actually feasible. And that SEO for is clearly a good basis for building these kind of systems. And and we believe SEO for is basically defining the state of the art and hands. So for the past 12 years, and we're working on keeping it that way. Thank you. happy to take any questions.

Oh, fantastic. I'm so happy you also and tackle the DARPA challenge. Thank you so much. And I'm going to stop sharing your screen for just a moment. I will give first dibs in terms of questions to our participants. And then I'll have a few more for my end. But this was really fantastic. Thanks a lot. It was really comprehensive overview. easy to understand. And yeah, and then pretty inspiring in terms of the results. And Richard, maybe you want to go first and perhaps you want to say a few words about your background, if you care. So good that has some context on it.

Sure, so I mainly come from artificial intelligence on a little bit to do with security for AI or AI security. So not so much at the OS level so much, but I am curious, um, can you describe how Sal four would succumb or not to something like a real hammer attack, which would have behavior outside of that abstract model that you have?

So that's a good question. Whoops. I, I've, I'm sorry, hold

on. Apologies, I got just interrupted. Not sure whether you heard that. So um, yes, I didn't. This the assumptions we have for these proofs are basically that the core assumptions, which of course, are not different from verified software, you have to make the same assumptions plus more, but we have to make the assumption that the hardware operates as specified. And row hammer is actually a hardware box, the hardware violates its contracts, the contract for memory is that if you write something to memory, and you read again, you read the same thing back and throw headless biolage. So there is no change general way of preventing these things. If the hardware is buggy, then it's buggy. Once you know about row hammer, then you can have specific defenses against these by ensuring your memory, the kernel isn't in control of physical memory allocation, and you can allocate memory so we'll hammer attacks will not hit anything sensitive. But that's that requires a model of the buck basically. He showed up that the only real defense against those things is you need to drive verification down into the hardware to ensure that the hardware actually behaves according to specifications. There's no other way on these kinds of things.

And have you have you collaborated with anybody on trying to start to do that kind of thing.

So one of the nice things is that the the highest a as the hardware software contract gives us a very well defined interfaces and to complete controls that property rights our hardware, people can work their bids, we work on Toby understand, which is the software. So I'm taking the easy way out and saying it's someone else's problem. But it basically comes down Yes, we agreed on the ISP as contract and both sides need to ensure that this contract is honored. And we obviously have it will operate with hardware verification people but it's it's not our space. What we have done in the more specifically in the time protection context, where we found that while actually all hardware present hardware is broken, in the sense that it doesn't give you the right model to the right mechanisms for enforcing security, protection against timing channels, then, of course, the conclusion is what. And that's the case, even if the hardware is correctly implemented, kind of. So the conclusion is, well, obviously, our hardware software contract is insufficient, it doesn't allow us to really provide security from timing channels. And that means it needs to be fixed. And we have a proposal published on how to fix the hardware software contract, it's a very moderate modest improvement, you just need to agree to some additional conditions that will not prevent any innovation on the hardware level. I don't think that trying to prevent people from doing speculative execution, it's reasonable, because that will never be accepted. Because the trouble away so much performance. So you need to have a much more, let's say targeted, you need some restrictions, right? You need to agree on additional contestations. But they need to be really as least as as little onerous as possible, and really targeted towards the weak marine climate. We tried to do that. And we work with people at ETH Zurich, the people who did the aviana, open source implementation of risk five processor, and so the group led by Luca Panini, and we could show that with some really very minor changes to the hardware, we create the right conditions that create a process led adheres to this modified contract that allows us to really thank you.

Fantastic. Thank you, David, your questions next?

Yeah, just following along the same line, just understanding more about what sort of hardware This is applicable to? And is it at all possible to apply this technology to defend against adversarial attacks in the hardware supply chain itself? Okay, so in terms of hardware requirements, the requirements of SEO for the hardware is that you have to take the mode basically. So multimode execution and memory, virtual memory. And beyond that correct implementation. So adherence to hardware software contract. Sorry, what was the same part of the equation about adversarial attacks on the hardware supply chain? Oh, yes. Yeah, that comes down to we have to trust that the hardware is implemented correctly, if someone builds a Trojan into the hardware, then all bets are off. As far as we're concerned. I happen to be involved with a company in unique which called penciled cyber, they have produced a RISC five implementation that has a pretty strong supply chain attack protection by using some good encryption or obfuscation if you like. So the idea is that the gates on the surrogate gate have extra inputs, and they only behave correctly if the right set of inputs basic encryption key are supplied. And by that it's infeasible to insert a Trojan because in, in order to insert the Trojan into the hardware in the production process, you need to understand how the circuit is operating. So you can the whole the whole point of a Trojan is it needs, you need to be able to trigger it some. And so there needs to be a way to supply an external input that causes the hardware to change its operation in order to enable this approach. And in order to do that, you need to have a reasonable understanding of how the circuit operates. And by having this encrypted implementation of a circuit that's infeasible. So that the idea is the key actually doesn't need to be extremely strong. It should you just have to be able to not break it. In timeframe. That's enough to understand the circuit reengineer it put the Trojan in, build this netlist again, send it to production and get it back quickly enough. So basically, we're talking about, say, a month or two is all this is key needs to be secure for once chip is produced, then you can publish the key there's no problem with that anymore. So that that's an interesting approach and not a hardware expert. I cannot guarantee that this is really sufficient under all circumstances, but it's certainly much stronger than you get from anything else that see. Thank you Interesting.

Next up, we have Ellen and Ellen, if you want to say word also, but you just said first and context. And

I'm Alan Clark, we have the PhD in astronomy, and the D h, high performance computing for a long time. But when I first got into security, designing a big distributed system for sharing, I'd never heard of capabilities, and I ended up reinventing. And just by chance, today, I'm wearing my granovetter Valley red shirt. Just it was on top of the pot, I'm wondering how the work you're doing relates to what's being done on top of the cherry Hart.

Yeah, so Jerry is of course at a hardware level implementation of capabilities and in the same sense as really a capability hardware had it. Like, going back to the old borrows machine and the four threes, two, etc. So what what Ceri capabilities, at least the last I've seen, I don't know what a whether there was any recent progress or extension of the model, what Jerry capabilities gives you is basically a hardware enforced point of safety. So you can't have stray pointers and compromise your system control flow integrity by basically getting to closing out of found accesses of arrays or snacks, etc. so that that's very powerful in the sense, it really helps to protect untrustworthy software. So library code that did not verified and may have these kind of control flow integrity bugs, for SEO for cherry doesn't really buy you much, because we sort of eliminate a lot of these attacks by construction and the risks we just proved on the side without a lot of effort they could possibly have saved us a little bit of work if we had cherry enabled hardware underneath SEO. So I see, cherry is sort of complimentary in the sense that SEO for proof gives you guaranteed protection between process a process isolation, whereas cherry gives you process internal safety increases by ensuring that code that isn't verified can at least not four, reduce attack vectors by all the phone accesses.

Okay, my understanding is that they're building a software stack on top of that, and I just wondered how that stack compared to the stack you've been talking about?

Well, so the Yes, I need to i, that's my understanding is look. And so basically, if you build software, application software on top of something like cherry, then you get a lot of guarantees for free. So you don't have to prove a point of safety because the hardware ensures that. And so in terms of SEO for as, as I said, the Jerry mobile basically gives you inter process protection versus SEO for gives you protection between processes. Now, in theory, you could say, okay, we don't need processes anymore, we run everything in a single address space. In my past life, we've been building a single address space operating system, we would have loved to have cherry hardware at that time. And there's advantages and disadvantages of this secret gray space model. Maybe with capability and hot hardware coming back there is a revival of that idea. But beyond that, I see this as really complimentary. It helps you giving assurance about your complex application level software, where you you can avoid some verification costs because you get properties for free. There's other ways you can achieve similar things people have been pretty successful in applying mobile checking on a large scale for things like point of safety etc. They, I guess everything else. I don't see it that Jerry mobile to being a replacement for SEO or negating the need for SEO core. I think you definitely need this strong in that process. Isolation unless you really go back to the SQL press space on the

Thank you. And okay, we have one more I'm Chris Goddard. And then I have a few more, I guess, theoretical questions.

Hi. I'm Chris, I hold the doctors mathematics. I've been working in software for a few years. So my question is more of a fairly general and open ended one, I was just interested in the proof languages that you use to construct your proofs. So I had a quick squiz at I think the repo that used to contain all the implementations of your proofs for STL, for a nice saw mentioned something called the ISOC proof method language, I was wondering if you might be able to speak to that or things around it. So I'm the operating system guy, I'm not the full of verification guy. All I know is that we do almost all our verification work in Isabelle Hall. And so that's a interactive steer improver that originally came out of Cambridge is now on, maintained and developed by the Isabel group at to Munich. It has a number of automation modules in there that tie to SMT solvers, it's a crock? I'm pretty vague on that. It's just not my domain. Okay, thanks. Now, that's interesting. I've just made a couple of things to look up.

Right. And I have a few more questions that are, I guess, more related to the theoretical aspects of, you know, why would a lay person care about this. And and, you know, in the book, we basically make the case that the insecure ability of our software stack and not just the insecurity, but really insecure ability almost at this point, is a substantial risk that will only increase and a few people in the in this group. And I have written quite eloquently about this, like David manhandle the fragile world hypothesis, and which he just talks about the risks of just if computer security continued, and, you know, the kind of withering away of our computer security infrastructure. So maybe you could kind of onboard as an input of like, one of the risks of, you know, we don't get around to securing more of our computer, and more of our computer infrastructure, infrastructure and, and could NCL, Floyd maupun, be scalable, to actually do that entire stack? Or, you know, what I am? What are, what are the wrist if we don't get around to solve this problem? And how can se of war help? Really Ananda, like global economic, maybe even civilizational? level?

Right? So I guess I'm preaching to the choir here in that, yes, software vulnerabilities, extremely scary. Even in areas where people are not so aware of the problem, right? I live in Sydney, and one of my catch cries is, there's no safety without security. And this is, for example, in the automotive sector, where people are only starting to really come around to the fact that you, you worry about safety all the time, you can like security, your system is not safe. This is VP can be attacked by Sandy by attackers. And it requires a completely different kind of thinking, versus the classical safety thinking is based on stochastic folds where independent, multiple folds are independent of each other, etc. None of which applies to software. And the most standard example is, I live in Sydney, winter Harbor, when there's an accident on the Harbour Bridge, and one lane is stolen, you feel it through the most of the CD, the traffic is massively affected. And my estimate is by placing 10 accidents around the place, you basically shut the city down for the day. And without killing anyone by just the economic damage alone is massive. Similar for other kinds of critical infrastructure, we know that power stick generators, particularly remote management's, which is almost all these days, are very, not particularly hard to attack. So this is something we're working on. And so the the whole, there's a true threat to society in terms of in in case of political tensions, you can really cripple an economy by using these cyber attacks, very targeted, or cyber criminals, organized crime can use it to extract huge amounts of money, as we've seen, for example, at the UK health system where they use ransomware acts on medical systems that are just not particularly protected from such attacks. So there's clearly is a huge problem. And in terms of SEO for a while, we're sort of at the beginning, right? We managed to do it, get some real strong security for 10,000 lines of code. So how does that scale Two systems that are millions and 10s of billions of lines of code for fortunately, it's not quite as bad as it sounds, we don't have to scale verification up by four orders of magnitude to make some real real progress, which is good in a lot of comes down to actually architecting the systems correctly. And as we shown in the DARPA Atkins program, this can even be done retroactively, if you really put your mind to it, it's still an expensive process, you have to understand the system to re engineer it, etc. And it still needs a lot of more support in terms of tooling, really trustworthy components on top, etc. But it's not a orders of magnitude problem. It's maybe a one order of magnitude of the, and we've seen with COVID, how, and how research can be enormously accelerated by just putting money behind it. That to me, one, that the really positive takeaway of the COVID pandemic was that when, when the pandemic started, there has never been a vaccine against the Coronavirus. And then they will decided to, there was a glitch need to solve this problem. And it took nine months, and we had how many, half a dozen of vaccines out there. And there's 1000 for now. So things can be accelerated a lot, if there is the political will to put money behind it. And in the donation cooperation, I guess, is really key. So

yeah, I guess also what you had in COVID, you saw that how quickly scientists could develop a vaccine? And then, you know, the, I guess, and it seems that then prevented vaccines from actually being distributed and getting to the right places. And I think with computer security, it's, I guess, similarly, so that, you know, we have an entire stack of an economy build up on insecure ball foundations, and, you know, it's hard, I think, unless they really get a wake up call, and that wake up call maybe to too loud or too expensive, really ever for for much to be left to be where I am. I have a, you know, you, you must really know this like, and, you know, we I guess it's, I think the moment that you start thinking about it, you don't really know what to worry about first, you know, a few things that, you know, one could worry about our neck, you know, weaponize Abul technologies, you know, you mentioned autonomous weapons, but of course, that also holds for self driving cars. You know, ultimately, it's not just about, you know, the the robots that are that are made out to kill, which is something that is, you know, people are extremely worried about NFL, I did a really fantastic video on the slaughter bots. And that is kind of terrifying, and is driving the point home about how dangerous they may be, but also holds maybe for just weaponized biotechnology, like, autonomous cars. But then we're also worried about, you know, for example, um, yeah, the electric grid, potentially, I going to buy a Porsche via a computer security attack. And then something that this group also is really interested in is, how did those system hold hold up as we kind of build more increasingly intelligent agents that we cooperate with? And so I was wondering whether, you know, like, those three threats, in particular about autonomous weapons are about weaponizing technology, maybe about computer security attacks? And then also, kind of like the, how well do does SL SL four actually hold up as we build increasingly Intelligent Systems? Do you have any ideas on this? Because those are things sent accurate, I guess, relevant for interest in the group?

Yeah, so I'm trying to remember all the tree but the International Atomic systems, these are only accelerating a problem that already exists. If someone drives I don't actually own the car. But I drive for occasionally, if some, if you drive for a halfway recent talk, then you being in control is an illusion, of course, because you're not in control, the computer is already a computer in control of the car. But you, anything you do is just getting input signals to the computer that controls the car. And of course, these cars already can be attacked. And that's been demonstrated. With autonomy, the problem gets scaled up, of course, because you have less direct input from the human and, and of course, because has this hundreds of difference of makes it said well, but of course, it's still a relatively homogenous ecosystem can for any particular type of cause there's a few percent on the road, right? And if you just can compromise all of those, which is pretty likely because that's the nature of software if you get one way and you can repeatedly do it, and do that. On all the other platforms, then yes, it just scales the whole problem up, but it's not a new problem. So it just shows that a lot of these really beneficial technologies, of course, have also their dangers that we need to be aware of them. People, there's still a tendency of sort of sweeping things under the carpet. And once, once something scales up, then you need a much bigger profit to sweep things under the rug, that it just stops the scale. So that that basically means here that the problem is there, it's been there for a long time, and it's just accelerating. And we need to get real about preventing those problems. In terms of what a CFO can do, what you need to work through years of introductory video, and the point made my mark was is very clear, right? If you need some fundamental technologies to secure the whole thing. And some of these are technologies for securing distributed system communication, that's encryption, that's blockchains, and all this sort of stuff. But in the end, it needs to it bottoms out somewhere where the rubber hits the road, or the bits hit the silicon. And this is where you need to base your security on some rock solid foundation. And this is what SEO for is this, there's no reason why SEO for cannot scale to certainly all the embedded cyber physical space, I think due to scale to something like cloud computing requires a fair amount of more effort in making the whole system more scalable, in terms of cyber physical systems with pretty much the already so that this technology is readily deployable, but it doesn't solve the problem in its own. And the other components mentioned specifically by Mark are absolutely essential, but they have to work together.

And, you know, obviously, you're not an AI researcher, or AI safety researcher or something, but do you have any, you know, a hunch on whether those systems could be safe with you know, and we, as, as a systems that we build, increasingly intelligent,

of course, AI systems have safety or security issues or multiple levels by you can attack the, the AI machinery itself, its algorithms, by Miss training, etc. But, and that's one thing, but that's the thing the AI people have to worry about, they need to find solutions to that, I can't help them with this. But in the end, if you assume this can be controlled, then if you can just bypass the system and insert arbitrary data or algorithms, then nothing else matters anymore. And this is where you need the rock solid foundation that provides that is provided by something like SEO or sem. Again, it's a combination of things. So if you need you need to the problems exist on different abstraction levels, and you have to have the right mechanism and saw solutions at the at each of these abstraction levels.

Actually, you know, one would expect it to be at least the necessary condition. I would think so. Yes. Yep. Yeah. Um, and so maybe, you know, before I ask you one last question, but why do you think that? Okay, well, actually, that let's make it one last question. So a, you know, what is kind of like the roadmap, what could SEO for be doing in five to 10 and 15 years and it is kind of insane or unfathomable, then there isn't enough funding to do those things that you like, actually funding constrained? So, you know, what would? What would help I guess, in Whoa, what would your plans be? What would help? What are concrete things when, you know, if someone realizes that this is a crucial thing to do, that people could do? And to help em? Yeah, as quick as concrete as possible in terms of your immediate plans, and part evoko plugin will be very useful.

Yeah. Thanks for referring to funding. You probably heard that the CSR or these national research organization we used to be part of decided we're no longer required. Despite them claiming to do cyber security for AI, it makes some sense. Fortunately, other people have realized that there's a real problem and there's a I think there's there's a lot of gathering of momentum of really putting money where it's needed. It's not only a money issue, obviously we can always do more with more money, but it's also people issue and that that's at the moment. My bigger concern actually is that the this kind of technology needs a lot of expertise, which is not which is extremely hot, sold after and there's just not enough of it and I'm doing my best to produce smart graduates from our advanced operating systems from program that understand this technology and the techniques behind it etc and, and also the the key ingredients for taking it further. But of course, there's a huge scalability problem here why they don't like credit for the visa year, that's really a drop in the ocean. So the besides the money issue, really speeding up the people skills. The expertise is really of critical importance. And we are observing that now in the automotive space where it said, there's a lot of momentum happening, people are really serious, getting serious about building a truly secure operating system on top of SEO for automotive use. And the money is there, or at least I'm reasonably confident that I can get enough parties to commit on it to do that. But having enough people to actually do it in a reasonable timeframe is there's a big challenge.

Have you ever thought of doing more like an online course that could cause error? Or something

like this? Yeah, I so I started putting my not I've been putting my slides online for a long time by last year started putting the actual lecture videos online, on YouTube. And the problem is the it's not just enough to have this material like part part of really reducing the skills and a lot of interaction we give our students a lot of guidance. And really, the whole course has has a lot of interaction between tutors and students, etc. And to scale something like that up. It certainly interested it would require a fair amount of effort and again, it's sort of a scalability issue you need to train the trainer's in order to really be able to scale this sort of thing up I really wish we would do it. I'm sort of notes to promise anything, not knowing how thinly spread I am already but it something like that would be really cool. Yeah,

I mean, it's just unfathomable for how potentially impactful This is, or high impact this will be in volume, people just are working on it now. But I'm guessing, I'm hoping it will change. No, we're only one minute over time. And is there any way in which people could help plug in and find your work and maybe leave us with somewhat of a carrot? Like you know, what, what what could you guys achieve in the first 210 years that would make us all a little bit less insecure.

So I think there's still an amazing lack of awareness about SEO for and the technology it represents. And that is sort of both in funding agencies in governments and in industry and sort of getting the word out is really one key factor. And of course, getting people to contribute to the SEO foundation both in terms of paying membership dues, but also really actively contributing is really cool to the way to scale it up the when we set this up, we sort of knew that the need to the product the ecosystem and we used depends on a particular organization. A year later the Big Bang happened then we were having had we not set up the foundation at that time the whole thing like we did so there was definitely some some good foresight there. And scaling this ecosystem up is just key and that includes awareness raising so I'm very grateful for you to give me this opportunity and ability to provide input and I really hope that you help putting getting the message out we really need to get the decision makers both in the industry and governments really aware of not only the needs but also the fact that there is already solutions out there that need scaling up.

Yeah, and in fact have been out there for a long time. Okay, got it. I can't thank you enough. Thank you so much for joining us and we'll certainly try to do our best and and we would love to have you on in whenever, whenever you you are interested again. So thanks a lot, I think terrifying and really useful. At the same time. I think there was an opportunities at the same time. It's a terrifying and very hopeful talk. So thank you so much for joining us. Thank you everyone for bearing with the time difference chasing and and I hope to see many of you again next week. So thanks a lot