×

Operating system verification—an overview. (English) Zbl 1192.68432

Summary: This paper gives a high-level introduction to the topic of formal, interactive, machine-checked software verification in general, and the verification of operating systems code in particular. We survey the state of the art, the advantages and limitations of machine-checked code proofs, and describe two specific ongoing larger-scale verification projects in more detail.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N25 Theory of operating systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi M, Lamport L 1991 The existence of refinement mappings. Theoretical Computer Sci. 82(2): 253–284 · Zbl 0728.68083 · doi:10.1016/0304-3975(91)90224-P
[2] Abrial J-R 1996 The B Book–Assigning Programs to Meanings, Cambridge University Press · Zbl 0915.68015
[3] Alkassar E, Hillebrand M, Rusev S K R Tverdyshev S 2007 Formal device and programming model for a serial interface. In: B Beckert, ed., Proceedings, 4th International Verification Workshop (VERIFY), Vol. 259 of CEUR Workshop Proceedings, Bremen, Germany 4–20
[4] Alkassar E, Schirmer N, Starostin A 2008 Formal pervasive verification of a paging mechanism. In: C R Ramakrishnan, J Rehof (eds), Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Vol. 4963 of Lecture Notes in Computer Science, Springer-Verlag 109–123 · Zbl 1134.68394
[5] Alves-Foss J, Taylor C 2004 An analysis of the gwv security policy, In: Fifth International Workshop on the ACL2 Prover and its Applications (ACL2-2004). Available from http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/alves-foss-taylor/ACL2004-final.pdf
[6] Archer M 2000 TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence 29(1–4): 139–181 · Zbl 1001.68127 · doi:10.1023/A:1018913028597
[7] Archer M 2006 Basing a modelling environment on a general purpose theorem prover, Technical Report NRL/MR/5546-06-8952, (Washington, DC, USA: NRL)
[8] Archer M, Heitmeyer C L, Riccobene E 2000 Using TAME to prove invariants of automata models: Two case studies. In: FMSP 00: Proceedings of the 3rd Workshop on Formal Methods in Software Practice, (New York, NY, USA: ACM) 25–36
[9] Archer M, Leonard E, Pradella M 2003 Analyzing security-enhanced Linux policy specifications. In: POLICY 03: Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks, (Washington, DC, USA: IEEE Computer Society) 158–169
[10] ARM 2000 ARM Architecture Reference Manual
[11] Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani S K, Ustuner A 2006 Thorough static analysis of device drivers. In: EuroSys 06: Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, (New York, NY, USA: ACM) 73–85
[12] Bell D E, LaPadula L J 1973 Secure computer systems: Mathematical foundations, vol. i, Technical Report MTR2547, The MITRE Corporation, Bedford, MA, USA (ESDTR73278I)
[13] Berson T, Jr G B 1979 KSOS: Development methodology for a secure operating system. In: AFIPS Conference Proceedings, 1979 National Computer Conference, Vol. 48, AFIPS Press 365–371
[14] Bertot Y, Castran P 2004 Interactive Theorem Proving and Program Development. CoqArt: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, Springer-Verlag
[15] Beuster G, Henrich N, Wagner M 2006 Real world verification–experiences from the Verisoft email client. In: G Sutcliffe, R Schmidt S Schulz, (eds), Proc. ESCoR 2006, Vol. 192 of CEUR Workshop Proceedings 112–115
[16] Bevier W R 1987 A verified operating system kernel, Technical Report 11, Computational Logic Inc., Austin, TX, USA
[17] Bevier W R 1988 Kit: A study in operating system verification, Technical Report 28, Computational Logic Inc., Austin, TX, USA
[18] Bevier W R 1989a Kit: A study in operating system verification. IEEE Transactions on Software Engineering 15(11): 1382–1396 · Zbl 05114649 · doi:10.1109/32.41331
[19] Bevier W R 1989b Kit and the short stack. J. Automated Reasoning 5(4): 519–530
[20] Bevier W R, Hunt W A, Moore J S Young W D 1989 An approach to systems verification. J. Automated Reasoning 5(4): 411–428
[21] Bevier W R, Smith L 1993a A mathematical model of the Mach kernel: Atomic actions and locks, Technical Report 89, Computational Logic Inc., Austin, TX, USA
[22] Bevier W R, Smith L 1993b A mathematical model of the Mach kernel: Entities and relations, Technical Report 88, Computational Logic Inc., Austin, TX, USA
[23] Beyer S, Jacobi C, Kröning D, Leinenbach D, Paul W J 2006 Putting it all together-formal verification of the VAMP. Int. J. on Software Tools for Technology Transfer (STTT) 8(4): 411–430 · Zbl 05075105 · doi:10.1007/s10009-006-0204-6
[24] Blazy S, Dargaye Z, Leroy X 2006 Formal verification of a C compiler front-end. In: J Misra, T Nipkow E Sekerinski, (eds), FM 2006: 14th International Symposium on Formal Methods, Vol. 4085 of Lecture Notes in Computer Science 460–475
[25] Bornat R 2000 Proving pointer programs in Hoare Logic. In: R Backhouse, J Oliveira, (eds), Mathematics of Program Construction (MPC 2000), Vol. 1837 of Lecture Notes in Computer Science Springer-Verlag 102–126 · Zbl 0963.68036
[26] Bowen J P, Hinchey M G 2005 Ten commandments revisited: a ten-year perspective on the industrial application of formal methods. In: FMICS 05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems, (New York, USA: ACM) 8–16
[27] Boyer R S, Moore J S 1988 A Computational Logic Handbook, (Boston, MA, USA: Academic Press) · Zbl 0655.68117
[28] Burstall R 1972 Some techniques for proving correctness of programs which alter data structures. In: B Meltzer, D Michie, (eds), Machine Intelligence 7, Edinburgh University Press 23–50 · Zbl 0259.68009
[29] Cock D, Klein G, Sewell T 2008 Secure microkernels, state monads and scalable refinement. In: C Munoz, O Ait, (eds), Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs08), Lecture Notes in Computer Science, Springer-Verlag 167–182 · Zbl 1165.68454
[30] Common Criteria 2006 Common Criteria for information technology security evaluation (CC v3{\(\cdot\)}1), http://www.commoncriteriaportal.org/ . Link visited July 2007
[31] Cook B, Gotsman A, Podelski A, Rybalchenko A, Vardi M Y 2007 Proving that programs eventually do something good. In: POPL 07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (New York, NY, USA: ACM) 265–276 · Zbl 1295.68083
[32] Cook B, Podelski A, Rybalchenko A 2006 Termination proofs for systems code. In: PLDI 06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, (New York, NY, USA: ACM) 415–426
[33] Dalinger I, Hillebrand MA, Paul WJ 2005 On the verification of memory management mechanisms. In: D Borrione, W J Paul, (eds), Proc. 13th IFIP Conference on Correct Hardware Design and Verification Methods (CHARME 2005), Vol. 3725 of Lecture Notes in Computer Science, Springer-Verlag 301–316 · Zbl 1159.68317
[34] Daum M, Maus S, Schirmer N, Seghir M N 2005 Integration of a software model checker into Isabelle. In: G Sutcliffe A Voronkov, (eds), 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR05), Vol. 3835 of Lecture Notes in Computer Science, Springer-Verlag 381–395 · Zbl 1143.68449
[35] Davis M, ed 1965 The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Raven Press, NY · Zbl 1099.03002
[36] Dawson J E 2009 Isabelle theories for machine words. In: Seventh International Workshop on Automated Verification of Critical Systems (AVOCS07), Electronic Notes in Computer Science, (Oxford, UK: Elsevier) (in press)
[37] de Roever W-P, Engelhardt K 1998 Data Refinement: Model-Oriented Proof Methods and their Comparison, number 47 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press
[38] Dennis J B, Van Horn E C 1966 Programming semantics for multiprogrammed computations. Communications of the ACM 9: 143–155 · Zbl 0139.32806 · doi:10.1145/365230.365252
[39] Derrin P, Elphinstone K, Klein G, Cock D, Chakravarty M M T 2006 Running the manual: An approach to high-assurance microkernel development. In: Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA
[40] DiBona C, Ockman S, Stone M 1999 Open Sources: Voices from the Open Source Revolution, Appendix A: The Tanenbaum-Torvalds Debate, OReilly. http://www.oreilly.com/catalog/opensources/book/appa.html , Link visited May 2008 · Zbl 0928.68027
[41] Dörrenbächer J 2006 VAMOS microkernel, formal models and verification. In: Talk given at the 2nd International Workshop on System Verification (SV 2006), NICTA, Sydney, Australia. http://www.cse.unsw.edu.au/formalmethods/events/svws-06/VAMOS_Microkernel.pdf. Link visited May 2008
[42] Duff T 1983 Duffs device, http://www.lysator.liu.se/c/duffs-device.html . Link visited May 2008
[43] Elkaduwe D, Derrin P, Elphinstone K 2007 A memory allocation model for an embedded microkernel. In: Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, NICTA, Sydney, Australia 28–34
[44] Elkaduwe D, Derrin P, Elphinstone K 2008 Kernel design for isolation and assurance of physical memory. In: 1st Workshop on Isolation and Integration in Embedded Systems, ACM SIGOPS, Glasgow, UK 35–40
[45] Elkaduwe D, Klein G, Elphinstone K 2007 Verified protection model of the seL4 microkernel, Technical report, NICTA. Available from http://ertos.nicta.com.au/publications/papers/Elkaduwe_GE_07.pdf
[46] Elphinstone K 2004 Future directions in the evolution of the L4 microkernel. In: G Klein, ed., Proceedings of the 1st internationalWorkshop on OS Verification 2004, Technical Report 0401005T-1, NICTA, Sydney, Australia
[47] Elphinstone K, Klein G, Derrin P, Roscoe T, Heiser G 2007 Towards a practical, verified kernel. In: Proceedings of the 11th Workshop on Hot Topics in Operating Systems, USENIX, San Diego, CA, USA
[48] Elphinstone K, Klein G, Kolanski R 2006 Formalising a high-performance microkernel. In: R Leino, ed., Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Microsoft Research Technical Report MSR-TR-2006-117, Seattle, USA 1–7
[49] Feiertag R J 1980 A technique for proving specifications are multilevel secure, Technical Report CSL-109, Computer Science Laboratory, SRI International, Menlo Park, CA, USA
[50] Feiertag R J, Neumann P G 1979 The foundations of a provably secure operating system (PSOS). In: AFIPS Conference Proceedings, 1979 National Computer Conference, New York, NY, USA 329–334
[51] Feng X 2007 An Open Framework for Certified System Software, PhD thesis, Department of Computer Science, Yale University, New Haven, CT, USA
[52] Feng X, Shao Z, Dong Y, Guo Y 2008 Certifying low-level programs with hardware interrupts and preemptive threads. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI08), (New York, NY, USA: ACM) To appear · Zbl 1191.68176
[53] Fetzer J H 1988 Program verification: the very idea. Communications of the ACM 31(9): 1048–1063 · doi:10.1145/48529.48530
[54] Fischer S 2008 Formal verification of a big integer library. In: DATE08 Workshop on Dependable Software Systems. Available from http://busserver.cs.uni-sb.de/publikationen/Fi08DATE.pdf
[55] Ford B, Hibler M, Lepreau J, Tullmann P, Back G, Clawson S 1996 Microkernels meet recursive virtual machines. In: Proceedings of the Second Symposium on Operating Systems Design and Implementation (OSDI96), Seattle, WA, USA 137–151
[56] Gargano M, Hillebrand M, Leinenbach D, Paul W 2005 On the correctness of operating system kernels. In: Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs05),Vol. 3603 of Lecture Notes in Computer Science, (Germany: Springer-Verlag, Berlin) 1–16 · Zbl 1152.68423
[57] Gödel K 1931 Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173–198. English translation, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I, in Davis (1965) 4–38 · Zbl 0002.00101 · doi:10.1007/BF01700692
[58] Goerigk W, Hoffmann U 1998 Rigorous compiler implementation correctness: How to prove the real thing correct. In: D Hutter, W Stephan, P Traverso M Ullmann, (eds), Applied Formal Methods–FM-Trends 98, Vol. 1641 of Lecture Notes in Computer Science, (Germany: Springer-Verlag, Berlin) 122–136
[59] Goguen J A, Meseguer J 1982 Security policies and security models. In: Proceedings of the 1982 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, New York, NY, USA 11–20
[60] Goguen J A, Meseguer J 1984 Unwinding and inference control. In: IEEE Symposium on Security and Privacy, IEEE Computer Society Press, New York, NY, USA 75–87
[61] Greenhills Software, Inc. 2008 Integrity real-time operating system, http://www.ghs.com/products/rtos/integrity.html
[62] Greve D, Richards R, Wilding M 2004 A summary of intrinsic partitioning verification. In: Fifth International Workshop on the ACL2 Prover and its Applications (ACL2-2004). Available from http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/greve-richards-wilding/acl2-paper.pdf
[63] Greve D, Wilding M, Vanfleet W M 2003 A separation kernel formal security policy. In: Fourth International Workshop on the ACL2 Prover and its Applications (ACL2-2003). Available from http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/greve-wilding-vanfleet/security-policy.pdf
[64] Greve D, Wilding M, Vanfleet W M 2005 High assurance formal security policy modeling. In: Proceedings of the 17th Systems and Software Technology Conference 2005 (SSTC05)
[65] Guttman J D, Herzog A L, Ramsdell J D, Skorupka C W 2005 Verifying information flow goals in security-enhanced Linux. Journal of Computer Security 13(1): 115–134
[66] Haigh J T, Young W D 1987 Extending the noninterference version of MLS for SAT. IEEE Transactions on Software Engineering 13(2): 141–150 · Zbl 05341363 · doi:10.1109/TSE.1987.226478
[67] Hansen P B 1970 The nucleus of a multiprogramming operating system. Communications of the ACM 13(4): 238–250 · Zbl 0191.18505 · doi:10.1145/362258.362278
[68] Hardin D S, Smith E W, Young W D 2006 A robust machine code proof framework for highly secure applications. In: ACL2 06: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, (New York, NY, USA: ACM) 11–20
[69] Hardy N 1985 KeyKOS architecture, ACM SIGOPS Operating Systems Review 19(4): 8–25 · Zbl 05445310 · doi:10.1145/858336.858337
[70] Harrison J 1996 HOL Light: a tutorial introduction. In: M Srivas, A Camilleri, (eds), Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD96), Vol. 1166 of Lecture Notes in Computer Science, Springer-Verlag 265–269
[71] Harrison J 2006 Towards self-verification of HOL Light. In:U Furbach, N Shankar, (eds), Proceedings of the third International Joint Conference on Automated Reasoning (IJCAR 2006), Vol. 4130 of Lecture Notes in Computer Science, Springer-Verlag, Seattle, WA 177–191
[72] Härtig H, Hohmuth M, Wolter J 1998 Taming Linux. In:K A Hawick, H A James, (eds), Proceedings of the 5th Annual Australasian Conference on Parallel And Real-Time Systems (PART 98), Springer-Verlag, Adelaide, Australia
[73] Heiser G, Elphinstone K, Kuz I, Klein G, Petters S M 2007 Towards trustworthy computing systems: Taking microkernels to the next level. ACM Operating Systems Review 41(3)
[74] Heitmeyer C L, Archer M, Leonard E I, McLean J 2006 Formal specification and verification of data separation in a separation kernel for an embedded system. In: CCS 06: Proceedings of the 13th ACM conference on Computer and communications security, (New York, NY, USA: ACM) 346–355
[75] Heitmeyer C L, Archer M, Leonard E, McLean J 2008 Applying formal methods to a certifiably secure software system. IEEE Transactions on Software Engineering 34(1): 82–98 · Zbl 05341154 · doi:10.1109/TSE.2007.70772
[76] Hennessy J, Patterson D 1996 Computer Architecture: A Quantitative Approach, Morgan Kaufmann, San Francisco, USA · Zbl 0844.68003
[77] Hillebrand M A, in der Rieden T, Paul W J 2005 Dealing with I/O devices in the context of pervasive system verification. In: ICCD 05: Proceedings of the 2005 International Conference on Computer Design, IEEE Computer Society, Washington, DC, USA 309–316
[78] Hillebrand M A, Paul W J 2008 On the architecture of system verification environments. In: Hardware and Software: Verification and Testing, Vol. 4899 of Lecture Notes in Computer Science, (Germany: Springer-Verlag, Berlin) 153–168
[79] Hoare C A R 1969 An axiomatic basis for computer programming. Communications of the ACM 12(10): 576–580 · Zbl 0179.23105 · doi:10.1145/363235.363259
[80] Hohmuth M, Härtig H 2001 Pragmatic nonblocking synchronization for real-time systems. In: Proceedings of the General Track: 2002 USENIX Annual Technical Conference, USENIX Association, Berkeley, CA, USA 217–230
[81] Hohmuth M, Tews H 2003 The semantics of C++ data types: Towards verifying low-level system components. In: D Basin, B Wolff, (eds), TPHOLs 2003, Emerging Trends Track, Technical Report No. 187, Institut für Informatik, Universität Freiburg, Freiburg, Germany 127–144
[82] Hohmuth M, Tews H 2005 The VFiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, Glasgow, UK. Available from http://wwwtcs.inf.tu-dresden.de/ tews/Plos-2005/ecoop-plos-05-a4.ps
[83] Hohmuth M, Tews H, Stephens S G 2002a Applying source-code verification to a microkernel: the VFiasco project. In: G Muller, E Jul, (eds), Proceedings of the 10th ACM SIGOPS European Workshop, (New York, NY, USA: ACM) 165–169
[84] Hohmuth M, Tews H, Stephens S G 2002b Applying source-code verification to a microkernel: the VFiasco project, Technical Report TUD-FI02-03-März 2002, Technische Universität Dresden, Dresden, Germany
[85] Huisman M, Jacobs B 2000 Java program verification via a Hoare logic with abrupt termination. In: FASE 00: Proceedings of the Third International Conference on Fundamental Approaches to Software Engineering, Vol. 1783 of Lecture Notes in Computer Science, Springer-Verlag, London, UK 284–303
[86] in der Rieden T, Tsyban A 2008 CVM–a verified framework for microkernel programmers. In: R Huuck, G Klein B Schlich, (eds), Proceedings of the 3rd international Workshop on Systems Software Verification (SSV08), Vol. 217 of Electronic Notes in Computer Science, Elsevier, Sydney, Australia 151–168
[87] Jacob J 1989 On the derivation of secure components. In: Proceedings of the IEEE Symposium on Security and Privacy, IEEE Computer Society, Washington, DC, USA 242–247
[88] Jacobs B, Meijer H, Poll E 2001VerifiCard: A European project for smart card verification. Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI)
[89] Jones S P 2003 Haskell 98 Language and Libraries: The Revised Report, Cambridge University Press
[90] Kaufmann M, Manolios P, Moore J S 2000 Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers
[91] Kemmerer R 1979 Formal verification of the UCLA security kernel: abstract model, mapping functions, theorem generation, and proofs., PhD thesis, University of California, Los Angeles, USA
[92] Kestrel Institute 1998 Specware Language Manual, Palo Alto, CA, USA
[93] Klein G, Nipkow T 2006 A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems 28(4): 619–695 · doi:10.1145/1146809.1146811
[94] Klein G, Tuch H 2004 Towards verified virtual memory in L4. In: K Slind, ed., TPHOLs Emerging Trends 04, Park City, UT, USA
[95] Kolanski R 2008 A logic for virtual memory. In: R Huuck, G Klein, B Schlich, (eds), Proceedings of the 3rd International Workshop on Systems Software Verification (SSV08), Vol. 217 of Electronic Notes in Computer Science, Elsevier, Sydney, Australia 61–77
[96] Kolanski R, Klein G 2006 Formalising the L4 microkernel API. In: B Jay, J Gudmundsson, (eds), Computing: The Australasian Theory Symposium (CATS 06), Vol. 51 of Conferences in Research and Practice in Information Technology, Hobart, Australia 53–68
[97] Leinenbach, D, Paul, W. Petrova, E. 2005 Towards the formal verification of a C0 compiler: code generation and implementation correctness. In: Third IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005 2–11
[98] Leinenbach D, Petrova E 2008 Pervasive compiler verification–from verified programs to verified systems. In: R Huuck, G Klein, B Schlich, (eds), Proceedings of the 3rd international Workshop on Systems Software Verification (SSV08), Vol. 217 of Electronic Notes in Computer Science, Elsevier, Sydney, Australia 23–40
[99] Leroy X 2006 Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: J G Morrisett, S L P Jones, (eds), 33rd symposium Principles of Programming Languages (POPL06), (New York, NY, USA: ACM) 42–54 · Zbl 1369.68124
[100] Leslie B, Chubb P, Fitzroy-Dale N, Götz S, Gray C, Macpherson L, Potts D, Shen Y, Elphinstone K, Heiser G 2005 User-level device drivers: Achieved performance. J. Computer Sci. and Technol. 20(5): 654–664 · Zbl 02241992 · doi:10.1007/s11390-005-0654-4
[101] Leslie B, van Schaik C, Heiser G 2005 Wombat: A portable user-mode Linux for embedded systems. In: Proceedings of the 6th Linux.Conf.Au, Canberra, Australia. http://lcs2005.linux.org.au . Link visited May 2008
[102] Liedtke J 1995 On {\(\mu\)}-kernel construction. In: Proceedings of 15th ACM Symposium on Operating System Principles (SOSP), Operating System Review 29(5), (New York, NY, USA: ACM) 237–250
[103] Lipton R J, Snyder L 1977 A linear time algorithm for deciding subject security. Journal of the ACM 24(3): 455–464 · Zbl 0358.68041 · doi:10.1145/322017.322025
[104] MacKenzie D 2001 Mechanizing Proof: Computing, Risk, and Trust, The MIT Press · Zbl 1063.68500
[105] Martin W B, White P, Goldberg A, Taylor F S 2000 Formal construction of the mathematically analyzed separation kernel. In: ASE 00: Proceedings of the 15th IEEE International Conference on Automated software engineering, IEEE Computer Society, Washington, DC, USA 133–141
[106] McCauley E J, Drongowski P J 1979 KSOS–the design of a secure operating system. In: AFIPS Conference Proceedings, 1979 National Computer Conference, Vol. 48, AFIPS Press 345–353
[107] Morgan C 1990 Programming from Specifications, 2nd edn, Prentice Hall · Zbl 0697.68018
[108] National Institute of Standards and Technology (NIST) 2002 Software errors cost U.S. economy $59{\(\cdot\)}5 billion annually, http://www.nist.gov/public_affairs/releases/n02-10.htm . Visited April 2008
[109] Naur P, Randell B eds 1969 Software Engineering. Report on a conference sponsored by the NATO Science Committee, Garmisch, Germany, 7th to 11th October 1968, Scientific Affairs Division, NATO, Brussels, Belgium
[110] Neumann P G, Boyer R S, Feiertag R J, Levitt K N, Robinson L 1980 A provably secure operating system: The system, its applications, and proofs. Second Edition, Technical Report CSL-116, Computer Science Laboratory, SRI International, Menlo Park, CA, USA
[111] Neumann P G, Feiertag R J 2003 PSOS revisited. In: ACSAC 03: Proceedings of the 19th Annual Computer Security Applications Conference, IEEE Computer Society, Washington, DC, USA 208–216
[112] Ni Z, Yu D, Shao Z 2007 Using XCAP to certify realistic system code: Machine context management, in Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs07), Vol. 4732 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Germany 189–206 · Zbl 1144.68325
[113] NICTA 2006 L4/Wombat performance, Web page, http://ertos.nicta.com.au/research/l4/performance.pml . Visited May 2008
[114] NICTA 2008 L4/Iguana OS web site, http://www.ertos.nicta.com.au/iguana/ . Visited May 2008
[115] Nipkow T, Paulson L, Wenzel M 2002 Isabelle/HOL – A Proof Assistant for Higher-Order Logic, Vol. 2283 of Lecture Notes in Computer Science, Springer-Verlag · Zbl 0994.68131
[116] Norrish M 1998 C formalised in HOL, PhD thesis, Computer Laboratory, University of Cambridge
[117] Norrish M Slind K 1998–2006 HOL-4 manuals. Available at http://hol.sourceforge.net/
[118] Open Kernel Labs, Inc., 2007 OKL web site, http://www.ok-labs.com . Visited May 2008
[119] Owre S, Rajan S, Rushby J, Shankar N, Srivas M 1996 PVS: Combining specification, proof checking, and model checking. In: R Alur, T Henzinger, (eds), Computer Aided Verification, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag 411–414
[120] Parker K J 2007 The Escapement Orbit
[121] Perrine T, Codd J, Hardy B 1984 An overview of the kernelized secure operating system (KSOS). In: Proceedings of the Seventh DoD/NBS Computer Security Initiative Conference 146–160
[122] Petrova E 2007 Verification of the C0 Compiler Implementation on the Source Code Level, PhD thesis, Saarland University, Computer Science Department, Saarbrücken, Germany
[123] Popek G J, Farber D A 1978 A model for verification of data security in operating systems. Communications of the ACM 21(9): 737–749 · Zbl 0399.68036 · doi:10.1145/359588.359597
[124] Popek G J, Kampe M, Kline C S, Walton E 1977 The UCLA data secure operating system, Technical report, UCLA
[125] Popek G J, Kampe M, Kline C S, Walton E 1979 UCLA data secure Unix. In: AFIPS Conference Proceedings: 1979 National Computer Conference (1979 NCC), AFIPS Press 355–364
[126] Rashid R, Julin D, Orr D, Sanzi R, Baron R, Forin A, Golub D Jones M 1989 Mach: A system software kernel. In: Proceedings of the 34th Computer Society International Conference COMPCON 89
[127] Reason J 1990 Human Error, Cambridge University Press
[128] Reynolds J C 2002 Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science 55–74
[129] Ridge T 2004 A mechanically verified, efficient, sound and complete theorem prover for first order logic. In: G Klein, T Nipkow, L Paulson, (eds), The Archive of Formal Proofs, http://afp.sf.net/entries/Verified-Prover.shtml . Formal proof development
[130] Robinson L, Levitt K N 1977 Proof techniques for hierarchically structured programs. Communications of the ACM 20(4): 271–283 · Zbl 0358.68030 · doi:10.1145/359461.359483
[131] Rockwell Collins, Inc. 2003 AAMP7r1 Reference Manual
[132] Rushby J 1992 Noninterference, transitivity, and channel-control security policies, Technical Report CS-92-02, Computer Science Laboratory, (Menlo Park, CA, USA: SRI International)
[133] Saydjari O, Beckman J, Leaman J 1987 Locking computers securely. In: 10th National Computer Security Conference 129–141
[134] Schirmer N 2004 A verification environment for sequential imperative programs in Isabelle/HOL. In: F Baader, A Voronkov, (eds), 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR04), Vol. 3452 of Lecture Notes in Computer Science, Springer-Verlag 398–414
[135] Schirmer N 2006 Verification of Sequential Imperative Programs in Isabelle/HOL, PhD thesis, Institut für Informatik, Technische Universität München, Munich, Germany · Zbl 1108.68410
[136] Schwichtenberg H 2004 Proof search in minimal logic. In: B Buchberger, J A Campbell, (eds), Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, Austria, September 22–24, 2004, Proceedings, Vol. 3249 of Lecture Notes in Computer Science, Springer-Verlag 15–25
[137] Scott D S 1970 Outline of a mathematical theory of computation. In: In 4th Annual Princeton Conference on Information Sciences and Systems 169–176
[138] Securityfocus 2008 Vulnerabilities web site, http://www.securityfocus.com/vulnerabilities . Visited May 2008
[139] Shapiro J S 2006 Programming language challenges in systems codes: why systems programmers still use C, and what to do about it. In: PLOS 06: Proceedings of the 3rd workshop on Programming languages and operating systems, (New York, NY, USA: ACM)
[140] Shapiro J S 2008 Coytos web site, http://www.coyotos.org/ . Link visited May 2008
[141] Shapiro J S, Doerrie M S, Northup E, Sridhar S, Miller M 2004 Towards a verified, general-purpose operating system kernel. In: G Klein, ed., Proceedings of the NICTA Formal Methods Workshop on Operating Systems Verification 2004. Technical Report 0401005T-1, NICTA, Sydney, Australia
[142] Shapiro J S, Smith J M, Farber D J 1999 EROS: a fast capability system. In:SOSP 99: Proceedings of the seventeenth ACM symposium on Operating systems principles, (New York, NY, USA: ACM) 170–185
[143] Shapiro J S, Weber S 2000 Verifying the EROS confinement mechanism. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy, IEEE Computer Society, Washington, DC, USA 166–176
[144] Slashdot 2006 Root exploit for NVIDIA closed-source Linux driver, http://it.slashdot.org/article.pl?sid=06/10/16/2038253 . Visited May 2008
[145] Spencer R, Smalley S, Loscocco P, Hibler M, Andersen D, Lepreau J 1999 The Flask security architecture: system support for diverse security policies. In: SSYM99: Proceedings of the 8th conference on USENIX Security Symposium, USENIX Association, Berkeley, CA, USA 123–139
[146] Sridhar S, Shapiro J S 2006 Type inference for unboxed types and first class mutability. In: PLOS 06: Proceedings of the 3rd workshop on Programming languages and operating systems, (New York, NY, USA: ACM) p. 7
[147] Starostin A 2006 Formal verification of a C-library for strings, Masters thesis, Saarland University, Computer Science Department, Saarbrücken, Germany. Available at http://www-wjp.cs.unisb.de/publikationen/St06.pdf
[148] Starostin A, Tsyban A 2008 Correct microkernel primitives. In: R Huuck, G Klein, B Schlich, (eds), Proceedings of the 3rd international Workshop on Systems Software Verification (SSV08), Vol. 217 of Electronic Notes in Computer Science, (Sydney, Australia: Elsevier) 169–185
[149] System Architecture Group 2003 The L4Ka::Pistachio microkernel, http://l4ka.org/projects/pistachio/pistachio-whitepaper.pdf . Link visited May 2008
[150] Tews H 2004 Verifying Duffs device: A simple compositional denotational semantics for goto and computed jumps, http://wwwtcs.inf.tu-dresden.de/tews/Goto/goto.ps . Link visited May 2008
[151] Tews H 2007 Formal methods in the Robin project: Specification and verification of the Nova microhypervisor. In: H Tews, ed., Proceedings of the C/C++ Verification Workshop 2007. Technical Report ICIS-R07015, Radboud University Nijmegen, Nijmegen, The Netherlands
[152] Tews H, Weber T, Poll E, van Eekelen M, van Rossum P 2008 Formal Nova interface specification (Robin deliverable D.12), http://www.cs.ru.nl/tews/Robin/specification-deliverable.pdf . Revision 45. Link visited May 2008
[153] Tews H, Weber T, Völp M 2008 A formal model of memory peculiarities for the verification of low-level operating-system code. In: R Huuck, G Klein, B Schlich, (eds), Proceedings of the 3rd international Workshop on Systems Software Verification (SSV08), Vol. 217 of Electronic Notes in Computer Science, (Australia: Elsevier, Sydney) 79–96
[154] Tuch H 2008a Formal Memory Models for Verifying C Systems Code, PhD thesis, School for Computer Science and Engineering, University of New South Wales, Sydney, Australia
[155] Tuch H 2008b Structured types and separation logic. In: R Huuck, G Klein, B Schlich, (eds), Proceedings of the 3rd International Workshop on Systems Software Verification (SSV08), Vol. 217 of Electronic Notes in Computer Science, (Australia: Elsevier, Sydney) 41–59
[156] Tuch H, Klein G, 2004 Verifying the L4 virtual memory subsystem. In: G Klein, ed., Proceedings of the 1st International Workshop on OS Verification 2004, Technical Report 0401005T-1, NICTA, Sydney, Australia 73–97
[157] Tuch H, Klein G, 2005 A unified memory model for pointers. In: Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR05), Montego Bay, Jamaica 474–488 · Zbl 1143.68464
[158] Tuch H, Klein G, Heiser G. 2005 OS verification–now!. In: Proceedings of the 10th Workshop on Hot Topics in Operating Systems, USENIX, Santa Fe, NM, USA 7–12
[159] Tuch H, Klein G, Norrish M 2007 Types, bytes, and separation logic. In: M Hofmann, M Felleisen, (eds), Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France 97–108 · Zbl 1295.68094
[160] Verisoft Project 2006 BMBF-funding improves the security of computer systems, http://www.verisoft.de/PressRelease20050826.html . Visited May 2008
[161] Verisoft Project 2008 Verisoft repository, http://www.verisoft.de/VerisoftRepository.html . Visited May 2008
[162] Walker B J, Kemmerer R A, Popek G J 1980 Specification and verification of the UCLA Unix security kernel. Communications of the ACM 23(2): 118–131 · Zbl 0427.68032 · doi:10.1145/358818.358825
[163] White P, Allen Goldberg A F S T 2002 Creating high confidence in a separation kernel, Automated Software Engineering 9(3): 263–284 · Zbl 1034.68637 · doi:10.1023/A:1016324624000
[164] Wiedijk F ed 2006 The Seventeen Provers of the World, Foreword by Dana S. Scott, Vol. 3600 of Lecture Notes in Computer Science, Springer-Verlag · Zbl 1114.03007
[165] Wiedijk F 2008 Formalising 100 theorems, http://www.cs.ru.nl/freek/100/ . Link visited May 2008
[166] Winskel G 1993 The formal semantics of programming languages, (Cambridge, UK: MIT Press) · Zbl 0919.68082
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.