iProve: A Scalable Approach to Consumer-Verifiable Software Guarantees

Formally proving complex program properties is still considered impractical for systems with over a million lines of code (MLOC). We present iProve, an approach that enables the generation and verification of proofs for interesting program properties in large Java systems. Desired properties are proven in iProve as a combination of two proofs: one of a complex property applied to a very tiny part of the code—a nucleus—and a proof of a simple property applied to the rest of the code—the body. We use iProve to prove properties such as communication security, deadlock immunity, data privacy, and resource usage bounds in Java programs with millions of LOC. iProve scales well, requires no access to source code, and allows nuclei to be reused with an unlimited number of systems and to be written in verification-friendly languages.