that does not occur after the kernel has been verified: implementation bug fixes.
We have presented our experience in formally verifying
seL4. We have shown that full, rigorous, formal verification
is practically achievable for OS microkernels.
The requirements of verification force the designers to
think of the simplest and cleanest way of achieving their
goals. We found repeatedly that this leads to overall better
design, for instance, in the decisions aimed at simplifying
concurrency-related verification issues.
Our future research agenda includes verification of the
assembly parts of the kernel, a multi-core version of the kernel, as well as formal verification of overall system security
and safety properties, including application components.
The latter now becomes much more meaningful than previously possible: application proofs can rely on the abstract,
formal kernel specification that seL4 is proven to implement.
We would like to acknowledge the contribution of the former
team members on this verification project: Timothy Bourke,
Jeremy Dawson, Jia Meng, Catherine Menon, and David Tsai.
NICTA is funded by the Australian Government
as represented by the Department of Broadband,
Communications and the Digital Economy and the
Australian Research Council through the ICT Centre of
1. Alkassar, E., Schirmer, n., Starostin,
A. Formal pervasive verification
of a paging mechanism. TACAS.
C. R. Ramakrishnan and J. Rehof,
eds. Volume 4963 of LnCS (2008).
2. Dennis, J.b., Van Horn, E. C.
Programming semantics for
CACM 9 (1966), 143–155.
3. Elkaduwe, D., klein, g., Elphinstone, k.
Verified protection model of the seL4
microkernel. vSTTE 2008—verified
Soft ware: Theories, Tools & Experiments.
J. Woodcock and n. Shankar eds.
Volume 5295 of LnCS (Toronto, Canada,
oct 2008), Springer, 99–114.
4 ISo/IEC. Programming languages—C.
Technical Report 9899: TC2, ISo/IEC
J TC1/SC22/ Wg14, May 2005.
5. Leroy, X. Formal certification of a compiler
back-end, or: Programming a compiler
with a proof assistant. 33rd POPL. J.g.
Ger win Klein national ICT Australia
(nICTA), university of South Wales
June andronick nICTA, unS W.
Kevin elphinstone nICTA, unS W.
Gernot heiser nIC TA, unS W, open
Dhammika elkaduwe nICTA, unSW,
now at university of Peradeniya,
Kai engelhardt nICTA, unS W.
Morrisett and S.L.P. Jones, eds. (new
york, ny, uSA, 2006), ACM, 42–54.
6. Liedtke, J. Towards real microkernels.
CACM 39, 9 (Sept 1996), 70–77.
7. ni, Z., yu, D., Shao. Z. using XCAP to
certify realistic system code: Machine
context management. 20th TPHOLs,
volume 4732 of LnCS (kaiserslautern,
germany, Sept 2007), Springer, 189–206.
8. nipkow, T., Paulson, L., Wenzel, M.
Isabelle/HOL—A Proof Assistant for
Higher-Order Logic. Volume 2283 of
LnCS (2002), Springer.
9. ormandy, T., Tinnes, J. Linux null pointer
dereference due to incorrect proto_ops
10. Saltzer, J.H., Schroeder, M.D. The
protection of information in computer
systems. Proc. IEEE 63 (1975), 1278–1308.
11. Shapiro, J.S., Smith, J.M., Farber, D.J.
ERoS: A fast capability system. 17th
SOSP (Charleston, SC, uSA, Dec
Rafal Kolanksi nICTA, unSW.
harvey tuch nICTA, unS W, now at
simon Winwood nICTA, unSW.
David cock nICTA.
Philip Derrin nICTA, now at open kernel
michael norrish nICTA, Australian
national university, Canberra.
thomas sewell nIC TA.
© 2010 ACM 0001-0782/10/0600 $10.00
Have you Considered All the Possibilities?
New & Noteworthy
Chapman & Hall/CRC Press
Save 20% on your online
order by entering promo
code 736DM at checkout
Discount expires July 31, 2010
CHAPMAN & HALL BOOKS
New Edition of a Bestseller!
Algorithms and Theory of
Two Volume Set
Praise for the Previous Edition
“… excellent survey of the state of the
art … highly recommended for anyone
interested in algorithms, data structures and the theory of computation …
an indispensable book of reference … .”
—R. Kemp, Zentralblatt MATH, Vol. 926
Catalog no. C8180
January 2010, 1938 pp.
$179.95 / £ 114.00
$143.96 / £ 91. 20
Flexible, Reliable Software
Using Patterns and
“… brings together a careful selection
of topics that are relevant, indeed
crucial, for developing good quality
software … leads the reader through
an experience of active learning.”
—Michael Kölling, Bestselling
Author and originator of the BlueJ
and Greenfoot environments
Catalog no. C3622
May 2010, 527 pp.
$69.95 / £ 44. 99
$55.96 / £ 35. 99
Providing an overview of the most
common chemoinformatics algorithms, this book explains how to
effectively apply algorithms and
graph theory for solving chemical
Catalog no. C2922
April 2010, 454 pp.
$99.95 / £ 63. 99
$79.96 / £ 51. 19