Querying Attack-Fault-Defense Trees: Property Specification in Smart Grid and Aerospace Case Studies

TL;DR

This paper presents AFDL, a logic-based framework and query language for analyzing safety, security, and defense interactions in complex systems, demonstrated through smart grid and aerospace case studies.

Contribution

Introduction of AFDL and LangAFDL, a formal framework and query language for comprehensive safety-security-defense analysis in critical systems.

Findings

AFDL effectively models safety, security, and defense interactions.

LangAFDL enables complex, intuitive queries including Boolean and quantified analysis.

Case studies demonstrate the framework's practical utility and expressiveness.

Abstract

This paper introduces AFDL, a logic-based framework for reasoning about safety, security, and defense interactions in Attack-Fault-Defense Trees, which is a model that captures all safety, security, and defense domains in a single framework. We showcase both AFDL and propose a structured domain specific query language, LangAFDL, which enables domain experts to express complex analysis goals through intuitive templates. LangAFDL supports both Boolean and quantified queries as well as minimal cut set analysis, capturing the interplay between safety, security, and defensive measures. We illustrate the expressiveness and utility of the approach through representative queries over two different real-world case studies: Gridshield and Ground Segment as a Service. The formalization lays the automated safety-security groundwork for analyses in mission-critical systems and paves the way for future tool development and integration into design workflows.