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.
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.
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.
|
|
June Andronick, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 |
|
|
|
David Cock
Lyrebird – assigning meanings to machines
Proceedings of the 5th Workshop on 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 Workshop on Scalable Trusted Computing, 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, New Delhi, India, August, 2010
To appear |
|
|
|
Michael von Tessin
Towards high-assurance multiprocessor virtualisation
Proceedings of the 6th International Verification Workshop, Edinburgh, UK, July, 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 OS 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
Correct OS kernel? Proof? Done!
USENIX ;login:, 34(6), 28–34, (December, 2009) |
|
|
|
Andrew Boyton
A verified shared capability model
Proceedings of the 4th Workshop on 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, 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 |
