CS7NS5 Assignment 1

Network Security Assignment Question

Security & Privacy Considerations of Dissertation:

‘An Equivalence Checker for Pi-Calculus Models’ Basil Contovounesios <contovob@tcd.ie>

Reactive systems are often formally modelled in one of two ways: in a process calculus such as the _π-calculus, in terms of message-passing; or as a labelled transition system (LTS), in terms of a set of states and a transition model. The latter representation is amenable to automata-theoretic algorithmics, but classic formulations cannot effectively capture real-world problems over unbounded domains. This can be mitigated by expressing the LTS of a process as a fresh-register automaton (FRA).

This dissertation builds on prior work in generating the LTS of a _π-calculus model represented as an FRA. The aim of the project is to create a model checking tool that implements and evaluates the performance characteristics of several bisimulation algorithms for determining process equivalence, including novel adaptations of classic partition refinement algorithms to FRAs. The result will include a survey of the completeness of existing symbolic approaches used by other verification tools.

1 Background

Historical models of computation such as register machines and the lambda calculus (on which most programming languages are based) capture the computational but not interactional or concurrent behaviour of computing systems [1, p. 3]. The ubiquity of communication and concurrency is not merely a modern trend; they are fundemantal behaviours of all computing systems in practice. In fact, each of their computations involves and can be modelled by communication between internal or external components. Formally reasoning about real-world systems is therefore significantly facilitated by a model of computation such as a process calculus, whose basic action is message-passing in the form of concurrent synchronisation over a shared channel.

The _π-calculus in particular was designed for characterising processes with mobile structure, that is the ability to form transient or virtual links with other processes [1, p. 77]. Obvious examples of mobility include connections over wireless networks or between clients and servers on the web, which are continually created and destroyed.

While such channels are typically regarded as transmitting static data, the _π-calculus additionally arranges for the transmission of arbitrary processes as messages. This affords the expressive power to elegantly model programming language paradigms [1, p. 113] as well as general computer and, in the interest of this assignment, security protocols [2], as will be described further on.

2 Motivation

Designing, implementing, and testing concurrent systems in general, and security protocols in particular, is notoriously difficult and error-prone. New bugs such as race conditions and vulnerabilities to attack are constantly being discovered, to say nothing of those that remain undetected. One approach for reducing these risks is to formally verify the systems, which entails modelling them in a formal language like the _π-calculus [2, p. 2]. It is then possible to reason about all possible behaviours of each system either algebraically, or through generating and analysing its entire state space as an LTS [3, p. 1].

On a theoretical level, models of computation like the _π-calculus describe both the implementation and behavioural specification of processes, meaning a single language can be used for both implementation and formal verification [4, p. 100]. This can mitigate at least to some extent the well-known risk of introducing bugs in the implementation of an otherwise correct specification. As such, it is of fundamental importance and interest to define when different processes are behaviourally equivalent, or even approximately so.

A particularly fine-grained, robust, and well-established notion of equivalence is that of bisimilarity, in which two potentially nondeterministic processes symmetrically simulate each other’s inputs and outputs [5]. It can be used to verify whether two processes behave as expected, describe similar behaviour at perhaps different levels of abstraction, or violate certain specified properties, regardless of context or environment [6, pp. xv, 73]. This final point affords greater compositional reasoning, i.e. the ability to infer global properties of an entire system while verifying its components in isolation [7, p. 81]. By contrast, classic model checkers like SPIN do not verify all interactions with the environment, and thus do not compose efficiently in real-world scenarios [3, p. 2].

3 Application

Although the _π-calculus operates at too low a level to be of practical use in realworld verification of, say, security protocols, it forms a simple yet expressive basis for application-specific abstractions at a higher level [1, p. 153]. An example of this is the ‘applied’ _π-calculus, which extends the original with cryptographic primitives and is used with the ProVerif symbolic protocol verifier [2].

