diff -r 34d01e9a772e -r 7d9c0ed02b56 Static.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Static.thy Fri May 03 08:20:21 2013 +0100 @@ -0,0 +1,871 @@ +theory Static +imports Static_type OS_type_def Flask_type Flask +begin + +locale tainting_s = tainting + +begin + +fun init_role_of_obj :: "t_object \ role_t option" +where + "init_role_of_obj (O_proc p) = init_role_of_proc p" +| "init_role_of_obj _ = Some R_object" + +definition init_sectxt_of_obj :: "t_object \ security_context_t option" +where + "init_sectxt_of_obj obj \ + (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of + (Some u, Some r, Some t) \ Some (u,r,t) + | _ \ None)" + +(* +definition init_sectxt_of_file:: "t_file \ security_context_t option" +where + "init_sectxt_of_file f \ + if (is_init_file f) then init_sectxt_of_obj (O_file f) + else if (is_init_dir f) then init_sectxt_of_obj (O_dir f) + else None" +*) + +definition sec_of_root :: "security_context_t" +where + "sec_of_root \ (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of + (Some u, Some t) \ (u, R_object, t))" + +definition sroot :: "t_sfile" +where + "sroot \ (Init [], sec_of_root, None, {})" + +definition init_cf2sfile :: "t_file \ t_sfile option" +where + "init_cf2sfile f \ + case (parent f) of + None \ Some sroot + | Some pf \ if (is_init_file f) then + (case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of + (Some sec, Some psec, Some aseclist) \ Some (Init f, sec, Some psec, set aseclist) + | _ \ None) else + (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of + (Some sec, Some psec, Some aseclist) \ Some (Init f, sec, Some psec, set aseclist) + | _ \ None)" + +definition init_cfs2sfiles :: "t_file set \ t_sfile set" +where + "init_cfs2sfiles fs \ {sf. \f \ fs. init_cf2sfile f = Some sf}" + +definition init_cfd2sfd :: "t_process \ t_fd \ (security_context_t \ t_open_flags \ t_sfile) option" +where + "init_cfd2sfd p fd = + (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of + (Some f, Some flags, Some sec) \ (case (init_cf2sfile f) of + Some sf \ Some (sec, flags, sf) + | _ \ None) + | _ \ None)" + +definition init_cfds2sfds :: "t_process \ (security_context_t \ t_open_flags \ t_sfile) set" +where + "init_cfds2sfds p \ { sfd. \ fd sfd f. init_file_of_proc_fd p fd = Some f \ init_cfd2sfd p fd = Some sfd}" + +definition init_ch2sshm :: "t_shm \ t_sshm option" +where + "init_ch2sshm h \ (case (init_sectxt_of_obj (O_shm h)) of + Some sec \ Some (Init h, sec) + | _ \ None)" + +definition init_cph2spshs + :: "t_process \ (t_sshm \ t_shm_attach_flag) set" +where + "init_cph2spshs p \ {(sh, flag)| sh flag h. (p, flag) \ init_procs_of_shm h \ + init_ch2sshm h = Some sh}" + +definition init_cp2sproc :: "t_process \ t_sproc option" +where + "init_cp2sproc p \ (case (init_sectxt_of_obj (O_proc p)) of + Some sec \ Some (Init p, sec, (init_cfds2sfds p), (init_cph2spshs p)) + | None \ None)" + +(* acient files of init-file +definition init_o2s_afs :: "t_file \ security_context_t set" +where + "init_o2s_afs f \ {sec. \ f'. f' \ f \ init_sectxt_of_obj (O_dir f') = Some sec}" *) + +definition init_cm2smsg :: "t_msgq \ t_msg \ t_smsg option" +where + "init_cm2smsg q m \ (case (init_sectxt_of_obj (O_msg q m)) of + Some sec \ Some (Init m, sec, (O_msg q m) \ seeds) + | _ \ None)" + +fun init_cqm2sms :: "t_msgq \ t_msg list \ (t_smsg list) option" +where + "init_cqm2sms q [] = Some []" +| "init_cqm2sms q (m#ms) = + (case (init_cqm2sms q ms, init_cm2smsg q m) of + (Some sms, Some sm) \ Some (sm # sms) + | _ \ None)" + +definition init_cq2smsgq :: "t_msgq \ t_smsgq option" +where + "init_cq2smsgq q \ (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of + (Some sec, Some sms) \ Some (Init q, sec, sms) + | _ \ None)" + +definition init_same_inode_files :: "t_file \ t_file set" +where + "init_same_inode_files f \ {f'. init_inum_of_file f = init_inum_of_file f'}" + +fun init_obj2sobj :: "t_object \ t_sobject option" +where + "init_obj2sobj (O_proc p) = + (case (init_cp2sproc p) of + Some sp \ Some (S_proc sp (O_proc p \ seeds)) + | _ \ None)" +| "init_obj2sobj (O_file f) = + (if (f \ init_files \ is_init_file f) + then Some (S_file (init_cfs2sfiles (init_same_inode_files f)) + (\ f'. f' \ (init_same_inode_files f) \ O_file f \ seeds)) + else None)" +| "init_obj2sobj (O_dir f) = + (if (is_init_dir f) then + (case (init_cf2sfile f) of + Some sf \ Some (S_dir sf) + | _ \ None) + else None)" +| "init_obj2sobj (O_msgq q) = + (case (init_cq2smsgq q) of + Some sq \ Some (S_msgq sq) + | _ \ None)" +| "init_obj2sobj (O_shm h) = + (case (init_ch2sshm h) of + Some sh \ Some (S_shm sh) + | _ \ None)" +| "init_obj2sobj (O_msg q m) = + (case (init_cq2smsgq q, init_cm2smsg q m) of + (Some sq, Some sm) \ Some (S_msg sq sm) + | _ \ None)" +| "init_obj2sobj _ = None" + +definition + "init_static_state \ {sobj. \ obj. init_alive obj \ init_obj2sobj obj = Some sobj}" + +fun is_init_sfile :: "t_sfile \ bool" +where + "is_init_sfile (Init _, sec, psec,asec) = True" +| "is_init_sfile _ = False" + +fun is_many_sfile :: "t_sfile \ bool" +where + "is_many_sfile (Created, sec, psec, asec) = True" +| "is_many_sfile _ = False" + +fun is_init_sproc :: "t_sproc \ bool" +where + "is_init_sproc (Init p, sec, fds, shms) = True" +| "is_init_sproc _ = False" + +fun is_many_sproc :: "t_sproc \ bool" +where + "is_many_sproc (Created, sec,fds,shms) = True" +| "is_many_sproc _ = False" + +fun is_many_smsg :: "t_smsg \ bool" +where + "is_many_smsg (Created,sec,tag) = True" +| "is_many_smsg _ = False" + +fun is_many_smsgq :: "t_smsgq \ bool" +where + "is_many_smsgq (Created,sec,sms) = (True \ (\ sm \ (set sms). is_many_smsg sm))" +| "is_many_smsgq _ = False" + +fun is_many_sshm :: "t_sshm \ bool" +where + "is_many_sshm (Created, sec) = True" +| "is_many_sshm _ = False" + +(* +fun is_init_sobj :: "t_sobject \ bool" +where + "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \ None)" +| "is_init_sobj (S_file sf tag) = (is_init_sfile sf)" +| "is_init_sobj (S_dir sf tag) = (is_init_sfile sf)" +| "is_init_sobj (S_msg" *) + +fun is_many :: "t_sobject \ bool" +where + "is_many (S_proc (Many, sec, fds, shms) tag) = True" +| "is_many (S_file sfs tag) = (\ sf \ sfs. is_many_sfile sf)" +| "is_many (S_dir sf ) = is_many_sfile sf" +| "is_many (S_msgq sq ) = is_many_smsgq sq" +| "is_many (S_shm sh ) = is_many_sshm sh" + +(* +fun update_ss_sp:: "t_static_state \ t_sobject \ t_sobject \ t_static_state" +where + "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = + (if (is_many_sproc sp) then ss \ {S_proc sp' tag'} + else (ss - {S_proc sp tag}) \ {S_proc sp' tag'})" + +fun update_ss_sd:: "t_static_state \ t_sobject \ t_sobject \ t_static_state" +where + "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = + (if (is_many_sfile sf) then ss \ {S_dir sf' tag'} + else (ss - {S_dir sf tag}) \ {S_dir sf' tag'})" +*) + +definition update_ss :: "t_static_state \ t_sobject \ t_sobject \ t_static_state" +where + "update_ss ss so so' \ if (is_many so) then ss \ {so'} else (ss - {so}) \ {so'}" + +definition add_ss :: "t_static_state \ t_sobject \ t_static_state" +where + "add_ss ss so \ ss \ {so}" + +definition del_ss :: "t_static_state \ t_sobject \ t_static_state" +where + "del_ss ss so \ if (is_many so) then ss else ss - {so}" + +(* +fun sparent :: "t_sfile \ t_sfile option" +where + "sparent (Sroot si sec) = None" +| "sparent (Sfile si sec spf) = Some spf" + +inductive is_ancesf :: "t_sfile \ t_sfile \ bool" +where + "is_ancesf sf sf" +| "sparent sf = Some spf \ is_ancesf spf sf" +| "\sparent sf = Some spf; is_ancesf saf spf\ \ is_ancesf saf sf" + +definition sfile_reparent :: "t_sfile \ t_sfile \ t_sfile" +where + "sfile_reparent (Sroot)" +*) + +(* +(* sfds rename aux definitions *) +definition sfds_rename_notrelated + :: "t_sfd set \ t_sfile \ t_sfile \ t_sfd set \ bool" +where + "sfds_rename_notrelated sfds from to sfds' \ + (\ sec flag sf. (sec,flag,sf) \ sfds \ (\ from \ sf) \ (sec,flag,sf) \ sfds')" + +definition sfds_rename_renamed + :: "t_sfd set \ t_sfile \ t_sfile \ t_sfile \ t_sfd set \ bool" +where + "sfds_rename_renamed sfds sf from to sfds' \ + (\ sec flag sf'. (sec,flag,sf) \ sfds \ (sf \ sf') \ + (sec, flag, file_after_rename sf' from to) \ sfds' \ (sec,flag,sf) \ sfds')" + +definition sfds_rename_remain + :: "t_sfd set \ t_sfile \ t_sfile \ t_sfile \ t_sfd set \ bool" +where + "sfds_rename_remain sfds sf from to sfds' \ + (\ sec flag sf'. (sec,flag,sf') \ sfds \ (sf \ sf') \ + (sec, flag, sf') \ sfds' \ (sec,flag, file_after_rename sf' from to) \ sfds')" + +(* for not many, choose on renamed or not *) +definition sfds_rename_choices + :: "t_sfd set \ t_sfile \ t_sfile \ t_sfile \ t_sfd set \ bool" +where + "sfds_rename_choices sfds sf from to sfds' \ + sfds_rename_remain sfds sf from to sfds' \ sfds_rename_renamed sfds sf from to sfds'" + +(* for many, merge renamed with not renamed *) +definition sfds_rename_both + :: "t_sfd set \ t_sfile \ t_sfile \ t_sfile \ t_sfd set \ bool" +where + "sfds_rename_both sfds sf from to sfds' \ + (\ sec flag sf'. (sec,flag,sf') \ sfds \ (sf \ sf') \ + (sec, flag, sf') \ sfds' \ (sec,flag, file_after_rename sf' from to) \ sfds')" + +(* added to the new sfds, are those only under the new sfile *) +definition sfds_rename_added + :: "t_sfd set \ t_sfile \ t_sfile \ t_sfd set \ bool" +where + "sfds_rename_added sfds from to sfds' \ + (\ sec' flag' sf' sec flag. (sec',flag',sf') \ sfds' \ (sec,flag,sf') \ sfds \ + (\ sf. (sec,flag,sf) \ sfds \ sf' = file_after_rename from to sf))" + +definition sproc_sfds_renamed + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "sproc_sfds_renamed ss sf from to ss' \ + (\ pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \ ss \ + (\ sfds'. S_proc (pi,sec,sfds',sshms) tagp \ ss \ sfds_rename_renamed sfds sf from to sfds'))" + +definition sproc_sfds_remain + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "sproc_sfds_remain ss sf from to ss' \ + (\ pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \ ss \ + (\ sfds'. S_proc (pi,sec,sfds',sshms) tagp \ ss \ sfds_rename_remain sfds sf from to sfds'))" + +(* for not many, choose on renamed or not *) +definition sproc_sfds_choices + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "sproc_sfds_choices ss sf from to ss' \ + (\ pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \ ss \ + (\ sfds'. S_proc (pi,sec,sfds',sshms) tagp \ ss \ sfds_rename_choices sfds sf from to sfds'))" + +(* for many, merge renamed with not renamed *) +definition sproc_sfds_both + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "sproc_sfds_both ss sf from to ss' \ + (\ pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \ ss \ + (\ sfds'. S_proc (pi,sec,sfds',sshms) tagp \ ss \ sfds_rename_both sfds sf from to sfds'))" + +(* remove (\ sp tag. S_proc sp tag \ ss \ S_proc sp tag \ ss'), + * cause sfds contains sfs informations *) +definition ss_rename_notrelated + :: "t_static_state \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "ss_rename_notrelated ss sf sf' ss' \ + (\ sq. S_msgq sq \ ss \ S_msgq sq \ ss') \ + (\ pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \ ss \ (\ sfds'. + S_proc (pi,sec,sfds',sshms) tagp \ ss'\ sfds_rename_notrelated sfds sf sf' sfds')) \ + (\ sfs sf'' tag. S_file sfs tag \ ss \ sf'' \ sfs \ (\ sf \ sf'') \ (\ sfs'. + S_file sfs tag \ ss' \ sf'' \ sfs')) \ + (\ sf'' tag. S_dir sf'' tag \ ss \ (\ sf \ sf'') \ S_dir sf'' tag \ ss')" + +(* rename from to, from should definited renamed if not many *) +definition all_descendant_sf_renamed + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "all_descendant_sf_renamed ss sf from to ss' \ + (\ sfs sf' tagf. sf \ sf' \ S_file sfs tagf \ ss \ sf' \ sfs \ (\ sfs'. + S_file sfs' tagf \ ss' \ file_after_rename from to sf' \ sfs' \ sf' \ sfs')) \ + (\ sf' tagf. sf \ sf' \ S_dir sf' tagf \ ss \ S_dir (file_after_rename from to sf') tagf \ ss' \ S_dir sf' tagf \ ss') \ + sproc_sfds_renamed ss sf from to ss'" + +(* not renamed *) +definition all_descendant_sf_remain + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "all_descendant_sf_remain ss sf from to ss' \ + (\ sfs sf' tag'. sf \ sf' \ S_file sfs tag' \ ss \ sf' \ sfs \ (\ sfs'. + S_file sfs' tag' \ ss \ file_after_rename from to sf' \ sfs' \ sf' \ sfs')) \ + (\ sf' tag'. sf \ sf' \ S_dir sf' tag' \ ss \ S_dir (file_after_rename from to sf') tag' \ ss' \ S_dir sf' tag' \ ss') \ + sproc_sfds_remain ss sf from to ss'" + +definition all_descendant_sf_choices + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "all_descendant_sf_choices ss sf from to ss' \ + all_descendant_sf_renamed ss sf from to ss' \ all_descendant_sf_remain ss sf from to ss'" + +definition all_descendant_sf_both + :: "t_static_state \ t_sfile \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "all_descendant_sf_both ss sf from to ss' \ + (\ sfs sf' tag'. sf \ sf' \ S_file sfs tag' \ ss \ sf' \ sfs \ (\ sfs'. + S_file sfs' tag' \ ss \ file_after_rename from to sf' \ sfs' \ sf' \ sfs')) \ + (\ sf' tag'. sf \ sf' \ S_dir sf' tag' \ ss \ + S_dir (file_after_rename from to sf') tag' \ ss' \ S_dir sf' tag' \ ss') \ + sproc_sfds_both ss sf from to ss'" + +definition ss_renamed_file + :: "t_static_state \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "ss_renamed_file ss sf sf' ss' \ + (if (is_many_sfile sf) + then all_descendant_sf_choices ss sf sf sf' ss' + else all_descendant_sf_renamed ss sf sf sf' ss')" + +(* added to the new sfs, are those only under the new sfile *) +definition sfs_rename_added + :: "t_sfile set \ t_sfile \ t_sfile \ t_sfile set \ bool" +where + "sfs_rename_added sfs from to sfs' \ + (\ sf'. sf' \ sfs' \ sf' \ sfs \ (\ sf. sf \ sfs \ sf' = file_after_rename from to sf))" + +(* added to the new sfile, are those only under the new sfile *) +definition ss_rename_added + :: "t_static_state \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "ss_rename_added ss from to ss' \ + (\ pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \ ss \ + S_proc (pi,sec,fds',shms) tagp \ ss' \ sfds_rename_added fds from to fds') \ + (\ sq. S_msgq sq \ ss' \ S_msgq sq \ ss) \ + (\ sfs sfs' tagf. S_file sfs' tagf \ ss' \ S_file sfs tagf \ ss \ + sfs_rename_added sfs from to sfs') \ + (\ sf' tagf. S_dir sf' tagf \ ss' \ S_dir sf' tagf \ ss \ + (\ sf. S_dir sf tagf \ ss \ sf' = file_after_rename from to sf))" + +definition sfile_alive :: "t_static_state \ t_sfile \ bool" +where + "sfile_alive ss sf \ (\ sfs tagf. sf \ sfs \ S_file sfs tagf \ ss)" + +definition sf_alive :: "t_static_state \ t_sfile \ bool" +where + "sf_alive ss sf \ (\ tagd. S_dir sf tagd \ ss) \ sfile_alive ss sf" + +(* constrains that the new static state should satisfy *) +definition ss_rename:: "t_static_state \ t_sfile \ t_sfile \ t_static_state \ bool" +where + "ss_rename ss sf sf' ss' \ + ss_rename_notrelated ss sf sf' ss' \ + ss_renamed_file ss sf sf' ss' \ ss_rename_added ss sf sf' ss' \ + (\ sf''. sf_alive ss sf'' \ sf \ sf'' \ + (if (is_many_sfile sf'') + then all_descendant_sf_choices ss sf'' sf sf' ss' + else all_descendant_sf_both ss sf'' sf sf' ss'))" + +(* two sfile, the last fname should not be equal *) +fun sfile_same_fname:: "t_sfile \ t_sfile \ bool" +where + "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')" +| "sfile_same_fname _ _ = False" + +(* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *) +definition ss_rename_no_same_fname:: "t_static_state \ t_sfile \ t_sfile \ bool" +where + "ss_rename_no_same_fname ss from spf \ + \ (\ to. sfile_same_fname from to \ parent to = Some spf \ sf_alive ss to)" + +(* is not a function, is a relation (one 2 many) +definition update_ss_rename :: "t_static_state \ t_sfile \ t_sfile \ t_static_state" +where + "update_ss_rename ss sf sf' \ if (is_many_sfile sf) + then (ss \ {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \ sf'' \ S_file sf'' tag \ ss} + \ {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \ sf'' \ S_dir sf'' tag \ ss}) + else (ss - {S_file sf'' tag | sf'' tag. sf \ sf'' \ S_file sf'' tag \ ss} + - {S_dir sf'' tag | sf'' tag. sf \ sf'' \ S_dir sf'' tag \ ss}) + \ {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \ sf'' \ S_file sf'' tag \ ss} + \ {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \ sf'' \ S_dir sf'' tag \ ss}" +*) +*) + +fun sectxt_of_sproc :: "t_sproc \ security_context_t" +where + "sectxt_of_sproc (pi,sec,fds,shms) = sec" + +fun sectxt_of_sfile :: "t_sfile \ security_context_t" +where + "sectxt_of_sfile (fi,sec,psec,asecs) = sec" + +fun asecs_of_sfile :: "t_sfile \ security_context_t set" +where + "asecs_of_sfile (fi,sec,psec,asecs) = asecs" + +definition search_check_s :: "security_context_t \ t_sfile \ bool \ bool" +where + "search_check_s pctxt sf if_file = + (if if_file + then search_check_file pctxt (sectxt_of_sfile sf) \ search_check_allp pctxt (asecs_of_sfile sf) + else search_check_dir pctxt (sectxt_of_sfile sf) \ search_check_allp pctxt (asecs_of_sfile sf))" + +definition sectxts_of_sfds :: "t_sfd set \ security_context_t set" +where + "sectxts_of_sfds sfds \ {ctxt. \ flag sf. (ctxt, flag, sf) \ sfds}" + +definition inherit_fds_check_s :: "security_context_t \ t_sfd set \ bool" +where + "inherit_fds_check_s pctxt sfds \ + (\ ctxt \ sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)" + +definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \ security_context_t set" +where + "sectxts_of_sproc_sshms sshms \ {ctxt. \ hi flag. ((hi, ctxt),flag) \ sshms}" + +definition inherit_shms_check_s :: "security_context_t \ t_sproc_sshm set \ bool" +where + "inherit_shms_check_s pctxt sshms \ + (\ ctxt \ sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)" + +(* +fun info_flow_sshm :: "t_sproc \ t_sproc \ bool" +where + "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = + (\ sh flag'. (sh, SHM_RDWR) \ shms \ (sh, flag') \ shms')" +*) +definition info_flow_sproc_sshms :: "t_sproc_sshm set \ t_sproc_sshm set \ bool" +where + "info_flow_sproc_sshms shms shms' \ (\ sh flag'. (sh, SHM_RDWR) \ shms \ (sh, flag') \ shms')" + +fun info_flow_sshm :: "t_sproc \ t_sproc \ bool" +where + "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" + +definition update_ss_shms :: "t_static_state \ t_sproc \ bool \ t_static_state" +where + "update_ss_shms ss spfrom tag \ {sobj. \ sobj' \ ss. + (case sobj' of + S_proc sp tagp \ if (info_flow_sshm spfrom sp) + then if (is_many_sproc sp) + then (sobj = S_proc sp tagp \ sobj = S_proc sp (tagp \ tag)) + else (sobj = S_proc sp (tagp \ tag)) + else (sobj = S_proc sp tag) + | _ \ sobj = sobj')}" + + + +(* all reachable static states(sobjects set) *) +inductive_set static :: "t_static_state set" +where + s_init: "init_static_state \ static" +| s_execve: "\ss \ static; S_proc (pi, pctxt, fds, shms) tagp \ ss; S_file sfs tagf \ ss; + (fi,fsec,pfsec,asecs) \ sfs; npctxt_execve pctxt fsec = Some pctxt'; + grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; + inherit_fds_check_s pctxt' fds'; fds' \ fds\ + \ (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) + (S_proc (pi, pctxt', fds', {}) (tagp \ tagf))) \ static" +| s_clone: "\ss \ static; S_proc (pi, pctxt, fds, shms) tagp \ ss; + permission_check pctxt pctxt C_process P_fork; + inherit_fds_check_s pctxt fds'; fds' \ fds; + inherit_shms_check_s pctxt shms'; shms' \ shms\ + \ (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \ static" +| s_kill: "\ss \ static; S_proc (pi, pctxt, fds, shms) tagp \ ss; + S_proc (pi', pctxt', fds', shms') tagp' \ ss; + permission_check pctxt pctxt' C_process P_sigkill\ + \ (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \ static" +| s_ptrace: "\ss \ static; S_proc sp tagp \ ss; S_proc sp' tagp' \ ss; + permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\ + \ (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \ static" +| s_exit: "\ss \ static; S_proc sp tagp \ ss\ \ (del_ss ss (S_proc sp tagp)) \ static" +| s_open: "\ss \ static; S_proc (pi, pctxt, fds, shms) tagp \ ss; S_file sfs tagf \ ss; sf \ sfs; + search_check_s pctxt sf True; \ is_creat_excl_flag flags; + oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\ + \ (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) + (S_proc (pi, pctxt, fds \ {(pctxt,flags,sf)}, shms) tagp)) \ static" +| s_open': "\ss \ static; S_proc (pi, pctxt, fds, shms) tagp \ ss; is_creat_excl_flag flags; + S_dir (pfi,fsec,pfsec,asecs) \ ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; + nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec; + permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\ + \ (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \ {fsec})} tagp)) + (S_proc (pi, pctxt, fds, shms) tagp) + (S_proc (pi, pctxt, fds \ {(pctxt, flags, (Created, nfsec, Some fsec, asecs \ {fsec}))}, shms) tagp) + ) \ static" +| S_readf: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; (fdctxt,flags,sf) \ fds; + permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \ ss; sf \ sfs; + permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\ + \ (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \ tagf)) \ static" +| S_writef: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; (fdctxt,flags,sf) \ fds; + permission_check pctxt fdctxt C_fd P_setattr; sf \ sfs; S_file sfs tagf \ ss; + permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\ + \ (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \ tagf))) \ static" +| S_unlink: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_file sfs tagf \ ss; + (Init f,fsec,Some pfsec,asecs) \ sfs; + search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; + permission_check pctxt fsec C_file P_unlink; + permission_check pctxt pfsec C_dir P_remove_name\ + \ ((ss - {S_file sfs tagf}) \ {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \ static" +| S_rmdir: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; + S_dir (fi,fsec,Some pfsec,asecs) \ ss; + search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; + permission_check pctxt fsec C_dir P_rmdir; + permission_check pctxt pfsec C_dir P_remove_name\ + \ (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \ static" +| S_mkdir: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_dir (fi,fsec,pfsec,asecs) \ ss; + search_check_s pctxt (fi,fsec,pfsec,asecs) False; + permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create; + permission_check pctxt fsec C_dir P_add_name\ + \ (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \ {fsec}))) \ static" +| s_link: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_dir (pfi,pfsec,ppfsec,asecs) \ ss; + S_file sfs tagf \ ss; sf \ sfs; nfsec = nfctxt_create pctxt pfsec C_file; + search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True; + permission_check pctxt (sectxt_of_sfile sf) C_file P_link; + permission_check pctxt pfsec C_dir P_add_name\ + \ (update_ss ss (S_file sfs tagf) + (S_file (sfs \ {(Created,nfsec,Some pfsec, asecs \ {pfsec})}) tagf)) \ static" +| s_trunc: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_file sfs tagf \ ss; sf \ sfs; + search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\ + \ (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \ tagp))) \ static" +(* +| s_rename: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_file sfs tagf \ ss; + (sf#spf') \ sfs; S_dir spf tagpf \ ss; \((sf#spf') \ (sf#spf)); + search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; + sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; + permission_check pctxt fctxt C_file P_rename; + permission_check pctxt pfctxt C_dir P_add_name; + ss_rename ss (sf#spf') (sf#spf) ss'; + ss_rename_no_same_fname ss (sf#spf') (sf#spf)\ + \ ss' \ static" +| s_rename': "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_dir (sf#spf') tagf \ ss; + S_dir spf tagpf \ ss; \((sf#spf') \ (sf#spf)); + search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; + sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; + permission_check pctxt fctxt C_dir P_reparent; + permission_check pctxt pfctxt C_dir P_add_name; + ss_rename ss (sf#spf') (sf#spf) ss'; + ss_rename_no_same_fname ss (sf#spf') (sf#spf)\ + \ ss' \ static" +*) +| s_createq: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; + permission_check pctxt pctxt C_msgq P_associate; + permission_check pctxt pctxt C_msgq P_create\ + \ (add_ss ss (S_msgq (Created,pctxt,[]))) \ static" +| s_sendmsg: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_msgq (qi,qctxt,sms) \ ss; + permission_check pctxt qctxt C_msgq P_enqueue; + permission_check pctxt qctxt C_msgq P_write; + permission_check pctxt pctxt C_msg P_create\ + \ (update_ss ss (S_msgq (qi,qctxt,sms)) + (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \ static" +| s_recvmsg: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; + S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \ ss; + permission_check pctxt qctxt C_msgq P_read; + permission_check pctxt mctxt C_msg P_receive\ + \ (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \ tagm)) \ static" +| s_removeq: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_msgq (qi,qctxt,sms) \ ss; + permission_check pctxt qctxt C_msgq P_destroy\ + \ (del_ss ss (S_msgq (qi,qctxt,sms))) \ static" +| s_createh: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; + permission_check pctxt pctxt C_shm P_associate; + permission_check pctxt pctxt C_shm P_create\ + \ (add_ss ss (S_shm (Created, pctxt))) \ static" +| s_attach: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_shm (hi,hctxt) \ ss; + if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read + else (permission_check pctxt hctxt C_shm P_read \ + permission_check pctxt hctxt C_shm P_write)\ + \ (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) + (S_proc (pi,pctxt,fds,shms \ {((hi,hctxt),flag)}) tagp)) \ static" +| s_detach: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_shm sh \ ss; + (sh,flag) \ shms; \ is_many_sshm sh\ + \ (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) + (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \ static" +| s_deleteh: "\ss \ static; S_proc (pi,pctxt,fds,shms) tagp \ ss; S_shm (hi,hctxt) \ ss; + permission_check pctxt hctxt C_shm P_destroy; \ is_many_sshm sh\ + \ (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \ static" + +(* +fun smsg_related :: "t_msg \ t_smsg list \ bool" +where + "smsg_related m [] = False" +| "smsg_related m ((mi, sec, tag)#sms) = + (if (mi = Init m) then True else smsg_related m sms)" + +fun smsgq_smsg_related :: "t_msgq \ t_msg \ t_smsgq \ bool" +where + "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \ (smsg_related m smsgslist))" + +fun smsg_relatainted :: "t_msg \ t_smsg list \ bool" +where + "smsg_relatainted m [] = False" +| "smsg_relatainted m ((mi, sec, tag)#sms) = + (if (mi = Init m \ tag = True) then True else smsg_relatainted m sms)" + +fun smsgq_smsg_relatainted :: "t_msgq \ t_msg \ t_smsgq \ bool" +where + "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = + ((qi = Init q) \ (smsg_relatainted m smsgslist))" +*) + +fun sfile_related :: "t_sfile \ t_file \ bool" +where + "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)" +(* +fun sproc_related :: "t_process \ t_sproc \ bool" +where + "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" +*) +fun init_obj_related :: "t_sobject \ t_object \ bool" +where + "init_obj_related (S_proc (Init p, sec, fds, shms) tag) (O_proc p') = (p = p')" +| "init_obj_related (S_file sfs tag) (O_file f) = (\ sf \ sfs. sfile_related sf f)" +| "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" +| "init_obj_related (S_msgq (Init q, sec, sms)) (O_msgq q') = (q = q')" +| "init_obj_related (S_shm (Init h, sec)) (O_shm h') = (h = h')" +| "init_obj_related (S_msg (Init q, sec, sms) (Init m, secm, tagm)) (O_msg q' m') = (q = q' \ m = m')" +| "init_obj_related _ _ = False" + +fun tainted_s :: "t_static_state \ t_sobject \ bool" +where + "tainted_s ss (S_proc sp tag) = (S_proc sp tag \ ss \ tag = True)" +| "tainted_s ss (S_file sfs tag) = (S_file sfs tag \ ss \ tag = True)" +| "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) = + (S_msgq (qi, sec, sms) \ ss \ (mi,sec,tag) \ set sms \ tag = True)" +| "tainted_s ss _ = False" + +(* +fun tainted_s :: "t_object \ t_static_state \ bool" +where + "tainted_s (O_proc p) ss = (\ sp. S_proc sp True \ ss \ sproc_related p sp)" +| "tainted_s (O_file f) ss = (\ sfs sf. S_file sfs True \ ss \ sf \ sfs \ sfile_related f sf)" +| "tainted_s (O_msg q m) ss = (\ sq. S_msgq sq \ ss \ smsgq_smsg_relatainted q m sq)" +| "tainted_s _ ss = False" +*) + +definition taintable_s :: "t_object \ bool" +where + "taintable_s obj \ \ ss \ static. \ sobj. tainted_s ss sobj \ init_obj_related sobj obj \ init_alive obj" + +definition deletable_s :: "t_object \ bool" +where + "deletable_s obj \ init_alive obj \ (\ ss \ static. \ sobj \ ss. \ init_obj_related sobj obj)" + +definition undeletable_s :: "t_object \ bool" +where + "undeletable_s obj \ init_alive obj \ (\ ss \ static. \ sobj \ ss. init_obj_related sobj obj)" + + +(**************** translation from dynamic to static *******************) + +definition cf2sfile :: "t_state \ t_file \ bool \ t_sfile option" +where + "cf2sfile s f Is_file \ + case (parent f) of + None \ if Is_file then None else Some sroot + | Some pf \ if Is_file + then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of + (Some sec, Some psec, Some asecs) \ + Some (if (\ deleted (O_file f) s \ is_init_file f) then Init f else Created, sec, Some psec, set asecs) + | _ \ None) + else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of + (Some sec, Some psec, Some asecs) \ + Some (if (\ deleted (O_dir f) s \ is_init_dir f) then Init f else Created, sec, Some psec, set asecs) + | _ \ None)" + +definition cfs2sfiles :: "t_state \ t_file set \ t_sfile set" +where + "cfs2sfiles s fs \ {sf. \ f \ fs. cf2sfile s f True = Some sf}" + +definition same_inode_files :: "t_state \ t_file \ t_file set" +where + "same_inode_files s f \ {f'. inum_of_file s f = inum_of_file s f'}" + +(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) +definition cfd2sfd :: "t_state \ t_process \ t_fd \ t_sfd option" +where + "cfd2sfd s p fd \ + (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of + (Some f, Some flags, Some sec) \ (case (cf2sfile s f True) of + Some sf \ Some (sec, flags, sf) + | _ \ None) + | _ \ None)" + + +definition cpfd2sfds :: "t_state \ t_process \ t_sfd set" +where + "cpfd2sfds s p \ {sfd. \ fd sfd f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}" + +definition ch2sshm :: "t_state \ t_shm \ t_sshm option" +where + "ch2sshm s h \ (case (sectxt_of_obj s (O_shm h)) of + Some sec \ + Some (if (\ deleted (O_shm h) s \ h \ init_shms) then Init h else Created, sec) + | _ \ None)" + +definition cph2spshs :: "t_state \ t_process \ t_sproc_sshm set" +where + "cph2spshs s p \ {(sh, flag) | sh flag h. (p, flag) \ procs_of_shm s h \ ch2sshm s h = Some sh}" + +definition cp2sproc :: "t_state \ t_process \ t_sproc option" +where + "cp2sproc s p \ (case (sectxt_of_obj s (O_proc p)) of + Some sec \ + Some (if (\ deleted (O_proc p) s \ p \ init_procs) then Init p else Created, sec, + cpfd2sfds s p, cph2spshs s p) + | _ \ None)" + +definition cm2smsg :: "t_state \ t_msgq \ t_msg \ t_smsg option" +where + "cm2smsg s q m \ (case (sectxt_of_obj s (O_msg q m)) of + Some sec \ + Some (if (\ deleted (O_msg q m) s \ m \ set (init_msgs_of_queue q)) then Init m else Created, + sec, O_msg q m \ tainted s) + | _ \ None)" + +fun cqm2sms:: "t_state \ t_msgq \ t_msg list \ (t_smsg list) option" +where + "cqm2sms s q [] = Some []" +| "cqm2sms s q (m#ms) = + (case (cqm2sms s q ms, cm2smsg s q m) of + (Some sms, Some sm) \ Some (sm#sms) + | _ \ None)" + +definition cq2smsgq :: "t_state \ t_msgq \ t_smsgq option" +where + "cq2smsgq s q \ (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of + (Some sec, Some sms) \ + Some (if (\ deleted (O_msgq q) s \ q \ init_msgqs) then Init q else Created, + sec, sms) + | _ \ None)" + +fun co2sobj :: "t_state \ t_object \ t_sobject option" +where + "co2sobj s (O_proc p) = + (case (cp2sproc s p) of + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) + | _ \ None)" +| "co2sobj s (O_file f) = + (if (f \ current_files s) then + Some (S_file (cfs2sfiles s (same_inode_files s f)) (O_file f \ tainted s)) + else None)" +| "co2sobj s (O_dir f) = + (case (cf2sfile s f False) of + Some sf \ Some (S_dir sf) + | _ \ None)" +| "co2sobj s (O_msgq q) = + (case (cq2smsgq s q) of + Some sq \ Some (S_msgq sq) + | _ \ None)" +| "co2sobj s (O_shm h) = + (case (ch2sshm s h) of + Some sh \ Some (S_shm sh) + | _ \ None)" +| "co2sobj s (O_msg q m) = + (case (cq2smsgq s q, cm2smsg s q m) of + (Some sq, Some sm) \ Some (S_msg sq sm) + | _ \ None)" +| "co2sobj s _ = None" + + +(***************** for backward proof when Instancing static objects ******************) + +definition next_nat :: "nat set \ nat" +where + "next_nat nset = (Max nset) + 1" + +definition new_proc :: "t_state \ t_process" +where + "new_proc \ = next_nat (current_procs \)" + +definition new_inode_num :: "t_state \ nat" +where + "new_inode_num \ = next_nat (current_inode_nums \)" + +definition new_msgq :: "t_state \ t_msgq" +where + "new_msgq s = next_nat (current_msgqs s)" + +definition new_msg :: "t_state \ t_msgq \ nat" +where + "new_msg s q = next_nat (set (msgs_of_queue s q))" + +definition new_shm :: "t_state \ nat" +where + "new_shm \ = next_nat (current_shms \)" + +definition new_proc_fd :: "t_state \ t_process \ t_fd" +where + "new_proc_fd \ p = next_nat (current_proc_fds \ p)" + +definition all_fname_under_dir:: "t_file \ t_state \ t_fname set" +where + "all_fname_under_dir d \ = {fn. \ f. fn # d = f \ f \ current_files \}" + +fun fname_all_a:: "nat \ t_fname" +where + "fname_all_a 0 = []" | + "fname_all_a (Suc n) = ''a''@(fname_all_a n)" + +definition fname_length_set :: "t_fname set \ nat set" +where + "fname_length_set fns = length`fns" + +definition next_fname:: "t_file \ t_state \ t_fname" +where + "next_fname pf \ = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \))) + 1)" + +definition new_childf:: "t_file \ t_state \ t_file" +where + "new_childf pf \ = next_fname pf \ # pf" + +definition s2ss :: "t_state \ t_static_state" +where + "s2ss s \ {sobj. \ obj. alive s obj \ co2sobj s obj = Some sobj}" + +end + +end \ No newline at end of file