History

Matthew Brecknell 84d2889d45 Isabelle2016: merge master into 2016		2016-02-19 16:17:26 +11:00
..
API_DP.thy	Add a top-level file for the capDL API proofs.	2014-07-24 19:56:24 +10:00
Arch_DP.thy	fewer warnings	2015-05-16 19:52:49 +10:00
CNode_DP.thy	Merge branch 'master' into aep-merge	2015-09-10 17:06:45 +10:00
IRQ_DP.thy	DSpecProofs, SepTactics, and SepTacticsExamples finished for isabelle2016-RC2	2016-02-11 11:15:59 +11:00
Invocation_DP.thy	fewer warnings	2015-05-16 19:52:49 +10:00
KHeap_DP.thy	add arch_tcb object to C, rename aep -> ntfn	2015-11-20 16:02:13 +11:00
Kernel_DP.thy	l4v-sabre: proof fix upto InfoFlowC	2016-02-17 11:18:03 +11:00
ProofHelpers_DP.thy	DSpecProofs, SepTactics, and SepTacticsExamples finished for isabelle2016-RC2	2016-02-11 11:15:59 +11:00
README.md	misc: Proofing and formatting of README.md files.	2014-07-28 13:15:48 +10:00
RWHelper_DP.thy	capDL-api: Port to Isabelle 2014.	2014-09-12 11:40:28 +10:00
Retype_DP.thy	proof/capDL-api: 2015 update	2015-05-14 11:41:20 +02:00
Sep_Tactic_Examples.thy	DSpecProofs, SepTactics, and SepTacticsExamples finished for isabelle2016-RC2	2016-02-11 11:15:59 +11:00
TCB_DP.thy	add arch_tcb object to C, rename aep -> ntfn	2015-11-20 16:02:13 +11:00

README.md

CapDL API Proofs

This proof develops a formal API description for a number of the seL4 system calls, of the capDL kernel specification. This API description is a set of lemmas describing the behaviour of various system calls in terms of a separation logic defined over that kernel specification.

When reasoning about system calls this proof treats the kernel like a library invoked directly from user-space and does not reason about scheduling. These proofs are used by the system initialiser proof, as described in the ICFEM '13 paper and Andrew Boyton's PhD thesis.

Building

To build from the l4v/ directory, run:

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

Important Theories

The top-level theory is API_DP. The seL4 API and kernel model are located in Kernel_DP.