Why Formal Verification Matters in the Sentry Microkernel

H2Lab Development Team 9 min read

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 model.

This is where formal verification becomes a decisive advantage. In Sentry, formal methods are not an afterthought or an academic exercise—they directly shape the kernel’s architecture and implementation, particularly in security-critical subsystems such as MPU (Memory Protection Unit) management.

What Does Formal Verification Mean in Sentry?

Formal verification consists in specifying the intended behavior of the kernel precisely and mathematically proving that the implementation satisfies those specifications. In Sentry, this approach is applied using static analysis and formally-grounded tools (like Frama-C), letting us establish strong guarantees about memory safety, isolation, and control flow.

Unlike testing, which can only demonstrate the presence of bugs in specific test cases, formal verification can prove the absence of entire classes of errors across all possible executions.

Security by Construction

The kernel is the most privileged component of any system. A single flaw can compromise all applications running on top of it. Formal verification helps Sentry address this risk at its root:

  • It proves that critical invariants hold in all executions.

  • It eliminates classes of bugs such as invalid memory accesses, inconsistent state transitions, or broken isolation assumptions.

  • It provides mathematical assurance that the verified properties hold for all possible paths.

This level of assurance is particularly relevant for embedded and cyber-physical systems, where failures can have safety, financial, or regulatory consequences.

A Kernel Designed for Verifiability

Formal verification strongly influences Sentry’s design:

  • Highly modular structure, enabling component-level reasoning.

  • Clear and explicit interfaces, which can be formally specified and verified.

  • Minimal and encapsulated assembly code, reducing the unverified surface and simplifying proofs.

In Sentry, the kernel is not merely verified after implementation; it is designed to be verifiable, which significantly lowers the cost and complexity of formal analysis.

MPU Management: A Concrete Case of Formal Verification

One of the most compelling applications of formal verification in Sentry is the management of MPU regions.

On ARM Cortex-M microcontrollers, the MPU is the primary hardware mechanism used to enforce memory isolation between tasks. Any mistake in MPU configuration can lead to severe vulnerabilities: unintended memory access, privilege escalation, or cross-task interference.

Sentry treats MPU management as a first-class, formally reasoned subsystem.

Example ACSL Specifications for MPU Invariants

Below are example fragments in the style of ACSL (ANSI/ISO C Specification Language) that express core invariants used in Sentry’s MPU management logic. These are illustrative, reflecting how formal annotations in mpu_pmsa_v8.h specify key guarantees.

About MPU mapping and W^X

On ARMv8-M the PMSAv8 MPU region validity predicate (in ACSL) says a region is valid if:

  • both base and limit are aligned to the MPU region alignment (32 bytes)

  • the limit is ≥ base

  • OR if the region is empty (RBAR/RLAR = 0)

That last point makes “unmapped” regions represent no actual memory mapping.

The architecture imposes Write-xor-Execute semantics via these properties:

  1. Executable permissions are encoded in the RBAR XN bit — noexec == 1 → non-executable.

  2. Access permission (AP) bits define read/write constraints.

  3. The Cortex-M PMSAv8 (as profiled in the kernel header) includes assertions that enforce W^X semantics when forging a resource:

    • if noexec == 0 (i.e., region is executable), then the access permission must be RO (read-only)

    • conversely, if the region is writable (non-RO), then noexec must be set

This part of the demonstration is made using assertion in the mpu_forge_ressource(), which is the arch-specific implementation of the MPU region set on armv8-m.
This function is verified using assertions in its implementation:

/*@
  requires \valid_read(desc);
  requires \valid(resource);
  assigns *resource;
  ensures (\result == K_STATUS_OKAY);
 */
