Idioma:

Threat Repair with Optimization Modulo Theories

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

arXiv.org, 2022-10

Texto completo disponível

Citações Citado por

Título:
Threat Repair with Optimization Modulo Theories
Autor: Tarrach, Thorsten ; Ebrahimi, Masoud ; König, Sandra ; Schmittner, Christoph ; Bloem, Roderick ; Nickovic, Dejan
Assuntos: Computer Science - Cryptography and Security ; Computer Science - Formal Languages and Automata Theory ; Computer Science - Logic in Computer Science ; Optimization ; Security ; Smart buildings ; Threat evaluation
É parte de: arXiv.org, 2022-10
Descrição: 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.
Editor: Ithaca: Cornell University Library, arXiv.org
Idioma: Inglês

Links

Voltar para lista de resultados