Description of field of research:
Bus-mastering DMA devices in modern computer systems are attached via a memory-management unit, called IOMMU or System MMU (SMMU) depending on the manufacturer. The IOMMU that can control which physical memory regions a device may access. As such, it presents an important mechanism for encapsulating untrusted devices and their drivers.
To make best use if the IOMMU, the device should only be able to access the absolute minimum portion of RAM, specifically the region(s) containing the buffer the device is to read or write. This required re-programming the IOMMU mappings for every I/O. However, this can introduce substantial overheads [Malka et al, FAST'15], leading to security-performance tradeoffs.
This project is to evaluate IOMMU performance trade-offs on recent x86 and Arm processors, and answer the following research questions:
- What does it cost to program the IOMMU or remove a mapping? Where are the costs incurred?
- What is the performance impact of the IOMMU on DMA operations?
- Does the cost of IOMMU manipulation outweigh the benefit from avoided copying that would result from keeping IOMMU mappings static?
School
Research Area
Civil Engineering
- Research Environment
- Expected Outcomes
- Our team
- References
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
1. Benchmarking setup that allows evaluating IOMMU overheads on Linux.
2. Report describing the evaluation results on multiple platforms and proposing a way forward for secure I/O encapsulation on seL4.
