Jakob Nordström: Verifying a fault-tolerant distributed aggregation protocol with the Coq proof assistant

Lunch is served at 12:00 noon (register at doodle.com/bkgrqqq7xq4i6vuk ). The presentation starts at *12:10* *pm* (note the time) and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

Abstract

Decentralized aggregation of data from network nodes is an important way of determining system-wide properties in distributed systems, e.g. in sensor networks. A scalable way of performing such aggregation is by maintaining a network overlay in the form of a tree, with data flowing from the leaves towards the root.

We describe a variant of the tree-based Generic Aggregation Protocol which is well suited to secure aggregation, and argue formally that the protocol has the expected behaviour for networks of arbitrary size, even in the presence of crash failures.

Practical verification techniques for communication protocols such as model checking usually require models with bounded state space. To reason about the protocol without such undue abstraction, we encode it as a transition system in the inductive logical framework of the Coq proof assistant and perform machine-assisted proofs.

Using Coq for verification requires knowledge of many techniques and theories unrelated to the problem domain, and we give an overview of the libraries, tools, and trade-offs involved.