SAVE: towards a foundation for safe and verified software

今天，软件是我们基础设施的一个组成部分，我们的社会越来越依赖于它的正常功能。虽然我们在创建用于证明程序肤浅属性的软件工具方面取得了实质性进展，但在实现安全和经过验证的软件方面，一个重要的、经常被忽视的方面是编写软件的语言。我们提倡一种全面的方法，它支持对编程语言的操作行为进行建模，并允许我们指定和验证程序的一般安全属性。这个项目的目标是双重的：首先，我们计划继续我们的工作，以实现一个实用的逻辑框架，用于对形式系统建模，特别是编程语言，并机械地检查它们的一些元理论属性。虽然我们已经朝着这个目标取得了实质性的进展，但在安全政策和现实语言的基础上进行快速原型设计和大规模实验仍面临重大挑战。第二，目标是将逻辑框架技术引入主流编程。这将是缩小规范和实际实现之间差距的重要一步，并促进对实际实现的推理。目标是为基于类型理论和逻辑的方法建立理论基础，建立有效的验证和编程工具，并通过实际应用证明其有效性。我们的研究最终有助于建立一个更安全的信息技术基础设施。

Today, software is an integral part of our infrastructure, and our society increasingly depends on its proper functioning. While we have made substantial progress in creating software tools for proving shallow properties of programs, one important, often neglected aspect of achieving safe and verified software is the language in which the software is written. We advocate a comprehensive approach which supports modelling the operational behavior of programming languages and allows us to specify and verify general safety properties about programs.The goal of this project is two-fold: First, we plan to continue our work towards a practical logical framework for modeling formal systems, in particular programming languages, and mechanically checking some of their meta-theoretic properties. While we have made substantial progress towards this goal, there are significant challenges to permit the rapid prototyping and large-scale experiments with safety policies and realistic languages.  Second, the goal is to bring logical framework technology to mainstream programming. This will be an important step towards narrowing the gap between specifications and practical implementations, and facilitate the reasoning about the actual implementation. The objective is to develop a theoretical foundation for the approach based on type theory and logic, build efficient verification and programming tools, anddemonstrate their effectiveness using realistic applications. Our research ultimately contributes towards a safer information technology infrastructure.