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. / Master of Science / This thesis addresses the critical issue of ensuring secure memory access in computing systems, focusing on Direct Memory Access (DMA) controllers. DMA devices can bypass the CPU to access a range of memory directly, enhancing transfer speeds but introducing security vulnerabilities like overwriting or leaking critical data if not configured correctly. This thesis proposes a method to model complex DMA driver source codes such that they can be rigorously analyzed with computer assistance. This approach is significant as it provides a structured methodology for analyzing DMA driver source code, reducing the risk of errors and vulnerabilities. The thesis also proposes a method to convert the abstract representation into executable source code, thus improving the reliability and security of DMA operations in computing systems.

Modern computer systems require efficient data transfers involving memory in order to get the best possible performance. However, even the most optimized CPUs take too long to access memory regions, which takes time away from doing the typical computations that a CPU is designed to do. To solve this, Direct Memory Access (DMA) is used, which allows peripherals and other hardware accelerators, such as stand-alone DMA Controllers (DMACs), to read and write memory without CPU intervention. However, DMA introduces security problems in which attackers are able to leak data and overwrite critical system components by bypassing typical operating system security mechanisms. This thesis presents a case study to model as well as verify DMA device driver code in HOL4, which is an interactive theorem prover (ITP) used for machine-checked verification. This thesis verifies parts of Intel's IXGBE X550 device driver, which is a complex, 10 Gbit Network Interface Card (NIC). This verification takes the first significant step towards proving that the DMA device driver configures the DMA device such that it preserves memory isolation, which ensures that only memory that is intended to be readable and writable will be accessed. This thesis also provides a formal method to verify that a loop terminates under all possible cases. This can be used to further verify the correctness of a DMA driver. These contributions allow for the overall increased security of memory when using DMA device drivers that are verified by this approach, leading to the hindrance of attacks on systems utilizing DMA. / Master of Science / Modern computer systems use Direct Memory Accesses (DMAs) in order to offload the CPU from doing memory transfers. However, this poses the problem that the CPU is not able to monitor every memory access made through DMA. This can lead to attackers utilizing vulnerabilities in the device drivers used to perform DMA operations. This thesis addresses this problem by modeling and verifying properties of a device driver that will prove that the driver configures DMA such that it is isolated. This thesis also models and verifies a loop to ensure that it terminates, further verifying the correctness of a function in a device driver. These contributions are significant because they allow for increased security of a computer system's memory, reducing the likelihood of attacks.