Abstract
We present a mechanism to trustworthy isolate I/O devices with Direct Memory Access (DMA), which ensures that an isolated I/O device cannot access sensitive memory regions. As a demonstrating platform, we use the Network Interface Controller (NIC) of an embedded system. We develop a run-time monitor that forces NIC reconfigurations, defined by untrusted software, to satisfy a security rule. We formalized the NIC in the HOL4 interactive theorem prover and we verified the design of the isolation mechanism. The verification is based on an invariant that is proved to be preserved by all NIC operations and that ensures that all memory accesses address allowed memory regions only. We demonstrate our approach by extending an existing Virtual Machine Introspection (VMI) with the monitor. The resulting platform prevents code injection in a connected and untrusted Linux (The HOL4 proofs and the source code of the monitor are published at https://github.com/kth-step/NIC-formalization-monitor.).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
AM335x and AMIC110 Sitara™ Processors, Technical Reference Manual, Texas Instruments Rev. P. https://www.ti.com/lit/ug/spruh73p/spruh73p.pdf
Alkassar, E., Hillebrand, M., Knapp, S., Rusev, R., Tverdyshev, S.: Formal device and programming model for a serial interface. In: Proceedings of VERIFY, pp. 4–20 (2007)
Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 225–239. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87873-5_19
Cavada, R., et al.: NuSMV 2.4 user manual. CMU and ITC-IRST (2005)
Chfouka, H., Nemati, H., Guanciale, R., Dam, M., Ekdahl, P.: Trustworthy prevention of code injection in Linux on embedded devices. In: Pernul, G., Ryan, P.Y.A., Weippl, E. (eds.) ESORICS 2015. LNCS, vol. 9326, pp. 90–107. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24174-6_5
MDam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. In: CCS, pp. 223–234. ACM (2013)
Duan, J.: Formal Verification of Device Drivers in Embedded Systems. The University of Utah, Salt Lake City (2013)
Fox, A., Myreen, M.O.: A trustworthy Monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243–258. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_18
Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In OSDI, pp. 653–669. USENIX (2016)
Klein, G., et al.: seL4: formal verification of an OS kernel. In: Operating Systems Principles, pp. 207–220. ACM (2009)
Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 806–809. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_51
Nemati, H., Guanciale, R., Dam, M.: Trustworthy virtualization of the ARMv7 memory subsystem. In: Italiano, G.F., Margaria-Steffen, T., Pokorný, J., Quisquater, J.-J., Wattenhofer, R. (eds.) SOFSEM 2015. LNCS, vol. 8939, pp. 578–589. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46078-8_48
Ryzhyk, L., Chubb, P., Kuz, I., Le Sueur, E., Heiser, G.: Automatic device driver synthesis with termite. In: SIGOPS, pp. 73–86. ACM (2009)
Ryzhyk, L., et al.: User-guided device driver synthesis. In: OSDI, pp. 661–676. USENIX (2014)
Schwarz, O., Dam, M.: Formal verification of secure user mode device execution with DMA. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 236–251. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13338-6_18
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6
Sun, J., Yuan, W., Kallahalla, M., Islam, N.: HAIL: a language for easy and correct device access. In: Proceedings of the 5th ACM International Conference on Embedded Software, pp. 1–9. ACM (2005)
Vasudevan, A., Chaki, S., Jia, L., McCune, J., Newsome, J., Datta, A.: Design, implementation and verification of an extensible and modular hypervisor framework. In: SP, pp. 430–444. IEEE (2013)
Verbeek, F., et al.: Formal API specification of the PikeOS separation kernel. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 375–389. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_26
Zhou, Z., Yu, M., Gligor, V.D.: Dancing with giants: wimpy kernels for on-demand isolated I/O. In: 2014 IEEE Symposium on Security and Privacy, pp. 308–323. IEEE (2014)
Acknowledgements
Work partially supported by the TrustFull project financed by the Swedish Foundation for Strategic Research.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Haglund, J., Guanciale, R. (2019). Trustworthy Isolation of DMA Enabled Devices. In: Garg, D., Kumar, N., Shyamasundar, R. (eds) Information Systems Security. ICISS 2019. Lecture Notes in Computer Science(), vol 11952. Springer, Cham. https://doi.org/10.1007/978-3-030-36945-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-36945-3_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-36944-6
Online ISBN: 978-3-030-36945-3
eBook Packages: Computer ScienceComputer Science (R0)