Elastispec: Formalizing Enterprise Firewall Management with Informal and Elastic Specifications

Managing enterprise network firewalls is an ad-hoc process today, where administrators must extract policies relevant to their enterprises from thousands of natural language vendor documents and tailor them to their unique context. In this paper, we present Elastispec, a first step towards principled management of enterprise firewall policies with informal and incomplete specifications. We make three contributions: (i) LLM-assisted formalization of vendor documents into a custom domain specific language that precisely captures the rich choices and options using a multi-step consistency-preserving LLM agent; (ii) mapping the DSL to a concrete network environment by correlating diverse and possibly imperfect enterprise data sources; and (iii) an interactive auditor that cross-checks firewall configurations against the formal but potentially partial specifications and reports potential compliance gaps along with conjectures for human validation. Evaluations with real-world enterprise firewall configurations and popular enterprise application vendor documents show that Elastispec is effective in enabling operators to audit their configurations against vendor documents by producing compliance trees, enabling comparative analysis across parallel application deployments, and detecting configuration errors that permit non-compliant traffic.