Alembic: Automated Model Inference for Stateful Network Functions


Soo-Jin Moon, Carnegie Mellon University; Jeffrey Helt, Princeton University; Yifei Yuan, Intentionet; Yves Bieri, ETH Zurich; Sujata Banerjee, VMware Research; Vyas Sekar, Carnegie Mellon University; Wenfei Wu, Tsinghua University; Mihalis Yannakakis, Columbia University; Ying Zhang, Facebook, Inc.


Network operators today deploy a wide range of complex stateful network functions (NFs). They typically only have access to the NFs’ binary executables, configuration interfaces, and manuals from vendors. To ensure correct behavior of NFs, operators use network testing and verification tools, which typically rely on models of the deployed NFs. The effectiveness of these tools depends upon the fidelity of such models. Today, models are handwritten, which can be error prone, tedious, and does not account for implementation-specific artifacts. To address this gap, our goal is to automatically infer behavioral models of stateful NFs for a given configuration. The problem is challenging because NF configurations can contain diverse rule types and the space of dynamic and stateful NF behaviors is large. In this work, we present Alembic, which synthesizes NF models viewed as an ensemble of finite-state machines (FSMs). Alembic consists of an offline stage that learns symbolic FSM representations for each NF rule type and a fast online stage that generates a concrete behavioral model for a given configuration using these symbolic FSMs. We demonstrate that Alembic is accurate, scalable and sheds light on subtle differences across NF implementations.

@inproceedings {227647,
title = {Alembic: Automated Model Inference for Stateful Network Functions},
booktitle = {16th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 19)},
year = {2019},
address = {Boston, MA},
url = {},
publisher = {{USENIX} Association},