CT-ISG: Modular Development of Certified Concurrent Code

CT-ISG：并发汇编代码的模块化验证PCC（Proof-carrying code）是一个通用的框架，原则上可以验证任意机器级程序的安全性。 然而，现有的PCC系统和类型化汇编语言（TAL）只能处理顺序程序。这严重限制了它们的适用性，因为许多现实世界的系统在其核心软件中使用某种形式的并发。 这项研究的重点是开发新的技术，认证低级别的并发程序。该PI还将开发新的教学材料和工具，传播他的研究成果向广大公众。霍尔逻辑可以与假设保证范式相结合的原因，对高层次的并发程序，但它不支持以及低层次的功能，如一流的代码指针，无限的动态线程创建和终止，共享线程之间的代码，和非原子机器代码块。 类型化汇编语言提供了一个更加模块化和可伸缩的框架，但它只能保证简单的类型安全。 拟议的研究将展示如何联合收割机的优势，建立一个强大的新框架，指定，组成，并验证高级属性的低级别并发代码。 本研究的结果将为真实多线程程序的认证提供基础，并对生成携带证明的并发代码取得重要进展。

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.