Refinement in the Formal Verification of the seL4 Microkernel
作者： Gerwin Klein , Thomas Sewell , Simon Winwood
DOI: 10.1007/978-1-4419-1539-9_11
关键词:
摘要: We present an overview of the different refinement frameworks used in L4.verified project to formally prove functional correctness seL4 microkernel. The verification is conducted interactive theorem prover Isabelle/HOL and proceeds two large steps: one proof between monadic, specifications HOL such a monadic specification C program. To connect these proofs into overall theorem, we map both statements common framework.
springer.com
core.ac.uk
doclsf.de 
researchgate.net 参考文章(20)
Norbert Schirmer, Verification of Sequential Imperative Programs in Isabelle/HOL pp. 1- 249 ,(2006)
Eyad Alkassar, Mark A. Hillebrand, Dirk C. Leinenbach, Norbert W. Schirmer, Artem Starostin, Alexandra Tsyban, Balancing the Load Journal of Automated Reasoning. ,vol. 42, pp. 389- 454 ,(2009) , 10.1007/S10817-009-9123-Z
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish, Mind the Gap: A Verification Framework for Low-Level C theorem proving in higher order logics. ,(2009) , 10.1007/978-3-642-03359-9_34
Kai Engelhardt, W. DeRoever, Data Refinement: Model-Oriented Proof Methods and their Comparison ,(1998)
Harvey Tuch, Formal Verification of C Systems Code Journal of Automated Reasoning. ,vol. 42, pp. 125- 187 ,(2009) , 10.1007/S10817-009-9120-2
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies, VCC: A Practical System for Verifying Concurrent C theorem proving in higher order logics. ,vol. 5674, pp. 23- 42 ,(2009) , 10.1007/978-3-642-03359-9_2
RICHARD J. FEIERTAG, PETER G. NEUMANN, The foundations of a provably secure operating system (PSOS) 1979 International Workshop on Managing Requirements Knowledge (MARK). pp. 329- 334 ,(1979) , 10.1109/MARK.1979.8817256
Norbert Schirmer, A verification environment for sequential imperative programs in isabelle/HOL international conference on logic programming. pp. 398- 414 ,(2005) , 10.1007/978-3-540-32275-7_26
Kevin Elphinstone, Philip Derrin, Timothy Roscoe, Gerwin Klein, Gernot Heiser, Towards a practical, verified kernel HOTOS'07 Proceedings of the 11th USENIX workshop on Hot topics in operating systems. pp. 20- ,(2007)
Bruce J. Walker, Richard A. Kemmerer, Gerald J. Popek, Specification and verification of the UCLA Unix security kernel Communications of The ACM. ,vol. 23, pp. 118- 131 ,(1980) , 10.1145/358818.358825