MLFM: Machine Learning Meets Formal Method for Faster Identification of Security Breaches in Network Functions Virtualization (NFV)

By virtualizing proprietary physical devices, Network Functions Virtualization (NFV) enables agile and cost-effective deployment of network services on top of a cloud infrastructure. However, the added complexity also increases the chance of incorrect or inconsistent configurations that could leave the services or infrastructure vulnerable to security threats. Therefore, the timely identification of such misconfigurations is important to ensure the security compliance of NFV. In this regard, a typical solution is to leverage formal method-based security verification as they can provide either a rigorous mathematical proof that all configurations satisfy the required security properties, or the counter-examples (i.e., misconfigurations causing the properties to be breached). To that end, a major challenge is that the sheer scale of large NFV environments can render formal security verification so costly that the significant delays before misconfigurations can be identified may leave a large attack window. In this paper, we propose a novel approach, MLFM, that combines the efficiency of Machine Learning (ML) and the rigor of Formal Methods (FM) for fast and provable identification of misconfigurations violating a security property in NFV. Our key idea lies in an iterative teacher-learner interaction in which the teacher (FM) can gradually (over many iterations) provide more representative training data (verification results), while the learner (ML) can leverage such data to gradually obtain more accurate ML models. As a result, a small portion of the configuration data will be enough to obtain a relatively accurate ML model. The model is then applied to the remaining data to prioritize the verification of what is more likely to cause violations. We experimentally evaluate our solution and compare it to an existing security verification tool to demonstrate its benefits.