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浏览器的常见组合，从而为最终用户提供类似的应用程序体验，同时为程序员提供更大的灵活性。为了教育我们工具的未来用户，我们还将开发一个在线导师计划，适合于入门的离散数学和逻辑类别，从而为学生提供了严格证明的有效性的即时反馈。COQ图书馆Bedrock的理论基础是汇编语言的高级分离逻辑。过去的几个项目已经证明了如何使用证明助手进行此类逻辑中的证据。 BedRock通过为大多数自动证明的工具提供工具来区分，程序员通过循环不变性和其他一些类型的注释为验证者提供帮助。我们将继续改善这种自动化支持，以进一步降低人类的验证成本，同时还调查了扩大基岩领域的方法，例如多核计划。我们还打算调查幻影监视器的新语义概念，该想法使基地计划可以催生任意自动机（与COQ中的过渡关系定义），该概念观察所有程序行为，并可能否决违反某些政策的行动。这是一项仅适用于有效规格的典型功能，我们希望将其用作统一的框架，以指定我们概念验证的分布式应用程序平台中组件之间的接口。