PhD Oral Exam - Alaa Oqaily, Information and Systems Engineering

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

Abstract

In recent years, the adoption of virtualized services has significantly changed how networks and applications are deployed. For example, Network Functions Virtualization (NFV) has revolutionized networking by decoupling Network Functions (NFs) from dedicated hardware, providing greater flexibility and scalability. Similarly, microservice architecture has transformed cloud application development by structuring it as a collection of small, loosely coupled services, enabling independent development, deployment, and scaling of various functionalities. However, despite their benefits, virtualized services, including NFV and microservices, introduce novel security and privacy challenges. For instance, attackers could exploit inconsistencies between different levels to bypass security mechanisms, leading to cloud-level security breaches that go undetected by NFV-level tenants. Similarly, microservice architectures face unique risks such as increased attack surfaces due to their distributed nature and managing the privacy of data across multiple microservices. To facilitate the adoption of virtual services, robust security auditing solutions are crucial for ensuring compliance and detecting potential breaches. Existing security auditing solutions face significant challenges. These approaches often fall short in verifying NFV security, as they tend to focus on individual levels, which can lead to overlooking inconsistencies or vulnerabilities that may exist between levels. This could leave potential breaches undetected, as 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 structure of microservices, along with privacy concerns, makes it challenging to centralize data for security verification in existing solutions. This thesis presents novel solutions for security verification in virtualized environments, addressing these limitations. Firstly, NFVGuard+ introduces a novel cross-level security verification approach that enhances efficiency by conducting resource-intensive verification at one level and then extending the results to other levels using relatively lightweight consistency checks. Furthermore, its practicality is ensured by automating key processes, such as identifying security properties, collecting verification data, and conducting verification, using a novel Entity-Relationship (ER) model of the NFV stack. Secondly, MLFM combines the efficiency of Machine Learning (ML) with the rigor of Formal Methods (FM) to enable fast and provable detection of security violations in NFV. The core idea is an iterative teacher-learner framework, 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, FLFM aims to tackle the security verification challenges in microservices arising from their distributed nature and privacy constraints. Additionally, it introduces a comprehensive framework designed to accommodate both horizontal and vertical FL scenarios, providing a scalable and robust approach to security verification.