__STATIC_FORCEINLINE kstatus_t mpu_forge_resource(const struct mpu_region_desc *desc,
                                                   layout_resource_t *resource)
{
    kstatus_t status = K_ERROR_INVPARAM;

    /* W^X conformity */
    /*@
      assert desc->noexec == 0 ==>
        (desc->access_perm == MPU_REGION_PERM_RO || desc->access_perm == MPU_REGION_PERM_PRIV_RO);
     */
    /*@
      assert (desc->access_perm != MPU_REGION_PERM_RO && desc->access_perm != MPU_REGION_PERM_PRIV_RO) ==>
        desc->noexec == 1;
    */
    resource->RBAR = ARM_MPU_RBAR_AP(
        desc->addr,
        desc->shareable ? ARM_MPU_SH_INNER : ARM_MPU_SH_NON,
        desc->access_perm,
        desc->noexec ? 1UL : 0UL
    );

    resource->RLAR = ARM_MPU_RLAR(desc->addr + desc->size - 1, desc->access_attrs);

    status = K_STATUS_OKAY;
    /*@ assert (status == K_STATUS_OKAY); */
    return status;
}

This function is called just before the mpu_add_ressource() function, that add the previously forged ressource into tasks memory map table.

The coverage of this function is made using two Frama-C covering tests:

  • syscall coverage analysis, that cover this call through the various memory-map related syscalls implementation
  • kernel startup coverage, that cover the initialisation-related mapping, at task context initialisation.

W-Xor-X demonstration at region forge time is not enough to demonstrate the entire properties. This also requires that:

  • no overlap exist between mapped region at any time of the task mapping
  • no invalid region is added to a task memory map table

This is added through other dedicated predicates and assertion, as described bellow.

Region-related predicates

A set of predicates has been written to verify region properties, including PMSAv8 conformity and overlapping check to already mapped regions.

 
/*@

  predicate aligned_32(ℤ addr) =
    (addr & MPU_REGION_ALIGN_MASK) == 0;

    predicate mpu_is_empty_region(ARM_MPU_Region_t r1) =
      r1.RBAR == 0 && r1.RLAR == 0;

  predicate valid_mpu_region(ℤ base, ℤ limit) =
    ((base == 0 && limit == 0) ||
    (
        aligned_32(base)
        && aligned_32(limit)
        && limit >= base
        && ((limit - base + 1) % MPU_REGION_ALIGN == 0)
    ));

  predicate valid_mpu_regions{L}(ARM_MPU_Region_t *regions, integer n) =
        \forall integer i;
            0 <= i < n ==>
            valid_mpu_region(regions[i].RBAR & MPU_RBAR_BASE_Msk,
                             regions[i].RLAR & MPU_RLAR_LIMIT_Msk);

  predicate non_empty_region(ℤ base, ℤ limit) =
    (limit - base + 1) >= MPU_REGION_ALIGN;

  // when either region is empty, they are considered disjoint
  predicate disjoint(ARM_MPU_Region_t r1, ARM_MPU_Region_t r2) =
      r1.RBAR == 0 && r1.RLAR == 0 ||
      r2.RBAR == 0 && r2.RLAR == 0 ||
      (
        (r1.RBAR & MPU_RBAR_BASE_Msk) <= (r2.RLAR & MPU_RLAR_LIMIT_Msk) ||
        (r2.RBAR & MPU_RBAR_BASE_Msk) <= (r1.RLAR & MPU_RLAR_LIMIT_Msk)
      );

  predicate regions_disjoint{L}(ARM_MPU_Region_t *regions, integer n) =
      \forall integer i, j;
        0 <= i < n && 0 <= j < n && i != j ==>
          disjoint(regions[i], regions[j]);
*/

These predicates then need to be added as pre and postconditions of programs that are responsible for manpulatin task memory regions.
This is done using a single primitive in the kernel, that add a new region to a given task region set. This primitive is denoted mgr_task_add_resource().

Region validity check

kstatus_t status;
task_t *cell;

// [...]
if (unlikely(mpu_region_is_valid(&resource) == SECURE_FALSE)) {
        status = K_ERROR_INVPARAM;
        goto err;
}
/* demonstrate that the effective run time check does match the predicate */
/*@ assert valid_mpu_regions(&resource, 1); */

Non-Overlapping check

In this function, the overlapping check is made using disjoint assertion between all the existing regions of the task and the new one that aim to be added:

/*@ ghost int is_disjoint = 0; */
/*@
      loop invariant 0 <= idx <= TASK_MAX_RESSOURCES_NUM;
      loop invariant \initialized(&cell->layout[idx]);
      loop assigns idx;
      loop variant TASK_MAX_RESSOURCES_NUM - idx;
 */
