CT-ISG: Modular Development of Certified Concurrent Code

摘要：PCC （proof -carrying code）是原则上可以验证任意机级程序安全特性的通用框架。然而，现有的PCC系统和类型化汇编语言（TAL）只能处理顺序程序。这严重限制了它们的适用性，因为许多现实世界的系统在其核心软件中使用某种形式的并发。本研究的重点是开发低级并发程序认证的新技术。私家侦探还将开发新的教材和工具，向公众传播他的研究成果。Hoare逻辑可以与假设-保证范式相结合来推断高级并发程序，但它不能很好地支持低级功能，如一等代码指针、无界动态线程创建和终止、线程之间的代码共享和非原子机器码块。类型化汇编语言提供了一个更加模块化和可伸缩的框架，但它只能证明简单类型的安全性。建议的研究将展示如何结合两者的优势来构建一个强大的新框架，用于指定、组合和验证低级并发代码的高级属性。本研究的结果将为验证现实的多线程程序提供基础，并在生成携带证明的并发代码方面取得重要进展。

ABSTRACT0524545Zhong ShaoYale UniversityCT-ISG: Modular Verification of Concurrent Assembly CodeProof-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.