equal
deleted
inserted
replaced
473 (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})" |
473 (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})" |
474 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>" |
474 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>" |
475 |
475 |
476 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
476 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
477 where |
477 where |
478 "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs s) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. |
478 "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. |
479 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
479 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
480 |
480 |
481 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
481 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
482 where |
482 where |
483 "current_msgqs [] = init_msgqs" |
483 "current_msgqs [] = init_msgqs" |
1415 |
1415 |
1416 locale tainting = flask + |
1416 locale tainting = flask + |
1417 |
1417 |
1418 fixes seeds :: "t_object set" |
1418 fixes seeds :: "t_object set" |
1419 assumes |
1419 assumes |
1420 seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj" |
1420 seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj" |
|
1421 and same_inode_in_seeds: "\<And> f f'. \<lbrakk>O_file f \<in> seeds; has_same_inode [] f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> seeds" |
|
1422 and flow_shm_in_seeds: "\<And> p p'. \<lbrakk>O_proc p \<in> seeds; info_flow_shm [] p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> seeds" |
1421 |
1423 |
1422 begin |
1424 begin |
1423 |
1425 |
1424 inductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100) |
1426 inductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100) |
1425 where |
1427 where |