2014-07-14 19:32:44 +00:00
|
|
|
(*
|
|
|
|
* Copyright 2014, General Dynamics C4 Systems
|
|
|
|
*
|
|
|
|
* This software may be distributed and modified according to the terms of
|
|
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
|
|
*
|
|
|
|
* @TAG(GD_GPL)
|
|
|
|
*)
|
|
|
|
|
|
|
|
chapter "Proofs"
|
|
|
|
|
|
|
|
(*
|
|
|
|
* List of rules to make various images.
|
|
|
|
*
|
|
|
|
* Some rules have duplicate targets of the form:
|
|
|
|
*
|
|
|
|
* theories [condition = "MOO", quick_and_dirty]
|
|
|
|
* "foo"
|
|
|
|
* theories
|
|
|
|
* "foo"
|
|
|
|
*
|
|
|
|
* The idea is that if the environment variable "MOO" is defined we
|
|
|
|
* execute the first rule (doing the proof in quick-and-dirty mode), and
|
|
|
|
* then find we need not take any action for the second. Otherwise, we
|
|
|
|
* skip the first rule and only perform the second.
|
|
|
|
*)
|
|
|
|
|
|
|
|
(*
|
|
|
|
* Refinement proof.
|
|
|
|
*)
|
|
|
|
|
|
|
|
session Refine = BaseRefine +
|
|
|
|
description {* Refinement between Haskell and Abstract spec. *}
|
2017-03-13 03:55:36 +00:00
|
|
|
theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
|
2017-01-30 01:22:22 +00:00
|
|
|
"refine/$L4V_ARCH/Refine"
|
2017-08-08 02:19:43 +00:00
|
|
|
theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
|
|
|
|
"refine/$L4V_ARCH/Refine"
|
2017-03-13 03:55:36 +00:00
|
|
|
theories
|
2017-02-22 04:29:02 +00:00
|
|
|
"refine/$L4V_ARCH/Refine"
|
2017-03-25 12:00:56 +00:00
|
|
|
|
|
|
|
session BaseRefine2 = BaseRefine +
|
|
|
|
description {* Intermediate point in refinement proof. Useful for machines with small RAM. *}
|
2017-08-08 06:11:20 +00:00
|
|
|
theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs]
|
2017-03-25 12:00:56 +00:00
|
|
|
"refine/$L4V_ARCH/Untyped_R"
|
|
|
|
"refine/$L4V_ARCH/Schedule_R"
|
|
|
|
theories
|
|
|
|
"refine/$L4V_ARCH/Untyped_R"
|
|
|
|
"refine/$L4V_ARCH/Schedule_R"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
session BaseRefine = AInvs +
|
|
|
|
description {* Background theory and libraries for refinement proof. *}
|
2017-08-08 06:11:20 +00:00
|
|
|
theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs]
|
2017-03-23 12:02:55 +00:00
|
|
|
"refine/$L4V_ARCH/Include"
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
2017-01-30 01:22:22 +00:00
|
|
|
"refine/$L4V_ARCH/Include"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
session AInvs = ASpec +
|
2017-08-08 06:11:20 +00:00
|
|
|
theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs]
|
2016-05-16 09:45:59 +00:00
|
|
|
"invariant-abstract/AInvs"
|
2017-03-23 12:02:55 +00:00
|
|
|
"invariant-abstract/KernelInit_AI"
|
|
|
|
"invariant-abstract/DetSchedSchedule_AI"
|
2017-08-08 06:11:20 +00:00
|
|
|
theories [condition = "AINVS_QUICK_AND_DIRTY", quick_and_dirty]
|
2016-08-03 05:36:28 +00:00
|
|
|
"invariant-abstract/AInvs"
|
|
|
|
"invariant-abstract/KernelInit_AI"
|
|
|
|
"invariant-abstract/DetSchedSchedule_AI"
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
|
|
|
"invariant-abstract/AInvs"
|
|
|
|
"invariant-abstract/KernelInit_AI"
|
2017-02-10 04:52:31 +00:00
|
|
|
"invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
* C Refinement proof.
|
|
|
|
*)
|
|
|
|
|
2014-09-18 10:12:43 +00:00
|
|
|
session CRefineSyscall = CBaseRefine +
|
2017-04-16 06:36:47 +00:00
|
|
|
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
|
|
|
|
"crefine/$L4V_ARCH/Syscall_C"
|
2014-09-18 10:12:43 +00:00
|
|
|
theories
|
2017-03-30 16:32:25 +00:00
|
|
|
"crefine/$L4V_ARCH/Syscall_C"
|
2014-09-18 10:12:43 +00:00
|
|
|
|
2014-07-14 19:32:44 +00:00
|
|
|
session CRefine = CBaseRefine +
|
2017-04-12 22:31:27 +00:00
|
|
|
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
|
|
|
|
"crefine/$L4V_ARCH/Refine_C"
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
2017-03-30 16:32:25 +00:00
|
|
|
"crefine/$L4V_ARCH/Refine_C"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
session CBaseRefine = CSpec +
|
2017-08-08 06:11:20 +00:00
|
|
|
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
|
2017-03-30 16:32:25 +00:00
|
|
|
"crefine/$L4V_ARCH/Include_C"
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
2017-03-30 16:32:25 +00:00
|
|
|
"crefine/$L4V_ARCH/Include_C"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
* CapDL Refinement
|
|
|
|
*)
|
|
|
|
|
|
|
|
session DBaseRefine = Refine +
|
|
|
|
theories
|
|
|
|
"drefine/Include_D"
|
|
|
|
|
|
|
|
session DRefine = DBaseRefine +
|
|
|
|
theories
|
|
|
|
"drefine/Refine_D"
|
|
|
|
|
|
|
|
session DPolicy = DRefine +
|
|
|
|
theories
|
|
|
|
"access-control/Dpolicy"
|
|
|
|
|
|
|
|
(*
|
|
|
|
* Infoflow and Access
|
|
|
|
*)
|
|
|
|
|
|
|
|
session Access in "access-control" = AInvs +
|
|
|
|
theories
|
|
|
|
"Syscall_AC"
|
|
|
|
"ExampleSystem"
|
|
|
|
|
|
|
|
session InfoFlow in "infoflow" = Access +
|
|
|
|
theories
|
|
|
|
"Noninterference"
|
|
|
|
theories
|
|
|
|
"Noninterference_Base_Refinement"
|
|
|
|
"PolicyExample"
|
|
|
|
"PolicySystemSAC"
|
|
|
|
"ExampleSystemPolicyFlows"
|
|
|
|
"Example_Valid_State"
|
|
|
|
|
2016-11-15 06:14:36 +00:00
|
|
|
session InfoFlowCBase = CRefine +
|
2017-08-08 06:11:20 +00:00
|
|
|
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
|
2016-11-15 06:14:36 +00:00
|
|
|
"infoflow/Include_IF_C"
|
|
|
|
theories
|
|
|
|
"infoflow/Include_IF_C"
|
|
|
|
|
|
|
|
session InfoFlowC = InfoFlowCBase +
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
|
|
|
"infoflow/Noninterference_Refinement"
|
2014-11-18 06:33:30 +00:00
|
|
|
"infoflow/Example_Valid_StateH"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
(*
|
|
|
|
* capDL
|
|
|
|
*)
|
|
|
|
|
|
|
|
session SepDSpec = DSpec +
|
|
|
|
theories
|
|
|
|
"sep-capDL/Frame_SD"
|
|
|
|
|
|
|
|
session DSpecProofs in "capDL-api" = SepDSpec +
|
|
|
|
theories
|
2014-07-24 09:56:24 +00:00
|
|
|
"API_DP"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
2014-08-13 12:08:46 +00:00
|
|
|
(*
|
|
|
|
* Static Separation Kernel Bisimilarity
|
|
|
|
*)
|
|
|
|
|
|
|
|
session Bisim in bisim = AInvs +
|
|
|
|
theories
|
|
|
|
"Syscall_S"
|
|
|
|
files
|
|
|
|
"document/root.tex"
|
|
|
|
"document/build"
|
|
|
|
"document/Makefile"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
(*
|
|
|
|
* Separation Logic
|
|
|
|
*)
|
|
|
|
|
2016-04-18 11:24:23 +00:00
|
|
|
session SepTactics = Word_Lib +
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
|
|
|
"../lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics"
|
|
|
|
|
|
|
|
session SepTacticsExamples = SepTactics +
|
|
|
|
theories [quick_and_dirty]
|
|
|
|
"capDL-api/Sep_Tactic_Examples"
|
|
|
|
|
|
|
|
|
2014-09-05 09:08:11 +00:00
|
|
|
(*
|
|
|
|
* Binary Verification Input Step
|
|
|
|
*)
|
|
|
|
session SimplExportAndRefine = CSpec +
|
|
|
|
theories
|
|
|
|
"asmrefine/SEL4SimplExport"
|
|
|
|
"asmrefine/SEL4GraphRefine"
|
|
|
|
|
2015-05-22 03:55:35 +00:00
|
|
|
session SimplExportOnly = CSpec +
|
|
|
|
theories
|
|
|
|
"asmrefine/SEL4SimplExport"
|
|
|
|
|
2014-07-14 19:32:44 +00:00
|
|
|
(*
|
|
|
|
* Libraries
|
|
|
|
*)
|
|
|
|
|
|
|
|
session AutoLevity = AutoLevity_Base +
|
|
|
|
theories
|
|
|
|
"../lib/autolevity_buckets/AutoLevity_Top"
|
|
|
|
|
2017-07-12 05:13:51 +00:00
|
|
|
session AutoLevity_Base = Word_Lib +
|
2014-07-14 19:32:44 +00:00
|
|
|
theories
|
|
|
|
"../lib/autolevity_buckets/AutoLevity_Base"
|
|
|
|
|