natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A certification or formal verification of a computer program is a formalized guarantee – a proof – that the program has given specified properties. For instance, it could be guaranteed to compute a given output based on a given input, or to always terminate, or to not include a certain kind of security hole.
Certifications often take the form of a proof that a program, regarded as a term of some sort (under programs as proofs), has a specified type. Thus, programming languages based on highly expressive type theories (including dependent types) are a natural place to do certified programming “natively”. Examples are Coq and Agda. In this case, the program is written at the same time as a proof of its certification. One often then wants to “extract” the executable code or “ignore” the proof part of the terms when actually running the code, for performance reasons; Coq and Agda include mechanisms designed for this.
It is also possible to write a program in some less strongly typed language and provide an “external” certification for it, rather than one built into the program itself. Computer proof assistants like Coq and Agda are also used for this, using a formal representation of some other programming language. There are also other program analysis tools which can produce automated proofs of certain aspects of a computer program, such as safety and termination (although of course a complete solution to termination-checking is impossible, being the halting problem).
So far, fully certified programming in the type-theoretic sense is largely an academic endeavor, see for instance (SpittersKrebbersvdWeegen); the tools available at present usually require too much time and effort to be worth the payoff in industry. As automation progresses, this may change.
From Ghani et al. 15:
The cost of software failure is truly staggering. Well known individual cases include the Mars Climate Orbiter failure (£80 million), Ariane Rocket disaster (£350 million), Pentium Chip Division failure (£300 million), and more recently the heartbleed bug (est. £400 million). There are many, many more examples. Even worse, failures such as one in the Patriot Missile System and another in the Therac-25 radiation system have cost lives. More generally, a 2008 study by the US government estimated that faulty software costs the US economy £100 billion annually.
There are many successful approaches to software verification (testing, model checking etc). One approach is to find mathematical proofs that guarantees of software correctness. However, the complexity of modern software means that hand-written mathematical proofs can be untrustworthy and this has led to a growing desire for computer-checked proofs of software correctness. Programming languages and interactive proof systems like Coq, Agda, NuPRL and Idris have been developed based on a formal system called Martin-Löf type theory. In these systems, we can not only write programs, but we can also express properties of programs using types, and write programs to express proofs that our programs are correct.
In this way, both large mathematical theorems such as the Four Colour Theorem, and large software systems such as the CompCert C compiler have been formally verified. However, in such large projects, the issue of scalability arises: how can we use these systems to build large libraries of verified software in an effective way?
This is related to the problem of reusability and modularity: a component in a software system should be replaceable by another which behaves the same way even though it may be constructed in a completely different way. That is, we need an “extensional equality” which is computationally well behaved (that is, we want to run programs using this equality). Finding such an equality is a fundamental and difficult problem which has remained unresolved for over 40 years.
But now it looks like we might have a solution! Fields medallist Vladimir Voevodsky has come up with a completely different take on the problem by thinking of equalities as paths such as those which occur in one of the most abstract branches of mathematics, namely homotopy theory, leading to Homotopy Type Theory (HoTT). In HoTT, two objects are completely interchangeable if they behave the same way. However, most presentations of HoTT involve axioms which lack computational justification and, as a result, we do not have programming languages or verification systems based upon HoTT. The goal of our project is to fix that, thereby develop the first of a new breed of HoTT-based programming languages and verification systems, and develop case studies which demonstrate the power of HoTT to programmers and those interested in formal verification.
Introduction:
Patrick Cousot, Radhia Cousot, A gentle introduction to formal verification of computer systems by abstract interpretation, NATO Science for Peace and Security Series - D: Information and Communication Security, Volume 25: Logics and Languages for Reliability and Security (2009)(doi:10.3233/978-1-60750-100-8-1)
Catherine Meadows, Program Verification and Security (doi:10.1007/978-1-4419-5906-5_863), In: Henk C. A. van Tilborg, Sushil Jajodia (ed.) Encyclopedia of Cryptography and Security Springer (2011)
Bas Spitters, Robberts Krebbers, Eelis van der Weegen, From computational analysis to thoughts about analysis in HoTT, MAP International spring school on formalization of Mathematics (2012) (pdf)
See also:
Sources listing real-world issues programming issues that might motivate verification of software include
Thomas Huckle, Tobias Neckel, Bits and Bugs: A Scientific and Historical Review on Software Failures in Computational Science, SIAM 2019 (doi:10.1137/1.9781611975567)
Computerworld, Top software failures in recent history, Feb 17, 2020
Wikipedia, List of software bugs
Software verification for cryptography:
Mihhail Aizatulin, Franccois Dupressoir, Andrew D. Gordon, Jan Jürjens, Verifying Cryptographic Code in C: Some Experience and the Csec Challenge (pdf)
Mihhail Aizatulin, Andy Gordon, Jan Jürjens, Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution, CCS ‘11 Proceedings of the 18th ACM Conference on Computer and Communications Security 2011 (pdf)
Matthias Berg, Formal Verification of Cryptographic Security Proofs, 2013 (pdf, doi:10.22028/D291-26528)
Adam Petcher, A Foundational Proof Framework for Cryptography, 2014 (pdf, harvard:17463136)
Adam Petcher, Greg Morrisett, The Foundational Cryptography Framework, In: R. Focardi, A. Myers (eds.) Principles of Security and Trust POST 2015. Lecture Notes in Computer Science, vol 9036. Springer, Berlin, Heidelberg (doi:10.1007/978-3-662-46666-7_4)
Andrew W. Appel, Verification of a Cryptographic Primitive: SHA-256, ACM Transactions on Programming Languages and SystemsApril 2015 Article No.: 7 (doi:10.1145/2701415, pdf)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala, Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises, 2019 IEEE Symposium on Security and Privacy (SP) (doi:10.1109/SP.2019.00005)
Mihhail Aizatulin, Verifying Cryptographic Security Implementations in C Using Automated Model Extraction (arXiv:2001.00806)
The general idea of verified programming via (dependent type theory):
Exposition:
Verification of cryptography via type theory:
Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon, Cryptographic Verification by Typing for a Sample Protocol Implementation, In: Aldini A., Gorrieri R. (eds) Foundations of Security Analysis and Design VI. FOSAD 2011. Lecture Notes in Computer Science, vol 6858. Springer (2011) (doi:10.1007/978-3-642-23082-0_3)
Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub, Modular code-based cryptographic verification, CCS ‘11: Proceedings of the 18th ACM conference on Computer and communications securityOctober 2011 Pages 341–350 (doi:10.1145/2046707.2046746)
Software verification via dependent type theory (such as in Coq):
Adam Chlipala, Implementing Certified Programming Language Tools in Dependent Type Theory PhD (2007) (pdf, web)
Adam Chlipala, Certified programming with dependent types, MIT Press 2013 (ISBN:9780262026659, pdf, book webpage)
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg, Dependent Type Theory for Verification of Information Flow and Access Control Policies, ACM Transactions on Programming Languages and Systems July 2013 Article No.: 6 (doi:10.1145/2491522.2491523)
Proposals for verification specifically via homotopy type theory:
Neil Ghani, Conor McBride, EPSRC research grant Homotopy Type Theory: Programming and Verification, 2015
Klaus Mainzer, From Proof Theory to Proof Assistants – Challenges of Responsible Software and AI, talk at Arbeitstagung Bern-München, ABM Spring 2019 (pdf, pdf)
Klaus Mainzer, Proof and Computation. Perspectives for Mathematics, Computer Science, and Philosophy, Chapter 1 in: Klaus Mainzer, Peter Schuster, Helmut Schwichtenberg (eds.), Proof and Computation II – From Proof Theory and Univalent Mathematics to Program Extraction and Verification, World Scientific 2021 (doi:10.1142/12263)
and here again specifically for cryptography:
Paventhan Vivekanandan, A Homotopical Approach to Cryptography, talk at FCS 2018 (pdf, easychair:GLtQ#), In: Charles Morisset and Limin Jia (eds.) FCS Informal Proceedings 55 (2018)
Paventhan Vivekanandan, HoTT-Crypt: A Study in Homotopy Type Theory based on Cryptography, Kalpa Publications in Computing Volume 9, 2018, Pages 75-90 (doi:10.29007/tvpp, web slides, pdf)
Verification for quantum programming languages
with Quipper:
Last revised on May 12, 2021 at 08:20:23. See the history of this page for a list of all contributions to it.