Modeling and Synthesis of Linux DMA Device Drivers using HOL4

Efficient memory access is critical for computing systems, yet the CPU's management of data transfers can create bottlenecks. To counter this, most advanced high-throughput systems utilize Direct Memory Access (DMA) controllers, where peripherals (such as network interfaces and USB devices) can access memory independently of the CPU, improving transfer speeds. However, this bypass also introduces security vulnerabilities if the DMA controller is not configured correctly, as DMA devices may be used to overwrite critical data or leak information. This thesis proposes a method to represent complex DMA driver source code as an abstract mathematical model in the formal analysis tool HOL4 (where users can define models and prove properties about them with HOL4 and checking the correctness of the proofs). This model enables the formal verification of the DMA driver source code's critical properties like memory isolation, initial configurations, and many more. Additionally, the thesis introduces a methodology to convert the verified HOL4 models into executable C source code, thus obtaining a formally verified C source code. The synthesized code is evaluated against the original driver source code by emulating the DMA operation in software and using fuzzing techniques for any compile and runtime errors. This validates the approach, demonstrating that converting a C driver source code into a HOL4 model and then back into C source code after verification yields a formally verified C source code. This thesis applies this methodology to DMA controllers for four devices namely Intel 8237a, Intel IXGBE x550 Ethernet Controller, MPC 5200 SoC, and STM32 DMAC.