Aragog: Scalable Runtime Verification of Shardable Networked Systems


Nofel Yaseen, University of Pennsylvania; Behnaz Arzani and Ryan Beckett, Microsoft Research; Selim Ciraci, Microsoft; Vincent Liu, University of Pennsylvania


Network functions like firewalls, proxies, and NATs are instances of distributed systems that lie on the critical path for a substantial fraction of today's cloud applications. Unfortunately, validating these systems remains difficult due to their complex stateful, timed, and distributed behaviors.

In this paper, we present the design and implementation of Aragog, a runtime verification system for distributed network functions that achieves high expressiveness, fidelity, and scalability. Given a property of interest, Aragogefficiently checks running systems for violations of the property with a scale-out architecture consisting of a collection of global verifiers and local monitors. To improve performance and reduce communication overhead, Aragog includes an array of optimizations that leverage properties of networked systems to suppress provably unnecessary system events and to shard verification over every available local and global component. We evaluate Aragog over several network functions including a NAT Gateway that powers Azure, identifying both design and implementation bugs in the process.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {258878,
author = {Nofel Yaseen and Behnaz Arzani and Ryan Beckett and Selim Ciraci and Vincent Liu},
title = {Aragog: Scalable Runtime Verification of Shardable Networked Systems},
booktitle = {14th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 20)},
year = {2020},
isbn = {978-1-939133-19-9},
pages = {701--718},
url = {},
publisher = {{USENIX} Association},
month = nov,
Artifact Evaluated

Presentation Video