Sage Journals: Discover world-class research

Abstract

The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a memory virtualization platform for ARMv7-A processors. The design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen. It is shown that this mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the processor. We prove memory isolation along with information flow security for an abstract top-level model of the virtualization mechanism. The abstract model is refined down to a transition system closely resembling a C implementation. Additionally, it is demonstrated how the gap between the low-level abstraction and the binary level-can be filled, using tools that check Hoare contracts. The virtualization mechanism is demonstrated on real hardware via a hypervisor hosting Linux and supporting a tamper-proof run-time monitor that provably prevents code injection in the Linux guest.

Keywords

Formal verification information flow security separation kernel hypervisor

Get full access to this article

View all access options for this article.

References

Alkassar,

Cohen,

Kovalev and

W.J.

Paul, Verification of TLB virtualization implemented in C, in: Proceedings of the 4th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE’12, Springer-Verlag, Berlin, Heidelberg, 2012, pp. 209–224. doi:10.1007/978-3-642-27705-4_17.

Alkassar,

M.A.

Hillebrand,

Paul and

Petrova, Automated verification of a small hypervisor, in: Verified Software: Theories, Tools, Experiments, Springer, 2010, pp. 40–54. doi:10.1007/978-3-642-15057-9_3.

ARM Cortex-A15 MPCore Processor – Technical Reference Manual, Technical document ARM DDI 0438I, ARM Limited, 2011.

ARM Security Technology – Building a Secure System using TrustZone Technology, Technical documentation ARM PRD29-GENC-009492C, ARM Limited, 2009.

ARMv7-AR Architecture Reference Manual. Technical documentation ARM DDI 0406B, ARM Limited, 2008.

Azevedo de Amorim,

Collins,

DeHon,

Demange,

Hriţcu,

Pichardie,

B.C.

Pierce,

Pollack and

Tolmach, A verified information-flow architecture, in: Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2014, pp. 165–178. doi:10.1145/2535838.2535839.

Barham,

Dragovic,

Fraser,

Hand,

Harris,

Ho,

Neugebauer,

Pratt and

Warfield, Xen and the art of virtualization, ACM SIGOPS Operating Systems Review 37(5) (2003), 164–177. doi:10.1145/1165389.945462.

Baumann,

Bormer,

Blasum and

Tverdyshev, Proving memory separation in a microkernel by code level verification, in: Object/Component/Service-Oriented Real-Time Distributed Computing Workshops (ISORCW), 2011 14th IEEE International Symposium on, IEEE, 2011, pp. 25–32.

Brumley,

Jager,

Avgerinos and

E.J.

Schwartz, BAP: A binary analysis platform, in: Proc. CAV’11, Lecture Notes in Computer Science, Vol. 6806, Springer, 2011, pp. 463–469.

10.

Chen,

Garfinkel,

E.C.

Lewis,

Subrahmanyam,

C.A.

Waldspurger,

Boneh,

Dwoskin and

D.R.

Ports, Overshadow: A virtualization-based approach to retrofitting protection in commodity operating systems, in: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XIII, ACM, New York, NY, USA, 2008, pp. 2–13. doi:10.1145/1346281.1346284.

11.

Chfouka,

Nemati,

Guanciale,

Dam and

Ekdahl, Trustworthy prevention of code injection in Linux on embedded devices, in: Proc. ESORICS, Lecture Notes in Computer Science, Springer, 2015, to appear.

12.

Cock,

Ge,

Murray and

Heiser, The last mile: An empirical study of some timing channels on sel4, 2014.

13.

Cohen,

Paul and

Schmaltz, Theory of multi core hypervisor verification, in: SOFSEM 2013: Theory and Practice of Computer Science, Springer, 2013, pp. 1–27. doi:10.1007/978-3-642-35843-2_1.

14.

Criswell,

Dautenhahn and

Adve, Virtual ghost: Protecting applications from hostile operating systems, in: Proceedings of the 19th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS’14, ACM, New York, NY, USA, 2014, pp. 81–96. doi:10.1145/2541940.2541986.

15.

Criswell,

Dautenhahn and

Adve, KCoFI: Complete control-flow integrity for commodity operating system kernels, in: IEEE Symposium on Security and Privacy, Oakland, Vol. 14, 2014.

16.

Criswell,

Geoffray and

Adve, Memory safety for low-level software/hardware interactions, in: Proceedings of the 18th Conference on USENIX Security Symposium, SSYM’09, USENIX Association, Berkeley, CA, USA, 2009, pp. 83–100.

