Systematic classification of attackers via bounded model checking

In this work, we study the problem of verification of systems in the presence of attackers using bounded model checking. Given a system and a set of security requirements, we present a methodology to generate and classify attackers, mapping them to the set of requirements that they can break. A naiv...

وصف كامل

محفوظ في:
التفاصيل البيبلوغرافية
المؤلفون الرئيسيون: ROTHSTEIN-MORRIS, Eric, SUN, Jun, CHATTOPADYAY, Sudipta
التنسيق: text
اللغة:English
منشور في: Institutional Knowledge at Singapore Management University 2020
الموضوعات:
الوصول للمادة أونلاين:https://ink.library.smu.edu.sg/sis_research/4634
https://ink.library.smu.edu.sg/context/sis_research/article/5637/viewcontent/1911.05808.pdf
الوسوم: إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
المؤسسة: Singapore Management University
اللغة: English
الوصف
الملخص:In this work, we study the problem of verification of systems in the presence of attackers using bounded model checking. Given a system and a set of security requirements, we present a methodology to generate and classify attackers, mapping them to the set of requirements that they can break. A naive approach suffers from the same shortcomings of any large model checking problem, i.e., memory shortage and exponential time. To cope with these shortcomings, we describe two sound heuristics based on cone-of-influence reduction and on learning, which we demonstrate empirically by applying our methodology to a set of hardware benchmark systems.