Interruptible mCertiKOS with Device Drivers

Commented Coq Development

Table of contents

Main Contextual Refinement Theorem

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
TTrapArgCode2
TTrapArgCode3		 TTrapArgCSource
TTrapArgCSource2		 TrapGenLink
TTrapArg TrapArgGen VMXCode VMXCSource TrapArgGenLink
Virtualization Module
VMX VMXGen VMXIntroCode VMXIntroCSource VMXGenLink
VMXGenAsm VMXGenAsmSource
VMXIntro VMXIntroGen VMCSCode VMCSCSource VMXIntroGenLink
VMXIntroGenAsm VMXIntroGenAsmSource
VMCS VMCSGen VMCSIntroCode VMCSIntroCSource VMCSGenLink
VMCSIntroCodeSetDesc
VMCSIntroCodeSetDefaults
VMCSIntro VMCSIntroGen EPTCode EPTCSource VMCSIntroGenLink
VMCSIntroGenAsm VMCSIntroGenAsmSource
VMCSIntroGenAsm1
VMCSIntro VMCSIntroGen EPTCode EPTCSource VMCSIntroGenLink
EPT EPTGen EPTOpCode EPTOpCSource EPTGenLink
EPTOp EPTOpGen EPTIntroCode EPTIntroCSource EPTOpGenLink
EPTIntroCodeEPTInit EPTOpGenAsmSource
EPTOpGenAsm
EPTIntro EPTIntroGen PProcCode PProcCSource EPTIntroGenLink
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
MShIntroCodeSharedMemInit		 MShIntroCSource ShareOpGenLink
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 DAbsHandlerCode DAbsHandlerCSource ContainerLink
Device Drivers
DAbsHandler AbsHandlerGen -- -- AbsHandlerLink
DHandler HandlerGen DHandlerOpCode DHandlerOpCSource HandlerLink
DHandlerOp HandlerOpGen DHandlerCxtCode DHandlerCxtCSource HandlerOpLink
DHandlerCxt HandlerCxtGen -- -- HandlerCxtLink
DHandlerAsm HandlerAsmGen DHandlerSwAsmCode DHandlerSwAsmSource HandlerAsmLink
DHandlerSw HandlerSwGen DHandlerIntroCode DHandlerIntroCSource HandlerSwLink
DHandlerIntro HandlerIntroGen DConsoleCode DConsoleCSource HandlerIntroLink
DConsole ConsoleGen DLApicCode DLApicCSource ConsoleLink
DLApic LApicGen DIoApicCode DIoApicCSource LApicLink
DIoApic IoApicGen DSerialCode DSerialCSource IoApicLink
DSerial SerialGen DSerialIntroCode DSerialIntroCSource SerialLink
DSerialIntro SerialIntroGen DAbsConsoleBuffIntroCode DAbsConsoleBuffIntroCSource SerialIntroLink
DAbsConsoleBuffIntro AbsConsoleBuffIntroGen -- -- AbsConsoleBuffIntroLink
DConsoleBuffIntro ConsoleBuffIntroGen MBootCode MBootCSource ConsoleBuffIntroLink
MBoot -- -- -- --