Secure Access Controller

Motivation

Advances in machine-assisted theorem proving, and formal methods techniques in general, have pushed the limits of software verification to the point where it is possible to prove properties of real-world applications. Our recently verified seL4 microkernel is one such example.

Formally verifying programs with sizes approaching 10,000 lines of code is a significant improvement over what formal methods were previously able to achieve with reasonable effort. However, 10,000 lines of code is still small in the context of contemporary software systems, which frequently comprise millions of lines of code. Thus the challenge remains as to how formal assurance can be given to real-world software systems of such size.

Our vision is for specifically targeted properties to be provably assured in very large and complex software systems. Our vision comes from the observation that not all software in a large system necessarily contributes to a property of interest. For example, a game installed on a smartphone contributes nothing to the ability to make reliable phone calls. If one can assure the game is isolated from the phone call software, one can focus verification effort on the phone call software to assure reliability of calls.

As a first step towards our vision, we have built a prototype secure access controller (SAC). The SAC provides an initial application domain for investigating developing large systems with formally assured properties.

Overview

The SAC is a conceptually simple device that manages network connections. A single user requires access to several independent networks of different security classifications. The user has a simple terminal connected to a network interface of the SAC. The SAC has additional network interfaces allowing it to be connected to each of the mutually distrusting classified networks. The user only needs to access one network at a time, and selects the network through a web interface provided by the SAC on a control network interface. This setup is depicted below.

The goal of the SAC is to route TCP/IP packets between the user's terminal and the currently selected network without allowing the information to be seen or manipulated by the other networks. The SAC must ensure that all data from one network is isolated from each of the other networks. While we assume that the user's terminal does not leak previously received information back to another network, we otherwise assume that all networks connected to the SAC are malicious and would collude.

Status

We have built a working prototype SAC upon the access-control guarantees provided by the verified seL4 microkernel and thus used seL4 to isolate components such that their implementation need not be reasoned about. This includes the incorporation of Intel's VT-d extensions into seL4's access control model, which enables seL4 to control device access to memory.

In our SAC case study, careful design and componentisation of a large system was used to reduce the run-time trusted computing base from millions of lines of code to just under 9,000. This is no simple task, as multiple copies of para-virtualised Linux are used for networking and providing the control interface. Additionally, we have modelled the design of the SAC and shown that the modelled system fulfils its security goal of isolating data between different networks.

To achieve the vision outlined in the motivation of formally assuring the a security property of the SAC, we need to connect the model used to prove security of the system with the actual implementation. In particular, we must still show that (1) the C implementation of trusted components in the SAC refine the behaviour modelled in the security proof, and (2) that the kernel operations in the security proof correctly model the actual behaviour of the seL4 kernel. The verification success of the seL4 kernel, with its C code shown to implement its functional specification, gives us confidence that both of these tasks are feasible. Carrying out this verification effort forms part of our ongoing work.

People

Publications

		Bernard Blackham and Gernot Heiser Correct, fast, maintainable – choose any three! Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys), Seoul, Korea, July, 2012
		Bernard Blackham, Vernon Tang and Gernot Heiser To preempt or not to preempt, that is the question Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys), Seoul, Korea, July, 2012
		Bernard Blackham, Yao Shi and Gernot Heiser Improving interrupt response time in a verifiable protected microkernel Proceedings of the 7th EuroSys Conference, Bern, Switzerland, April, 2012
		Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor OS kernels Proceedings of the 2nd Workshop on Systems for Future Multi-core Architectures, Bern, Switzerland, April, 2012
		Gernot Heiser, Toby Murray and Gerwin Klein It's time for trustworthy systems IEEE: Security and Privacy, 2012(2), 67–70, (March, 2012)
		Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser Timing analysis of a protected operating system kernel Proceedings of the 32nd IEEE Real-Time Systems Symposium, Vienna, Austria, November, 2011
		Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein seL4 enforces integrity 2nd International Conference on Interactive Theorem Proving, Nijmegen, The Netherlands, August, 2011
		Bernard Blackham, Yao Shi and Gernot Heiser Protected hard real-time: The next frontier Proceedings of the 2nd Asia-Pacific Workshop on Systems (APSys), Shanghai, China, July, 2011
		Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski What if you could actually Trust your kernel? Proceedings of the 13th Workshop on Hot Topics in Operating Systems, Napa, CA, USA, May, 2011
		Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood Provable security: How feasible is it? Proceedings of the 13th Workshop on Hot Topics in Operating Systems, Napa, CA, USA, May, 2011
		June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Proceedings of the 5th Systems Software Verification, Vancouver, Canada, October, 2010
		David Cock Lyrebird – assigning meanings to machines Proceedings of the 5th Systems Software Verification, Vancouver, Canada, October, 2010
		Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The road to trustworthy systems Proceedings of the 5th ACM Workshop on Scalable Trusted Computing (ACMSTC), Chicago, IL, USA, October, 2010 Invited paper
		Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Walker capDL: A language for describing capability-based systems Proceedings of the 1st Asia-Pacific Workshop on Systems (APSys), New Delhi, India, August, 2010
		Michael von Tessin Towards high-assurance multiprocessor virtualisation Proceedings of the 6th International Verification Workshop, Edinburgh, UK, July, 2010
		June Andronick From a proven correct microkernel to trustworthy large systems International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Paris, France, June, 2010
		Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an operating system kernel Communications of the ACM, 53(6), 107–115, (June, 2010)
		Dhammika Elkaduwe A principled approach to kernel memory management, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2010
		Gerwin Klein, Thomas Sewell and Simon Winwood Refinement in the formal verification of seL4 Springer, March, 2010
		Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, 34(6), 28–34, (December, 2009)
		Andrew Boyton A verified shared capability model Proceedings of the 4th Systems Software Verification, Aachen, Germany, October, 2009
		Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 Best Paper Award!
		Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 — formally verifying a high-performance microkernel Proceedings of the 14th International Conference on Functional Programming, Edinburgh, UK, August, 2009
		Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008
		David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August, 2008
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel design for isolation and assurance of physical memory 1st Workshop on Isolation and Integration in Embedded Systems, Glasgow, UK, April, 2008
		Gernot Heiser Your system is secure? Prove it! USENIX ;login:, 32(6), 35–38, (December, 2007)
		Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007
		Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, 41(4), 3–11, (July, 2007)
		Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007
		Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone A memory allocation model for an embedded microkernel Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES), Sydney, Australia, January, 2007
		Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: An approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006
		Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel data – first class citizens of the system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006
		Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, 30(6), 9–13, (December, 2005)
		Kevin Elphinstone Future directions in the evolution of the L4 microkernel Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004