Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation

Developing and certifying in Coq/MathComp of Datalog optimizations for network verification

Abstract : Over the last decades, the world has gone more and more digital. This trend was not refuted in 2020 or 2021, as professional and personal services are increasingly provided and accessed through computers, tablets and mobile devices. This intense digital shift means that network failures are more costly and prejudicial than ever, let alone critical in many instances. We emphasize that the failures we mention and are interested in do not result from external attacks – which do occur on a weekly, if not daily basis and in industrial proportions –, but are to be seen as bugs.These bugs stem, first and foremost, from the extremely high complexity of network design, which in turn comes from the intrinsically distributed nature of networks. Moreover, networking has run for a long time on a duct tape culture, in the sense that it lacked formal foundations, and the possibilities that the existence and study of such foundations unlock.Over the last ten to fifteen years, researchers with a background in programming language theory have started to take an interest in networking, and how they could apply their theoretical tools and approaches to this field. Combined with the critically increased need for safety (and security), this situation led to the introduction of formal methods for networks. This trend is also fostered by the latest advances in formal methods, both in terms of modeling techniques and computational efficiency (e.g. the existence of fast solvers such as Z3).One such tool that was introduced is Network Optimized Datalog (NoD), a Datalog engine developed at Microsoft and tailored to handle programs that describe, in the form of horn clauses, the behavior of a particular network. Although an interesting step in the desired direction, using this engine requires engineers to manually write encodings of each analyzed network, which in itself is a complex and error-prone process.Moreover, NoD does not scale with naive translations of real-size networks. In practice, the authors work with programs that contain many inlined values, using manual, convoluted, undocumented and unjustified Datalog-level program transformations. This gap in an otherwise remarkable tool led us to work on the design and automatization of such program transformations, this time with a full formalization.However, having a formalization of non-trivial operations is not enough to trust them. The aim of our work has then been the formal verification of these transformations in the Coq proof assistant, using (and slightly extending) an existing Coq implementation of Datalog.Although inspired by network verification, our work is not circumscribed to it. Concretely, the analyses and rewritings we provide can be used – and relevant – in other contexts. Moreover, we believe that this works brings a new insight into the semantics and formal study of Datalog programs, which may serve as the basis of future works in other contexts.
Document type :
Complete list of metadata
Contributor : ABES STAR :  Contact
Submitted on : Friday, April 15, 2022 - 3:31:09 PM
Last modification on : Saturday, April 16, 2022 - 3:43:30 AM


Version validated by the jury (STAR)


  • HAL Id : tel-03643235, version 1



Pierre-Léo Bégay. Developing and certifying in Coq/MathComp of Datalog optimizations for network verification. Other [cs.OH]. Université Grenoble Alpes [2020-..], 2021. English. ⟨NNT : 2021GRALM052⟩. ⟨tel-03643235⟩



Record views


Files downloads