seL4 and BEAM: A match made in Erlang
summary
Ports the open-source BEAM to a freestanding seL4 microkernel on ARMv7, implementing a minimal POSIX layer (pthread wrappers, basic filesystem, LWIP network stack) so multiple BEAM instances run as isolated seL4 processes. Demonstrates a weather‑station system with an Elixir sensor, a C I2C driver, remote Scenic UI and VPN transport; uses seL4 IPC, shared memory or loopback TCP for Erlang distribution and optional filters. Claims containment via formal verification of seL4 and practical BEAM on seL4 interop, and shows it works end‑to‑end.
AI-written summary · about
chapters (8)
- 0:0001:29 - Intro
- 1:3004:41 - Connected Industrial Devices
- 4:4209:06 - Achieving Security and Resilience
- 9:0711:26 - seL4: Microkernel
- 11:2716:25 - seL4: Formal Verification
- 16:2622:22 - BEAM and seL4: Example
- 22:2325:27 - BEAM Communication
- 25:2826:23 - Summary and Future
related talks
48mGetting to Know the Erlang Virtual Machine, the BEAM
38mDemos and Lightning Talks
24mFantastic Voyage III: Destination BEAM
42mThe Soul of Erlang and Elixir
44mLFE - a lisp flavour on the Erlang VM
45m12 years supporting Software Architecture teaching with BEAMs
38mMembrane Framework: Bringing BEAM into multimedia
50mGrisp: Building Space Ships With Erlang