1%
2% Copyright 2014, General Dynamics C4 Systems
3%
4% SPDX-License-Identifier: GPL-2.0-only
5%
6
7\chapter{\label{ch:intro}Introduction}
8
9% FIXME: Use of service, mechanism and abstraction is munged through the rest of the manual
10
11The seL4 microkernel is an operating-system kernel designed to be a secure,
12safe, and reliable foundation for systems in a wide variety of application
13domains. As a microkernel, it provides a small number of mechanisms that can be
14used to build applications, such as virtual address spaces, threads, and
15inter-process communication (IPC).
16
17The small number of mechanisms translates to a small implementation on the order
18of $10,000$ lines of C code, depending on architecture and configured features.
19This has enabled formal verification of the
20kernel~\cite{Boyton_09,Cock_KS_08,Derrin_EKCC_06,Elkaduwe_KE_08,Klein_EHACDEEKNSTW_09,Tuch_KN_07,Winwood_KSACN_09}
21in the Isabelle/HOL theorem prover, which in turn enabled proofs of the kernel's
22enforcement of integrity~\cite{Sewell_WGMAK_11} and
23confidentiality~\cite{Murray_MBGBSLGK_13}. The kernel's small size was also
24instrumental in performing a complete and sound analysis of worst-case execution
25time~\cite{Blackham_SCRH_11,Blackham_SH_12}. \citet{Klein_AEMSKH_14} give a
26comprehensive technical summary of the verification, and the seL4 white
27paper~\cite{whitepaper} provides a shorter, but more accessible overview.
28
29Functional correctness proofs for the kernel are available for multiple
30architectures and platforms. For Arm32, this optionally includes hypervisor
31extensions, and the security proofs mentioned above. See the seL4 documentation
32site for the currently supported proofs~\cite{doc_site_proofs}.
33
34This manual describes the seL4 kernel's API from a user's point of view. The
35document starts by giving a brief overview of the seL4 microkernel design,
36followed by a reference of the high-level API exposed by the seL4 kernel to
37userspace.
38
39While we have tried to ensure that this manual accurately reflects the behaviour
40of the seL4 kernel, this document is by no means a formal specification of the
41kernel. When the precise behaviour of the kernel under a particular circumstance
42needs to be known, users should refer to the abstract specification of
43seL4~\cite{seL4_spec}, which gives a fully formal description.
44