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
11This file lists known caveats in the seL4 API and implementation.
12
13* Implementation Correctness
14
15Only the ARMv7 version on the imx6 platform of seL4 has a correctness proof.
16This proof covers the functional behaviour of the C code of the kernel. It
17does not cover machine code, compiler, linker, boot code, cache and TLB
18management. Compiler and linker can be removed from this list by additionally
19running the binary verification phase of the proof. The proof shows that the
20seL4 C code implements the abstract API specification of seL4, and that this
21specification satisfies the following high-level security properties:
22  * integrity (no write without authority), 
23  * confidentiality (no read without authority), and
24  * intransitive non-interference (isolation between adequately 
25    configured user-level components).
26
27The security property proofs depend on additional assumptions on the correct
28configuration of the system.
29
30
31* Real Time
32
33This version of seL4 is not a real-time kernel. It has a small number of
34potentially long-running kernel operations that are not preemptible (e.g.,
35endpoint deletion and recycling, scheduling, frame and CNode initialisation).
36This may change in future versions.
37
38
39* Recycle Operation
40
41The Recycle operation will not necessarily reset all aspects of an object to
42its initial state. For instance, Recycle for a badged endpoint capability will
43only cancel messages with this badge. Recycle for a page directory will not
44revoke all installed page caps, it will only unmap them. For the precise
45behaviour see the specification.
46
47
48* IPC buffer in globals frame may be stale
49
50When a thread invokes its own TCB object to (re-)register its IPC buffer and
51the thread is re-scheduled immediately, the userland IPC buffer pointer in the
52globals frame may still show the old value. It is updated on the next thread
53switch.
54
55
56* Re-using Address Spaces (ARM and x86):
57
58Before an ASID/page directory/page table can be reused, all frame caps
59installed in it should be revoked. The kernel will not do this automatically
60for the user.
61
62If, for instance, page cap c is installed in the address space denoted by a
63page directory under ASID A, and the page directory is subsequently revoked or
64deleted, and then a new page directory is installed under that same ASID A,
65the page cap c will still retain some authority in the new page directory,
66even though the user intention might be to run the new page directory under a
67new security context. The authority retained is to perform the unmap operation
68on the page the cap c refers to.
69