Abstract
Due to the characteristics and connectivity of today's critical infrastructure like the Cyber Physical Systems (CPS), cyber-attacks on these systems are currently difficult to prevent in an efficient and sustainable manner. Prevention and mitigation need accurate identification and evaluation of: system vulnerabilities, likely threats and attacks, and applicable hardening measures. Furthermore, the ability to prioritize hardening measures based on accurate assessments of threat risk and consequence and mitigation availability, applicability, and cost is also needed.
To address this challenge we created HESTIA: High-level and Extensible System for Training and Infrastructure risk Assessment. We describe the architecture and working principles of HESTIA. We present a formal model of the HESTIA system. We validate the HESTIA system using formal proofs and a case-study based proof tracing. We hope that the HESTIA system model will enable CPS engineers to build software that can iteratively: 1) specify a CPS (system), 2) select applicable attacks and hardening measures from a library (delta), 3) check system and delta specifications for consistency and applicability, and 4) apply deltas on system specifications, forming a new CPS model. HESTIA enables the discovery of attack-defend scenarios through simulation and the design of optimal hardening strategies for a given CPS.
The contributions reported in this dissertation are: (a) present a requirement for high-level and reconfigurable system for adversary-aware infrastructure risk assessment by performing a review of the existing literature; (b) present the architecture and workflow of HESTIA: a high-level and extensible system for adversary-aware infrastructure risk assessment; (c) formalize the HESTIA process and workflow; (d) present METICS: a realistic case study of a CPS organization; and (e) validate the HESTIA system using formal verification and proof tracing using the METICS case study.