H2Lab Development Team

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…

During the last months, a lot of work has been done in the Sentry kernel in order to validate the absence of run time error, including all undefined behaviors, but also usual RTEs such as invalid memory access, out-of-bounds and integer algorithmic errors not being…