17.

Criswell,

Lenharth,

Dhurjati and

Adve, Secure virtual architecture: A safe execution environment for commodity operating systems, in: Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP’07, ACM, New York, NY, USA, 2007, pp. 351–366. doi:10.1145/1294261.1294295.

18.

Dam,

Guanciale,

Baumann and

Nemati, Cache storage channels: Alias-driven attacks and verified countermeasures, in: Security and Privacy (SP), 2016 IEEE Symposium on, IEEE, 2016, to appear.

19.

Dam,

Guanciale,

Khakpour,

Nemati and

Schwarz, Formal verification of information flow security for a simple ARM-based separation kernel, in: Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, ACM, 2013, pp. 223–234. doi:10.1145/2508859.2516702.

20.

Dam,

Guanciale and

Nemati, Machine code verification of a tiny ARM hypervisor, in: Proceedings of the 3rd International Workshop on Trustworthy Embedded Devices, TrustED’13, ACM, New York, NY, USA, 2013, pp. 3–12. doi:10.1145/2517300.2517302.

21.

P.B.

Daniel and

Marco, Understanding the Linux Kernel, O’Reilly Media, Inc., 2005.

22.

A.C.J.

Fox and

M.O.

Myreen, A trustworthy monadic formalization of the ARMv7 instruction set architecture, in: Proc. ITP’10, Lecture Notes in Computer Science, Vol. 6172, Springer, 2010, pp. 243–258.

23.

Ganesh and

D.L.

Dill, A decision procedure for bit-vectors and arrays, in: Proc. CAV’07, Lecture Notes in Computer Science, Vol. 4590, Springer, 2007, pp. 519–531.

24.

Gu,

Koenig,

Ramananandro,

Shao,

X.N.

Wu,

S.-C.

Weng,

Zhang and

Guo, Deep specifications and certified abstraction layers, in: ACM SIGPLAN Notices, Vol. 50, ACM, 2015, pp. 595–608.

25.

Hawblitzel,

Howell,

J.R.

Lorch,

Narayan,

Parno,

Zhang and

Zill, Ironclad apps: End-to-end security via automated full-system verification, in: 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14), USENIX Association, Broomfield, CO, 2014, pp. 165–181.

26.

Heiser and

Leslie, The OKL4 microvisor: Convergence point of microkernels and hypervisors, in: Proceedings of the First ACM Asia-Pacific Workshop on Workshop on Systems, ACM, 2010, pp. 19–24. doi:10.1145/1851276.1851282.

27.

Heitmeyer,

Archer,

Leonard and

McLean, Applying formal methods to a certifiably secure software system, IEEE Trans. Softw. Eng. 34(1) (2008), 82–98. doi:10.1109/TSE.2007.70772.

28.

O.S.

Hofmann,

Kim,

A.M.

Dunn,

M.Z.

Lee and

Witchel, Inktag: Secure applications on an untrusted operating system, in: Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS’13, ACM, New York, NY, USA, 2013, pp. 265–278. doi:10.1145/2451116.2451146.

29.

G.C.

Hunt and

J.R.

Larus, Singularity: Rethinking the software stack, ACM SIGOPS Operating Systems Review 41(2) (2007), 37–49. doi:10.1145/1243418.1243424.

30.

Iqbal,

Sadeque and

R.I.

Mutia, An overview of microkernel, hypervisor and microvisor virtualization approaches for embedded systems, Report, Department of Electrical and Information Technology, Lund University, Sweden, 2110, 2009.

31.

P.A.

Karger and

R.R.

Schell, Thirty years later: Lessons from the Multics security evaluation, in: ACSAC, IEEE Computer Society, 2002, pp. 119–126.

32.

Khakpour,

Schwarz and

Dam, Machine assisted proof of ARMv7 instruction level isolation properties, in: Certified Programs and Proofs, Springer, 2013, pp. 276–291. doi:10.1007/978-3-319-03545-1_18.

33.

Klein,

Elphinstone,

Heiser,

Andronick,

Cock,

Derrin,

Elkaduwe,

Engelhardt,

Kolanski,

Norrish,

Sewell,

Tuch and

Winwood, seL4: Formal verification of an OS kernel, in: Proc. SOSP’09, ACM, 2009, pp. 207–220. doi:10.1145/1629575.1629596.

34.

Leinenbach and

