About

The Sentry kernel is a high security level micro-kernel implementation made for high security embedded systems that include micro-controllers in association with dedicated Secure Element component for security cryptographic functions.

Complete Sentry documentation is published on readthedocs.

Sentry kernel uses The Meson Build System.

Prerequisites

Tools installation

Before building the project, one needs to install the build system and related tool. This project use the meson reference implementation in python. All dependencies are described in requirements.txt.

pip3 install -r requirements.txt

Cross Toolchain

This kernel aims to be fully portable. Its initial target are ARM Cortex-M MCUs (starting with STM32) and thus one needs a cross toolchain for such target. One can use any cross toolchain as long as this is a GNU compatible compiler for Cortex-M. The reference toolchain used for CI/CD is bundled in this project using meson wrap mechanism.

Cross-toolchain relative need to be declared so that the meson build system is able to detect overall cross-compilers and associated tools. This is done by defining cross-files. The meson build system describes these cross file here.

Project bootstrap

A common good practice is do not inject environment variable for build configuration. For this purpose, meson does not allow using relative path in toolchain definition. Toolchain path must be absolute.

One needs to deliver to the meson build system the kernel configuration based on Kconfig. This can be done with kconfiglib that is listed in requirements.txt. The kernel configuration is generated into a local .config` file that holds the complete kernel configuration, and that is used at build time to select the corresponding sources and features.

Using defconfigs

defconfig files are stored in configs/ directory and can be used directly. In that case, the defconfig must be parsed in order to forge a .config file. This file is then passed to the config option at setup time:

defconfig configs/stm32f4_debug_defconfig
meson setup -Dconfig=.config [...]

If a complete config file is used, it can be directly passed to the config option.

Setting custom configurations

Generating the configuration is made using the standard Linux Kconfig UI. This interface can be called by ninja by targetting the kconfig module's menuconfig target:

ninja -C builddir kconfig@@menuconfig

Or by calling menuconfig directly. This, one need to have kconfig venv set correctly (srctree and subprojects). This can be done by using Meson devenv

meson devenv -C builddir
menuconfig

How to build

About build options

The Sentry kernel has the following configuration options, that can be added at meson setup time using -D<optname>=<optvalue>

• with_doc (boolean, false): Enable support for building docs
• with_tests (boolean, false): Enable unit test suite support through meson test
• with_proof (boolean, false): Enable support for frama-C analysis through meson test
• with_kernel (boolean, true): Enable kernel binary build
• with_uapi (boolean, true): Enable kernel UAPI library build
• with_idle (boolean, true): Enable kernel Idle task build
• with_tools (boolean, true): Enable build host native tooling build
• config: (string): path to the defconfig file. Can be externally provided, while respecting the kernel Kconfig
• dts (string): DTS file path, may be local or any externaly provided DTS file
• dts-include-dirs (array): DTS file include dir for dtsi resolution, depending on the DTS file content

It is to note that all the with_ options are not mandatory, while others are.

meson setup

The first step in meson build is project setup, this will create a specific build directory for the given options. This step also configures the toolchain to use.

Some cross-files describing toolchain configuration are set in support/meson directory. More than one cross file can be used if needed.

meson setup [-Doption ...] --cross-file=</path/to/cross/file> <builddir>

A typical complete setup of the Sentry kernel can then be, in a standalone mode:

defconfig configs/stm32f429i_disc1_autotest_defconfig
meson setup -Dwith_doc=true -Dwith_tests=true -Ddts=dts/examples/stm32f429i_disc1_autotest.dts -Dconfig=.config --cross-file support/meson/armv7m.ini --cross-file support/meson/cortex-m4.ini builddir

build

Once meson build directory is setup, the build step is as simple as calling ninja.

ninja -C builddir

proof

Sentry kernel proof is supported by Frama-C framework. It is based on the analysis of the libsentry sources, which include all the kernel drivers, services, etc. except the kernel entrypoint.

INFO: the Frama-C framework used is Cobalt (27), with why3 and cvc4. Meson check that they are installed on the system.

Frama-C targetts are hosted in the proof directory and are activable using the with_proof option:

meson setup -Dwith_proof=true [...]

It can be directly used with the cross configuration, as frama-C only preprocess the sources and then natively parse the C code into its own AST in order to analyse the source correctness.

FramaC execution is controled through the meson test framework (see tests chapter) and thus is directly accessible through the test command. All Frama-C tests are a part of the same suite denoted proof. If both proofs and tests are enabled in the very same time, the proof tests can then be called separatelly by calling only the proof suite.

FramaC tests can be listed using:

$ meson test -C builddir/ --list
sentry-kernel:proof / frama-C-parsing
sentry-kernel:proof / frama-c-eva-entrypoint
sentry-kernel:proof / frama-C-eva-handler-systick
sentry-kernel:proof / frama-c-eva-handler-svc
sentry-kernel:proof / frama-c-eva-zlib
sentry-kernel:proof / frama-C-eva-handler-systick-redalarm
sentry-kernel:proof / frama-c-eva-handler-svc-redalarm
sentry-kernel:proof / frama-c-eva-zlib-redalarm
[...]

Each Frama-C execution is stored in a dedicated build directory that hold all usual files such as session file, red alarms, flamgraph and so on, that allows various post-processing, such as results analysis or Frama-C tools usage such as ivette or frama-c-gui.

tests

Unit testing

Sentry kernel supports unit testing. This is done using the gtest framework. Analysis of various components of the Sentry kernel is made by emulating, for each subcomponent, the ecosystem it needs in order to simulate the target. For e.g., the EXTI driver is unit-tested using an emulated EXTI device mapped at the very same memory address map as the effective device, so that the device driver do not need any modifiacations while tested.

Other non-HW related components are tested for their expected behavior, in multiple nominal and borderline cases.

Enabling the test suite is made by activating the tests at setup time:

meson setup -Dwith_tests=true [...]

The test framework is based on multiple test suites. The suite names can be listed using the standard meson test target:

meson test -C <builddir> --list
sentry-kernel:ut-utils / io
sentry-kernel:ut-utils / bits
sentry-kernel:ut-bsp / exti

Each test suite (or even test) can be executed independently if needed:

meson test -C <builddir> --suite ut-utils
[...]

Pre-integration tests with autotest

Sentry support a special applications named autotest (see concepts) that is built in autotest mode in order to execute and validate the overall Sentry UAPI for efficient performance and anti-regression testing.

When build in autotest mode, the build system generate a dedicated firmware.hex file, in which Sentry kernel automatically load and start the autotest application. Autotest results can be manually read from serial output, or can be parsed, generating a full report using robotframework. The robot files are written in the tools/robot subdir and can be directly called by robotframework, generating a complete report.

When installed, the kernel build system install target deploy the robot files in the $datadir/robotframework directory

In order to support example robot files, robotframework-pyocd>=0.2.0 and robotframework-pyserial>=1.2.0 python packages are required. A typical usage of robot files of the kernel would be, considering the following pyocd list content:

pyocd list
  #   Probe/Board       Unique ID                  Target
---------------------------------------------------------------------
  0   STLINK-V3         004300483232510239353236   ✔︎ stm32u5a5zjtxq
      NUCLEO-U5A5ZJ-Q

  1   STM32 STLink      0671FF575251717867205336   ✔︎ stm32f429zitx
      DISCO-F429Z

robot --variable FIRMWARE_FILE:builddir/firmware.hex --variable PROBE_UID:004300483232510239353236 -d results ./tools/robot/sentry-autotest.robot

All results (report and logs) are then deployed in the results local directory.

Documentation

Sentry documentation is written in the doc/ subdirectory. It can be build if the with_doc flag is set to true.

There are multiple doc types:

• concepts: Overall Sentry concepts definition, and high level documentation, targetting the user or application developer
• internals: Sentry internal code hierarchy, mostly built using doxygen. This doc is for kernel developers
• mandb: Sentry UAPI manuals, in groff (man) format, so that it can be used with the man utitily

The ninja targets associated to these documentations are doc-concepts (doc-concepts-pdf for PDF generation), doc-internals and mandb.

Generated documentation is in the $BUILDDIR/doc directory, and are also deployed in /usr/share/doc in case of the usage of the install target.

More information about the various concepts of the Sentry-kernel and its build system can be found in the concepts documentation.