Overview
Syllabus
Intro
Motivating Example: Stateful Firewall (FW)
Today: Need NF Models for Testing and Verification
Limitation of Handwritten Model: Inaccuracy
Challenges on Large Configuration Space
We Can Compose Models of Individual Rules
Use Symbolic Models to represent Large Sets
Exploit Independence to Create an Ensemble of FSMS
Challenges on Inferring NF Behavior
Background on L* for Black-box FSM Inference
Practical Challenges of Applying L* for an NF
Generating Input Alphabet to handle Large Traffic Space
Learning the State Granularity
Alembic Workflow: Offline
Evaluation Summary
Evaluation Setup
Firewall Case Study: Untangle Firewall
Limitations and Future Work
Conclusions: Alembic can accurately model stateful NFS
Taught by
USENIX