Sentry secure embedded kernel for Outpost Operating system

Repository on GitHub, which provides public git repositories with URLs.

Repository on GitHub, which uses git. git can track the changes, who made them, and when they were made.

Milestoning is considered with respect for the semvers concept. New releases are made only when a milestone is reached, leaving interim version separated. Release publication requires test-farm based complete non-regression testing on multiple hardware targets.

Repository on GitHub, which uses git. git is distributed.

version numbering is using the semantic versioning model. While being in 0.x version, ABI violation is allowed, but starting with v1.0.0, any ABI violation will require a major number update. feature update and patches already respects semvers in the 0.x consecutive deliveries.

releases are based on git tags through the github releasing model.

Example : https://github.com/outpost-os/sentry-kernel/releases/tag/v0.2.2 Releases notes are based on automatic github release changelog generation, with proper formatting configured.

The github security report model is activated. Any PR related to a CVE patch must be denoted "cve:" as defined in the CONTRIBUTING.md file. Moreover, the cve and security labels exists so that the release changelog generation automatically instanciate the CVE chapter with the corresponding updates

https://github.com/outpost-os/sentry-kernel/blob/main/CONTRIBUTING.md As defined in the CONTRIBUTING file, bug reports can be submitted through github issues (or github discussions if needed)

The Github issue tracker is used for tracking individual issues

The project being relatively young as an Open-Source project, no external bug reports has been delivered yet. Although all bug reports published are: - fixed through PR - associated to a milestone if moved forward to next release

The usage of Github issues and security report allows archive of such events (https://github.com/outpost-os/sentry-kernel/issues)

The project describes the vulnerability reporting process (Github based) in https://github.com/outpost-os/sentry-kernel/blob/main/.github/SECURITY.md Security reporting is activated.

All informations are defined in https://github.com/outpost-os/sentry-kernel/blob/main/.github/SECURITY.md

The project has defined the usual 90 days embargo, as defined by projectzero for security reporing, and as such considers interact as soon as possible with the reporter.

Project is based on meson build system. Overall build and build options are considered at CI level and rebuilt for each PR.

We use standard tooling: - meson as a build system - Kconfig as a configuration system

Only FLOSS are used for building.

Bot unit testing and autotest build profile exists in order to validate the kernel behavior. The testing model is fully defined in https://outpost-sentry.readthedocs.io/en/latest/tests/index.html

As meson is used, test targets are generated through meson build system in the way test manipulation is defined. See https://github.com/outpost-os/sentry-kernel/blob/main/kernel/tests/meson.build for root automatic test definition for standard test target

Multiple testing consideration are made: - unit testing with mocking of various kernel subcomponents : through the meson test target - autotest-based dynamic testing directly on-target (ARM thumb7(e)m and thumbv8m) : through the autotest profile build and run - noRTE and some behabior analysis using Frama-C formal proofness and contracts definition : through the meson test target

autotest and formal proofness is made in ordrer to cover all the kernel through its runtime inputs (entrypoint, syscall, interrupts handlers, etc.) so that the kernel is covered with various inputs values including corrupted one, using the Frama-C evaluated values model (https://frama-c.com/fc-plugins/eva.html).

Any new functionalty requires testing inclusion, starting with autotest fuzzer updates. formal proofness coverage is made automatical through fully random-based kernel inputs forge. Autotest aim to validate the requested behavior of the kernel, while Frama-C detect any newly included RTE.

Any new functionality must have the autotest testing suite being updated accordingly. This is defined in the CONTRIBUTING document.

test policy is fully documented in https://outpost-sentry.readthedocs.io/en/latest/tests/index.html (for unit testing and autotest) and in https://outpost-sentry.readthedocs.io/en/latest/proof/index.html for formal proofness.

The project uses the meson build system warning_level=3

The project must not build with warnings (Werror usage). Only unit tests builds accept such case.

No warning allowed for any target-related components (kernel, autotest, production-related tooling, Rust UAPI library)

The overall secure software designed is controlled by: - previous French ANSSI embedded security expert - Ledger Dungeon laboratory (https://donjon.ledger.com/), responsible for product security design

The same developers and security reviewers do hold this part of the security analysis.

The sentry kernel itself, being a micro-kernel, do not hold cryptographic algorithm.

The sentry kernel itself, being a micro-kernel, do not hold cryptographic algorithm.

No cryptographically-related mechanism is stored in the kernel local tooling. the cryptography that is responsible for ensuring global project security (not being kernel-relative) is leaved to the Operating System SDK.

The sentry kernel itself, being a micro-kernel, do not hold cryptographic algorithm.

The sentry kernel itself, being a micro-kernel, do not hold cryptographic algorithm.

The sentry kernel itself, being a micro-kernel, do not hold cryptographic algorithm.

There is no forward secrecy notion as the software is for very small embedded systems only.

There is no user (and thus password) notion as the kernel target small embedded systems.

The kernel delivers a rng API that do respects the FIPS-140-2 requirements, that include verification of the TRNG hardware backend output. This verification is verified through formal contracts that validate the FIPS-140-2 specific software-level verifications over KRNG hardware output.

sources and documentation are using https. There is no SSH notion on-target

Only https is used for both sources and website.

No unpatched public vulnerability by now.

We aim to fix as soon as possible any vulnerability as it is a major requirement in the usage of the kernel. Pro-active RTE research and behavior validation is also controlled through formal proofness and autotesting using test farm.

GitGuardian is used in order to verify any credential leak

Frama-C (https://frama-c.com/index.html) is used in order to cover overall kernel code, for UB, RTE and invalid functional behavior. Frama-C delivers coverage results. Typically, syscall coverage reaches approx. 92%.

Through formal proofness, all UB and RTE are searched, Frama-C being a sound tool.

All Frama-C relative red-alarm (effective RTE or UB) not being a false positive are fixed. Any autotest-related kernel fuzzing that do not match expected behavior is fixed as soon as found. No delivered vulnerability report received by now.

static analysis is spawned in the CI each time a commit is made on any PR, and in the main branch push events.

Kernel autotest mode (see https://outpost-sentry.readthedocs.io/en/latest/tests/autotest.html) is used for dynamic testing.

C RTE and UB are catched through formal proffness value analysis with Frama-C. There is no dynamic memory at micro-kernel level. UAPI is written in Rust.

autotest is an assertion-based dynamic testing tool for the micro-kernel.

Any invalid dynamic autotest assertion requires fixes so that overall test suite is valid.