SAVE: towards a foundation for safe and verified software

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

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.