CAREER: A Formal Verification Platform Focused on Programmer Productivity

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

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.