كشف سناريوهاي نفوذ به شبكه هاي كامپيوتري با استفاده از بررسي كننده مدل SPIN  Fulltext 

[ مهدي آبادي ] - دانشكده فني و مهندسي دانشگاه تربيت مدرس
[ سعيد جليلي ] - دانشكده فني و مهندسي دانشگاه تربيت مدرس

خلاصه مقاله:

هر سناريوي نفود يك توالي از سوء استفاده هاي قابل اجرا توسط نفوذي است كه با يك هدف خاص مانند دستيابي به پايگاه داده ها، جلوگيري از سرويس و غيره انجام مي شود. در اين مقاله، چگونگي استفاده از شيوه بررسي مدل LTL براي كشف خودكار سناريوهاي نفوذ به شبكه هاي كامپيوتري نشان داده مي شود. بدين منظور، فرض مي شود كه در شبكه مورد نظر يك سيستم تشخيص نفوذ مبتني بر شبكه (NIDS) وجود دارد و نفوذي قصد دارد با انجام يك توالي از سوء استفاده ها و بدون اين كه NIDS هشداري را اعلام كند به هدف خود برسد. براي كشف سناريوي نفوذ، ابتدا اجزاء شبكه با استفاده از زبان مدل سازي PROMELA توصيف مي شوند. سپس، مشخصه اي كه نقيض هدف نفوذي را توصيف مي كند، در منطق زماني LTL بيان مي شود. در نهايت، به كمك بررسي كننده مدل SPIN كه يك بررسي كننده مدل LTL است، هر گونه تخطي از مشخصه فوق (به عبارت ديگر سناريوي نفوذ) بدست اورده مي شود. همچنين، الگوريتمي ارائه مي شود كه با استفاده از آن ميتوان از روي سناريوي نفوذ كشف شده سناريوي نفوذ حداقل را بدست اورد.

سناريوي نفوذ ، بررسي مدل ، وارسي خودكار ، منطق زماني LTL