مهسا افشارفرنیا - دانشجوی، کارشناسی ارشد دانشکده برق و کامپیوتر دانشگاه شهید بهشتی
حسن حقیقی - استادیار، دانشکده برق و کامپیوتر دانشگاه شهید بهشتی

با توجه به حساسیت اطلاعات سامانههایC4I تهدیدهای امنیتی وارده به این سامانهها در حال افزایش میباشند، لذا امنیت وقابلیت اطمینان یک چالش اساسی برای حفظ یکپارچگی، محرمانگی، در دسترس بودن و پاسخگو بودن برای این سامانهها می-باشد. استفاده از روشهای صوری بهمنظور توصیف، درستییابی و تولید برنامه صوری در دامنههای کاربردی مهم، از جمله سامانههایC4Iموجب افزایش قابلیت اطمینان این سامانهها، امنیت فضای سایبری و تبادل اطلاعات، خواهد شد. یکی از تکنیکها برایکشف و ردیابی حملات، شبیهسازی مهاجم و مدلسازی نحوه انتشار کرمها در حملات سایبری زنجیرههای مارکوف میباشند. در این مقاله سعی خواهد شد فرمالیسمی مبتنی برZ برای توصیف سامانههایC4I احتمالاتی که با کمک زنجیرههای مارکوف مدل می- شوند، ارائه شود. وجود چنین فرمالیسمی برخلاف روشهای دیگر مدلسازی مانند زنجیرههای مارکوف، علاوه بر توصیف نیازمندی های احتمالاتی، امکان توصیف نیازمندیهای وظیفهمندی سیستمهایC4Iرا نیز دربردارد. همچنین میتوان از ابزارهای متداولz مانندZ-evesبرای بررسی نوع و کنترل سازگاری توصیفهای آن، استفاده نمود. در نهایت برای نشان دادن قابلیت بکارگیری فرمالیسم ارائه شده، این فرمالیسم را بر روی مطالعه موردی در مورد نحوهی انتشار کرمها در حملات سایبری اعمال خواهیم کرد.

توصیف صوری، زنجیرههای مارکوف، زنجیره مارکوف زمان پیوسته، زنجیره مارکوف زمان گسسته، حملات سایبری