Santen, Verifying the Microsoft Hyper-V hypervisor with VCC, in: Proc. FM’09, Lecture Notes in Computer Science, Vol. 5850, Springer, Berlin/Heidelberg, 2009, pp. 806–809.

35.

Leroy, Formal verification of a realistic compiler, Communications of the ACM 52(7) (2009), 107–115. doi:10.1145/1538788.1538814.

36.

M.K.

McKusick and

G.V.

Neville-Neil, The Design and Implementation of the FreeBSD Operating System, Addison-Wesley Professional, 2004.

37.

McVoy and

Staelin, Lmbench: Portable tools for performance analysis, in: Proceedings of the 1996 Annual Conference on USENIX Annual Technical Conference, ATEC’96, Berkeley, CA, USA, 1996, USENIX Association, p. 23.

38.

Murray,

Matichuk,

Brassil,

Gammie,

Bourke,

Seefried,

Lewis,

Gao and

Klein, sel4: From general purpose to a proof of information flow enforcement, in: Security and Privacy (SP), 2013 IEEE Symposium on, IEEE, 2013, pp. 415–429. doi:10.1109/SP.2013.35.

39.

M.O.

Myreen,

M.J.C.

Gordon and

Slind, Machine-code verification for multiple architectures – An application of decompilation into logic, in: Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17–20 November 2008, 2008, pp. 1–8. doi:10.1109/FMCAD.2008.ECP.24.

40.

Nemati,

Guanciale and

Dam, Trustworthy virtualization of the ARMv7 memory subsystem, in: SOFSEM 2015: Theory and Practice of Computer Science – 41st International Conference on Current Trends in Theory and Practice of Computer Science, Pec Pod Sněžkou. Proceedings, Czech Republic, January 24–29, 2015, 2015, pp. 578–589.

41.

Paul,

Schmaltz and

Shadrin, Completing the automated verification of a small hypervisor–assembler code verification, in: Software Engineering and Formal Methods, Springer, 2012, pp. 188–202. doi:10.1007/978-3-642-33826-7_13.

42.

Richards, Modeling and security analysis of a commercial real-time operating system kernel, in: Design and Verification of Microprocessor Systems for High-Assurance Applications,

D.S.

Hardin, ed., Springer, US, 2010, pp. 301–322. doi:10.1007/978-1-4419-1539-9_10.

43.

Schwarz and

Dam, Formal verification of secure user mode device execution with DMA, in: Hardware and Software: Verification and Testing, Springer, 2014, pp. 236–251.

44.

T.A.L.

Sewell,

M.O.

Myreen and

Klein, Translation validation for a verified OS kernel, in: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, 2013, pp. 471–482. doi:10.1145/2491956.2462183.

45.

Steinberg and

Kauer, NOVA: A microhypervisor-based secure virtualization architecture, in: Proceedings of EuroSys, 2010.

46.

The BeagleBoard.org Foundation. The BeagleBoard-xM, 2010.

47.

Tinnes, Linux null pointer dereference due to incorrect proto-ops initializations, 2009 (cve-2009-2692).

48.

Varanasi and

Heiser, Hardware-supported virtualization on ARM, in: Proceedings of the Second Asia-Pacific Workshop on Systems, APSys’11, ACM, New York, NY, USA, 2011, pp. 11:1–11:5.

49.

Vasudevan,

Chaki,

Jia,

McCune,

Newsome and

Datta, Design, implementation and verification of an extensible and modular hypervisor framework, in: Proceedings of the 2013 IEEE Symposium on Security and Privacy, SP’13, IEEE Computer Society, Washington, DC, USA, 2013, pp. 430–444. doi:10.1109/SP.2013.36.

50.

Wahbe,

Lucco,

T.E.

Anderson and

S.L.

Graham, Efficient software-based fault isolation, in: ACM SIGOPS Operating Systems Review, Vol. 27, ACM, 1994, pp. 203–216.

51.

M.M.

Wilding,

D.A.

Greve,

R.J.

Richards and

D.S.

Hardin, Formal verification of partition management for the AAMP7G microprocessor, in: Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, US, 2010, pp. 175–191. doi:10.1007/978-1-4419-1539-9_6.

52.

Zhao,

Li,

De Sutter and

Regehr, ARMor: Fully verified software fault isolation, in: Embedded Software (EMSOFT), 2011 Proceedings of the International Conference on, IEEE, 2011, pp. 289–298.

Provably secure memory isolation for Linux on ARM

Abstract

Keywords

Get full access to this article

References