Formally Verified Isolation of DMA

被引：0
作者：
Haglund, Jonas [1 ]
Guanciale, Roberto [1 ]
机构：
[1] KTH Royal Inst Technol, Dept TCS, Stockholm, Sweden
来源：
2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD | 2022年 / 3卷
关键词：
formal verification; interactive theorem proving; DMA; I/O security; memory isolation; VERIFICATION; MODEL;
D O I：
10.34727/2022/isbn.978-3-85448-053-2_18
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Every computer having a network, USB or disk controller has a Direct Memory Access Controller (DMAC) which is configured by a driver to transfer data between the device and main memory. The DMAC, if wrongly configured, can therefore potentially leak sensitive data and overwrite critical memory to overtake the system. Since DMAC drivers tend to be buggy (due to their complexity), these attacks are a serious threat. This paper presents a general formal framework for modeling DMACs and verifying under which conditions they are isolated. These conditions can be used as a specification for guaranteeing that a driver configures the DMAC correctly. The framework provides general isolation theorems that are common to all DMACs, leaving to the user only the task of verifying proof obligations that are DMAC specific. This provides a reusable verification infrastructure that reduces the verification effort of DMACs. Models and proofs have been developed in the HOL4 interactive theorem prover. To demonstrate the usefulness of the framework, we instantiate it with a DMAC of a USB.
引用
收藏
页码：118 / 128
页数：11
相关论文
共 56 条
[11]  
Ben-Yehuda M., 2007, Proc. Linux Symp, V1, P9
[12]  
Clarke E.M., 1987, Technical Report CMU-CS-87-145
[13]  
Dam Mads, 2013, P 2013 ACM SIGSAC C, P223
[14]   Dark Side of the Shader: Mobile GPU-Aided Malware Delivery [J].
Danisevskis, Janis ;
Piekarska, Marta ;
Seifert, Jean-Pierre .
INFORMATION SECURITY AND CRYPTOLOGY - ICISC 2013, 2014, 8565 :483-495
[15]  
de Roever W.-P., 2012, Concurrency Verification: Introduction to Compositional and Non-Compositional Methods
[16]  
Dittia ZD, 1997, IEEE INFOCOM SER, P823, DOI 10.1109/INFCOM.1997.644547
[17]   Automatic analysis of DMA races using model checking and k-induction [J].
Donaldson, Alastair F. ;
Kroening, Daniel ;
Rummer, Philipp .
FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (01) :83-113
[18]  
Dong N., 2021, Formal Methods in Computer Aided Design
[19]  
Duan J., 2013, Ph.D. dissertation
[20]  
Duflot L, 2011, LECT NOTES COMPUT SC, V6961, P378, DOI 10.1007/978-3-642-23644-0_20
123456