Security Verification of PCI-Based CXL Drivers in the Linux Kernel Using ESBMC

This repository contains the operational models and test scripts used for the formal verification of the CXL drivers in the Linux Kernel, specifically focusing on the cxl_map_regs and cxl_probe_regs functions. The models simulate the behavior of these functions, providing detailed assertions for memory safety, register probing, and concurrency. Using ESBMC (Efficient SMT-Based Bounded Model Checker), the code performs unbounded verification by fully unrolling loops to capture all possible iterations. The verification tests, which include handling valid and invalid inputs, concurrency scenarios, and error cases, were executed across multiple kernel configurations, identifying several potential vulnerabilities in memory handling and register initialisation. The repository includes all necessary files to replicate the verification process, along with the CXL driver source code and test results.