Threat Repair with Optimization Modulo Theories

TL;DR

This paper introduces a formal, model-based approach for automatically preventing security threats by encoding system models and threats as SMT formulas, and solving an optimization problem to suggest repairs.

Contribution

It presents a novel method that uses SMT solvers to automatically identify and repair security threats in system models, with automatic explanations for failures.

Findings

Successfully applied to automotive and smart home case studies

Automates threat prevention and provides explanations when prevention fails

Demonstrates effectiveness on industrial-strength example

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.