BP: Formal Proofs, the Fine Print and Side Effects
T Murray, Paul Van Oorschot
IEEE | Published : 2018
Given recent high-profile successes in formal verification of security-related properties (e.g., for seL4), and the rising popularity of applying formal methods to cryptographic libraries and security protocols like TLS, we revisit the meaning of security-related proofs about software. We re-examine old issues, and identify new questions that have escaped scrutiny in the formal methods literature. We consider what value proofs about software systems deliver to end-users (e.g., in terms of net assurance benefits), and at what cost in terms of side effects (such as changes made to software to facilitate the proofs, and assumption-related deployment restrictions imposed on software if these pro..View full abstract
We thank David Basin, Virgil Gligor, Cormac Herley, Benjamin Pierce and John Regehr for insightful feedback, and anonymous referees. The second author is Canada Research Chair in Authentication and Computer Security, and acknowledges NSERC for funding the chair and a Discovery Grant.