SHF: Small: Automating Software Verification using Natural Proofs

软件的自动算法验证，即使在程序员用不变量注释辅助的情况下，今天也陷入了僵局，因为底层的技术问题无法用计算机解决（无法确定）。因此，当前的工具在大多数非浅层的软件规范中表现很差，这些规范不承认可确定的验证，因此在整个验证过程中需要人工帮助。这导致未受过正式方法培训的程序员对这些工具的采用受到限制。这个项目通过一种叫做自然证明的新方法来解决这个问题。自然证明是证明的一个子类，它可以被有效地搜索，并且体现了人们使用的通用策略，并且适用于大多数程序。因此，自然证明产生了在大多数情况下工作的自动（尽管不完整）技术，避开了不可判定性障碍。该项目的目标是构建用于验证各种安全属性的自然证明技术，包括跨越整个系统的隐私、完整性和访问控制，并帮助程序员以很少的注释开销来验证他们的程序。应用程序包括对软件安全属性的更多自动验证，例如Android平台，以及大规模开放在线课程（MOOCs）中可扩展的编程练习自动评分。

The automated algorithmic verification of software, even when assisted by programmer annotations with invariants, is at an impasse today because the underlying technical problems are not solvable using computers (undecidable). Consequently, current tools perform very poorly for most non-shallow specifications of software, which do not admit decidable verification, and hence require manual help throughout the verification process. This has lead to limited adoption of these tools by the wider population of programmers untrained in formal methods. This project addresses this problem through a new radical approach called natural proofs. Natural proofs are a subclass of proofs that can be effectively and efficiently searched for, and embody common tactics that people use and that work for most programs. Natural proofs hence yield automatic though incomplete techniques that work in most situations, side-stepping undecidability barriers. The project's goal is to build natural proof techniques for the verification of a variety of security properties, including privacy, integrity, and access control, that span across entire systems, and that help programmers verify their programs with very little annotation overhead. Applications include more automated verification of security properties of software, such as an Android platform, as well as scalable auto-grading of programming exercises in Massive Open Online Courses (MOOCs).