Fine-grained symbolic verification of heterogeneous systems: systematic exploration and formal analysis of “what-if” attack scenarios

The rapid evolution of distributed ecosystems, ranging from web-based authentication platforms to industrial IoT and au- tonomous robotic swarms, has introduced unprecedented se- curity challenges. As these systems become more heteroge- neous, integrating diverse hardware, software stacks, and communication paradigms, traditional “all-or-nothing” secu- rity assessments often fail to capture the nuances of modern, multi-layered threats. This thesis addresses the problem of au- tomatically verifying security properties in complex environments where trust assumptions are partially violated. The core contribution of this work is the development of a uni- fied formal framework for the symbolic verification of security protocols across both coupled (point-to-point) and decoupled (publish/subscribe) communication architectures. By shift- ing the focus from monolithic entities to an interface-based modelling approach, we enable a fine-grained threat analysis. This allows for the systematic exploration of “what-if” scenar- ios, where an adversary might compromise specific functional interfaces, while other components remain secure. We first apply this methodology to the Italian Electronic Iden- tity Card (CIE) ecosystem, identifying and mitigating vul- nerabilities in multi-factor authentication schemes through dynamic attack scenario exploration. The framework is then extended to uncoupled systems by introducing a novel com- positional model based on directed hypergraphs. This model formalises unique security dynamics, such as read and write amplification laws inherent in topic-based communication. xix To address the limitations of stateless security measures, the thesis further investigates the integration of service mesh ar- chitectures as enforcement points for end-to-end security in- variants. We propose and implement stateful access control policies within the mesh, with a dedicated management layer to handle state-aware requirements. The effectiveness of the proposed approach is demonstrated through the verification of the Atomic Broadcast protocol, showing how the combination of formal modelling and service mesh orchestration can successfully neutralise complex attack scenarios that bypass traditional defences. Ultimately, this re- search provides a rigorous, platform-independent benchmark for securing modern, heterogeneous distributed systems. Keywords: Symbolic formal verification, Fine-grained threat modelling, Heterogeneous systems, “What-if” analysis, Ser- vice mesh, Stateful access control.