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