Most verification tools use a symbolic model of protocols like that described so far. The alternative is the computational model used in cryptography, in which messages are bitstrings rather than terms in a process algebra. While the latter is more realistic, it is less amenable to automated proofs [8, p. 100]. Furthermore, an attack on a protocol found in the symbolic model translates readily into a practical attack in the computational model, but the opposite is not always true [2, p. 3].

At its core, the protocol verification works by generating the set of messages an adversary may know, and equating message secrecy to not being present in that set. The verifier can also attempt to prove certain security properties such as secrecy or authentication, by checking that they hold for all traces of a protocol. For example, partial knowledge of a message or the unreachability of a particular state can be modelled in this way. With partial knowledge, however, an adversary can still detect changes in a secret. This leads to the requirement for a stronger notion of secrecy in which processes are indistinguishable to an adversary, which constitutes a behavioural equivalence rather than a trace property [2, pp. 4–6].

4 Limitations and Conclusion

The equivalence properties in ProVerif can be proven for applied _π-calculus terms with different message structure, but only if two processes are otherwise the same. Thus the tool cannot always decide the equivalence of arbitrary processes. This is just one of several tradeoffs faced by verification tools. For example, full model verification tends to be more costly than property verification [9, p. 173]. Similarly, supporting unbounded attack domains or concurrent protocol sessions comes at the cost of completeness or greater automation (otherwise requiring manual proof input from the user).

As suggested previously, model checking is inherently limited in its ability to catch bugs in the implementation of a model, and this is true for both symbolic and computational models. A particular challenge is presented by side channel attacks which cannot be modelled effectively, such as those targeting power consumption. Nevertheless, tooling is becoming increasingly sophisticated. There has been work on automated model extraction and code generation to and from _π-calculus models [8], as well as on simultaneously proving the cryptographic security and program correctness of the OpenSSL HMAC implementation [10].

Ultimately, formal verification is but one of many tools for mitigating risk, and is best used systematically in conjunction with others. My personal interests lie in the pursuit of its applicability to programming language and compiler theory, for creating safer and more expressive languages.

References

Robin Milner. Communicating and Mobile Systems: the _π-Calculus. Cambridge University Press, 1999.
Bruno Blanchet. ‘Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif’. In: Foundations and Trends^®in Privacy and Security 1–2 (Oct. 2016), pp. 1–135. doi: 10.1561/3300000004.
Seng Leung. ‘Modelling Concurrent Systems. Generation of Labelled Transition Systems of Pi-Calculus Models through the Use of Fresh-Register Automata’. MA thesis. Trinity College, University of Dublin, Apr. 2020.
Luca Aceto, Anna Ingolfsdottir and Jiří Srba. ‘The Algorithmics of Bisimilarity’. In: Advanced Topics in Bisimulation and Coinduction. Ed. by Davide Sangiorgi and Jan Rutten. Cambridge University Press, 2011. Chap. 3, pp. 100–172. doi: 1017/CBO9780511792588.004.
Damien Pous and Davide Sangiorgi. ‘Bisimulation and coinduction enhancements: a historical perspective’. In: Formal Aspects of Computing 6 (2019), pp. 733– 749.
Robin Milner. The Space and Motion of Communicating Agents. Cambridge University Press, 2009.
Sergey Berezin, Sérgio Campos and Edmund M. Clarke. ‘Compositional Reasoning in Model Checking’. In: Compositionality: The Significant Difference. Ed. by Willem-Paul de Roever, Hans Langmaack and Amir Pnueli. Springer, 1998, pp. 81– 102. doi: 1007/3-540-49213-5.
Matteo Avalle, Alfredo Pironti and Riccardo Sisto. ‘Formal verification of security protocol implementations: a survey’. In: Formal Aspects of Computing 1 (2014), pp. 99–123. doi: 10.1007/s00165-012-0269-9.
Michael Huth and Mark Ryan. Logic in Computer Science. Modelling and Reasoning about Systems. 2nd ed. Cambridge University Press, 2004.
Lennart Beringer et al. ‘Verified Correctness and Security of OpenSSL HMAC’. In: USENIX Security. Proceedings of the 24th USENIX Security Symposium. Aug. 2015, pp. 207–221.