Welcome to Sentry documentation!

Contents:

• Sentry Concepts
  • Initial conception model
    • Micro-kernel design
    • Application developer model
    • About general tasking model
    • Tasks properties
    • job entrypoint
    • Mapping tasks
  • Architectural model
    • Micro-kernel responsibility
    • Micro-kernel design: handles
    • Micro-kernel design: events
    • Other user-space/kernel-space communication concepts
    • Micro-kernel design for portability
  • About events
    • About shared memories
    • About DMA streams
    • About signals
    • About Interrupts
  • Security in Sentry
    • Security requirements
    • About stack smashing protection
    • About compile-time hardening
    • About the usage of anti-temper detection coprocessor
• Sentry UAPI
  • UAPI model
    • UAPI introduction
    • UAPI abstraction
  • Syscalls
    • About basics
    • Syscall definition
• Sentry Build system
  • Basics and targets
    • Dependencies
    • About Sentry sources hierarchy
    • Cross-compilation concept
    • Bootstraping Sentry build
    • Building Sentry
    • Testing Sentry
    • Prooving Sentry
  • System View Description (SVD) integration
  • Devicetree integration
    • Properties
    • chosen node
    • reserved-memory node
• Sentry software architecture
  • Hardware support in Sentry
    • Basics about HAL
  • Adding a new board
  • Adding a new SoC
    • Update SVD database
    • Adding the manufacturer dtsi file
    • Adding a new SoC BSP in Sentry sources
  • Adding a new architecture
  • Sentry schedulers
    • Scheduling basics
    • RRMQ scheduler
    • RMA scheduler
    • FIFO scheduler
    • Scheduling and syscalls
  • Task layout
    • Introduction to generic task layout
    • Layout initialization at system startup
    • Forging and holding task layout
    • Increase context switch speed
  • About user devices
    • Device list generation and kernel storage
    • (Un)mapping devices
    • Linking IRQ with its owner
• Sentry Tests
  • Unit testing Sentry
    • Unit testing framework
    • Building and testing modules on build host
    • Mocking externals, checking behaviors
  • Sentry Autotest mode
    • About Autotest
    • Runtime kernel testing
    • Defining a test
    • About tests and capabilities
• Sentry Formal Proof
  • Basic principles
    • About Frama-C
    • Frama-C integration in Sentry
    • Impact of formal proofness in kernel design
  • Value analysis
    • About EVA
    • EVA integration with Sentry kernel
    • EVA coverage
    • Alarms and reports
  • Functional correctness
    • About WP
    • WP and composition-based correctness
    • Correctness of hardware manipulation
    • Correctness of security model

This is the Sentry kernel architecture and API documentation. 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.

The Sentry kernel is a part of the Camelot Operating System, built to deploy a high level security upto the micro-controller, ensuring secure manipulation of complex or performance critical I/O the SE is not able to handle.