Threat Repair with Optimization Modulo Theories

Thorsten Tarrach, Masoud Ebrahimi, Sandra König, Christoph Schmittner, Roderick Bloem, Dejan Nickovic

Research output: Working paperPreprint

Abstract

We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure is a suggestion of model attribute repair that eliminates threats. Whenever threat prevention fails, we automatically explain why the threat happens. We implement our approach using the state-of-the-art Z3 SMT solver and interface it with the threat analysis tool THREATGET. We demonstrate the value of our procedure in two case studies from automotive and smart home domains, including an industrial-strength example.
Original languageEnglish
Publication statusPublished - 6 Oct 2022

Keywords

  • cs.CR
  • cs.FL
  • cs.LO

Fingerprint

Dive into the research topics of 'Threat Repair with Optimization Modulo Theories'. Together they form a unique fingerprint.

Cite this