Secure microkernels, state monads and scalable refinement. (English) Zbl 1165.68454
Mohamed, Otmane Ait (ed.) et al., Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18–21, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-71065-3/pbk). Lecture Notes in Computer Science 5170, 167-182 (2008).
Summary: We present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. We achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties.
We report on our experience in applying the techniques in an extensive (100,000 lines of proof) case study-the formal verification of an executable model of the seL4 operating system microkernel.
For the entire collection see [Zbl 1149.68013].
We report on our experience in applying the techniques in an extensive (100,000 lines of proof) case study-the formal verification of an executable model of the seL4 operating system microkernel.
For the entire collection see [Zbl 1149.68013].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Bevier, W.R.: Kit: A study in operating system verification. IEEE Transactions on Software Engineering 15(11), 1382–1396 (1989) · doi:10.1109/32.41331 |
| [2] | de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998) · Zbl 0955.68076 · doi:10.1017/CBO9780511663079 |
| [3] | Derrin, P., Elphinstone, K., Klein, G., Cock, D., Chakravarty, M.M.T.: Running the manual: An approach to high-assurance microkernel development. In: Proc. ACM SIGPLAN Haskell Workshop, Portland, OR, USA (September 2006) · doi:10.1145/1159842.1159850 |
| [4] | Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975) · Zbl 0308.68017 · doi:10.1145/360933.360975 |
| [5] | Elkaduwe, D., Derrin, P., Elphinstone, K.: A memory allocation model for an embedded microkernel. In: Proc. 1st MIKES, Sydney, Australia, pp. 28–34 (2007) |
| [6] | Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: Proc. 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA (May 2007) |
| [7] | Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: AFIPS Conf. Proc., 1979 National Comp. Conf., New York, NY, USA, June 1979, pp. 329–334 (1979) |
| [8] | Fu, G.: Design and implementation of an operating system in Standard ML. Master’s thesis, Dept.of Information and Computer Sciences, Univ.Hawaii at Manoa (1999) |
| [9] | Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 1–16. Springer, Heidelberg (2005) · Zbl 1152.68423 · doi:10.1007/11541868_1 |
| [10] | Hallgren, T., Hook, J., Jones, M.P., Kieburtz, R.B.: An overview of the Programatica Tool Set. In: High Confidence Software and Systems Conference (2004) |
| [11] | Hallgren, T., Jones, M.P., Leslie, R., Tolmach, A.: A principled approach to operating system construction in Haskell. In: Proc. ICFP 2005, pp. 116–128. ACM Press, New York (2005) · Zbl 1302.68084 |
| [12] | Harrison, W.L., Kieburtz, R.B.: The logic of demand in Haskell. Journal of Functional Programming 15(6), 837–891 (2005) · Zbl 1085.68023 · doi:10.1017/S0956796805005666 |
| [13] | Hohmuth, M., Tews, H.: The VFiasco approach for a verified operating system. In: Proc. 2nd ECOOP-PLOS Workshop, Glasgow, UK (October 2005) |
| [14] | Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 147–162. Springer, Heidelberg (2005) · Zbl 1152.68521 · doi:10.1007/11541868_10 |
| [15] | Liedtke, J.: On {\(\mu\)}-kernel construction. In: 15th ACM Symposium on Operating System Principles (SOSP) (December 1995) |
| [16] | Mossakowski, T., Schröder, L., Goncharov, S.: A generic complete dynamic logic for reasoning about purity and effects. In: Fiadeiro, J., Inverardi, P. (eds.) Proc. FASE 2008. LNCS, vol. 4961, pp. 199–214. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-78743-3_15 |
| [17] | Shapiro, J.: Coyotos (2006), http://www.coyotos.org |
| [18] | Staples, M.: A Mechanised Theory of Refinement. PhD thesis, University of Cambridge (1999) |
| [19] | Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, pp. 97–108. ACM Press, New York (2007) · Zbl 1295.68094 |
| [20] | Walker, B., Kemmerer, R., Popek, G.: Specification and verification of the UCLA Unix security kernel. Commun. ACM 23(2), 118–131 (1980) · Zbl 0427.68032 · doi:10.1145/358818.358825 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
