Communications - June 2010

that does not occur after the kernel has been verified: implementation bug fixes.

6. concLusion

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.

acknowledgments

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 Excellence program.

References

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). Springer, 109–123.

2. Dennis, J.b., Van Horn, E. C. Programming semantics for multiprogrammed computations. 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 (unSW), Sydney.

June andronick nICTA, unS W.

Kevin elphinstone nICTA, unS W.

Gernot heiser nIC TA, unS W, open kernel Labs.

Dhammika elkaduwe nICTA, unSW, now at university of Peradeniya, Sri Lanka.

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 initializations. http://www.cr0.org/misc/ CVE-2009–2692.txt, 2009.

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 1999), 170–185.

Rafal Kolanksi nICTA, unSW.

harvey tuch nICTA, unS W, now at VMWare.

simon Winwood nICTA, unSW.

David cock nICTA.

Philip Derrin nICTA, now at open kernel Labs.

michael norrish nICTA, Australian national university, Canberra.

thomas sewell nIC TA.

Have you Considered All the Possibilities?

Save 20%
on these
New & Noteworthy
Resources
from
Chapman & Hall/CRC Press

Save 20% on your online
order by entering promo
code 736DM at checkout
Discount expires July 31, 2010

www.crcpress.com

CHAPMAN & HALL BOOKS

New Edition of a Bestseller!

Algorithms and Theory of Computation Handbook, Second Edition— 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.

ISBN: 978-1-58488-818-5

$179.95 / £ 114.00

$143.96 / £ 91. 20

Flexible, Reliable Software

Using Patterns and Agile Development

“… 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.

ISBN: 978-1-4200-9362-9

$69.95 / £ 44. 99

$55.96 / £ 35. 99

Handbook of Chemoinformatics Algorithms

Providing an overview of the most common chemoinformatics algorithms, this book explains how to effectively apply algorithms and graph theory for solving chemical problems.