What question did this study set out to answer?

This research introduces the BioOS Causal Constitution, aiming to enhance kernel-level security through causal ancestry enforcement.

May 27, 2026Open Access

BioOS Causal Constitution: A Turing-Incomplete Kernel Safety Layer for Digital Causal Closure

Puntos clave

This research introduces the BioOS Causal Constitution, aiming to enhance kernel-level security through causal ancestry enforcement.
Introduced a Turing-incomplete DSL called .bio for safety-critical state machines.
Defined DCCRing0Guard, a kernel guard with six invariants to track causal tokens from hardware interrupts.
Implemented empirical validation with a Python oracle, property-based tests, and an attack suite against a Linux kernel.
Blocked five out of six representative attacks as predicted.
Successfully delineated the trust boundary despite one expected bypass due to root tampering.
No unexpected bypasses were observed, confirming the robustness of the causal invariants.

Resumen

The BioOS Causal Constitution is a kernel-level security primitive that enforces causal ancestry instead of traditional access permissions. A system call is permitted if and only if a verified causal chain exists from a physical hardware interrupt (IRQ) to the call site within a bounded time window. In the absence of such a chain, protected resources do not appear as “denied” – they appear to not exist (e. g. ENODEV, ECONNREFUSED). The work introduces the. bio specification language, a deliberately Turing-incomplete DSL for safety‑critical state machines with a small-step operational semantics and a termination theorem that guarantees a finite, enumerable state space. On top of this DSL, the paper defines DCCRing0Guard, a six‑invariant kernel guard that tracks causal tokens from hardware IRQs to file, network, and exec operations, and compiles it to six eBPF/LSM programs on Linux 6. 1. Formally, the paper states a compiler soundness theorem for the. bio → eBPF/LSM backend and a safety bisimulation between a JavaScript emulator (bioₖernelₑmu) and the live kernel implementation (DCC Ring 0). All six security invariants (no autonomous write, causality window, protected file immutability, op‑class matching, TOCTOU rollback, and full causal chain requirement) are checked with the Z3 SMT solver; any violation yields an UNSAT proof. On the empirical side, a three‑layer validation framework is presented: (1) a faithful Python oracle that re‑implements the BPF semantics, (2) six Hypothesis property‑based tests that exercise the invariants over more than 7, 500 random inputs, and (3) a 13‑test attack suite that is run both against the oracle and a live Linux 6. 1. 0‑48 kernel in blocking mode. The experiments confirm that five representative attacks are blocked as predicted, while one expected bypass (root tampering with BPF maps) cleanly delineates the trust boundary; no unexpected bypasses are observed. The guarantees are explicitly scoped to software‑level adversaries at the kernel boundary (system calls for file, network, and exec). Physical compromise, firmware or bootloader manipulation, and off‑host disk access are out of scope, but any software attack that reaches the DCCRing0Guard interfaces remains subject to the same causal invariants and is blocked in the absence of a valid physical causal chain.

Leer artículo completoexternamente

Me gusta

Guardar

Ver artículo completo