for (uint8_t idx = 0; idx < TASK_MAX_RESSOURCES_NUM; ++idx) {
    if (unlikely(mpu_regions_overlap(cell->layout[idx], resource) == SECURE_TRUE)) {
        status = K_ERROR_INVPARAM;
        /*@ ghost is_disjoint = 1; */
        goto err;
    }
    /*@ assert disjoint(cell->layout[idx], resource); */
}

Context Switch

At context switch, the above updated table is the lonely one used in order to map the newly scheduled task, meaning that this table is the single source of memoyr mapping configuration. This is why the lonely table writter is stricty verified.

 

How Frama-C coverage is used

Frama-C is called using both EVA and WP plugins through the following entrypoint:

 
int map_resource(void)
{
    /*
     * here we define unpredictable resource ID and layout,
     * to cover any possible resource structure input values, so
     * that we can demonstrate that only valid (aligned, non-overlapping)
     * resources are mapped.
     * NOTE: this do not check the resource ownership, as this is done by
     * the task manager itself.
     */
    volatile uint8_t resource_id = 0;
    volatile layout_resource_t resource;
    /*
     * call kernel startup up to task manager initialisation. This part noRTE has already
     * been demonstrated in another Frama-C test that targets kernel entrypoint directly
     */
    if (prepare_startup() != 0) {
        return -1;
    }
    /* as we do not check ownership but only mapping, we use idle task as vehicle */
    mgr_task_add_resource(mgr_task_get_idle(), resource_id, resource);
    return 0;
}

This entrypoint has  the following properties:

  • resource_id unconstrained (volatile nondeterministic)

  • resource unconstrained (volatile full layout_resource_t)

  • no precondition on the shape of the descriptor or its fields

Important: the test does not assume anything about resource — it may hold any bit pattern. That means:

  • Frama-C’s WP plugin generates obligations for all possible values of the layout_resource_t inputs passed to mgr_task_add_resource.

  • As part of the manager implementation, mgr_task_add_resource will forge an MPU resource using the kernel’s internal data and architecture model.

  • The forging logic includes those important W^X assertions inside mpu_forge_resource.

Because those assertions are in the resource construction code, the only way for the overall proof to succeed for every nondeterministic input resource descriptor is if:

  1. invalid region configurations are either rejected or proven unreachable — i.e., they violate mpu_region_is_valid or internal access-permission invariants; and

  2. only valid MPU regions that satisfy alignment, size, and access permission constraints (including W^X) can ever flow into the low-level MPU configuration logic.

Frama-C tries to discharge all obligations (e.g., prove no runtime errors, prove postconditions, prove assertions). If any possible value could produce a region that violates W^X (e.g., writable and executable), the corresponding WP proof obligation would not be discharged.

Thus:

✔ The test covers all possible bit patterns for resource
✔ The proof infrastructure uses mpu_region_is_valid to reject invalid base/limit configurations via its ACSL predicate in mpu_pmsa_v8.h

When launched, the Frama-C test demonstrates the W^X property by:

  • constraining the set of acceptable region configurations to only those where write and execute are not simultaneously permitted; and

  • ensuring that any path through mgr_task_add_resource that could lead to invalid combinations cannot happen under the ACSL and proof conditions.

Test results show that Frama-C is able to demonstrate that all assertions and obligations are valid, whatever the input is, and as such demonstrate the effective W^X property.

Conclusion

Sentry demonstrates that formal verification is not an abstract academic ideal, but a practical engineering tool for building secure micro-kernels. Nowhere is this more concrete than in its MPU subsystem:

  • Memory isolation is backed by mathematically proven invariants.

  • Subtle, low-level bugs are eliminated by design.

  • Security properties are guaranteed rather than assumed.

By integrating formal methods into both architecture and implementation, Sentry raises the bar for what it means to be “secure by design” in embedded systems.

You should also read:

Exploring Pointer-Free Data Exchange in Sentry

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:…

Continue reading...

Formal proof in embedded systems part 3

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…

Continue reading...

Sentry Kernel key concepts part 1: Basics

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)…

Continue reading...