Abstract
We propose a model-based procedure for preventing security threats using formal models. We encode system models and 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. 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.
Original language | English |
---|---|
Title of host publication | Computer Safety, Reliability, and Security - 42nd International Conference, SAFECOMP 2023, Toulouse, France, September 20-22, 2023, Proceedings |
Pages | 135-148 |
Number of pages | 14 |
Volume | 14181 |
ISBN (Electronic) | 978-3-031-40923-3 |
DOIs | |
Publication status | Published - 20 Sept 2023 |
Event | SAFECOMP 2023: 42nd International Conference on Computer Safety, Reliability and Security: DECSoS 2023: 18th International Workshop on Dependable Smart Embedded Cyber-Physical Systems and Systems-of-Systems - Toulouse, Toulouse, France Duration: 19 Sept 2023 → 22 Sept 2023 https://safecomp2023.cnrs.fr/workshops/ |
Workshop
Workshop | SAFECOMP 2023: 42nd International Conference on Computer Safety, Reliability and Security |
---|---|
Country/Territory | France |
City | Toulouse |
Period | 19/09/23 → 22/09/23 |
Internet address |
Research Field
- Dependable Systems Engineering