History

Miki Tanaka 9fb7c5cf4d arm_hyp ainvs: fix a typo		2018-01-30 12:00:25 +11:00
..
ARM	arm ainvs: fix a typo	2018-01-30 12:00:21 +11:00
ARM_HYP	arm_hyp ainvs: fix a typo	2018-01-30 12:00:25 +11:00
X64	x64: update ainvs for asid_map removal	2018-01-11 18:48:37 +11:00
ADT_AI.thy	x64: merge master	2017-07-21 11:27:12 +10:00
AInvs.thy	x64: merge master	2017-07-21 11:27:12 +10:00
AInvsPre.thy	x64: merge master	2017-07-21 11:27:12 +10:00
Arch_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
BCorres2_AI.thy	arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)	2017-11-27 22:05:34 +11:00
BCorres_AI.thy	arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)	2017-11-27 22:05:34 +11:00
Bits_AI.thy	Isabelle2017: update AInvs for RC0	2017-10-30 12:23:26 +11:00
CNodeInv_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
CSpaceInvPre_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
CSpaceInv_AI.thy	Isabelle2017: update AInvs for RC0	2017-10-30 12:23:26 +11:00
CSpacePre_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
CSpace_AI.thy	x64: merge master	2017-07-21 11:27:12 +10:00
DetSchedAux_AI.thy	arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)	2017-11-27 22:05:34 +11:00
DetSchedDomainTime_AI.thy	VER-849: abstractly declare a threads registers have changed	2017-12-13 12:13:36 +11:00
DetSchedInvs_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
DetSchedSchedule_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
Deterministic_AI.thy	VER-849: abstractly declare a threads registers have changed	2017-12-13 12:13:36 +11:00
Detype_AI.thy	Expand eval_bool; add a method word_eqI_solve.	2017-11-01 17:30:46 +11:00
EmptyFail_AI.thy	arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)	2017-11-27 22:05:34 +11:00
Finalise_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
Include_AI.thy	arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)	2017-11-27 22:05:34 +11:00
InterruptAcc_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
Interrupt_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
InvariantsPre_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
Invariants_AI.thy	add constant definitions for bounds on untyped object sizes	2017-12-18 12:58:27 +11:00
IpcCancel_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
Ipc_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
KHeapPre_AI.thy	ainvs: integrate all architectures	2017-08-09 16:57:39 +10:00
KHeap_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
KernelInitSepProofs_AI.thy	Isabelle2016-1: update references to renamed constants and facts	2017-01-05 14:23:05 +11:00
KernelInitSep_AI.thy	Isabelle2016-1: update references to renamed constants and facts	2017-01-05 14:23:05 +11:00
KernelInit_AI.thy	SELFOUR-421: fix coding style	2016-09-22 19:23:28 +10:00
LevityCatch_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
README.md	misc: Proofing and formatting of README.md files.	2014-07-28 13:15:48 +10:00
Retype_AI.thy	arm/arm_hyp ainvs: rename wellformed_arch_obj to arch_valid_obj	2017-08-18 09:49:11 +10:00
Schedule_AI.thy	arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)	2017-11-27 22:05:34 +11:00
SubMonad_AI.thy	repairing AInvs: checks up to the middle of VSpace_AI	2016-01-12 18:10:36 +11:00
Syscall_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
TcbAcc_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
Tcb_AI.thy	arm ainvs: wp rules for simple_ko setter/getter	2017-12-14 18:02:44 +11:00
Untyped_AI.thy	add constant definitions for bounds on untyped object sizes	2017-12-18 12:58:27 +11:00
VSpaceEntries_AI.thy	Isabelle2017: update AInvs for RC0	2017-10-30 12:23:26 +11:00
VSpacePre_AI.thy	Removes all trailing whitespaces	2017-07-12 15:13:51 +10:00
VSpace_AI.thy	x64: merge master	2017-07-21 11:27:12 +10:00

README.md

Abstract Spec Invariant Proof

This proof defines and proves the global invariants of seL4's abstract specification. The invariants are phrased and proved using a monadic Hoare logic described in a TPHOLS '08 paper.

Building

To build from the l4v/ directory, run:

./isabelle/bin/isabelle build -d . -v -b AInvs

Important Theories

The top-level theory where the invariants are proved over the kernel is Syscall_AI; the bottom-level theory where they are defined is Invariants_AI.