Abstract
dc:description.abstractModern 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.
Degree
thesis:*- Name thesis:degree_name
- Master of Science
- Level thesis:degree_level
- masters
- Discipline thesis:degree_discipline
- Computer Engineering
- Department dc:contributor.department
- Electrical and Computer Engineering
- Grantor dc:publisher
- Virginia Tech
- Year dc:date.issued
- 2024
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Platt, Robert Davis
- Chair dc:contributor.committeechair
-
- Ravindran, Binoy
- Committee members dc:contributor.committeemember
-
- Xiong, Wenjie
- Verbeek, Freek
Subjects
dc:subject × 5Rights
dc:rights- Statement dc:rights
-
- In Copyright
- Licence dc:rights.uri
- Language dc:language.iso
- en
Identifiers
dc:identifier.*- Dc Identifier Other
- vt_gsexam:40932
- OAI identifier oai:identifier
- oai:vtechworks.lib.vt.edu:10919/119205