Modern societies depend on complex digital and cyber-physical systems for essential functions, including critical infrastructure, healthcare, transport and national security. In these settings, security and safety claims must be precise and unambiguous. This theme focuses on how such claims are constructed, justified and sustained over time.

This theme centres on formal guarantees of security and safety in high integrity systems. Formal guarantees aim to provide rigorous claims about security and safety properties, often grounded in mathematics, logic and formal methods. However, guarantees do not exist in isolation. They are shaped by design choices and the communities that develop, deploy and rely on them. This theme brings together researchers from formal methods, systems engineering and security, while engaging with broader disciplines, to understand how guarantees are defined and proven, and also how they are interpreted, communicated and maintained as systems move from specification and development to deployment and real-world use.

The key research strands are:

• End-to-end guarantees across complex systems: this strand brings together questions about the security and safety guarantees themselves and how they can be maintained across the full lifecycle of a system. This includes reasoning about end-to-end guarantees, from the initial specification of security goals through design, implementation, deployment and operation. It considers interactions between different guarantees where trade-offs occur, and the role of assumptions in shaping claims.
• The gap between models and reality: formal guarantees are typically grounded in abstract models. This strand investigates the gap between formal models and real-world systems, and how that gap can affect the applicability and strength of guarantees in practice. A particular focus is on making this gap better understood across disciplines and stakeholder communities.
• Influences on formal guarantees: this strand focuses on the factors that shape whether formal security and safety guarantees can be developed in practice. This includes technical barriers, for example, the scalability and cost of formal methods tools, limitations of existing tools and system complexity. It also includes influences such as stakeholder engagement and designing guarantees that are appropriate for, and reflect the needs of, the communities and users who depend on them.

Key Objectives

• To develop approaches for end-to-end reasoning about security and safety guarantees in high-integrity systems.
• To define and communicate the gap between formal models and operational systems, making the implications more visible across key stakeholder groups.
• To identify and better understand the technical constraints that shape the abilities of formal methods tools.
• To explore how contextual understanding can inform the development of guarantees are appropriate, meaningful and trusted by key stakeholder groups.

Key Questions

• How can security and safety guarantees be reasoned about across the full system lifecycle, including interactions, trade-offs and evolving assumptions?
• How do gaps between formal methods and real-world systems affect the validity and reliability of security and safety guarantees in practice?
• What technical barriers limit the development and application of formal methods, and what can be done to break down these barriers?
• How can security and safety guarantees be designed and communicated in ways that reflect the needs and expectations of diverse stakeholder communities?

Key Actions and Outputs

• Workshop on guarantees in practice: this workshop will bring together researchers from formal methods, security, mathematics and related disciplines to explore guarantees, assumptions and the model-reality gap. Anticipated outputs include a shared research agenda.
• Initiate interdisciplinary research and funding proposals