Kry10 and the seL4 Platform - seL4 Summit 2022
Members of the Kry10 Team attended the 2022 seL4 Summit in Munich, sharing some of the latest work based on the seL4 platform. The event was attended by a combination of technical researchers, members of the seL4 Foundation as well as customers, partners, and companies that are interested in leveraging the seL4 Microkernel.
It’s been a while since we’ve been able to travel to have rich, engaging in person conversations with people -some that we’ve been working with but never actually met outside of video conferencing and others we’ve just not been able to engage with in person for over 2 years. It really demonstrated the importance of being able to meet face to face, engage in conversation and share the work that’s been happening over the past year.
It was a great forum for sharing ideas, networking and conversations with customers who were interested in the work the Kry10 team has been doing on the platform. The event was sold out but don’t worry -you can still see the presentations even if you weren’t able to make the trip! A big thank you to the seL4 Foundation, and the sponsors of the event for creating a great forum for a great event!
Boyd Multerer “Kr10 Secure Platform”
The promise of IoT and connected devices has yet to be fully realized as customers confront some critical challenges of security, reliability and manageability. Key to the challenge is that most of the current IoT platforms are running on platforms from the previous century. In this presentation, Boyd talks about his conversations with customers across various industries and how it helped define the modern platform he wanted to build to address customer needs. Boyd introduces the Kry10 Platform with its Trust but Isolate philosophy, and then shows how the Kry10 Operating System implements this philosophy to achieve a secure and robust platform for industrial connected devices.He also tries out a few new jokes- not to be missed.
Matt Brecknell “Explaining the seL4 integrity theorems”
Kry10 is building a cost-effective platform for connected devices, with extreme security and reliability. We choose to build on seL4 because its capability model gives us the mechanisms, and its verification gives us the confidence that we need. But how do we understand what the verification says about how we should use seL4's mechanisms to build secure systemsIn this presentation, Matt at the seL4 integrity theorems, which give us an abstract way to understand the authorities that components in a system have over each other.
Kent McLeod “Multiprocessing on seL4 with verified kernels”
Verified multicore seL4 seem too far away? Think again, this talk presents a simple multikernel approach to achieve this goal that is attainable using the verified unicore kernel we already have. While this solution does not provide all the benefits of a single system image it allows us to build static systems on a verified seL4 using multiple cores today. This talk will detail how to construct such a system, the work involved and examples of how it can be used.
Ihor Kuz “seL4 and BEAM, a match made in Erlang”
The BEAM provides strong fault-recovery mechanisms based on its supervision trees and a "crash and restart" philosophy coupled with dynamic code (re)loading. This, combined with seL4's strong isolation, leads to systems that can realize the full "prevent, contain, and recover" strategy. In this presentation we will demonstrate what can be achieved by combining seL4 and the BEAM. We will also describe our experience with building BEAM-based systems on seL4, including porting the BEAM to run on seL4, integrating the BEAM with seL4 inter-process communication mechanisms and other C-based components, and creating a powerful Elixir-based development environment for seL4 systems.