1596 by (drule_tac p'= p' in cp2sproc_exit, simp+) |
1608 by (drule_tac p'= p' in cp2sproc_exit, simp+) |
1597 |
1609 |
1598 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm |
1610 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm |
1599 cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other |
1611 cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other |
1600 |
1612 |
|
1613 lemma current_proc_has_sp: |
|
1614 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp" |
|
1615 by (auto simp:cp2sproc_def split:option.splits dest!:current_has_sec') |
|
1616 |
|
1617 lemma current_proc_has_sp': |
|
1618 "\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" |
|
1619 by (auto dest:current_proc_has_sp) |
|
1620 |
|
1621 |
|
1622 |
|
1623 (* simpset for cf2sfiles *) |
|
1624 |
|
1625 lemma cf2sfiles_open: |
|
1626 "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk> |
|
1627 \<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = ( |
|
1628 if (f' = f \<and> opt \<noteq> None) |
|
1629 then (case cf2sfile (Open p f flag fd opt # s) f of |
|
1630 Some sf \<Rightarrow> {sf} |
|
1631 | _ \<Rightarrow> {} ) |
|
1632 else cf2sfiles s f')" |
|
1633 apply (frule vt_grant_os, frule vd_cons) |
|
1634 apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open |
|
1635 split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open) |
|
1636 apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+ |
|
1637 done |
|
1638 |
|
1639 lemma cf2sfiles_other: |
|
1640 "\<lbrakk>valid (e # s); |
|
1641 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
1642 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
1643 \<forall> p f. e \<noteq> UnLink p f; |
|
1644 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> cf2sfiles (e # s) = cf2sfiles s" |
|
1645 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1646 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI) |
|
1647 apply (drule Set.CollectD, erule bexE, rule CollectI) |
|
1648 apply (rule_tac x = f' in bexI, case_tac e) |
|
1649 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps |
|
1650 split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other') |
|
1651 apply (drule_tac f' = f' in cf2sfile_rmdir) |
|
1652 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+ |
|
1653 |
|
1654 apply (rule_tac x = f' in bexI, case_tac e) |
|
1655 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps |
|
1656 split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other') |
|
1657 apply (drule_tac f' = f' in cf2sfile_rmdir) |
|
1658 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+ |
|
1659 done |
|
1660 |
|
1661 lemma cf2sfile_linkhard1': |
|
1662 "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk> |
|
1663 \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'" |
|
1664 apply (drule same_inode_files_prop1) |
|
1665 by (simp add:cf2sfile_linkhard1) |
|
1666 |
|
1667 lemma cf2sfiles_linkhard: |
|
1668 "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. |
|
1669 if (f' = f \<or> f' \<in> same_inode_files s oldf) |
|
1670 then (case (cf2sfile (LinkHard p oldf f # s) f) of |
|
1671 Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf} |
|
1672 | _ \<Rightarrow> {}) |
|
1673 else cf2sfiles s f')" |
|
1674 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1675 apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard |
|
1676 split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1) |
|
1677 done |
|
1678 |
|
1679 lemma cf2sfile_unlink': |
|
1680 "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk> |
|
1681 \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'" |
|
1682 apply (drule same_inode_files_prop1) |
|
1683 by (simp add:cf2sfile_unlink) |
|
1684 |
|
1685 lemma cf2sfiles_unlink: |
|
1686 "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = ( |
|
1687 if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> |
|
1688 (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then |
|
1689 (case (cf2sfile s f) of |
|
1690 Some sf \<Rightarrow> cf2sfiles s f' - {sf} |
|
1691 | _ \<Rightarrow> {}) |
|
1692 else cf2sfiles s f')" |
|
1693 apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits) |
|
1694 apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp) |
|
1695 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1696 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink) |
|
1697 apply (simp add:current_files_unlink, simp, erule conjE) |
|
1698 apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink) |
|
1699 apply (simp add:current_files_unlink same_inode_files_prop1, simp) |
|
1700 apply (rule_tac x = f'a in bexI, simp, simp) |
|
1701 apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+) |
|
1702 apply (erule conjE|erule exE|erule bexE)+ |
|
1703 apply (case_tac "f'a = f", simp) |
|
1704 apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink) |
|
1705 apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1) |
|
1706 apply (rule_tac x = f'a in bexI, simp, simp) |
|
1707 |
|
1708 apply (rule impI)+ |
|
1709 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1710 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink) |
|
1711 apply (simp add:current_files_unlink, simp, (erule conjE)+) |
|
1712 apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink) |
|
1713 apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp) |
|
1714 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink) |
|
1715 apply (simp add:current_files_unlink, simp) |
|
1716 apply (case_tac "f'a = f", simp) |
|
1717 apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp) |
|
1718 apply (erule bexE, erule conjE) |
|
1719 apply (rule_tac x = f'' in bexI) |
|
1720 apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1) |
|
1721 apply (simp, simp, erule same_inode_files_prop4, simp) |
|
1722 apply (rule_tac x = f'a in bexI) |
|
1723 apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1) |
|
1724 apply (simp, simp) |
|
1725 |
|
1726 |
|
1727 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1728 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink) |
|
1729 apply (simp add:current_files_unlink, simp) |
|
1730 apply (rule_tac x = f'a in bexI) |
|
1731 apply (frule_tac f' = f'a in cf2sfile_unlink) |
|
1732 apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp) |
|
1733 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink) |
|
1734 apply (simp add:current_files_unlink, simp) |
|
1735 apply (rule_tac x = f'a in bexI) |
|
1736 apply (frule_tac f' = f'a in cf2sfile_unlink) |
|
1737 apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp) |
|
1738 done |
|
1739 |
|
1740 lemma cf2sfiles_closefd: |
|
1741 "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = ( |
|
1742 case (file_of_proc_fd s p fd) of |
|
1743 Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and> |
|
1744 (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) |
|
1745 then (case (cf2sfile s f) of |
|
1746 Some sf \<Rightarrow> cf2sfiles s f' - {sf} |
|
1747 | _ \<Rightarrow> {}) |
|
1748 else cf2sfiles s f' |
|
1749 | _ \<Rightarrow> cf2sfiles s f')" |
|
1750 |
|
1751 apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd") |
|
1752 apply (simp_all add:current_files_simps split:if_splits) |
|
1753 |
|
1754 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1755 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1756 apply (simp add:current_files_closefd, simp) |
|
1757 apply (rule_tac x = f'a in bexI) |
|
1758 apply (frule_tac f = f'a in cf2sfile_closefd) |
|
1759 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) |
|
1760 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1761 apply (simp add:current_files_closefd, simp) |
|
1762 apply (rule_tac x = f'a in bexI) |
|
1763 apply (frule_tac f = f'a in cf2sfile_closefd) |
|
1764 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) |
|
1765 |
|
1766 apply (rule conjI, clarify, frule file_of_pfd_is_file, simp) |
|
1767 apply (frule is_file_has_sfile', simp, erule exE, simp) |
|
1768 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1769 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1770 apply (simp add:current_files_closefd, simp, erule conjE) |
|
1771 apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd) |
|
1772 apply (simp add:current_files_closefd same_inode_files_prop1, simp) |
|
1773 apply (rule_tac x = f'a in bexI, simp, simp) |
|
1774 apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+) |
|
1775 apply (erule conjE|erule exE|erule bexE)+ |
|
1776 apply (case_tac "f'a = a", simp) |
|
1777 apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp) |
|
1778 apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1) |
|
1779 apply (rule_tac x = f'a in bexI, simp, simp) |
|
1780 |
|
1781 apply (rule impI)+ |
|
1782 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1783 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1784 apply (simp add:current_files_closefd, simp, (erule conjE)+) |
|
1785 apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd) |
|
1786 apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp) |
|
1787 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1788 apply (simp add:current_files_closefd, simp) |
|
1789 apply (case_tac "f'a = a", simp) |
|
1790 apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp) |
|
1791 apply (erule bexE, erule conjE) |
|
1792 apply (rule_tac x = f'' in bexI) |
|
1793 apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1) |
|
1794 apply (simp, simp, erule same_inode_files_prop4, simp) |
|
1795 apply (rule_tac x = f'a in bexI) |
|
1796 apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1) |
|
1797 apply (simp, simp) |
|
1798 |
|
1799 apply (rule conjI, clarify) |
|
1800 |
|
1801 apply (rule impI) |
|
1802 apply (case_tac "a \<in> files_hung_by_del s", simp_all) |
|
1803 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1804 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1805 apply (simp add:current_files_closefd, simp) |
|
1806 apply (rule_tac x = f'a in bexI) |
|
1807 apply (frule_tac f = f'a in cf2sfile_closefd) |
|
1808 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) |
|
1809 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1810 apply (simp add:current_files_closefd, simp) |
|
1811 apply (rule_tac x = f'a in bexI) |
|
1812 apply (frule_tac f = f'a in cf2sfile_closefd) |
|
1813 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) |
|
1814 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) |
|
1815 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1816 apply (simp add:current_files_closefd, simp) |
|
1817 apply (rule_tac x = f'a in bexI) |
|
1818 apply (frule_tac f = f'a in cf2sfile_closefd) |
|
1819 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) |
|
1820 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) |
|
1821 apply (simp add:current_files_closefd, simp) |
|
1822 apply (rule_tac x = f'a in bexI) |
|
1823 apply (frule_tac f = f'a in cf2sfile_closefd) |
|
1824 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) |
|
1825 done |
|
1826 |
|
1827 lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other |
|
1828 cf2sfiles_unlink cf2sfiles_closefd |
|
1829 |
|
1830 |
|
1831 (* simpset for co2sobj *) |
|
1832 |
|
1833 lemma co2sobj_execve: |
|
1834 "\<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) |
|
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 (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_clone: |
|
1851 "\<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') |
|
1853 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)) |
|
1855 | _ \<Rightarrow> None) |
|
1856 else co2sobj s obj )" |
|
1857 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1858 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
1859 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'") |
|
1860 apply (drule current_proc_has_sp', simp, simp) |
|
1861 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) |
|
1862 apply (rule conjI, rule impI, simp) |
|
1863 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits) |
|
1864 |
|
1865 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
|
1866 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
|
1867 apply (simp add:is_dir_in_current) |
|
1868 done |
|
1869 |
|
1870 lemma co2sobj_ptrace: |
|
1871 "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = ( |
|
1872 case obj of |
|
1873 O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'') |
|
1874 then (case (cp2sproc s p'') of |
|
1875 Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s)) |
|
1876 | _ \<Rightarrow> None) |
|
1877 else if (info_flow_shm s p p'') |
|
1878 then (case (cp2sproc s p'') of |
|
1879 Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s)) |
|
1880 | _ \<Rightarrow> None) |
|
1881 else co2sobj s (O_proc p'') |
|
1882 | _ \<Rightarrow> co2sobj s obj)" |
|
1883 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1884 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted) |
|
1885 |
|
1886 apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits |
|
1887 dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
1888 |
|
1889 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
|
1890 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
|
1891 apply (simp add:is_dir_in_current) |
|
1892 done |
|
1893 |
|
1894 lemma co2sobj_open: |
|
1895 "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk> |
|
1896 \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of |
|
1897 O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None) |
|
1898 then (case (cf2sfile (Open p f flag fd opt # s) f) of |
|
1899 Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s)) |
|
1900 | _ \<Rightarrow> None) |
|
1901 else co2sobj s (O_file f') |
|
1902 | O_proc p' \<Rightarrow> if (p' = p) |
|
1903 then (case (cp2sproc (Open p f flag fd opt # s) p) of |
|
1904 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
|
1905 | _ \<Rightarrow> None) |
|
1906 else co2sobj s (O_proc p') |
|
1907 | _ \<Rightarrow> co2sobj s obj )" |
|
1908 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1909 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits |
|
1910 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
1911 |
|
1912 apply (simp split:if_splits t_object.splits) |
|
1913 apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+) |
|
1914 apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f") |
|
1915 apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp) |
|
1916 apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps) |
|
1917 apply (simp add:tainted_eq_Tainted) |
|
1918 apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current) |
|
1919 apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits) |
|
1920 |
|
1921 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
1922 |
|
1923 apply (frule is_dir_in_current) |
|
1924 apply (frule_tac f' = list in cf2sfile_open) |
|
1925 apply (simp add:current_files_simps split:option.splits) |
|
1926 apply (simp split:if_splits option.splits) |
|
1927 done |
|
1928 |
|
1929 lemma co2sobj_readfile: |
|
1930 "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = ( |
|
1931 case obj of |
|
1932 O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of |
|
1933 Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s) |
|
1934 then (case (cp2sproc s p') of |
|
1935 Some sp \<Rightarrow> Some (S_proc sp True) |
|
1936 | _ \<Rightarrow> None) |
|
1937 else co2sobj s obj) |
|
1938 | _ \<Rightarrow> None) |
|
1939 | _ \<Rightarrow> co2sobj s obj)" |
|
1940 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1941 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits |
|
1942 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
1943 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
1944 |
|
1945 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
|
1946 simp:current_files_simps cf2sfiles_simps cf2sfile_simps |
|
1947 dest:is_file_in_current is_dir_in_current) |
|
1948 done |
|
1949 |
|
1950 lemma co2sobj_writefile: |
|
1951 "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = ( |
|
1952 case obj of |
|
1953 O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of |
|
1954 Some f \<Rightarrow> (if (f \<in> same_inode_files s f') |
|
1955 then Some (S_file (cf2sfiles s f') |
|
1956 (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s)) |
|
1957 else co2sobj s obj) |
|
1958 | _ \<Rightarrow> None) |
|
1959 | _ \<Rightarrow> co2sobj s obj)" |
|
1960 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1961 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
1962 |
|
1963 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
1964 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
1965 same_inode_files_prop6 |
|
1966 dest:is_file_in_current is_dir_in_current) |
|
1967 |
|
1968 (* should delete has_same_inode !?!?*) |
|
1969 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
1970 |
|
1971 lemma co2sobj_closefd: |
|
1972 "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = ( |
|
1973 case obj of |
|
1974 O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of |
|
1975 Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> |
|
1976 f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f. |
|
1977 f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) |
|
1978 then (case (cf2sfile s f, co2sobj s (O_file f')) of |
|
1979 (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b) |
|
1980 | _ \<Rightarrow> None) |
|
1981 else co2sobj s obj) |
|
1982 | _ \<Rightarrow> co2sobj s obj) |
|
1983 | O_proc p' \<Rightarrow> (if (p = p') |
|
1984 then (case (cp2sproc (CloseFd p fd # s) p) of |
|
1985 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
|
1986 | _ \<Rightarrow> None) |
|
1987 else co2sobj s obj) |
|
1988 | _ \<Rightarrow> co2sobj s obj) " |
|
1989 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
1990 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
1991 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits |
|
1992 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
1993 |
|
1994 apply (frule is_file_in_current) |
|
1995 apply (case_tac "file_of_proc_fd s p fd") |
|
1996 apply (simp add:tainted_eq_Tainted) |
|
1997 apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp) |
|
1998 apply (frule_tac f' = list in cf2sfiles_closefd, simp) |
|
1999 apply (simp add:is_file_simps current_files_simps) |
|
2000 apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits |
|
2001 dest!:current_file_has_sfile' dest:hung_file_in_current)[1] |
|
2002 |
|
2003 apply (simp add:is_dir_simps, frule is_dir_in_current) |
|
2004 apply (frule_tac f = list in cf2sfile_closefd) |
|
2005 apply (clarsimp simp:current_files_closefd split:option.splits) |
|
2006 apply (drule file_of_pfd_is_file', simp+) |
|
2007 done |
|
2008 |
|
2009 lemma co2sobj_unlink: |
|
2010 "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = ( |
|
2011 case obj of |
|
2012 O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> |
|
2013 (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) |
|
2014 then (case (cf2sfile s f, co2sobj s (O_file f')) of |
|
2015 (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b) |
|
2016 | _ \<Rightarrow> None) |
|
2017 else co2sobj s obj |
|
2018 | _ \<Rightarrow> co2sobj s obj)" |
|
2019 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2020 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2021 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits |
|
2022 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
2023 apply (frule is_file_in_current) |
|
2024 apply (frule_tac f' = list in cf2sfile_unlink, simp) |
|
2025 apply (frule_tac f' = list in cf2sfiles_unlink, simp) |
|
2026 apply (simp add:is_file_simps current_files_simps) |
|
2027 apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits |
|
2028 dest!:current_file_has_sfile')[1] |
|
2029 |
|
2030 apply (simp add:is_dir_simps, frule is_dir_in_current) |
|
2031 apply (frule_tac f' = list in cf2sfile_unlink) |
|
2032 apply (clarsimp simp:current_files_unlink split:option.splits) |
|
2033 apply (drule file_dir_conflict, simp+) |
|
2034 done |
|
2035 |
|
2036 lemma co2sobj_rmdir: |
|
2037 "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj" |
|
2038 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2039 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2040 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits |
|
2041 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
2042 apply (simp add:is_file_simps dir_is_empty_def) |
|
2043 apply (case_tac "f = list", drule file_dir_conflict, simp, simp) |
|
2044 apply (simp add:cf2sfiles_other) |
|
2045 apply (auto simp:cf2sfile_simps dest:is_dir_in_current) |
|
2046 done |
|
2047 |
|
2048 lemma co2sobj_mkdir: |
|
2049 "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = ( |
|
2050 if (obj = O_dir f) |
|
2051 then (case (cf2sfile (Mkdir p f i # s) f) of |
|
2052 Some sf \<Rightarrow> Some (S_dir sf) |
|
2053 | _ \<Rightarrow> None) |
|
2054 else co2sobj s obj)" |
|
2055 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2056 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2057 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits |
|
2058 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
2059 apply (frule_tac cf2sfiles_other, simp+) |
|
2060 apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir) |
|
2061 apply (frule current_file_has_sfile, simp, erule exE, simp) |
|
2062 apply (drule cf2sfile_mkdir1, simp+) |
|
2063 done |
|
2064 |
|
2065 lemma same_inodes_Tainted: |
|
2066 "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)" |
|
2067 apply (frule same_inode_files_prop8, frule same_inode_files_prop7) |
|
2068 apply (auto intro:has_same_inode_Tainted) |
|
2069 done |
|
2070 |
|
2071 lemma co2sobj_linkhard: |
|
2072 "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> |
|
2073 \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = ( |
|
2074 case obj of |
|
2075 O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf) |
|
2076 then (case (cf2sfile (LinkHard p oldf f # s) f) of |
|
2077 Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s)) |
|
2078 | _ \<Rightarrow> None) |
|
2079 else co2sobj s obj |
|
2080 | _ \<Rightarrow> co2sobj s obj)" |
|
2081 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2082 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2083 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits |
|
2084 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
2085 apply (frule_tac cf2sfiles_linkhard, simp+) |
|
2086 apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard) |
|
2087 apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted |
|
2088 split:option.splits if_splits dest:Tainted_in_current |
|
2089 dest!:current_has_sec' current_file_has_sfile')[1] |
|
2090 |
|
2091 apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current) |
|
2092 apply (frule is_dir_in_current) |
|
2093 apply (frule current_file_has_sfile, simp) |
|
2094 apply (drule cf2sfile_linkhard1, simp+) |
|
2095 done |
|
2096 |
|
2097 lemma co2sobj_truncate: |
|
2098 "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = ( |
|
2099 case obj of |
|
2100 O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0) |
|
2101 then Some (S_file (cf2sfiles s f') (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s)) |
|
2102 else co2sobj s obj |
|
2103 | _ \<Rightarrow> co2sobj s obj)" |
|
2104 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2105 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2106 |
|
2107 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2108 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2109 same_inode_files_prop6 |
|
2110 dest:is_file_in_current is_dir_in_current) |
|
2111 |
|
2112 (* should delete has_same_inode !?!?*) |
|
2113 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
2114 |
|
2115 lemma co2sobj_kill: |
|
2116 "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj" |
|
2117 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2118 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2119 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2120 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2121 same_inode_files_prop6 |
|
2122 dest:is_file_in_current is_dir_in_current) |
|
2123 done |
|
2124 |
|
2125 lemma co2sobj_exit: |
|
2126 "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj" |
|
2127 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2128 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2129 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2130 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2131 same_inode_files_prop6 |
|
2132 dest:is_file_in_current is_dir_in_current) |
|
2133 done |
|
2134 |
|
2135 lemma co2sobj_createmsgq: |
|
2136 "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = ( |
|
2137 case obj of |
|
2138 O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of |
|
2139 Some sq \<Rightarrow> Some (S_msgq sq) |
|
2140 | _ \<Rightarrow> None) |
|
2141 else co2sobj s obj |
|
2142 | _ \<Rightarrow> co2sobj s obj)" |
|
2143 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2144 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2145 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2146 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2147 same_inode_files_prop6 |
|
2148 dest!:current_has_smsgq' |
|
2149 dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq) |
|
2150 done |
|
2151 |
|
2152 lemma co2sobj_sendmsg: |
|
2153 "\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = ( |
|
2154 case obj of |
|
2155 O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of |
|
2156 Some sq \<Rightarrow> Some (S_msgq sq) |
|
2157 | _ \<Rightarrow> None) |
|
2158 else co2sobj s obj |
|
2159 | _ \<Rightarrow> co2sobj s obj)" |
|
2160 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2161 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2162 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2163 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2164 same_inode_files_prop6 |
|
2165 dest!:current_has_smsgq' |
|
2166 dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg) |
|
2167 done |
|
2168 |
|
2169 lemma co2sobj_recvmsg: |
|
2170 "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = ( |
|
2171 case obj of |
|
2172 O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of |
|
2173 Some sq \<Rightarrow> Some (S_msgq sq) |
|
2174 | _ \<Rightarrow> None) |
|
2175 else co2sobj s obj |
|
2176 | O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s) |
|
2177 then (case (cp2sproc s p') of |
|
2178 Some sp \<Rightarrow> Some (S_proc sp True) |
|
2179 | _ \<Rightarrow> None) |
|
2180 else co2sobj s obj |
|
2181 | _ \<Rightarrow> co2sobj s obj)" |
|
2182 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2183 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2184 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2185 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2186 same_inode_files_prop6 |
|
2187 dest!:current_has_smsgq' |
|
2188 dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg) |
|
2189 done |
|
2190 |
|
2191 lemma co2sobj_removemsgq: |
|
2192 "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk> |
|
2193 \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj" |
|
2194 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2195 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2196 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2197 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2198 same_inode_files_prop6 |
|
2199 dest!:current_has_smsgq' |
|
2200 dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq) |
|
2201 done |
|
2202 |
|
2203 lemma co2sobj_createshm: |
|
2204 "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = co2sobj s obj" |
|
2205 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) |
|
2207 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 |
|
2209 same_inode_files_prop6 ch2sshm_simps |
|
2210 dest!:current_shm_has_sh' |
|
2211 dest:is_file_in_current is_dir_in_current) |
|
2212 done |
|
2213 |
|
2214 lemma co2sobj_detach: |
|
2215 "\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = ( |
|
2216 case obj of |
|
2217 O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of |
|
2218 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
|
2219 | _ \<Rightarrow> None) |
|
2220 else co2sobj s obj |
|
2221 | _ \<Rightarrow> co2sobj s obj)" |
|
2222 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2223 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2224 |
|
2225 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2226 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
2227 same_inode_files_prop6 ch2sshm_simps |
|
2228 dest!:current_shm_has_sh' |
|
2229 dest:is_file_in_current is_dir_in_current) |
|
2230 done |
|
2231 |
|
2232 lemma co2sobj_deleteshm: |
|
2233 "\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = ( |
|
2234 case obj of |
|
2235 O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of |
|
2236 Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s)) |
|
2237 | _ \<Rightarrow> None) |
|
2238 | _ \<Rightarrow> co2sobj s obj)" |
|
2239 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2240 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2241 |
|
2242 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
2243 simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
|
2244 same_inode_files_prop6 ch2sshm_simps |
|
2245 dest!:current_shm_has_sh' |
|
2246 dest:is_file_in_current is_dir_in_current) |
|
2247 done |
|
2248 |
|
2249 lemma co2sobj_attach: |
|
2250 "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = ( |
|
2251 case obj of |
|
2252 O_proc p' \<Rightarrow> if (p' = p) |
|
2253 then (case (cp2sproc (Attach p h flag # s) p) of |
|
2254 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> |
|
2255 (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h))) |
|
2256 | _ \<Rightarrow> None) |
|
2257 else if (\<exists> flag'. (p', flag') \<in> procs_of_shm s h) |
|
2258 then (case (cp2sproc s p') of |
|
2259 Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or> |
|
2260 (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR))) |
|
2261 | _ \<Rightarrow> None) |
|
2262 else co2sobj s obj |
|
2263 | _ \<Rightarrow> co2sobj s obj)" |
|
2264 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
2265 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
2266 |
|
2267 apply (rule conjI|rule impI|erule exE)+ |
|
2268 apply (simp split:option.splits) |
|
2269 apply (rule impI, frule current_proc_has_sp, simp) |
|
2270 apply ((erule exE)+, auto simp:cp2sproc_attach tainted_eq_Tainted)[1] |
|
2271 apply (rule impI|rule conjI)+ |
|
2272 apply (subgoal_tac "p \<in> current_procs (Attach p h flag # s)") |
|
2273 apply (drule_tac p = p in current_proc_has_sp, simp, erule exE) |
|
2274 apply (auto simp:tainted_eq_Tainted)[1] |
|
2275 apply (simp, rule impI) |
|
2276 apply (subgoal_tac "nat \<in> current_procs (Attach p h flag # s)") |
|
2277 apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE) |
|
2278 apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE) |
|
2279 apply (auto simp:cp2sproc_attach tainted_eq_Tainted)[1] |
|
2280 apply simp |
|
2281 |
|
2282 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
|
2283 simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
|
2284 same_inode_files_prop6 |
|
2285 dest:is_file_in_current is_dir_in_current) |
|
2286 done |
|
2287 |
|
2288 |
|
2289 lemma co2sobj_other: |
|
2290 "\<lbrakk>valid (e # s); alive (e # s) obj; |
|
2291 \<forall> p f fds. e \<noteq> Execve p f fds; |
|
2292 \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms; |
|
2293 \<forall> p p'. e \<noteq> Ptrace p p'; |
|
2294 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt; |
|
2295 \<forall> p fd. e \<noteq> ReadFile p fd; |
|
2296 \<forall> p fd. e \<noteq> WriteFile p fd; |
|
2297 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
2298 \<forall> p f. e \<noteq> UnLink p f; |
|
2299 \<forall> p f. e \<noteq> Rmdir p f; |
|
2300 \<forall> p f i. e \<noteq> Mkdir p f i; |
|
2301 \<forall> p f f'. e \<noteq> LinkHard p f f'; |
|
2302 \<forall> p f len. e \<noteq> Truncate p f len; |
|
2303 \<forall> p q. e \<noteq> CreateMsgq p q; |
|
2304 \<forall> p q m. e \<noteq> SendMsg p q m; |
|
2305 \<forall> p q m. e \<noteq> RecvMsg p q m; |
|
2306 \<forall> p q. e \<noteq> RemoveMsgq p q; |
|
2307 \<forall> p h. e \<noteq> CreateShM p h; |
|
2308 \<forall> p h flag. e \<noteq> Attach p h flag; |
|
2309 \<forall> p h. e \<noteq> Detach p h; |
|
2310 \<forall> p h. e \<noteq> DeleteShM p h |
|
2311 \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj" |
|
2312 apply (frule vt_grant, case_tac e) |
|
2313 apply (auto intro:co2sobj_kill co2sobj_exit) |
|
2314 done |
|
2315 |
|
2316 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile |
|
2317 co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard |
|
2318 co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg |
|
2319 co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm |
|
2320 |
1601 end |
2321 end |
1602 |
2322 |
1603 (*<*) |
2323 (*<*) |
1604 end |
2324 end |
1605 (*>*) |
2325 (*>*) |