Ihor Kuz

Operating system engineer @ Kry10 & seL4 TSC member

Dr Ihor Kuz is an operating system engineer at Kry10, helping develop the Kry10 OS and Platform. Ihor has previous experience leading the team developing the seL4 microkernel, and has been involved with seL4 for as long as it’s been around. He is also an associate professor at UNSW in Australia and has taught distributed systems and Erlang there for many years.

Talk:
Freestanding Erlang: Porting BEAM close to the metal

Audience: intermediate

Erlang and Elixir are great languages for programming concurrent and fault-tolerant applications yet they still require BEAM to run them on real-world hardware. BEAM is a complex piece of software that leverages general purpose operating systems to enable concurrent applications to scale to incredible levels.

But what if you want to run Erlang or Elixir without an OS? Modern operating systems such as Linux are large and complex and can be the wrong choice to deploy on for embedded applications that prioritize security and robustness.

What would it take to run the open-source BEAM implementation in a freestanding environment with no external OS services but still presented a partial POSIX system interface? Would this implementation still allow for useful applications? What are the tradeoffs and what features do we need to give up? This talk tries to answer these questions by presenting a recent project that ported BEAM to a freestanding environment for ARMv7 application processors.

OBJECTIVE

Explain how the BEAM virtual machine can be run in a minimal self-hosted process environment without a runtime dependency on a large general-purpose operating system and discuss what tradeoffs are associated with this approach and why you would want to do this when seeking better security and robustness.

AUDIENCE

Embedded systems software developers as well as anyone else interested in understanding or removing various abstraction layers that sit between our high-level software and the physical machines that compute it.

Talk:
seL4 and BEAM: a match made in Erlang

Audience: Intermediate

Erlang and Elixir can be used to develop robust and highly-available embedded applications with effective fault-tolerance, but the BEAM virtual machine still relies on the underlying operating system to provide a security and robustness foundation which can be insufficient when the OS cannot prevent other components from crashing the system.

The seL4 microkernel is a formally verified operating system kernel designed for embedded systems. seL4 provides isolation mechanisms that can prevent errors or attacks from spreading to other components but it expects each component to mange its own error detection and fault recovery.

I will demonstrate how combining the seL4 microkernel and the BEAM provide an exciting opportunity to fill these gaps. I will also describe my experience with building BEAM-based systems on seL4, integrating BEAM and seL4’s inter-process communication mechanisms to allow robust communication between Beam apps and native OS components.

OBJECTIVES

Show how the high-availability programming and communication abstractions of the BEAM can be combined with the communication and programming abstractions of a formally verified microkernel to design and build highly secure and robust internet-connected embedded systems.

AUDIENCE

Embedded systems software developers that are interested in designing and building systems with high levels of security and robustness.