Formal Analysis by Abstract Interpretation: Case Studies in Modern Protocols

The book outlines how formal static analysis techniques can be defined and applied to modern protocols, related to new paradigms such as the IoT, Industry 4.0 and Smart Energy. The application of such robust techniques can lead to better understanding of modern-day protocols and systems, both within the context of classical requirements, such as functional security, and the more challenging properties related to the presence of vulnerabilities at levels of specification and design. The book challenges current mainstream thinking that large scale systems are simply infeasible and non-suitable case studies for formal analysis techniques, and goes to demonstrate that such systems can benefit from the application of such techniques.

The book gives us a static analysis framework with a focus on capturing name substitutions occurring as a result of processes communicating with one another. First, a non-standard denotational semantics for the formal language is constructed based on domain theory. The semantics is shown to be sound with respect to transitions in the standard structural operational semantics. Finally, the non-standard semantics is abstracted to operate over finite domains so as to ensure the termination of the static analysis. The safety of the abstract semantics is proven with respect to the non-standard semantics. This framework demonstrates that the choice of the name substitution property is a fundamental one, in that it can be used to understand a wide range of system and protocol properties ranging from security and safety-related ones to testing coverage to mutation-based properties. As such, the book lays down a simple but effective method for the static analysis of systems and protocols that go beyond simple toy examples into the realm of complex systems.

One of the main motivations in writing this book was to give the reader the benefit of understanding how a highly theoretical area in computer science can have applications in complex industrial settings, two universes that are often hard to combine. More specifically, it is envisaged that the reader will: first, gain knowledge and experience of the abstract interpretation method of formal analysis and how it can be varied to express various properties and applied for different purposes, for example, in testing, mutation and semantic ambiguity resolution contexts, and second, they will be challenged to think of how such method can be used in analysing modern protocols; in other words, protocols of significance complexity as opposed to the majority of current literature that applies only to toy-style protocols. The expectation is that the book will encourage readers, in particular those working in research, to think and reflect on new directions for future research benefiting from the approach discussed throughout.

The book is composed of five chapters along with the introduction (Chapter 1) and the conclusion (Chapter 7). From these five chapters, the first two (Chapters 2 and 3) define the formal language and its denotational semantics, both concrete and abstract, and hence are an essential reading in order to understand any of the three case studies presented in the following three chapters (Chapters 4-6). The case studies themselves can be read individually, in any order, and according to the needs of the reader, as they are not inter-related.

The primary audience of this book is the academic community (postgraduate and researchers), particularly at the intersection of formal methods, IoT systems, networks and program analysis areas. The book is also suitable for the industrial research community, particularly those working with the IoT and communication networks research. Finally, the book is also expected to be useful to anyone interested in the standardisation of protocols, particularly, IoT and Industry 4.0 protocol standards.

Special thanks to my PhD supervisor, Dr Geoff Hamilton, whose comments and feedback over the years were inspirational in defining the static analysis framework.