Keynote: Security Under the BEAM
summary
Claims a working platform that marries the BEAM and OTP fault model with a formally verified microkernel and management stack, shipping an early Kry10 Secure Platform that uses the seL4 microkernel (≈10,000 LOC with proofs in Isabelle) plus signed manifests, WireGuard tunnels, and key-backed over-the-air updates. Demonstrates a Scenic-based outbound-only UI, tooling to instantiate systems (mix kos.new), restartable services with hot swap semantics, subsecond boot times, and targeted protections to prevent lateral migration on devices where 70% of IoT projects otherwise fail. Kry10 Secure Platform Scenic UI formal proofs mix kos.new
AI-written summary · about
chapters (7)
- 0:0003:21 - Intro
- 3:2207:54 - IoT: Momentum and Challenges
- 7:5513:39 - Platform Requirements
- 13:4017:21 - What's a Microkerner + Formal Methods
- 17:2227:53 - The Kry10 Platform
- 27:5430:27 - Summary
- 30:2843:22 - QnA
related talks
37mSecurity of the BEAM
41mFireside chat on security for practitioners & academics
43mClosing Keynote
15mKeynote: The Security Symphony
23mKeynote: Zephyr & IoT Security
17mKeynote: Modern Least Privilege with DevSecOps
01h 05mKeynote: Can we reason about the security of concurrent systems code?
29mEnabling a secure IoT from design to deployment