History

Gerwin Klein 6fd6d6bd48 arm/arm-hyp: proof updates for Arm cache fix This commit updates the proofs for seL4/seL4#485, which fixes the security and correctness bug seL4/seL4#481. The bug was that caches are not sufficiently flushed in retype for frames that can be mapped uncached later. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>		2021-08-16 16:47:10 +10:00
..
ARM	arm/arm-hyp: proof updates for Arm cache fix	2021-08-16 16:47:10 +10:00
ARM_HYP	arm/arm-hyp: proof updates for Arm cache fix	2021-08-16 16:47:10 +10:00
RISCV64	machine+design: update for platform constant changes	2020-11-16 16:52:40 +11:00
X64	machine+design: update for platform constant changes	2020-11-16 16:52:40 +11:00
MachineExports.thy	all: remove theory import path references	2020-11-02 10:16:17 +10:00
MachineMonad.thy	all: remove theory import path references	2020-11-02 10:16:17 +10:00
README.md	license: provide documentation under CC-BY-SA-4.0	2020-03-16 14:19:15 +08:00
Setup_Locale.thy	licenses: convert license tags to SPDX	2020-03-13 14:38:24 +08:00

The Machine Interface Specification of seL4

l4v/spec/machine/

This directory contains the Isabelle sources for the machine interface specification used in the abstract and design specifications of seL4.

Overview

ARMMachineTypes: ARM register set and related definitions.
MachineOps: definitions for the machine interface functions. Most interface functions are left non-deterministic. Some are assumed not to mutate C-observable state, others are defined in more detail.
MachineTypes: entry point to select a machine. Currently ARM only.
Platform: word size and other basic platform definitions.

This module is not built in isolation, but included in the ASpec and ExecSpec sessions.

the theory ARMMachineTypes is generated from Haskell using the tool in tools/haskell-translator and the skeleton file in spec/design/m-skel.