Threat Repair with Optimization Modulo Theories

Autor:	Tarrach, Thorsten, Ebrahimi, Masoud, König, Sandra, Schmittner, Christoph, Bloem, Roderick, Nickovic, Dejan
Rok vydání:	2022
Předmět:	Computer Science - Cryptography and Security Computer Science - Formal Languages and Automata Theory Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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.
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2210.03207 Zobrazit plný text záznamu View this record from Arxiv