1%
2% Copyright 2014, General Dynamics C4 Systems
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(GD_GPL)
9%
10
11\chapter{\label{ch:intro}Introduction}
12
13% FIXME: Use of service, mechanism and abstraction is munged through here and the rest of the manual
14
15The seL4 microkernel is an operating-system kernel designed to be
16a secure, safe, and reliable foundation for systems in a wide variety of
17application domains. As a microkernel, it provides a small number of
18services to applications, such as abstractions to create and manage virtual address
19spaces, threads, and inter-process communication (IPC). The small number
20of services provided by seL4 directly translates to a small
21implementation of approximately $8700$ lines of C code. This has allowed
22the ARMv6 version of the kernel to be formally proven in the Isabelle/HOL 
23theorem prover to adhere to its formal
24specification~\cite{Boyton_09,Cock_KS_08,Derrin_EKCC_06,Elkaduwe_GE_08,Klein_EHACDEEKNSTW_09,Tuch_KN_07,Winwood_KSACN_09},
25which in turn enabled proofs of the kernel's enforcement of
26integrity~\cite{Sewell_WGMAK_11} and
27confidentiality~\cite{Murray_MBGBSLGK_13}. The kernel's small size was
28also instrumental in performing a complete and sound analysis of
29worst-case execution time~\cite{Blackham_SCRH_11,Blackham_SH_12}.
30
31This manual describes the seL4 kernel's API from a user's point of view.
32The document starts by giving a brief overview of the seL4 microkernel
33design, followed by a reference of the high-level API exposed by the
34seL4 kernel to userspace.
35
36While we have tried to ensure that this manual accurately reflects the
37behaviour of the seL4 kernel, this document is by no means a formal
38specification of the kernel. When the precise behaviour of the kernel
39under a particular circumstance needs to be known, users should refer to
40the seL4 abstract specification, which
41gives a formal description of the seL4 kernel.
42