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