SHF: Small: Automating Software Verification using Natural Proofs

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

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).