An Automated Network Security Workflow based on OpenC2 and VEREFOO

This thesis describes the design, implementation and validation of a connector that act as an automated bridge between the OpenC2 Context Discovery (CTXD) specification and the VEREFOO formal verification framework. The main objective is to create a closed-loop system for proactive security policy management in modern, dynamic network environments. This thesis project addresses a fundamental challenge: bridging the structural gap between network context information, which is often non-standardized and the rigorous, structured input format required by formal verification tools. The connector is specifically built to manage real-time network topological data, provided in OpenC2 CTXD JSON format, and translate it into a comprehensive network graph model that is compliant with VEREFOO's NFV XML schema. The implementation of the connector is detailed in a Python script that operate a multi-stage workflow. First, it performs data extraction and aggregation, parsing multiple JSON files to collect a holistic view of network services, links, and configurations. It then executes the data model mapping, which includes prioritizing IPv4 addresses for unique node identification, using heuristics to automatically deduce the functional role of each network element (e.g., FORWARDER, WEBSERVER), and ensuring graph coherence by creating nodes for implicit network elements and enforcing bidirectional link relationships. Once the VEREFOO-compliant XML is generated, the connector automates its submission to the VEREFOO RESTful API. It is designed to handle both synchronous and asynchronous responses, employing a robust polling mechanism to retrieve the final verification results. The most critical function of the connector is the output analysis, where it parses the VEREFOO response, identifies policy violations flagged by an isSat="false" status, and translates them into precise, actionable OpenC2 commands. For example, a violated ReachabilityProperty triggers an allow command, while a violated IsolationProperty generates a deny command. In summary, this thesis presents a solution that fills the critical gap between network discovery and security policy enforcement. It moves beyond traditional manual and reactive security measures by demonstrating an automated, continuous process where network context is dynamically discovered, the security provided by formally verification, and corrective actions are automatically generated. This approach significantly enhances network security by minimizing human error and providing a verifiable foundation for security policy compliance.