1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8 * CAMKES 9 *) 10 11chapter CAmkES 12 13session CamkesAdlSpec (Camkes) in "adl-spec" = Access + 14 options [document = pdf] 15 theories 16 "Wellformed_CAMKES" 17 "Examples_CAMKES" 18 document_files 19 "imgs/compilation.pdf" 20 "imgs/composite-passthrough.pdf" 21 "imgs/dataport.pdf" 22 "imgs/echo.pdf" 23 "imgs/event.pdf" 24 "imgs/terminal.pdf" 25 "intro.tex" 26 "root.tex" 27 "comment.sty" 28 "ulem.sty" 29 30(* Base session for CAmkES<->CapDL reasoning. This session is intended to be simply a combination 31 * of CamkesAdlSpec and DSpec, and is defined because we can't easily depend on both. 32 *) 33session CamkesCdlBase (Camkes) = DPolicy + 34 sessions 35 DSpec 36 CamkesAdlSpec 37 Lib 38 theories 39 "DSpec.Syscall_D" 40 "CamkesAdlSpec.Wellformed_CAMKES" 41 "CamkesAdlSpec.Examples_CAMKES" 42 "Lib.LemmaBucket" 43 44(* CAmkES<->CapDL reasoning. *) 45session CamkesCdlRefine (Camkes) in "cdl-refine" = CamkesCdlBase + 46 theories 47 Policy_CAMKES_CDL 48 Eval_CAMKES_CDL 49 50session CamkesGlueSpec (Camkes) in "glue-spec" = HOL + 51 options [document = pdf] 52 directories 53 "example-procedure" 54 "example-event" 55 "example-dataport" 56 "example-untrusted" 57 "example-trusted" 58 theories 59 Abbreviations 60 CIMP 61 Connector 62 Types 63 UserStubs 64 "example-procedure/GenSimpleSystem" 65 "example-event/GenEventSystem" 66 "example-dataport/GenDataportSystem" 67 "example-untrusted/EgTop" 68 "example-trusted/EgTop2" 69 document_files 70 "dataport.camkes" 71 "event.camkes" 72 "imgs/echo.pdf" 73 "imgs/filter.pdf" 74 "imgs/thydeps.pdf" 75 "intro.tex" 76 "root.bib" 77 "root.tex" 78 "filter.camkes" 79 "simple.camkes" 80 "comment.sty" 81 "ulem.sty" 82 83session CamkesGlueProofs (Camkes) in "glue-proofs" = AutoCorres + 84 options [document = pdf, quick_and_dirty] 85 theories 86 Syntax 87 RPCFrom 88 RPCTo 89 EventFrom 90 EventTo 91 DataIn 92 document_files 93 "eventfrom-emit-underlying.c" 94 "eventto-poll.c" 95 "eventto-wait.c" 96 "from-echo-int.c" 97 "intro.tex" 98 "root.bib" 99 "root.tex" 100 "simple.camkes" 101 "to-echo-int.c" 102 "comment.sty" 103 "ulem.sty" 104