论文标题
通过优化模型理论维修的威胁维修
Threat Repair with Optimization Modulo Theories
论文作者
论文摘要
我们提出了一个基于模型的程序，用于自动使用正式模型防止安全威胁。我们将系统模型和潜在威胁编码为满意度模型理论（SMT）公式。该模型使我们可以将安全问题作为满意度查询。我们将预防威胁的预防作为优化问题。我们的威胁预防程序的结果是模型属性维修的建议，以消除威胁。每当预防威胁失败时，我们会自动解释为什么威胁发生。我们使用最先进的Z3 SMT求解器实施我们的方法，并将其与威胁分析工具威胁接口。我们在来自汽车和智能家居领域的两个案例研究中证明了我们的程序的价值，包括工业强度的示例。
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.
