Many-to-many information flow policies

تکنیک های جریان اطلاعات معمولا اطلاعات را با توجه به سطح امنیتی مناسب طبقه بندی می کنند و سیاست هایی را که بر مبنای روابط باینری بین سطوح فردی هستند، به عنوان مثال، نشان می دهد که اطلاعات از یک سطح به دیگری مجاز است. ما استدلال می کنیم که برخی از ویژگی های جریان اطلاعات به طور طبیعی نیازمند الگوهای هماهنگی است که شامل مجموعه ای از سطوح امنیتی به جای سطوح فردی است: برخی از اطلاعات مخفی می تواند به راحتی به مجموعه ای از کانال های محرمانه از سطوح امنیتی غیر قابل انعطاف افشا شود؛ یک گروه از سازمان های رقیب ممکن است موافقت کنند که اسرار آنها را افشا کنند، با افشای اطلاعات فردی ناخواسته، و غیره. به این مبنا، یک پایه معنایی برای خواص مبتنی بر مدل های علیت محاسبات مطالعه می کنیم. ما یک زبان ساده برای بیان سیاست های جریان اطلاعات پیشنهاد می کنیم که در آن رابطه جریان پذیرفته شده بین سطح امنیت فردی با یک رابطه بین مجموعه ای از سطوح امنیتی جایگزین می شود، به این ترتیب امکان جریان اطلاعات هماهنگ را می گیرد. جریان اطلاعات از لحاظ وابستگی های علی بیان می شود و رضایت از یک سیاست با توجه به ساختار رویدادی که فرض می شود ساختار علیت محاسبات سیستم را تصدیق می کند، تعریف می شود. ما همچنین به طور پیشینی فرصت های کاربردی رویکرد ما را با تمرکز بر روی سیستم های مشخص شده به عنوان شبکه های امن پتری، یک فرمالیزم با معناشناسی علمی اثبات شده بررسی می کنیم. ما نشان می دهیم که چگونه روش های تایید مبتنی بر بازرسی شبکه های پتری برای حل مشکل بررسی رضایت از سیاست می تواند مورد استفاده قرار گیرد.