Formal methods¶

Formal methods are tools based on mathematics and logic for developing and reasoning about information processing systems. They cover software, hardware, and combinations of the two. The application of formal methods to security has, over recent decades, become an established research area that focuses on the specification and proof of security properties. Their use requires a precise specification of

the system itself, using an appropriate level of abstraction, which may be an idealised design, code, or something in between,
the hostile environment in which the system operates, and
the properties—possibly other than security properties—that the system must satisfy.

Formal reasoning makes it possible to prove that a system satisfies the specified properties in a hostile environment or, alternatively, to identify vulnerabilities with respect to a well-defined class of attackers.

Formal methods can be applied widely and are important in many other technical areas of this material. Formalisms have applications across the entire system stack (from hardware to information systems). Prerequisites for studying formal methods include background knowledge of logic, discrete mathematics, automated reasoning, formal languages, and the semantics of programming languages.

Modelling and abstraction are cornerstones of formal methods. The CyBOK text provides information on their application in several areas of cybersecurity, including access control, secure information flow, cryptographic protocols, and program correctness. The text covers different approaches to formal analysis and proof, for example those based on semantics, games, simulation, equivalence, or refinement. Through these, you can become familiar with both logic-based and behaviour-based approaches. In the former, requirements are expressed using logical formulae, and in the latter using models of secure behaviour. Examples of practical tools for these approaches include general-purpose automated theorem provers such as Isabelle/HOL and Coq, satisfiability solvers such as Z3, and model checkers such as SPIN, FDR, and PRISM.

System development often follows a traditional cycle of coding, testing, and fixing. In security-critical systems, “test–fix” can in practice be “break–patch”, because errors may lead to security vulnerabilities. For example, a program that lacks bounds checking when writing to memory can be subject to a buffer overflow attack. Similarly, a system that does not check all access requests may lead to unauthorised use of resources. Even small errors can have devastating effects in practice. Some attackers are extremely skilled at finding and exploiting flaws that seem utterly insignificant. Formal methods offer the possibility to improve the system development cycle by ensuring that systems meet their requirements or are at least free of certain classes of defects.

Formal methods can be used at different stages of system development and operation, and they can be applied to different system artefacts.

System design: They can be used to specify and verify all kinds of designs—or to find errors in them. Cryptographic protocols are a good example, where formal methods have significantly improved security.
Code level: Programs contain errors that often represent security vulnerabilities. With the right tools, searching for defects is straightforward. Formal tools range from simple static analysers to full-scale interactive verification. The former can ensure “low-level” properties, such as the absence of certain types of security bugs, even in very large code bases. The latter can be used to prove deep properties, but usually only for small programs.
Configuration level: The security of systems also depends on how they are configured. For example, access control mechanisms require a specification of who is allowed to do what.

Above, the impact of formalisms on eliminating vulnerabilities has been emphasised. Conversely, formalisms can provide a strong mathematical foundation for the development of secure systems. Such application of mathematical methods to the construction of correctly functioning programs or systems (not merely to the detection of errors) was the original motivation of the early developers of formal methods. The core idea is to view programs and systems as mathematical objects, about which conclusions are drawn using mathematics and logic. Both perspectives—finding faults and constructing fault-free systems—are applicable to security but are not exclusive to it.

When the application domain is security, two extensions are required. First, the environment is hostile and a threat model must be constructed for it, where the threat is usually an active attacker. Second, some security properties differ from traditional properties of program correctness in that they cannot be inferred from individual program executions, not even by enumerating all possibilities. Executions under different inputs must be compared, and often pairwise comparison suffices, although it must cover all pairs. Such properties are called hyperproperties. Central examples in security are non-interference and the absence of side channels. For example, the absence of Spectre and Meltdown vulnerabilities from a system are hyperproperties. They were not discovered using formal methods, but after their discovery they could be formalised and it was possible to build mechanisms into tools for detecting similar problems. According to the 2021 preprint article A Survey of Practical Formal Methods for Security, it is still the case that “methods demonstrate the presence of a problem, not its absence”. The article expresses this for formal methods and security vulnerabilities by adapting Dijkstra’s famous and still valid statement from 1969, in which testing appeared instead of methods and the problem was a software bug.

Even closer to practice is the survey article Formal verification: will the seedling ever flower? (2017), which, despite its title, presents several very successful projects. It also contains experience-based advice on the selection of formal methods and tools. Finally, it is worth mentioning the theoretical but fairly accessible article Blueprint for a science of cybersecurity, which includes, among other things, an explanation of hyperproperties (the article appears in an NSA future publication from 2012).

Example: CSP in the modelling of cryptographic protocols

CSP (communicating sequential processes) is an abstract language for describing systems that operate concurrently and communicate by exchanging messages. They consist of processes that “live” through events. Processes express which events may occur and how they are ordered sequentially or in parallel. Some events synchronise different processes. It is natural to interpret these as the sending and receiving of messages, but that is not the only possibility.

A cryptographic protocol is modelled by defining the parties, the attacker, and the network (media) as processes in which the events are messages of a given form that are “sent” along channels. Of course, nothing is actually sent, and talk of channels is merely illustrative. CSP is in fact a process algebra, in which new processes can be “calculated” from existing ones, for example by putting them in parallel or in sequence, or by defining a communication channel between them.

Security goals are modelled by imposing requirements on the kinds of event sequences, or traces, that can occur in such a system. That is, all possible event sequences must satisfy certain properties. This is sufficient to model confidentiality and authenticity. If one wishes to study non-repudiation or availability, it is also necessary to require that certain kinds of event sequences are possible, that is, that certain events do indeed occur. To do this, one must take into account the kinds of failures that may occur in processes (examples include deadlock and its variant livelock).

The (trace-)semantics of a process thus consists of all possible event sequences it can perform. Requirements on traces can be checked by proving them formally or by using an automatic model checker. The most suitable for CSP is called FDR, which does not in fact check a single model, but instead compares two processes, P and Q. The comparison determines whether P is a refinement of Q, meaning that the semantics of P is included in the semantics of Q. The starting point Q is often referred to as a specification, which the implementation P refines. In trace semantics, P is a refinement of Q if every event sequence possible for P is also possible for Q—that is, nothing happens in the implementation that has not been specified.

The name FDR comes from the words Failures Divergences Refinement. A failure means a blockage as mentioned above, and a divergence means an infinite loop; in the general semantics, these must also be taken into account. FDR works by exploring all states in a given state space (“following the traces”). Consequently, it can only handle finite-state systems (up to a few million states). Therefore, the method can only be used to study systems with a bounded number of parties, in practice just a few. A protocol itself must in principle work with an unbounded set of participants. Developed at the University of Oxford in the 1990s, FDR is now a commercial product: code can also be downloaded for trial use from the FDR4 page.