Sentry-kernel for Camelot-OS

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.

Releases notes are based on automatic github release changelog generation, with proper formatting configured. For e.g. https://github.com/camelot-os/sentry-kernel/releases/tag/v0.4.0

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/camelot-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/camelot-os/sentry-kernel/issues)

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

All informations are defined in https://github.com/camelot-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 OSS tools are required for building.

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://sentry-kernel.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/camelot-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

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://sentry-kernel.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. Rust part use both clippy and miri for static analysis check

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 and current French ANSSI embedded security experts

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.

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 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://sentry-kernel.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.