History

Matthew Brecknell 84d2889d45 Isabelle2016: merge master into 2016		2016-02-19 16:17:26 +11:00
..
Asid_D.thy	fix DSpecProofs	2014-09-09 15:57:52 +10:00
CNode_D.thy	add arch_tcb object to C, rename aep -> ntfn	2015-11-20 16:02:13 +11:00
CSpace_D.thy	more fixes in DRefine: some changes in proofs involving uint / unat	2016-01-28 14:07:42 +11:00
Decode_D.thy	add arch_tcb object to C, rename aep -> ntfn	2015-11-20 16:02:13 +11:00
Endpoint_D.thy	terminology in comments: async ep -> notifications	2015-11-24 16:58:22 +13:00
Intents_D.thy	l4v-sabre: change type of irq to be 10 word	2016-02-17 11:18:02 +11:00
Interrupt_D.thy	msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API	2016-02-02 15:57:28 +11:00
Invocations_D.thy	msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API	2016-02-02 15:57:28 +11:00
KHeap_D.thy	release cleanup	2014-07-17 18:22:50 +02:00
Monads_D.thy	Import release snapshot.	2014-07-14 21:32:44 +02:00
PageTableUnmap_D.thy	more fixes in DRefine: some changes in proofs involving uint / unat	2016-01-28 14:07:42 +11:00
PageTable_D.thy	page_map_unmap_cancel : cdl spec changed and drefine fixed.	2014-09-05 14:48:22 +10:00
README.md	misc: Proofing and formatting of README.md files.	2014-07-28 13:15:48 +10:00
Schedule_D.thy	Import release snapshot.	2014-07-14 21:32:44 +02:00
Syscall_D.thy	Wait -> Recv: update specs	2015-11-20 16:02:14 +11:00
Tcb_D.thy	add arch_tcb object to C, rename aep -> ntfn	2015-11-20 16:02:13 +11:00
Types_D.thy	l4v-sabre: change type of irq to be 10 word	2016-02-17 11:18:02 +11:00
Untyped_D.thy	release cleanup	2014-07-17 18:22:50 +02:00

README.md

The capDL Specification of seL4

l4v/spec/capDL/

This directory contains the Isabelle sources of the seL4 behaviour specification on the capDL abstraction level. The key features of this abstraction level are that it models the complete protection state of the kernel in terms of capabilities, and models, as far as possible, only the protection state of the kernel (no memory or other state). This means, the capDL specification contains a significantly higher degree of nondeterminism compared to the other seL4 specs.

This specification is useful for the user-level initialiser that brings the system from boot state into a defined protection state defined by a concrete capDL description.

There is a refinement proof between the abstract specification and the capDL specification in proof/drefine/. The capDL spec also forms the basis of the system initialiser proofs.

Top-Level Theory

The top-level theory file in the specification is Syscall_D, the top-level function in that theory is call_kernel.

Entry Points

A key theory in the capDL spec is Types_D which defines a new capability type that in addition to the seL4 capabilities contains 'virtual' capabilities which store protection state information. For instance, the state of MMU page tables is uniformly modelled as capabilities.

Building

The corresponding Isabelle session is DSpec. To build, run in directory l4v/spec:

make DSpec