PI: Alexandra Silva, University College London, Co-I: Matteo Sammartino, Royal Holloway, University of London

  • Modern technology relies on complex and safety-critical networking systems.
  • Automated verification techniques can detect unintended network behaviour and security vulnerabilities.
  • Our approach incrementally learns a state-based model from a network by observing its behaviour.
  • Long-term objectives include achieving scalability of learning and verification of network programs

As complex networking systems, such as Software Defined Networks, Cloud Computing and the Internet of Things, become more and more popular, automated verification tools capable of assessing the security and reliability of such systems are in high demand.

Classical approaches to verification tasks require the existence of a model of the system of interest, able to express all its relevant behaviour. Unfortunately, in reality such a model rarely exists, as networking systems may be extremely heterogeneous and parts may lack a formal specification, or the manual construction of a model is simply unfeasible.

Our approach aims to address this issue by automatically inferring a model of a network in a black-box fashion, by observing its behaviour. The goal is to provide a modular framework for learning and verifying networking systems, based on the NetKat language, which provides a compositional programming abstraction of networking behaviour. The envisioned framework is shown in the diagram: the learner interacts with the system via queries, aiming to gather observations (membership query) and to check the correctness of the model (equivalence query); the oracle includes a verification component, which compares the current model against NetKat policies, allowing one to check for specific properties incrementally, as the model is being learnt.

The main objectives for this project are taming the complexity of networks and achieving scalability of learning and verification. One of the key challenges is the fact that NetKAT models are non-deterministic, hence they lack canonical representatives; this hinders convergence of learning.  To tackle this issue, we have investigated a general framework that allows deriving canonical representatives for a wide class of non-deterministic systems.

Stefan Zetzsche, the RA who was employed on this project is now an Applied Scientist in the Automated Reasoning Group at AWS, working on the Dafny programming language.

PUBLICATIONS. [1] Gerco van Heerdt, Clemens Kupke, Jurriaan Rot and Alexandra Silva. “Learning weighted automata over principal ideal domains.” FOSSACS 2020. [2] S. Zetzsche, A. Silva, and M. Sammartino, “Bases for algebras over a monad”. [3] Stefan Zetzsche, Gerco van Heerdt, Matteo Sammartino and Alexandra Silva, “Canonical automata via distributive law homomorphisms” accepted at MFPS ’21. [4] Stefan Zetzsche, Alexandra Silva and Matteo Sammartino, “Guarded Kleene Algebra with Tests: Automata Learning”. Accepted at MFPS ’22. [5] Generators and Bases for Monadic Closure. Submitted to CALCO ’23.

RELATED GRANTS. EPSRC Standard Grant “Verification of Hardware Concurrency via Model Learning (CLeVer)” (EP/S028641/1), £693K.

IMPACT. “The completeness, fidelity, and trustworthiness of models is an important challenge for Arm. Arm is highly interested in the development of techniques that offer the potential to make the design of these models more automatic – both tools that provide a design aid for human designers, and tools that automate the modelling process altogether.” – Dominic Mulligan, Staff Research Engineer, Arm Research –