Language-Based System Software Verification

Last modified: April 2, 2008 by dongyuan

"Who would have thought that the programming languages of the 21st century will be built upon foundations of logic theory from the 19th and 20th? by Philip Wadler"

Content

• Introduction

• Logic

• Hoare Logic

• Separation Logic

• Type System and Programming Language

• Typed Assembly Languages (TALs)

• Proof-Carrying Code

• Tools

• Compiler Certification

• Operating System Verification and

• Hypervisor(VMM) verification

• Target Machine

• Conference

Introduction

• C Jones, P O'Hearn and J Woodcock. Verified Software: A Grand Challenge, IEEE Computer, March 2006, pp93-95. (PDF).

• Tony Hoare and Jay Misra. Verified software: theories, tools, experiments: Vision of a Grand Challenge project, The VSTTE conference, July 2005 (PDF).

• Leslie Lamport. The Future of Computing: Logic or Biology (PDF).

• Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing (PDF).

• Philip Wadler. New Languages, Old Logic, (HTML) (Chinese Version, HTML).

• Fred B. Schneider, Greg Morrisett, and Robert Harper. A Language-Based Approach to Security (PDF).

Logic

• Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems (Second Edition), Cambridge University Press, 2004.

• Dirk van Dalen. Logic and Structure. (Fourth Edition). Springer, 2004.

• Mark Ryan and Martin Sadler, Valuation Systems and Consequence Relations. In Handbook of Logic in Computer Science (Volume 1 Bacground: Mathematical Structures). Oxford University Press, 1992.

• Henk Barendregt and Herman Geuvers. Proof-Assistants Using Dependent Type Systems. Download the reprint. Also in Handbook of Automated Reasoning (Volume 2), MIT Press, 2001.

Hoare Logic

• Robert W. Floyd. Assigning meanings to programs. In Proc. Amer. Math. Soc. Symposia in Applied Mathematics, volume 19, pages 19-31, 1967. (PDF)

• C.A.R. Hoare. An axiomatic basis for computer programming, CACM 12(10), 1969, pages 576 - 580.

• C.A.R. Hoare. Proof of a Program : FIND, CACM, 14(1), 1971, pages 39-45.

Separation Logic

• Reynolds's LICS survey

• OHearn's logic papers

  • PW O'Hearn,Resources, Concurrency and Local Reasoning, Theoretical Computer Science 375(1-3) , pp271-307, May 2007. (Prelim version appeared in CONCUR'04, LNCS 3170, pp49-67.) (PDF).

  • Samin Ishtiaq, Peter O'Hearn BI as an Assertion Language for Mutable Data Structures. Proceedings of POPL'01. (PDF).

Type System and Programming Language

• Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002

• John C. Mitchell. Foundations for Programming Languages.(Third Edition). The MIT Press, 2000

• John Reynolds. Theories of Programming Languages. Cambridge University Press, 1998.

• Robert Harper, Programming Languages: Theory and Practice. Carnegie Mellon University, November 2001. Working draft available for downloading: website.

TAL

• The TAL webpage.

• N. Hamid, et al. A Syntactic Approach to Foundational Proof-Carrying Code

Proof-Carrying Code

• Necula's PCC papers

  • G. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang., pages 106-119, ACM Press, Jan. 1997

• Appel's FPCC papers

  • A. W. Appel and A. P. Felty, A semantic model of types and machine instructions for proof-carrying code. In POPL'00, pages 243-253. ACM Press, 2000.

  • A. W. Appel, foundational proof-carrying code, In LICS'01, pages 247-258, IEEE Comp. Soc., J

• FLINT Group's papers

  • GA Syntactic Approach to Foundational Proof-Carrying Code. Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, pages 89-100, July 2002.

  • Building Certified Libraries for PCC: Dynamic Storage Allocation (Extended Version). Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. In Science of Computer Programming (Special Issue ESOP 2003), 50 (1-3): 101-127, March 2004.

  • Certified Assembly Programming with Embedded Code Pointers. Zhaozhong Ni and Zhong Shao. In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL'06), Charleston, South Carolina, pages 320-333, January 2006.

  • Modular Verification of Assembly Code with Stack-Based Control Abstractions. Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006.

  • An Open Framework to Foundational Proof-Carrying Code. Xinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07), Nice, France, pages 67-78, January 2007.

  • Certified Self-Modifying Code. Hongxu Cai, Zhong Shao, and Alexander Vaynberg. In Proc. 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07), San Diego, CA, June 2007.

Proof-Assistant Tools

Coq/CoqIDE/ProofGeneral:

• Pennsylvania PL Club, Using Proof Assistants for Programming Language Research. Jan. 8, 2008.

• Gerard Huet, Gilles Kahn and Christine Paulin-Mohring. The Coq Proof Assistant: A Tutorial (Version 8.1). Feb. 8, 2007.

