mCertiKOS_hyp
Commented Coq development
Table of contents
Main Contextual Refinement Theorem
Security Theorems
Layers of mCertiKOS
Layer
Refinement Proof
Code Verification
Source Code
Linking
Trap Module
TSysCall
SysCallGen
SysCallGenAsm
SysCallGenAsmSource
SysCallGenLink
SysCallGenAsm2
TDispatch
DispatchGen
TTrapCode
TTrapCSource
DispatchGenLink
TTrap
TrapGen
TTrapArgCode
TTrapArgCSource
TrapGenLink
TTrapArgCode2
TTrapArg
TrapArgGen
VMXCode
VMXCSource
TrapArgGenLink
Process Management
PProc
ProcGen
PUCtxtCode
PUCtxtCSource
ProcGenLink
PUCtxtAsmCode
PUCtxtAsmSource
PUCtxtAsmCode1
PUCtxt
UCtxtGen
PIPCCode
PIPCCSource
UCtxtGenLink
PIPC
IPCGen
PIPCIntroCode
PIPCIntroCSource
IPCGenLink
PIPCIntro
IPCIntroGen
PThreadCode
PThreadCSource
IPCIntroGenLink
PThread
ThreadGen
PTDIntroAsmCode
PTDIntroAsmSource
ThreadGenLink
PTDIntroAsmCode1
PTDIntro
TDIntroGen
PCurIDCode
PCurIDCSource
TDIntroGenLink
PCurIDAsmCode
PCurIDAsmCSource
PCurID
CurIDGen
PAbQCode
PAbQCSource
CurIDGenLink
PAbQ
AbQGen
--
--
AbQGenLink
PTdQ
TdQGen
PTdQIntroCode
PTdQIntroCSource
TdQGenLink
PTdQIntro
TdQIntroGen
PTCBCode
PTCBCSource
TdQIntroGenLink
PTCB
TCBGen
PTCBIntroCode
PTCBIntroCSource
TCBGenLink
PTCBIntro
TCBIntroGen
PKCtxCode
PKCtxCSource
TCBIntroGenLink
PKCtx
KCtxGen
PKCtxIntroCode
PKCtxIntroCSource
KCtxGenLink
PKCtxIntro
KCtxIntroGen
MShareCode
MShareCSource
KCtxIntroGenLink
MShareAsmCode
MShareAsmSource
Memory Management
MShare
ShareGen
MShareOpCode
MShareOpCSource
ShareGenLink
MShareOp
ShareOpGen
MShIntroCode
MShIntroCSource
ShareOpGenLink
MShIntroCodeSharedMemInit
MShIntro
ShIntroGen
MPMapCode
MPMapCSource
ShIntroGenLink
MPMap
PMapGen
MPTBitCode
MPTBitCSource
PMapGenLink
MPTBit
PTBitGen
MPTInitCode
MPTInitCSource
PTBitGenLink
MPTInit
PTInitGen
MPTKernCode
MPTKernCSource
PTInitGenLink
MPTKern
PTKernGen
MPTComCode
MPTComCSource
PTKernGenLink
MPTCom
PTComGen
MPTOpCode
MPTOpCSource
PTComGenLink
MPTOp
PTOpGen
MPTIntroCode
MPTIntroCSource
PTOpGenLink
MPTIntro
PTIntroGen
MATCode
MATCSource
PTIntroGenLink
MAT
ATGen
MATOpCode
MATOpCSource
ATGenLink
MATOp
ATOpGen
MATIntroCode
MATIntroCSource
ATOpGenLink
MATIntro
ATIntroGen
MContainerCode
MContainerCSource
ATIntroGenLink
MContainer
ContainerGen
MBootCode
MBootCSource
ContainerGenLink
MBoot
--
--
--
--