CAREER: A Formal Verification Platform Focused on Programmer Productivity

CAREER：专注于程序员生产力的正式验证平台

• 批准号: 1253229
• 负责人: Adam Chlipala
• 金额: $ 52万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-06-01 至 2018-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1253229&HistoricalAwards=false
• 关键词: CAREER; Formal; Verification; Platform; Focused

Billions of people depend daily on software systems built on top of slowly changing operating systems, programming languages, and library interfaces. A unifying theme of this infrastructure, from operating systems to Web browsers, is the use of nested sandboxes, involving multiple levels of abstraction, with complete mediation of resource accesses within and across levels. That is, as a program runs, several layers of abstraction are checking all resource accesses for conformance to security and isolation policies. This run-time checking imposes substantial overhead and is also quite inflexible. Often some sandbox layer is fundamentally incompatible with a new programming technique that could bring improved performance, security, etc. We will study how the Bedrock system may be used to replace restrictive run-time policy enforcement with open-ended compile-time policy enforcement, by requiring programmers to distribute code with formal mathematical proofs of policy conformance. As a concrete case study, we will implement a platform to replace today's common combinations of cloud hosting and Web browsers, providing a similar application experience to end users while giving programmers much more flexibility. To educate the future users of our tools, we will also develop an online tutor program suitable for use in introductory discrete math and logic classes, giving students instant feedback on the validity of their rigorous proofs.The theoretical foundation of Bedrock, a Coq library, is higher-order separation logic for assembly languages. Several past projects have demonstrated how proofs in such logics may be carried out using proof assistants. Bedrock is distinguished by providing tools for mostly automated proofs, where the programmer provides help to the verifier through loop invariants and a few other types of annotation. We will continue improving this automation support to lower the human cost of verification further, while also investigating ways to broaden Bedrock's domain, such as to multi-core programs. We also intend to investigate the new semantic idea of phantom monitors, which allow Bedrock programs to spawn arbitrary automata (defined with their transition relations in Coq) that watch all program behavior and may veto actions that violate some policy. This is a compile time-only feature to support effective specifications, and we hope to use it as a unifying framework for specifying the interfaces between components in our proof-of-concept distributed application platform.

数十亿人每天依赖于构建在缓慢变化的操作系统、编程语言和库接口之上的软件系统。从操作系统到 Web 浏览器，该基础设施的一个统一主题是使用嵌套沙箱，涉及多个抽象级别，并完全协调级别内和级别之间的资源访问。也就是说，当程序运行时，多个抽象层会检查所有资源访问是否符合安全和隔离策略。这种运行时检查会带来大量开销，而且非常不灵活。通常，某些沙箱层与新的编程技术根本不兼容，而新的编程技术可以带来性能、安全性等方面的改进。我们将研究如何使用基岩系统以开放式编译时策略实施来取代限制性运行时策略实施，要求程序员分发具有策略一致性的正式数学证明的代码。作为一个具体的案例研究，我们将实现一个平台来取代当今云托管和 Web 浏览器的常见组合，为最终用户提供类似的应用程序体验，同时为程序员提供更大的灵活性。为了教育我们工具的未来用户，我们还将开发一个适合在离散数学和逻辑入门课程中使用的在线导师程序，为学生提供有关其严格证明有效性的即时反馈。Bedrock（Coq 库）的理论基础，是汇编语言的高阶分离逻辑。过去的几个项目已经演示了如何使用证明助手来执行此类逻辑的证明。 Bedrock 的特点是提供大多数自动化证明的工具，程序员通过循环不变量和一些其他类型的注释为验证者提供帮助。我们将继续改进这种自动化支持，以进一步降低验证的人力成本，同时还会研究扩大 Bedrock 领域的方法，例如多核程序。我们还打算研究幻像监视器的新语义概念，它允许 Bedrock 程序生成任意自动机（用 Coq 中的转换关系定义）来监视所有程序行为，并可能否决违反某些策略的操作。这是一个仅编译时的功能，用于支持有效的规范，我们希望将其用作统一框架，用于指定我们的概念验证分布式应用程序平台中组件之间的接口。