1<!--
2    Copyright 2014, General Dynamics C4 Systems
3
4    SPDX-License-Identifier: GPL-2.0-only
5-->
6
7# Known caveats in the seL4 API and implementation
8
9## Implementation Correctness
10
11Only the ARMv7 version on the imx6 platform of seL4 has the full stack of
12correctness proofs. This proof covers the functional behaviour of the C code of
13the kernel. It does not cover machine code, compiler, linker, boot code, cache
14and TLB management. Compiler and linker can be removed from this list by
15additionally running the binary verification tool chain for seL4. The proof
16shows that the seL4 C code implements the abstract API specification of seL4,
17and that this specification satisfies the following high-level security
18properties:
19
20  * integrity (no write without authority),
21  * confidentiality (no read without authority), and
22  * intransitive non-interference (isolation between adequately
23    configured user-level components).
24
25The security property proofs depend on additional assumptions on the correct
26configuration of the system. See the `l4v` repository on github for more
27details.
28
29The x64 port of the kernel without VT-x and VT-d support has a functional
30correctness proof between abstract specification and C code, but without
31security theorems, and the ARMv7 version of the kernel with hypervisor
32extensions also has a functional correctness proofs, but without the security
33theorems. For the precise configuration of these three verified platforms, see
34the corresponding files in the `config/` directory.
35
36Proofs for the MCS version (mixed-criticality systems) and for seL4 on the
37RISC-V architecture are in progress.
38
39
40## Real Time
41
42The default version of seL4 must be configured carefully for use in real-time
43requirements. It has a small number of potentially long-running kernel
44operations that are not preemptible (e.g., endpoint deletion, certain
45scheduling states, frame and CNode initialisation). These can (and must) be
46avoided by careful system configuration if low latency is required.
47
48The MCS configuration of the kernel addresses many of these problems and
49provides principled access control for execution time, but its formal
50verification is currently still in progress.
51
52
53## IPC buffer in globals frame may be stale
54
55When a thread invokes its own TCB object to (re-)register its IPC buffer and
56the thread is re-scheduled immediately, the userland IPC buffer pointer in the
57globals frame may still show the old value. It is updated on the next thread
58switch.
59
60
61## Re-using Address Spaces (ARM and x86):
62
63Before an ASID/page directory/page table can be reused, all frame caps
64installed in it should be revoked. The kernel will not do this automatically
65for the user.
66
67If, for instance, page cap c is installed in the address space denoted by a
68page directory under ASID A, and the page directory is subsequently revoked or
69deleted, and then a new page directory is installed under that same ASID A,
70the page cap c will still retain some authority in the new page directory,
71even though the user intention might be to run the new page directory under a
72new security context. The authority retained is to perform the unmap operation
73on the page the cap c refers to.
74