Difference between revisions of "TACL Seminar Spring '05"
m (→Dan Wang)
m (→Dinghao Wu)
|Line 44:||Line 44:|
Revision as of 15:29, 15 August 2006
|Feb 9||Dan Wang||Opportunities and Challenges in End-to-End Verification of Software Systems||Abstract|
|Feb 10||Dinghao Wu||Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code||Abstract|
|Feb 16||Gang Tan||Structured Verification of Unstructured Machine Code||Abstract|
|Feb 23||NJ PLS|
|Mar 2||Xinming Ou||MulVAL: An Automatic Network Vulnerability Analyzer||Abstract|
|Mar 9||George Reis||SWIFT: Software Implemented Fault Tolerance||Abstract|
|Mar 16||Bolei Guo||Low-Level Pointer Analysis||Abstract|
|Mar 23||Dominic Duggan - Stevens|
|Mar 28||Neal Glew - Intel Research||Inlining, Dynamic Loading and Type Safety||Abstract|
|Apr 6||Neil Vachharajani||Opportunities for Coarse-Grained Parallel Execution||Abstract|
|Apr 13||Yitzhak Mandelbaum||A Calculus for Specifying Ad Hoc Data Formats||Abstract|
|Apr 22||IBM PL Day|
|Apr 27||Rob Simmons||Metatheoretic Approaches to Formalizing High-level Languages||Abstract|
|May 25||Aarti Gupta - NEC||Verifying C Programs by Model Checking||Abstract|
Opportunities and Challenges in End-to-End Verification of Software Systems
I'll start out by taking a brief tour that covers my past experience on various projects and how those experiences shape my current view of the importance and practicality of end-to-end system verification. My basic thesis is that end-to-end system verification is theoretically/technically possible, but often *economically* impractical. More importantly the marketplace for verified software systems is likely to significantly expand within this century.
I'll will also discuss on going research in developing simpler and flexible semantic techniques for the verification of Foundational Proof-Carrying code systems. In particular, I will discuss how to build proofs of type soundness using higher-order abstract encodings of syntax without the need for meta-logical approaches to soundness.
Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code
Proof-Carrying Code (PCC) is a general framework for the mechanical verification of safety properties of machine-language programs. It allows a code producer to provide an executable program to a code consumer, along with a machine-checkable proof of safety such that the code consumer can check the proof before running the program. A weakness of previous PCC systems is that the proof-checking infrastructure is based on some complicated logic that is not necessarily sound.
Foundational Proof-Carrying Code (FPCC) aims to build the safety proof based on the simple and trustworthy foundations of mathematical logic. There are three major components in an FPCC system: a compiler, a proof checker, and the safety proof of an input machine-language program. The compiler should produce machine code accompanied by a proof of safety. The proof checker verifies, sometimes also discovers, the safety proof before the program gets executed. We have built an end-to-end FPCC system. Our prototype system compiles Core ML programs to SPARC code, accompanied with programs in a low-level typed assembly language; these typed assembly programs serve as the proof witnesses of safety of the corresponding SPARC machine code. Our Flit proof checker includes a simple logic programming engine enabling efficient proof-checking.
In this talk, I'll present the design of interfaces between these components and show how to build an end-to-end FPCC system. We have come to the conclusion that: (1) a type system (a low-level typed assembly language) should be designed to check machine code; (2) the proof-checking should be factored into two stages, namely typechecking of the input machine code and verification of soundness of the type system. Since a type checker can be efficiently interpreted as a logic program, Flit's logic programming engine enables efficient proof-checking.
I'll also briefly present my research on software model checking and program verification.