A formal basis for the design and analysis of firewall security policies

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