Abstract

Advancements in virtualization technologies and frameworks have profoundly transformed the deployment and management of networks and applications. Network Functions Virtualization (NFV), for instance, has revolutionized the networking landscape by decoupling Network Functions (NFs) from dedicated hardware, offering enhanced flexibility, scalability, and cost-efficiency. In parallel, the microservice architecture has transformed cloud application development by structuring it as a collection of small, loosely coupled services. This design enables independent development, deployment, and scaling of individual functionalities, promoting agility and resilience in modern cloud environments. However, despite their benefits, NFV and microservices introduce novel security and privacy challenges. For instance, attackers could exploit inconsistencies across different system layers to bypass security mechanisms, resulting in cloud-level breaches that remain
undetected by NFV tenants. Similarly, the distributed nature of microservice architectures expands the attack surface and complicates the management of data privacy across multiple independent services. To facilitate their adoption, robust security auditing solutions are crucial for ensuring compliance and detecting potential breaches. However, existing security auditing solutions face significant challenges. They often fall short in verifying NFV
security because they focus on individual levels, which can lead to overlooking cross-level inconsistencies or vulnerabilities. As a result, potential breaches may go undetected, since issues at one level might not be visible or addressed by audits focused solely on other levels. Moreover, verifying each level separately would be both expensive and impractical. Additionally, the complexity and scale of these virtual environments can render verification solutions, such as formal security checks, prohibitively expensive. This could lead to delays in detecting misconfigurations, creating a significant window of vulnerability where services or infrastructure remain exposed to potential attacks. Moreover, the distributed nature of microservices, combined with privacy concerns, makes it difficult to centralize data for security verification using existing solutions. This thesis presents novel solutions for security verification in virtualized environments, addressing the aforementioned challenges. Firstly, it introduces NFVGuard+, a cross-level security verification approach that efficiently ensures security throughout the NFV stack by conducting resource-intensive verification at one level and then propagating the results to other levels using relatively lightweight consistency checks. Furthermore, its practicality is ensured by automating key verification processes by leveraging a novel Entity-Relationship (ER) model of the NFV stack. Secondly, it presents MLFM, an approach that combines the efficiency of Machine Learning (ML) with the rigor of Formal Methods (FM) to enable fast and provable detection of security violations in large NFV environments. The core idea is an iterative teacher-learner interaction, where FM (the teacher) progressively refines verification results to generate representative training data, while ML (the learner) utilizes this data to build increasingly accurate models. This interaction allows a relatively small subset of configuration data to train an effective ML model, which can then be used to prioritize verification efforts on configurations most likely to contain security violations. Finally, it introduces FLFM, a Federated Learning (FL)-guided Formal Method (FM) approach for the security verification of microservice-based cloud applications. FLFM enables scalable and decentralized verification while preserving privacy by eliminating the need for applications to share their sensitive local data.