Skip to main content
Top

2022 | Book

Formal Analysis by Abstract Interpretation

Case Studies in Modern Protocols

insite
SEARCH

About this book

The book provides a gentle introduction and definition of the denotational-based abstract interpretation method. The book demonstrates how the above method of formal analysis can be used, not only to address the security of systems, but other more general and interesting properties related to the testing, mutating and semantic ambiguity resolution of protocols. The book presents three case studies, all related to current complex protocols and standards used in industry, particularly in the context of IoT and Industry 4.0.

Table of Contents

Frontmatter
Chapter 1. Introduction
Abstract
We introduce in this chapter some of the areas in computer science on which the book is based. We provide some background and discussion of the literature in areas such as the specific class of formal languages used for describing systems with the mobility of structures, known as calculi for mobility, a specific approach for defining the meaning of such languages, known as denotational semantics and finally, we give some background on the method of static program analysis, and particularly, abstract interpretation-based analysis. We also give an overview of the literature related to the three modern protocols used as our case studies.
Benjamin Aziz
Chapter 2. Process Algebra: Syntax and Semantics
Abstract
This chapter presents the syntax and semantics of our process algebraic formal language. The syntax describes the constructs comprising a process, while the semantics defines its meaning. This meaning is given in two ways. The first is structural operational, describing how a process may change its shape (structure) and how it may evolve based on the laws of communication. The second is a non-standard semantics designed to capture a specific meaning: name substitutions that occur as a result of processes communicating with one another. As we find out in later chapters, this meaning is fundamental as it underlines the definition of many useful safety and security properties in modern-day protocols.
Benjamin Aziz
Chapter 3. Formal Analysis by Abstract Interpretation
Abstract
This chapter presents a method for approximating the non-standard semantics capturing message-passing properties defined in Chap. 2. The approximation is based on limiting the number of distinguishable copies a process can produce of new names and input parameters. This then leads to the generation of a finite semantic domain and an abstract interpretation function that is used to give an abstract semantics for a process. The chapter concludes with two examples of simple systems that demonstrate how the analysis can be applied to better understand the behaviour of systems: the example of a simple file transfer protocol system and the example of a simple distance-bounding protocol.
Benjamin Aziz
Chapter 4. First Case Study: The MQTT Protocol
Abstract
This chapter present a formal model of the MQ Telemetry Transport protocol based on a timed message-passing process algebra, the formal language used throughout this book. We explain the modelling choices that we made, including pointing out ambiguities in the original protocol specification, and we carry out an abstract interpretation-based static analysis of the formal protocol model, which is based on an approximation of a name-substitution semantics for algebra, as defined in earlier chapters of the book. The analysis reveals that the protocol behaves correctly as specified against the first two quality of service modes of operation providing at most once and at least once delivery semantics to the subscribers. However, we find that the third and highest quality of service semantics is prone to error and at best ambiguous in certain aspects of its specification. Finally, we suggest an enhancement of this level of QoS for the protocol. This chapter represents the first case study in this book.
Benjamin Aziz
Chapter 5. Second Case Study: The Hermes Protocol
Abstract
The increasing complexity and criticality of industrial automation systems, embodied by the concept of Industry 4.0, which bring together concepts like Cyber-Physical Systems, Internet of Things, Big Data and Artificial Intelligence, call for more formality in specifying the technology standards underlying these systems. This chapter presents a formal model of an Industry 4.0 machine-2-machine communication protocol, Hermes, used in specifying electronic board transfers in an assembly line. Our analysis of the formal specification reveals that, despite the robustness of the protocol, many testing scenarios have been ignored in the protocol standard and in particular, scenarios that include simultaneous machine errors. Therefore, the analysis presented here paves the way for a better-informed testing strategy in Industry 4.0 systems that implement the protocol. This chapter represents the second case study of the current book.
Benjamin Aziz
Chapter 6. Third Case Study: An Electric Vehicle Charging Protocol
Abstract
Modern-day renewable and smart energy systems are increasingly playing an important role in our societies. Electric vehicle charging service infrastructures are becoming ever more popular and accessible, although at a pace not well understood yet in terms of the reliability and security of this new paradigm. Often, solutions are rolled out to the market with little or no analysis of their resilience and even at the standards level, specifications of systems and protocols often omit or skim over the question of reliability. This chapter will present a new formal approach for analysing the effects of single failures on process algebraic specifications used often in specifying communication protocols. This new approach is applied to one part of an international standard protocol, the Open Charge Point Protocol, for electric vehicle charging, and demonstrates how the effects of specification faults can impact the safety and security of the protocol. This chapter represents the third case study of analysing modern and complex protocols in the current book.
Benjamin Aziz
Chapter 7. Conclusion
Abstract
This chapter concludes the book.
Benjamin Aziz
Metadata
Title
Formal Analysis by Abstract Interpretation
Author
Dr. Benjamin Aziz
Copyright Year
2022
Electronic ISBN
978-3-030-91153-9
Print ISBN
978-3-030-91152-2
DOI
https://doi.org/10.1007/978-3-030-91153-9

Premium Partner