مدل سازی صوری افزونگی و ناسازگاری خط مشی های امنیتی در سیستم های کنترل دسترسی حالتمند

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

Keywords:

خط مشی امنیتی , مدل صوری , حفاظ حالتمند , منطق قابل فسخ