Alembic: Automated Model Inference for Stateful Network Functions

on YouTube ↗27m

" summary

Alembic automatically synthesizes per-rule symbolic FSMs (using an L–style learner) and composes them into an offline symbolic FSM learning database and a fast online ensemble instantiation* for a concrete config. Evaluation reports 100% match under targeted IPERS testing, 99.8% under random packets, and ~95% on rule-activation tests; a 1,000-rule config answers in ~5 seconds. Findings include vendor-specific behavior (unexpected handshake checks), very large real FSMs (tens to hundreds of states), and varied handling of out-of-window packets.

AI-written summary · about

" chapters (20)

1. 0:00Intro
2. 0:31Motivating Example: Stateful Firewall (FW)
3. 2:07Today: Need NF Models for Testing and Verification
4. 2:35Limitation of Handwritten Model: Inaccuracy
5. 5:21Challenges on Large Configuration Space
6. 5:53We Can Compose Models of Individual Rules
7. 6:52Use Symbolic Models to represent Large Sets
8. 7:36Exploit Independence to Create an Ensemble of FSMS
9. 8:52Challenges on Inferring NF Behavior
10. 10:08Background on L* for Black-box FSM Inference
11. 11:04Practical Challenges of Applying L* for an NF
12. 11:29Generating Input Alphabet to handle Large Traffic Space
13. 13:58Learning the State Granularity
14. 14:59Alembic Workflow: Offline
15. 16:15Evaluation Summary
16. 16:37Evaluation Setup
17. 18:59Firewall Case Study: Untangle Firewall
18. 20:13Scalability of Alembic Online
19. 20:23Limitations and Future Work
20. 21:10Conclusions: Alembic can accurately model stateful NFS

" related talks

• 18mLiveness Verification of Stateful Network FunctionsAditya Akella, Soudeh Ghorbani, Anubhavnidhi Abhashkumar, Farnaz Yousefi, Kausik Subramanian, Kartik Hans · NSDI 2020
• 20mNetSMC: A Custom Symbolic Model Checker for Stateful Network VerificationLimin Jia, Vyas Sekar, Yifei Yuan, Soo-Jin Moon, Sahil Uppal · NSDI 2020
• 18mAPKeep: Realtime Verification for Real NetworksXu Liu, Peng Zhang, Hao Li, Hongkun Yang, Ning Kang, Zhengchang Gu · NSDI 2020
• 16mSequence Abstractions for Flexible, Line-Rate Network MonitoringDavid Walker, Ryan Beckett, Ratul Mahajan, Xiaoqi Chen, Andrew Johnson · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)
• 18mActive Learning of Symbolic NetKAT AutomataNate Foster, Alexandra Silva, Tiago Ferreira, Mark Moeller, Thomas Lu · PLDI 2025
• 27mNetComplete: Practical Network-Wide Configuration Synthesis with AutocompletionAhmed El-Hassany · NSDI '18
• 39mIn situ model-based learning in PAMELATom Marble, Paul Robertson · Clojure/conj 2016
• 29mSynthesis of dependable and self-driving communication networksStefan Schmid · FRIDA 2025