BEAM Guest Environment
The BEAM Language Plane hosts unmodified Erlang/OTP applications inside minimal, isolated seL4 Protection Domains. By stripping away conventional operating system layers, we run the BEAM runtime directly on top of the Synrc system-call translator, creating high-assurance, single-purpose unikernels with a micro-sized Trusted Computing Base (TCB).
ERLANG/OTP 20 & SYNRC CORE
The single-core OTP 20.3.8.26 build removes SMP scheduler synchronization, locks, JIT dependencies, and atomic memory operations. This yields a frozen, highly audit-ready VM footprint linked against musl libc.
/* Erlang/OTP 20 Single-Core Emulator */
int main(int argc, char **argv) {
synrc_init_sel4();
beam_start_single_core();
return 0;
}
SYNRC SYSCALL TRAP
Synrc intercepts standard Linux system calls made by the musl-linked BEAM, providing a minimal trap surface (approx. 50 calls) for memory mapping, futex synchronization, time, and an in-memory VFS.
/* Minimal Syscall Translation */
long syscall_trap(long num, long a1, long a2) {
switch (num) {
case SYS_mmap: return do_mmap(a1, a2);
case SYS_futex: return do_futex(a1, a2);
case SYS_clock: return do_clock();
}
return -ENOSYS;
}
CAPABILITY-MEDIATED I/O
The BEAM protection domain contains no device driver registers. All network and storage interactions are offloaded to sDDF (seL4 Device Driver Framework) shared-memory rings and notifications.
/* sDDF Ring-Buffer I/O Handoff */ sddf_ring_t *tx_ring = get_tx_ring(); sddf_enqueue(tx_ring, packet_buf, len); sel4_notify(nic_pd_cap);
SMP MULTI-CORE TARGETS
For workloads requiring multi-core scaling, the SMP tree introduces a fixed worker thread pool (workers 6–15) mapped directly to seL4 execution contexts, utilizing work-stealing and cross-core notifications.
/* Static SMP Worker Loop */
void *worker_run(void *arg) {
worker_env_t *env = (worker_env_t *)arg;
while (1) {
beam_sched_run(env->queue);
sel4_yield();
}
}
Bytecode Safety Properties
- Memory Safety — No raw pointer arithmetic; all accesses are verified by the BEAM runtime.
- Type Safety — Strict runtime type validation preventing object injection and type confusion.
- Control-Flow Integrity — ROP, JOP, and COP mitigation through software-managed call stacks and the lack of dense native instructions.
- Resource Preemption — Reduction counting prevents individual actor processes from monopolizing scheduler execution.
NIST SP 800-53 Mapping
- AC-3 / AC-6 (Access Control) — Enforced by seL4 capability matrices and isolated static memory regions.
- SC-7 (Boundary Protection) — Strict spatial and temporal separation between the BEAM PD, VMM, and driver domains.
- CM-2 / CM-7 (Config Management) — System topology, thread configurations, and device bounds are fixed at build time.
- AU-12 (Audit Event Generation) — Audit metrics are pushed directly to the Monitor PD over unidirectional channels.
Specification & Architecture
By executing intermediate bytecode instructions rather than native machine codes, the BEAM runtime acts as a high-assurance sandbox. This virtualization layer blocks standard stack-smashing, use-after-free, and return-oriented programming (ROP) exploits. Because the virtual machine call stack is decoupled from the native physical registers, attacker-controlled data streams cannot hijack the instruction pointer.
The Synrc layer sits between the seL4 microkernel and the BEAM runtime, presenting a bare-minimum POSIX interface. Rather than running a full general-purpose operating system kernel, Synrc handles only the syscalls needed for memory management (mmap/mprotect), synchronization (futex), and threads (clone). It lacks raw hardware access, translating all virtual socket and file operations directly into sDDF shared-memory rings.
Under the Microkit framework, the system is constructed statically at compile time. The memory mappings, IRQ channels, scheduling priorities (using the Mixed-Criticality Scheduling model), and core affinities are immutable. The BEAM domain runs alongside separate VMM, Console, Monitor, and Storage protection domains, ensuring that a vulnerability in the application runtime cannot compromise the hardware or sibling domains.