1829 |
1829 |
1830 |
1830 |
1831 (* simpset for co2sobj *) |
1831 (* simpset for co2sobj *) |
1832 |
1832 |
1833 lemma co2sobj_execve: |
1833 lemma co2sobj_execve: |
|
1834 "\<lbrakk>valid (Execve p f fds # s); alive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = ( |
|
1835 if (obj = O_proc p) |
|
1836 then (case (cp2sproc (Execve p f fds # s) p) of |
|
1837 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)) |
|
1838 | _ \<Rightarrow> None) |
|
1839 else co2sobj s obj )" |
|
1840 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1841 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
1842 apply (case_tac "cp2sproc (Execve p f fds # s) p") |
|
1843 apply (drule current_proc_has_sp', simp, simp) |
|
1844 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits) |
|
1845 apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
|
1846 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
|
1847 apply (simp add:is_dir_in_current) |
|
1848 done |
|
1849 |
|
1850 lemma co2sobj_execve': |
1834 "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = ( |
1851 "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = ( |
1835 if (obj = O_proc p) |
1852 if (obj = O_proc p) |
1836 then (case (cp2sproc (Execve p f fds # s) p) of |
1853 then (case (cp2sproc (Execve p f fds # s) p) of |
1837 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)) |
1854 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)) |
1838 | _ \<Rightarrow> None) |
1855 | _ \<Rightarrow> None) |
1845 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
1862 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
1846 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
1863 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
1847 apply (simp add:is_dir_in_current) |
1864 apply (simp add:is_dir_in_current) |
1848 done |
1865 done |
1849 |
1866 |
1850 lemma co2sobj_clone: |
1867 lemma co2sobj_clone': |
1851 "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = ( |
1868 "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = ( |
1852 if (obj = O_proc p') |
1869 if (obj = O_proc p') |
1853 then (case (cp2sproc (Clone p p' fds shms # s) p') of |
1870 then (case (cp2sproc (Clone p p' fds shms # s) p') of |
1854 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
1871 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
1855 | _ \<Rightarrow> None) |
1872 | _ \<Rightarrow> None) |
1861 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) |
1878 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) |
1862 apply (rule conjI, rule impI, simp) |
1879 apply (rule conjI, rule impI, simp) |
1863 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits) |
1880 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits) |
1864 |
1881 |
1865 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
1882 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
|
1883 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
|
1884 apply (simp add:is_dir_in_current) |
|
1885 done |
|
1886 |
|
1887 lemma co2sobj_clone: |
|
1888 "\<lbrakk>valid (Clone p p' fds shms # s); alive (Clone p p' fds shms # s) obj\<rbrakk> |
|
1889 \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = ( |
|
1890 if (obj = O_proc p') |
|
1891 then (case (cp2sproc (Clone p p' fds shms # s) p') of |
|
1892 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
|
1893 | _ \<Rightarrow> None) |
|
1894 else co2sobj s obj )" |
|
1895 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1896 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other |
|
1897 cq2smsgq_other tainted_eq_Tainted) |
|
1898 apply (rule conjI, rule impI, simp) |
|
1899 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'") |
|
1900 apply (drule current_proc_has_sp', simp, simp) |
|
1901 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) |
|
1902 apply (simp add:tainted_eq_Tainted, rule impI, rule notI) |
|
1903 apply (drule Tainted_in_current, simp+) |
|
1904 apply (rule impI, simp) |
|
1905 apply (drule current_proc_has_sp, simp, (erule exE|erule conjE)+) |
|
1906 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted Tainted_in_current split:option.splits) |
|
1907 |
|
1908 apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
1866 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
1909 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
1867 apply (simp add:is_dir_in_current) |
1910 apply (simp add:is_dir_in_current) |
1868 done |
1911 done |
1869 |
1912 |
1870 lemma co2sobj_ptrace: |
1913 lemma co2sobj_ptrace: |
2199 dest!:current_has_smsgq' |
2242 dest!:current_has_smsgq' |
2200 dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq) |
2243 dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq) |
2201 done |
2244 done |
2202 |
2245 |
2203 lemma co2sobj_createshm: |
2246 lemma co2sobj_createshm: |
2204 "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = co2sobj s obj" |
2247 "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = ( |
|
2248 case obj of |
|
2249 O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of |
|
2250 Some sh \<Rightarrow> Some (S_shm sh) |
|
2251 | _ \<Rightarrow> None) |
|
2252 else co2sobj s obj |
|
2253 | _ \<Rightarrow> co2sobj s obj)" |
2205 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
2254 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
2206 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
2255 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
2207 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
2256 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
2208 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
2257 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
2209 same_inode_files_prop6 ch2sshm_simps |
2258 same_inode_files_prop6 ch2sshm_simps |