Formal Methods for Security

This Knowledge Area surveys the most relevant topics in formal methods for security. As a discipline, formal methods address foundations, methods and tools, based on mathematics and logic, for rigorously developing and reasoning about computer systems, whether they be software, hardware, or a combination of the two. The application of formal methods to security has emerged over recent decades as a well-established research area focused on the specification and proof of security properties of systems, their components, and protocols. This requires a precise specification of:

• the system at an appropriate level of abstraction, such as design or code,
• the adversarial environment that the system operates in, and
• the properties, including the security properties, that the system should satisfy.

Formal reasoning allows us to prove that a system satisfies the specified properties in an adversarial environment or, alternatively, to identify vulnerabilities in the context of a welldefined class of adversaries.

Formal methods have a wide scope of applicability. Hence this Knowledge Area is relevant to many other KAs as it encompasses general approaches to modelling, analysis, and verification that relate to many technical aspects of cybersecurity. Moreover, as formal methods for security have applications across the entire system stack, this KA leverages background knowledge of hardware and software security from other chapters. As specific prerequisites, this KA benefits from background knowledge of logic, discrete mathematics, theorem proving, formal languages, and programming semantics, at a Computer Science undergraduate level, and provides references covering these topics; some relevant text books include [1, 2, 3]. Modelling and abstraction are cornerstones of formal methods. This KA covers their application across security topics, including access control, secure information flow, security protocols, and program correctness. These can be considered with respect to requirements such as authentication, confidentiality, anonymity, and integrity, and in the context of specific attacker models that capture different classes of attacker capabilities, giving rise to threats to the system.

We cover a variety of approaches to formal analysis and verification, including those founded on semantics, games, simulation, equivalence, and refinement. This includes both logic-based approaches (where requirements are expressed as logical statements) and behavioural approaches (given by models of secure behaviour). Our emphasis is on state-of-the-art practical applications of formal methods, enabled by tool support. Hence, the KA covers representative examples of mature tools for these approaches as applied in practice, including generalpurpose theorem provers such as Isabelle/HOL and Coq, satisfiability solvers such as Z3, model checkers such as SPIN, FDR, and PRISM, and more specialised security-specific verification tools such as Tamarin, ProVerif, CryptoVerif, and EasyCrypt. We also cover representative examples of tool support for program development and code analysis.

Finally, we provide real-world examples where formal methods have been effective in verifying the security of systems and their components or where analysis has been instrumental in identifying vulnerabilities.

Structure.      We have structured this KA along three dimensions: foundations and methods for modelling systems, types of systems, and level of abstraction. After motivating the use of formal methods for security, we survey the different foundations and methods, along with associated tools. We subsequently consider their application to different kinds of systems, as well as differentiating between levels of abstraction, such as programs versus designs. In particular, we explore hardware, protocols, software and large-scale systems, and system configuration. These categories overlap, of course (e.g., systems are built from hardware and software) and a formal method may be used across multiple categories (e.g., methods for the analysis of side-channels or secure information flow are used for both hardware and software). Nevertheless, these categories serve as a convenient structure to introduce the different approaches, and to highlight their scope and reach with respect to different formal analysis problems.