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 here and the rest of the manual
10
11The seL4 microkernel is an operating-system kernel designed to be
12a secure, safe, and reliable foundation for systems in a wide variety of
13application domains. As a microkernel, it provides a small number of
14services to applications, such as abstractions to create and manage virtual address
15spaces, threads, and inter-process communication (IPC). The small number
16of services provided by seL4 directly translates to a small
17implementation of approximately $8700$ lines of C code. This has allowed
18the ARMv6 version of the kernel to be formally proven in the Isabelle/HOL 
19theorem prover to adhere to its formal
20specification~\cite{Boyton_09,Cock_KS_08,Derrin_EKCC_06,Elkaduwe_GE_08,Klein_EHACDEEKNSTW_09,Tuch_KN_07,Winwood_KSACN_09},
21which in turn enabled proofs of the kernel's enforcement of
22integrity~\cite{Sewell_WGMAK_11} and
23confidentiality~\cite{Murray_MBGBSLGK_13}. The kernel's small size was
24also instrumental in performing a complete and sound analysis of
25worst-case execution time~\cite{Blackham_SCRH_11,Blackham_SH_12}.
26
27This manual describes the seL4 kernel's API from a user's point of view.
28The document starts by giving a brief overview of the seL4 microkernel
29design, followed by a reference of the high-level API exposed by the
30seL4 kernel to userspace.
31
32While we have tried to ensure that this manual accurately reflects the
33behaviour of the seL4 kernel, this document is by no means a formal
34specification of the kernel. When the precise behaviour of the kernel
35under a particular circumstance needs to be known, users should refer to
36the seL4 abstract specification, which
37gives a formal description of the seL4 kernel.
38