• David Aspinall and Thomas Kleymann, User Manual for Proof General 3.5 (HTML and PDF). April 2004.

• Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions), ISBN 3540208542 (buy it online), Springer, 2004.

• Useful Coq resources (packages):
      http://www.lri.fr/~sozeau/research/russell.fr.html
      http://lambda-the-ultimate.org/node/2626
      http://www.lix.polytechnique.fr/~assia/Publi/ssrdoc.pdf
      http://research.microsoft.com/research/downloads/Details/6658d5cc-9965-4e6f-9fe1-b3d94e6b8346/Details.aspx

Compiler Certification

• USTC, security soft lab.

  • CHEN Yiyun, HUA Baojian, GE Lin, and WANG Zhifang . A pointer logic for safety verification of pointer programs(In Chinese). Chinese Journal of Computers. Vol 31, No. 3, pages 372-380. 2008.

  • CHEN Yiyun, GE Lin , HUA Baojian, LI Zhaopeng, LIU Cheng, and WANG Zhifang. A pointer logic and certifying compiler. 2007.

• Xavier Leroy's work.

  • Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 2008.

  • Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460-475. Springer, 2006.

  • Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languages, pages 42-54. ACM Press, 2006.

• Andrew W. W. Appel, Sandrine Blazy. Separation Logic for Small-step Cminor (extended version), 2007.

• Dirk Leinenbach, Wolfgang Paul, and Elena Petrova. Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In IEEE Conference on Software Engineering and Formal Methods (SEFM’05), 2005.

• J Strother Moore. A mechanically verified language implementation. Journal of Auto mated Reasoning, 5(4):461–492, 1989.

OS Verification

• Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In Proc. 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, Arizona, pages to appear, June 2008. (Certified Operating System)

• Galen C. Hunt and James R. Larus, Singularity: Rethinking the software stack, 2007 (Singularity)

• Michael Hohmuth, and Hendrik Tews. The VFiasco approach for a verified operating system 2005 (VFiasco)

• Mauro Gargano, Mark Hillebrand, Dirk Leinenbach and Wolfgang Paul, On the corrctness of Operating system kernels, 2005 (Verisoft)

• Jonathan Shapiro, Michael Scott Doerrie, Eric Northup, Swaroop Sridhar, and Mark Miller, Towards a verified, General Purpose Operating Sysytem Kernel, 2004 (Coyotos)

• Fred Barnes, Christian Jacobsen and Brian Vinter, Rmox: A Raw-Metal occam Experiment, 2003 (RMox)

• B. Bershad, S. Savage, et. al. Extensibility, Safety and Performance in the SPIN Operating System. 1995 (SPIN)

• William R. Bevier, Kit: A study in Operating Sysytem Verification, 1988 (Kit)

Hypervisor Verification

• Basic idea About hypervisor. see Hypervior and Virtualization.

• Open Robust Infrastructures (Robin Project):

  • Hendrik Tews, Micro hypervisor verification: possible approaches and relevant properties, April 2, 2007.

• The Hypervisor Verification Project, by Microsoft

  • Ernie Cohen, Validating the Microsoft Hypervisor, FM 2006: Formal Methods 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27.

  • Ernie Cohen, The Hypervisor Verification Project, IFIP Working Group 2.3 Programming Methodology, 2007.

• Microsoft's VCC

  • Wolfram Schulte: Experiments in Verifying Low Level Concurrent C Code. ICECCS 2007: 299

• Verisoft XT project , 2008

  • Eyad Alkassar and Wolfgang Paul, On the verification of a ”baby” hypervisor for a RISC machine; draft 0, January, 2008

• CMU, Externally-verifiable Code Execution on Computing System. http://www.cs.cmu.edu/~arvinds/verifiable_code_exec.html

Target Machine

• MIPS

  • Dominic Sweetman. See MIPS Run, Second Edition. Morgan Kaufmann, 2006.

  • Robert Britton. MIPS Assembly Language Programming. Prentice Hall, 2003.

  • GPL. List of MIPS Simulators and Emulators.

• X86

  • Tom Shanley. Protected Mode Software Architecture. Addison Wesley Developers Press, 1997.

  • Frank van Gilluwe. The Undocumented PC, Second Edition. Addison-Wesley, 1997.

  • Timothy R. Butler et. al. Bochs: The Open Source IA-32 Emulation Project.

Related Conference

• POPL, ACM Symposium on Principles of Programming Languages. 2008

• PLDI, CM SIGPLAN Conference on Programming Language Design and Implementation. 2008.

• ICFP , ACM SIGPLAN International Conference on Functional Programming.

• TLDI, ACM SIGPLAN International Workshop on Types in Language Design and Implementation.

• SEFM, IEEE International Conference on Software Engineering and Formal Methods.

• SSV, Systems Software Verification.

• TASE, IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering.