Karl Palmskog: Verifying a fault-tolerant distributed aggregation protocol with the Coq proof assistant

Lunch is served at 12:00 noon (register at doodle.com/xg9awrz9dsn99dc8 no later than Nov 29). The presentation starts at 12:10 pm and ends at 1 pm. After a break, those of us who so wish reconvene for roughly two more hours of technical discussions (ending at the latest 3 pm).

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.