1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11chapter "Restricted capabilities in the Separation Kernel Abstract Specification" 12 13theory Separation 14imports 15 "ASepSpec.Syscall_SA" 16 "AInvs.AInvs" 17 "Lib.Bisim_UL" 18 "Lib.LemmaBucket" 19begin 20 21text {* 22 The seL4 kernel, when appropriately restricted, is a separation kernel. Any 23 two processes in separate domains should behave the same as if they were 24 processes running on two physically separated machines. They should not be 25 aware of each other's existence and should not be able to communicate with 26 each other except through well-defined channels. Importantly, it must be 27 possible to show that there are no back channels through which one process 28 can determine whether another process exists or what it is doing. 29 30 In seL4 we achieve this by restricting the capabilities that a thread may 31 possess. The restrictions are summarised in the predicate @{text 32 separate_state} below (which indirectly depends on further predicates @{text 33 separate_cnode_cap}, @{text separate_cap}, etc). 34 35 a) A thread may only possess \emph{notification capabilities} 36 (@{text NotificationCap}). 37 38 b) Threads do not have caller capabilities. (A caller capability is a 39 capability, placed in a special slot in the TCB, to allow replies. Since the 40 @{text Reply} capability is disallowed so is the caller capability.) 41 42 c) Pointers to other capability tables are disallowed meaning that the 43 capability tree is flat. i.e. of depth 1 44 45 Initialising the kernel so that these restrictions hold is not covered in 46 the bisimulation proof, but can be achieved using the capDL initialiser. 47 48 Note that this proof does not preclude threads from communicating via shared 49 memory if the threads have been set up accordingly, which again can be done 50 via the capDL initialiser. 51 52 The proof does show that the kernel API after reaching a state that 53 satisifies @{text separate_state} is that of a static separation kernel, 54 that is, it only provides system calls for sending and receiving on 55 notification objects and otherwise exhibits no dynamic behaviour. 56 57 Systems with such a setup satisfy the preconditions of our separate 58 non-intereference proof, which shows that information travels only along 59 these authorised channels. 60*} 61 62definition 63 separate_cap :: "cap \<Rightarrow> bool" 64where 65 "separate_cap cap \<equiv> case cap of 66 NotificationCap ptr badge rights \<Rightarrow> rights \<subseteq> {AllowRecv, AllowSend} 67 | NullCap \<Rightarrow> True 68 | _ \<Rightarrow> False" 69 70 71lemma separate_capE: 72 "\<lbrakk> separate_cap cap; cap = NullCap \<Longrightarrow> R; \<And>ptr badge rights. \<lbrakk> cap = NotificationCap ptr badge rights \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 73 unfolding separate_cap_def 74 by (fastforce split: cap.splits) 75 76definition 77 "separate_cnode_cap cs cap \<equiv> case cap of 78 CNodeCap p bits guard \<Rightarrow> (bits + length guard = word_bits) \<and> 79 (\<forall>off. case_option True separate_cap (cs (p, off))) 80 | NullCap \<Rightarrow> True 81 | _ \<Rightarrow> False" 82 83definition 84 "separate_tcb p cs \<equiv> case_option True (separate_cnode_cap cs) (cs (p, tcb_cnode_index 0)) 85 \<and> cs (p, tcb_cnode_index 3) = Some NullCap" \<comment> \<open>ctable and caller cap\<close> 86 87lemma separate_cnode_cap_rab: 88 "\<lbrakk> separate_cnode_cap cs cap; length cref = word_bits \<rbrakk> \<Longrightarrow> 89 resolve_address_bits (cap, cref) = (case cap of 90 CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then 91 returnOk ((p, drop (length guard) cref), []) 92 else 93 (throwError (GuardMismatch (length cref) guard)) 94 | _ \<Rightarrow> throwError InvalidRoot)" 95 unfolding separate_cnode_cap_def resolve_address_bits_def 96 by (auto simp: word_bits_def split: cap.split_asm) 97 98definition 99 "separate_state s \<equiv> \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)" 100 101 102lemma separate_cnode_capE: 103 "\<lbrakk> separate_cnode_cap cs cap; 104 cap = NullCap \<Longrightarrow> R; 105 \<And>p bits guard. \<lbrakk> cap = CNodeCap p bits guard; bits + length guard = word_bits; 106 (\<forall>off cap'. cs (p, off) = Some cap' \<longrightarrow> separate_cap cap') \<rbrakk> \<Longrightarrow> R \<rbrakk> 107 \<Longrightarrow> R" 108 unfolding separate_cnode_cap_def 109 by (auto split: cap.splits option.splits) 110 111lemma valid_sep_cap_not_cnode: 112 "\<lbrakk> s \<turnstile> cap; \<forall>off cap'. caps_of_state s (p, off) = Some cap' \<longrightarrow> separate_cap cap'; cap = CNodeCap p bits guard; bits \<le> length cref - length guard \<rbrakk> 113 \<Longrightarrow> \<exists>cap'. caps_of_state s (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap'" 114 apply (clarsimp simp: valid_cap_simps not_less in_monad) 115 apply (drule_tac offset = "take bits (drop (length guard) cref)" in cap_table_at_cte_at) 116 apply simp 117 apply (fastforce simp: cte_wp_at_caps_of_state separate_cap_def is_cap_simps) 118 done 119 120lemma bisim_gen_asm_r: 121 assumes bs: "F \<Longrightarrow> bisim_underlying sr r P P' a b" 122 shows "bisim_underlying sr r P (P' and K F) a b" 123 using bs 124 by (fastforce intro!: bisim_underlyingI elim: bisim_underlyingE1 bisim_underlyingE2) 125 126lemma bisim_separate_cap_cases: 127 assumes nc: "cap = NullCap \<Longrightarrow> bisim R Pn Pn' m m'" 128 and ac: "\<And>ptr badge rights. \<lbrakk> cap = NotificationCap ptr badge rights \<rbrakk> 129 \<Longrightarrow> bisim R (Pa ptr badge rights) (Pa' ptr badge rights) m m'" 130 shows "bisim R (\<lambda>s. (cap = NullCap \<longrightarrow> Pn s) 131 \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa ptr badge rights s)) 132 ((\<lambda>s. (cap = NullCap \<longrightarrow> Pn' s) 133 \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa' ptr badge rights s)) 134 and K (separate_cap cap)) m m'" 135 using assms 136 apply - 137 apply (rule bisim_gen_asm_r) 138 apply (erule separate_capE, simp_all) 139 done 140 141lemma caps_of_state_tcb: 142 "\<lbrakk> get_tcb p s = Some tcb; option_map fst (tcb_cap_cases idx) = Some getF \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb)" 143 apply (drule get_tcb_SomeD) 144 apply clarsimp 145 apply (drule (1) cte_wp_at_tcbI [where t = "(p, idx)" and P = "(=) (getF tcb)", simplified]) 146 apply simp 147 apply (clarsimp simp: cte_wp_at_caps_of_state) 148 done 149 150lemma caps_of_state_tcb_cap_cases: 151 "\<lbrakk> get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some ((the (option_map fst (tcb_cap_cases idx))) tcb)" 152 apply (clarsimp simp: dom_def) 153 apply (erule caps_of_state_tcb) 154 apply simp 155 done 156 157lemma separate_state_get_tcbD: 158 "\<lbrakk>separate_state s; get_tcb p s = Some tcb \<rbrakk> \<Longrightarrow> 159 separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> tcb_caller tcb = NullCap" 160 unfolding separate_state_def 161 apply (drule spec [where x = p]) 162 apply (simp add: tcb_at_def separate_tcb_def caps_of_state_tcb_cap_cases dom_tcb_cap_cases) 163 done 164 165end 166