CT-ISG: Modular Development of Certified Concurrent Code

Yale University, New Haven CT

Investigators

Abstract

ABSTRACT 0524545 Zhong Shao Yale University CT-ISG: Modular Verification of Concurrent Assembly Code Proof-carrying code (PCC) is a general framework that can in principle verify safety properties of arbitrary machine-level programs. Existing PCC systems and typed assembly languages (TAL), however, can only handle sequential programs. This severely limits their applicability since many real-world systems use some forms of concurrency in their core software. This proposed research focuses on developing new techniques for certifying low-level concurrent programs. The PI will also develop new instructional material and tools for disseminating his research results to the general public. Hoare logic can be combined with the assume-guarantee paradigm to reason about high-level concurrent programs but it does not support well low-level features such as first-class code pointers, unbounded dynamic thread creation and termination, sharing of code between threads, and non-atomic machine code blocks. Typed assembly language provides a more modular and scalable framework but it can certify simple type safety only. The proposed research will show how to combine the strengths of the two to build a powerful new framework for specifying, composing, and verifying advanced properties on low-level concurrent code. The results from this research will provide a foundation for certifying realistic multi-threaded programs and make an important advance toward generating proof-carrying concurrent code.