VTechWorks staff will be away for the winter holidays starting Tuesday, December 24, 2024, through Wednesday, January 1, 2025, and will not be replying to requests during this time. Thank you for your patience, and happy holidays!
 

Modeling and Synthesis of Linux DMA Device Drivers using HOL4

Simple item page
dc.contributor.authorGawali, Aditya Rajendraen
dc.contributor.committeechairRavindran, Binoyen
dc.contributor.committeememberZeng, Haiboen
dc.contributor.committeememberVerbeek, Freeken
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2024-06-01T08:03:02Zen
dc.date.available2024-06-01T08:03:02Zen
dc.date.issued2024-05-31en
dc.description.abstractEfficient 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.en
dc.description.abstractgeneralThis 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.en
dc.description.degreeMaster of Scienceen
dc.format.mediumETDen
dc.identifier.othervt_gsexam:40631en
dc.identifier.urihttps://hdl.handle.net/10919/119216en
dc.language.isoenen
dc.publisherVirginia Techen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectLinux Device Driversen
dc.subjectState Machinesen
dc.subjectHOL4 Modelingen
dc.subjectDevice Driver Synthesisen
dc.titleModeling and Synthesis of Linux DMA Device Drivers using HOL4en
dc.typeThesisen
thesis.degree.disciplineComputer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.levelmastersen
thesis.degree.nameMaster of Scienceen

Files

Original bundle
Now showing 1 - 1 of 1
Name:
Gawali_A_T_2024.pdf
Size:
863.07 KB
Format:
Adobe Portable Document Format
Download

Collections

Masters Theses