nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Trustworthy Isolation of DMA Enabled Devices

verfasst von : Jonas Haglund, Roberto Guanciale

Erschienen in: Information Systems Security

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.).

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel WiP: Criminal Smart Contract for Private Key Theft in End to End Encrypted Applications

Nächstes Kapitel Toward Implementing Spatio-Temporal RBAC Extensions

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_19CrossRef

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_5CrossRef

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_18CrossRef

Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In OSDI, pp. 653–669. USENIX (2016)

10.

Klein, G., et al.: seL4: formal verification of an OS kernel. In: Operating Systems Principles, pp. 207–220. ACM (2009)

11.

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_51CrossRef

12.

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_48CrossRefMATH

13.

Ryzhyk, L., Chubb, P., Kuz, I., Le Sueur, E., Heiser, G.: Automatic device driver synthesis with termite. In: SIGOPS, pp. 73–86. ACM (2009)

14.

Ryzhyk, L., et al.: User-guided device driver synthesis. In: OSDI, pp. 661–676. USENIX (2014)

15.

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_18CrossRef

16.

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_6CrossRef

17.

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)

18.

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)

19.

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_26CrossRef

20.

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)

Titel: Trustworthy Isolation of DMA Enabled Devices
verfasst von: Jonas Haglund
Roberto Guanciale
Verlag: Springer International Publishing
Buch: Information Systems Security
Print ISBN: 978-3-030-36944-6

Electronic ISBN: 978-3-030-36945-3

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-36945-3_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner