Camelot OS

Micro-kernels such as Sentry aim to provide strong isolation, minimal trusted computing bases, and high assurance for embedded and security-critical systems. However, achieving these goals in practice is difficult: subtle bugs in low-level code, memory protection, or context switching can completely undermine the intended security…

When diving into Sentry-micro-kernel concepts, one design choice really stood out: no pointer passing between user space and kernel space. Instead of relying on pointers, Sentry uses a dedicated buffer called svc_exchange to transfer data between applications and the kernel. This simple but powerful approach:…

Alongside noRTE coverage, the Sentry kernel aims to hold functional proofs for its critical functions. One of them is the memory management part, that is responsible to ensure the W^X property of all memory regions mapped, for both kernel an user tasks. This work has…

When it comes to embedded systems, security and reliability aren’t just features—they’re requirements. That’s why we built the Sentry Kernel, a preemptive micro-kernel designed for micro-controllers, with security baked in from the ground up. 🔑 Key Highlights: Minimal attack surface: Only critical devices (like DMA)…

To complete the Sentry-kernel entrypoint noRTE coverage (https://lnkd.in/evZeGVmG), a lot of work has been made in order to cover other kernel interfaces, starting with handlers and the bigger of all: the syscall gate. This work has been done again with Frama-C framework, by crafting an…