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