The seL4 microkernel https://sel4.systems/

CAVEATS-generic.txt 2.8KB

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