Systematic Classification of Attackers via Bounded Model Checking

TL;DR

This paper introduces a methodology using bounded model checking to classify attackers based on which security requirements they can compromise, employing heuristics to improve scalability.

Contribution

It presents a novel approach to systematically generate and classify attackers in security verification, with heuristics to handle large models effectively.

Findings

Heuristics improve scalability of attacker classification

Methodology successfully applied to hardware benchmarks

Classifies attackers based on broken security requirements

Abstract

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.