Abstract
The Verisoft project aims at the pervasive formal verification from the application layer over the system level software, comprising a microkernel and a compiler, down to the hardware. The different layers of the system give rise to various abstraction levels to conduct the reasoning steps efficiently. The lower the abstraction level the more details and invariants are necessary to ensure overall system correctness. Illustrated by a page-fault handler we discuss the layers and the trade-off between efficiency of reasoning at a more abstract layer versus the development of meta-theory to transfer the verification results between the layers.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bevier, W.R., Hunt Jr., W.A., Moore, J S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5(4), 411–428 (1989)
Moore, J S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 161–172. Springer, Heidelberg (2003)
Neumann, P.G., Feiertag, R.J.: PSOS Revisited. In: 19th Annual Computer Security Applications Conference (ACSA 2003), Las Vegas, NV, USA, pp. 208–216. IEEE Computer Society, Los Alamitos (2003), http://csdl.computer.org/comp/proceedings/acsac/2003/2041/00/20410208abs.htm
Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. Comm. ACM 23(2), 118–131 (1980)
Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.M.: Towards trustworthy computing systems: Taking microkernels to the next level. SIGOPS Oper. Syst. Rev. 41(4), 3–11 (2007)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL 2007, pp. 97–108. ACM Press, New York (2007)
Tuch, H., Klein, G.: Verifying the L4 virtual memory subsystem. In: Proc. NICTA Formal Methods Workshop on Operating Systems Verification, pp. 73–97 (2004)
Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München (April 2006)
Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 189–206. Springer, Heidelberg (2007)
Hohmuth, M., Tews, H., Stephens, S.G.: Applying source-code verification to a microkernel: The VFiasco project. In: SIGOPS 2002, pp. 165–169. ACM Press, New York (2002)
Tverdyshev, S., Shadrin, A.: Formal verification of gate-level computer systems. In: Rozier, K.Y. (ed.) LFM 2008. NASA STI, NASA, pp. 56–58 (2008)
Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 7, pp. 23–50. Edinburgh University Press (1972)
Daum, M., Maus, S., Schirmer, N., Seghir, M.N.: Integration of a software model checker into Isabelle. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 381–395. Springer, Heidelberg (2005)
Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 34–50. Springer, Heidelberg (2004)
Ballarin, C.: Interpretation of locales in Isabelle: Theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, pp. 31–43. Springer, Heidelberg (2006)
Petrova, E.: Verification of the C0 Compiler Implementation on the Source Code Level. PhD thesis, Saarland University, Computer Science Department (2007)
Leinenbach, D.: Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University, Computer Science Department (2008)
Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Woodcock, J., Shankar, N. (eds.) VSTTE 2008. LNCS. Springer, Heidelberg (2008)
Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 109–123. Springer, Heidelberg (2008)
Tverdyshev, S., Alkassar, E.: Efficient bit-level model reductions for automated hardware verification. In: TIME 2008, pp. 164–172. IEEE Computer Society Press, Los Alamitos (2008)
Wenzel, M.: Isabelle/Isar — A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Technische Universität München (2002)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A. (2008). The Verisoft Approach to Systems Verification. In: Shankar, N., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2008. Lecture Notes in Computer Science, vol 5295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87873-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-87873-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87872-8
Online ISBN: 978-3-540-87873-5
eBook Packages: Computer ScienceComputer Science (R0)