{"id":{"repo_id":"vt","oai_identifier":"oai:vtechworks.lib.vt.edu:10919/119216"},"canonical_url":"https://search.dev.ndltd.org/etd/vt/oai:vtechworks.lib.vt.edu:10919/119216","repository":{"repo_id":"vt","name":"Virginia Tech","base_url":"https://vtechworks.lib.vt.edu/oai/request"},"display":{"title":"Modeling and Synthesis of Linux DMA Device Drivers using HOL4","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Gawali, Aditya Rajendra"],"institution":"Virginia Tech","degree_name":"Master of Science","degree_level":"masters","degree_discipline":"Computer Engineering","degree_department":"Electrical and Computer Engineering","school":null,"contributors":[],"advisors":[],"committee_chairs":["Ravindran, Binoy"],"committee_members":["Zeng, Haibo","Verbeek, Freek"],"year":2024,"date_issued":"2024-05-31","date_published":"2024-05-31","updated_at":"2026-07-22T22:19:01Z","subjects":["Linux Device Drivers","State Machines","HOL4 Modeling","Device Driver Synthesis"],"languages":["en"],"rights":["In Copyright"],"rights_urls":["http://rightsstatements.org/vocab/InC/1.0/"],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["vt_gsexam:40631"],"render_values":[{"text":"vt_gsexam:40631","href":null,"code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/10919/119216","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeechair","label":"Committee Chair","values":["Ravindran, Binoy"]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Zeng, Haibo","Verbeek, Freek"]},{"key":"dc:contributor.department","label":"Department","values":["Electrical and Computer Engineering"]},{"key":"dc:creator","label":"Author","values":["Gawali, Aditya Rajendra"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2024-06-01T08:03:02Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2024-06-01T08:03:02Z"]},{"key":"dc:date.issued","label":"Date","values":["2024-05-31"]},{"key":"dc:publisher","label":"Institution","values":["Virginia Tech"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Virginia Polytechnic Institute and State University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Linux Device Drivers","State Machines","HOL4 Modeling","Device Driver Synthesis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["In Copyright"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/vocab/InC/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["vt_gsexam:40631"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/10919/119216"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.abstractgeneral","label":"General Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Master of Science"]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["ETD"]},{"key":"dc:title","label":"Title","values":["Modeling and Synthesis of Linux DMA Device Drivers using HOL4"]}]}],"canonical_facts":{"dc:contributor.committeechair":["Ravindran, Binoy"],"dc:contributor.committeemember":["Zeng, Haibo","Verbeek, Freek"],"dc:contributor.department":["Electrical and Computer Engineering"],"dc:creator":["Gawali, Aditya Rajendra"],"dc:date.accessioned":["2024-06-01T08:03:02Z"],"dc:date.available":["2024-06-01T08:03:02Z"],"dc:date.issued":["2024-05-31"],"dc:description.abstract":["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."],"dc:description.abstractgeneral":["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."],"dc:description.degree":["Master of Science"],"dc:format.medium":["ETD"],"dc:identifier.other":["vt_gsexam:40631"],"dc:identifier.uri":["https://hdl.handle.net/10919/119216"],"dc:language.iso":["en"],"dc:publisher":["Virginia Tech"],"dc:rights":["In Copyright"],"dc:rights.uri":["http://rightsstatements.org/vocab/InC/1.0/"],"dc:subject":["Linux Device Drivers","State Machines","HOL4 Modeling","Device Driver Synthesis"],"dc:title":["Modeling and Synthesis of Linux DMA Device Drivers using HOL4"],"dc:type":["Thesis"],"thesis:degree_discipline":["Computer Engineering"],"thesis:degree_level":["masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Virginia Polytechnic Institute and State University"]},"updated_at":"2026-07-22T22:19:01Z"}