1 theory Dynamic2static

     2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2

     3 begin

     4 

     5 context tainting_s begin

     6 

     7 lemma many_sq_imp_sms:

     8   "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm"

     9 sorry

    10 

    11 definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100)

    12 where

    13   "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss"

    14 

    15 lemma [simp]: "ss \<doteq> ss"

    16 by (auto simp:init_ss_eq_def)

    17 

    18 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101)

    19 where

    20   "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"

    21 

    22 lemma s2ss_included_sobj:

    23   "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"

    24 by (simp add:s2ss_def, rule_tac x = obj in exI, simp)

    25 

    26 lemma init_ss_in_prop:

    27   "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>

    28    \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"

    29 apply (simp add:init_ss_in_def init_ss_eq_def)

    30 apply (erule bexE, erule conjE)

    31 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj)

    32 done

    33 

    34 

    35 

    36 

    37 

    38 

    39 lemma d2s_main_execve:

    40   "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static"

    41 apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve)

    42 sorry

    43 

    44 lemma d2s_main:

    45   "valid s \<Longrightarrow> s2ss s \<propto> static"

    46 apply (induct s, simp add:s2ss_nil_prop init_ss_in_def)

    47 apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init)

    48 apply (frule vd_cons, frule vt_grant_os, simp)

    49 apply (case_tac a) 

    50 apply (clarsimp simp add:s2ss_execve)

    51 apply (rule conjI, rule impI)

    52 

    53 

    54 

    55 sorry

    56 

    57 definition enrich:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"

    58 where

    59   "enrich s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. obj' \<notin> objs \<and> alive s' obj \<and> co2sobj s' obj' = co2sobj s' obj"

    60 

    61 definition reserve:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"

    62 where

    63   "reserve s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj"

    64 

    65 definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool"

    66 where

    67   "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enrich s objs s' \<and> reserve s objs s'"

    68 

    69 definition is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"

    70 where

    71   "is_created s obj \<equiv> init_alive obj \<longrightarrow> deleted obj s"

    72 

    73 definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"

    74 where

    75   "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s"

    76 

    77 lemma is_inited_eq_not_created:

    78   "is_inited s obj = (\<not> is_created s obj)"

    79 by (auto simp:is_created_def is_inited_def)

    80 

    81 (* recorded in our static world *)

    82 fun recorded :: "t_object \<Rightarrow> bool"

    83 where

    84   "recorded (O_proc p)     = True"

    85 | "recorded (O_file f)     = True"

    86 | "recorded (O_dir  f)     = True"

    87 | "recorded (O_node n)     = False" (* cause socket is temperary not considered *)

    88 | "recorded (O_shm  h)     = True"

    89 | "recorded (O_msgq q)     = True"

    90 | "recorded _              = False"

    91 

    92 lemma enrichability: 

    93   "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>

    94    \<Longrightarrow> enrichable s objs"

    95 proof (induct s arbitrary:objs)

    96   case Nil

    97   hence "objs = {}" 

    98     apply (auto simp:is_created_def)

    99     apply (erule_tac x = x in ballE)

   100     apply (auto simp:init_alive_prop)

   101     done

   102   thus ?case using Nil unfolding enrichable_def enrich_def reserve_def

   103     by (rule_tac x = "[]" in exI, auto)

   104 next

   105   case (Cons e s)

   106   hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj \<Longrightarrow> enrichable s objs"

   107     and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"

   108     and os: "os_grant s e" and se: "grant s e" and vd: "valid s"

   109     by (auto dest:vt_grant_os vd_cons vt_grant)

   110   show ?case

   111   proof (cases e)

   112     case (Execve p f fds)

   113     hence p4: "e = Execve p f fds" by simp

   114     from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs"

   115       by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"])

   116     show "enrichable (e # s) objs"

   117     proof (case "is_inited s (O_proc p)")

   118       apply (simp add:enrichable_def p4)

   119 

   120       

   121   

   122     apply auto

   123     apply (auto simp:enrichable_def)

   124 apply (induct s)

   125 

   126 

   127 

   128 done

   129 

   130 

   131 (* for the object set, there exists another trace which keeps this objects but also add new identical objects

   132  * that have the same static-signature

   133  *)

   134 

   135 definition potential_trace:: "t_state \<Rightarrow> bool"

   136 where

   137   "potential_trace s \<equiv> \<forall> obj. alive s obj \<and> is_created s obj \<longrightarrow> 

   138       (\<exists> s' obj'. valid s' \<and> s2ss s' = ss \<and> obj' \<noteq> obj \<and> co2sobj s' obj = co2sobj s' obj)

   139      "

   140 

   141 lemma s2d_main_general:

   142   "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<and> (\<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<longrightarrow> (\<exists> s'. valid s' \<and> s2ss s' = ss \<and> (\<exists> obj'. obj' \<noteq> obj \<and> co2sobj s' obj = co2sobj s' obj')))"

   143 apply (erule static.induct)

   144 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) defer

   145 

   146 apply (erule exE|erule conjE)+

   147 

   148 apply (simp add:update_ss_def)

   149 

   150 sorry

   151 

   152 lemma s2d_main:

   153   "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"

   154 apply (erule static.induct)

   155 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)

   156 

   157 apply (erule exE|erule conjE)+

   158 

   159 apply (simp add:update_ss_def)

   160 

   161 sorry

   162 

   163 

   164 lemma t2ts:

   165   "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"

   166 apply (frule tainted_in_current, frule tainted_is_valid)

   167 apply (frule s2ss_included_sobj, simp)

   168 apply (case_tac sobj, simp_all)

   169 apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits)

   170 apply (drule dir_not_tainted, simp)

   171 apply (drule msgq_not_tainted, simp)

   172 apply (drule shm_not_tainted, simp)

   173 done

   174 

   175 lemma delq_imp_delqm:

   176   "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"

   177 apply (induct s, simp)

   178 by (case_tac a, auto)

   179 

   180 lemma tainted_s_subset_prop:

   181   "\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj"

   182 apply (case_tac sobj)

   183 apply auto

   184 done

   185 

   186 theorem static_complete: 

   187   assumes undel: "undeletable obj" and tbl: "taintable obj"

   188   shows "taintable_s obj"

   189 proof-

   190   from tbl obtain s where tainted: "obj \<in> tainted s"

   191     by (auto simp:taintable_def)

   192   hence vs: "valid s" by (simp add:tainted_is_valid)

   193   hence static: "s2ss s \<propto> static" using d2s_main by auto

   194   from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj" 

   195     apply (clarsimp simp add:taintable_def)

   196     apply (frule tainted_in_current)

   197     apply (case_tac obj, simp_all add:co2sobj.simps)

   198     apply (frule current_proc_has_sp, simp, auto)

   199     done

   200   from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" 

   201     by (auto simp:undeletable_def)

   202   with vs sobj have "init_obj_related sobj obj"

   203     apply (case_tac obj, case_tac [!] sobj)

   204     apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)

   205     apply (frule not_deleted_init_file, simp+) 

   206     apply (drule is_file_has_sfile', simp, erule exE)

   207     apply (rule_tac x = sf in bexI)

   208     apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1]

   209     apply (drule root_is_init_dir', simp)

   210     apply (frule not_deleted_init_file, simp, simp)

   211     apply (simp add:cf2sfile_def split:option.splits if_splits)

   212     apply (simp add:cf2sfiles_def)

   213     apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file)

   214 

   215     apply (frule not_deleted_init_dir, simp+)

   216     apply (simp add:cf2sfile_def split:option.splits if_splits)

   217     apply (case_tac list, simp add:sroot_def, simp)

   218     apply (drule file_dir_conflict, simp+)

   219     done

   220   with tainted t2ts init_alive sobj static

   221   show ?thesis unfolding taintable_s_def 

   222     apply (simp add:init_ss_in_def)

   223     apply (erule bexE)

   224     apply (simp add:init_ss_eq_def)

   225     apply (rule_tac x = "ss'" in bexI)

   226     apply (rule_tac x = "sobj" in exI)

   227     by (auto intro:tainted_s_subset_prop)

   228 qed

   229 

   230 lemma cp2sproc_pi:

   231   "\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs"

   232 by (simp add:cp2sproc_def split:option.splits if_splits)

   233 

   234 lemma cq2smsgq_qi:

   235   "\<lbrakk>cq2smsgq s q = Some (Init q', sec, sms); valid s\<rbrakk> \<Longrightarrow> q = q' \<and> \<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs"

   236 by (simp add:cq2smsgq_def split:option.splits if_splits)

   237 

   238 lemma cm2smsg_mi:

   239   "\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk> 

   240    \<Longrightarrow> m = m' \<and> \<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs"

   241 by (clarsimp simp add:cm2smsg_def split:if_splits option.splits)

   242 

   243 lemma ch2sshm_hi:

   244   "\<lbrakk>ch2sshm s h = Some (Init h', sec); valid s\<rbrakk> \<Longrightarrow> h = h' \<and> \<not> deleted (O_shm h) s \<and> h \<in> init_shms"

   245 by (clarsimp simp:ch2sshm_def split:if_splits option.splits)

   246 

   247 lemma root_not_deleted:

   248   "\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False"

   249 apply (induct s, simp)

   250 apply (frule vd_cons, frule vt_grant_os, case_tac a, auto)

   251 done

   252 

   253 lemma cf2sfile_fi:

   254   "\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and> 

   255      (if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f 

   256       else \<not> deleted (O_dir f) s \<and> is_init_dir f)"

   257 apply (case_tac f)

   258 by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted

   259         split:if_splits option.splits) 

   260 

   261 lemma init_deled_imp_deled_s: 

   262   "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj"

   263 apply (rule notI)

   264 apply (clarsimp simp:s2ss_def)

   265 apply (case_tac obj, case_tac [!] obja, case_tac sobj)

   266 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps)

   267 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps

   268            split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)

   269 done

   270 

   271 lemma deleted_imp_deletable_s:

   272   "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"

   273 apply (simp add:deletable_s_def)

   274 apply (frule d2s_main)

   275 apply (simp add:init_ss_in_def)

   276 apply (erule bexE)

   277 apply (rule_tac x = ss' in bexI)

   278 apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s)

   279 apply (case_tac obj, case_tac [!] sobj)

   280 apply auto

   281 apply (erule set_mp)

   282 apply (simp)

   283 apply auto

   284 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI)

   285 apply auto

   286 done

   287 

   288 lemma init_related_imp_init_sobj:

   289   "init_obj_related sobj obj \<Longrightarrow> is_init_sobj sobj"

   290 apply (case_tac sobj, case_tac [!] obj, auto)

   291 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto)

   292 done

   293 

   294 theorem undeletable_s_complete:

   295   assumes undel_s: "undeletable_s obj"

   296   shows "undeletable obj"

   297 proof-

   298   from undel_s have init_alive: "init_alive obj"

   299     and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj" 

   300     using undeletable_s_def by auto

   301   have "\<not> (\<exists> s. valid s \<and> deleted obj s)" 

   302   proof

   303     assume "\<exists> s. valid s \<and> deleted obj s"

   304     then obtain s where vs: "valid s" and del: "deleted obj s" by auto

   305     from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) 

   306     with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" 

   307       and related: "init_obj_related sobj obj" 

   308       apply (simp add:init_ss_in_def init_ss_eq_def)

   309       apply (erule bexE, erule_tac x= ss' in ballE)

   310       apply (auto dest:init_related_imp_init_sobj)

   311       done

   312     from init_alive del vs have "deletable_s obj" 

   313       by (auto elim:deleted_imp_deletable_s)

   314     with alive_s

   315     show False by (auto simp:deletable_s_def)

   316   qed

   317   with init_alive show ?thesis 

   318     by (simp add:undeletable_def)

   319 qed

   320 

   321 theorem final_offer:

   322   "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"

   323 apply (erule swap)

   324 by (simp add:static_complete undeletable_s_complete)

   325 

   326 (************** static \<rightarrow> dynamic ***************)

   327 

   328 

   329 lemma set_eq_D:

   330   "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"

   331 by auto

   332 

   333 lemma cqm2sms_prop1:

   334   "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"

   335 apply (induct queue arbitrary:sms)

   336 apply (auto simp:cqm2sms.simps split:option.splits)

   337 done

   338 

   339 lemma sq_sm_prop:

   340   "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk>

   341    \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"

   342 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)

   343 

   344 declare co2sobj.simps [simp add]

   345 

   346 lemma tainted_s_imp_tainted:

   347   "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"

   348 apply (drule s2d_main)

   349 apply (erule exE, erule conjE, simp add:s2ss_def)

   350 apply (rule_tac x = s in exI, simp)

   351 apply (case_tac sobj, simp_all)

   352 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 

   353 apply (rule_tac x = obj in exI, simp)

   354 apply (case_tac obj, (simp split:option.splits if_splits)+)

   355 

   356 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 

   357 apply (rule_tac x = obj in exI, simp)

   358 apply (case_tac obj, (simp split:option.splits if_splits)+)

   359 done

   360 

   361 lemma has_same_inode_prop3:

   362   "has_same_inode s f f' \<Longrightarrow> has_same_inode s f' f"

   363 by (auto simp:has_same_inode_def)

   364 

   365 theorem static_sound:

   366   assumes tbl_s: "taintable_s obj"

   367   shows "taintable obj"

   368 proof-

   369   from tbl_s obtain ss sobj where static: "ss \<in> static"

   370     and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj"

   371     and init_alive: "init_alive obj" by (auto simp:taintable_s_def)

   372   from static sobj tainted_s_imp_tainted 

   373   obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj"

   374     and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast

   375   

   376   from co2sobj related vs

   377   have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')"

   378     apply (case_tac obj', case_tac [!] obj)

   379     apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)

   380     apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def

   381                split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)

   382     done

   383   with tainted' vs have tainted: "obj \<in> tainted s"

   384     by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted)

   385   from sobj related init_alive have "appropriate obj"

   386     by (case_tac obj, case_tac [!] sobj, auto)

   387   with vs init_alive tainted

   388   show ?thesis by (auto simp:taintable_def)

   389 qed

   390 

   391 end

   392 

   393 end