Alembic: Automated Model Inference For Stateful Network Functions

Network operators today deploy a wide range of complex, stateful network functions (NFs). Typically, they 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 often rely on models of the deployed NFs. The effectiveness of these tools depends on 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 an 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.