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 formal proof (whence “formal methods” WLBF09) 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).
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 medalist 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:
Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John Fitzgerald, Formal methods: Practice and experience, ACM Computing Surveys 41 19 (2009) 1–36 [doi:10.1145/1592434.1592436]
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, 25 Logics and Languages for Reliability and Security (2009)[doi:10.3233/978-1-60750-100-8-1, pdf, pdf]
John Harrison, Formal Verification, Lecture notes Marktoberdorf 2010 [web, pdf, pdf]
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 9036, Springer (2015) [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)
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)
Program verification via Hoare calculus:
For quantum programming languages:
The general idea of verified programming via dependent type theory:
Per Martin-Löf, Constructive Mathematics and Computer Programming, Studies in Logic and the Foundations of Mathematics Volume 104, 1982, Pages 153-175 (doi:10.1016/S0049-237X(09)70189-2)
Thomas Streicher, p. 1-2 of: Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993) [pdf, pdf]
Exposition:
Software verification via dependent type theory (such as in Coq or Agda):
Adam Chlipala, Implementing Certified Programming Language Tools in Dependent Type Theory, Berkeley (2007) [UCB/EECS-2007-113, 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)
On Agda as a dependently typed certification language:
Verification of (blockchain-like) hashgraph consensus algorithms:
Background:
Pierre Tholoniat, Vincent Gramoli, Formal Verification of Blockchain Byzantine Fault Tolerance, in Handbook on Blockchain, Optimization and Its Applications 194, Springer (2022) [arXiv:1909.07453, doi:10.1007/978-3-031-07535-3_12]
Leemon Baird, Mance Harmon, and Paul Madsen, Hedera: A Public Hashgraph Network & Governing Council, (last update 2020) [pdf]
With Coq:
Hedera blog: Coq Proof Completed By Carnegie Mellon Professor Confirms Hashgraph Consensus Algorithm Is Asynchronous Byzantine Fault Tolerant (Oct 2018)
Hedera blog: Formal Methods: The Importance of Being Fault Tolerant in a World with Bad Actors (2018)
Leemon Baird: Formal Methods: A Deep Dive Using the Coq Proof Assistant – Hedera18 (2018) [video: YT]
Matthew Salazar, Consensus, Blockchain and Proof Assistants (2018) [pdf, pdf]
Karl Crary, Formalizing the Hashgraph gossip protocol, talk at CyLab Partners Conference (2019) [pdf]
Karl Crary, Verifying the Hashgraph Consensus Algorithm [arXiv:2102.01167, pdf]
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, Grigore Roşu, Towards a Verified Model of the Algorand Consensus Protocol in Coq, Formal Methods. FM 2019 International Workshops. Lecture Notes in Computer Science 12232 (2019) 362-367 [arXiv:1907.05523, doi:10.1007/978-3-030-54994-7_27]
With Agda:
See also:
Bas Spitters, Formal verificaton at Concordium Blockchain Research Center
Søren Eller Thomsen, Bas Spitters, Formalizing Nakamoto-Style Proof of Stake [eprint:2020/917]
1st Workshop on Formal Methods for Blockchains(October 2019)
Quantstamp blog: Formally Verifying Hedera Hashgraph’s Stablecoin Framework (2020)
Sudhani Verma; Divakar Yadav; Girish Chandra, Introduction of Formal Methods in Blockchain Consensus Mechanism and Its Associated Protocols, IEEE Access 10 (2022) [doi:10.1109/ACCESS.2022.3184799, pdf]
Quantstamp blog: Applying lightweight formal methods and SAT solvers to build better blockchain applications (July 2023)
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)
Explicitly using type equivalences:
First, on the problem of debugging quantum programs, as maybe first highlighted by VRSAS 2015, Rand (2018) and Ying & Feng (2018):
Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, Jonathan M. Smith, Programming the quantum future, Communications of the ACM 58 8 (2015) 52–61 [doi:10.1145/2699415, pdf, web, promo vid:YT]
[p 6:] “In quantum computation, the cost of debugging is likely to be quite high. To begin with, observing a quantum system can change its state. A debugger for a quantum program would therefore necessarily give incomplete information about its state when run on actual quantum hardware. The alternative is to use a quantum simulator for debugging. But this is not practical due to the exponential cost of simulating quantum systems. Moreover, it can be expected that the initial quantum computers will be rare and expensive to run and therefore that the cost of runtime errors in quantum code will initially be much higher than in classical computing. This shifts the cost-benefit analysis for quantum programming toward strong compile-time correctness guarantees, as well as formal specification and verification.”
(with an eye towards Quipper)
Andriy Miranskyy, Lei Zhang, Javad Doliskani, Is Your Quantum Program Bug-Free?, in ICSE-NIER ‘20: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: New Ideas and Emerging Results (2020) 29–32 [arXiv:2001.10870, doi:10.1145/3377816.3381731]
“The classical parts of a quantum program can be debugged using traditional methods. The quantum parts, however, can not be treated in the same way because of the properties of a QC – such as superposition, entanglement, and no-cloning – which are governed by the laws of quantum mechanics. The purpose of debugging a program is to present the user with human readable, i.e., classical, information about the runtime state of the system. Extracting classical information from a quantum state is done using measurement which is usually a non-unitary operation and results in collapse of the state, and hence an unintended behavior of the program.”
On formal verification of quantum computing with/of quantum programming languages:
general:
Mingsheng Ying, Yuan Feng, Model Checking Quantum Systems — A Survey [arXiv:1807.09466]
“But to check whether a quantum system satisfies a certain property at a time point, one has to perform a quantum-measurement on the system, which can change the state of the system. This makes studies of the long-term behaviours of quantum systems much harder than that of classical system.”
“The state spaces of the classical systems that model-checking algorithms can be applied to are usually finite or countably infinite. However, the state spaces of quantum systems are inherently continuous even when they are finite-dimensional. In order to develop algorithms for model-checking quantum systems, we have to exploit some deep mathematical properties of the systems so that it suffices to examine only a finite number of (or at most countably infinitely many) representative elements, e.g. those in an orthonormal basis, of their state spaces.”
(repeated in Ying & Feng (2021, Sec. 1.3))
Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying, Model Checking Applied to Quantum Physics [arXiv:1902.03218]
Mingsheng Ying, Yuan Feng, Model Checking Quantum Systems – Principles and Algorithms, Cambridge University Press (2021) [ISBN:9781108484305]
Christophe Chareton, Sébastien Bardin, Dongho Lee, Benoît Valiron, Renaud Vilmart, Zhaowei Xu, Formal Methods for Quantum Programs: A Survey, in: Handbook of Formal Analysis and Verification in Cryptography, CRC (2023) [arXiv:2109.06493, doi:10.1201/9781003090052]
Marco Lewis, Sadegh Soudjani, Paolo Zuliani, Formal Verification of Quantum Programs: Theory, Tools and Challenges [arXiv:2110.01320]
“Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware.”
Carmelo R. Cartiere, Formal Methods for Quantum Software Engineering, in: Quantum Software Engineering, Springer (2022) [doi:10.1007/978-3-031-05324-5_5]
“The characteristic difficulty in creating pure quantum software is mainly due to the inaccessibility to intermediate states, which makes debugging practically impossible. However, the use of formal methods, which apply rigorous mathematical models to ensure error-free software, can overcome this barrier and enable the production of reliable quantum algorithms and applications right out of the box.”
with QML:
with QPMC:
Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang, QPMC: A Model Checker for Quantum Programs and Protocols, in Formal Methods. FM 2015, Lecture Notes in Computer Science 9109, Springer (2015) [doi:10.1007/978-3-319-19249-9_17]
“In practice, however, security analysis of quantum cryptographic protocols is notoriously difficult; for example, the manual proof of BB84 in [15] contains about 50 pages. It is hard to imagine such an analysis being carried out for more sophisticated quantum protocols. Thus, techniques for automated or semi-automated verification of these protocols will be indispensable.”
Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)
Robert Rand, Formally Verified Quantum Programming, UPenn (2018) [ediss:3175]
[p. iv:] “We argue that quantum programs demand machine-checkable proofs of correctness. We justify this on the basis of the complexity of programs manipulating quantum states, the expense of running quantum programs, and the inapplicability of traditional debugging techniques to programs whose states cannot be examined.”
[p. 3:] “Quantum programs are tremendously difficult to understand and implement, almost guaranteeing that they will have bugs. And traditional approaches to debugging will not help us: We cannot set breakpoints and look at our qubits without collapsing the quantum state. Even techniques like unit tests and random testing will be impossible to run on classical machines and too expensive to run on quantum computers – and failed tests are unlikely to be informative”
[p. 4:] “Thesis Statement: Quantum programming is not only amenable to formal verification: it demands it.”
“The overarching goal of this thesis is to write and verify quantum programs together. Towards that end, we introduce a quantum programming language called Qwire and embed it inside the Coq proof assistant. We give it a linear type system to ensure that it obeys the laws of quantum mechanics and a denotational semantics to prove that programs behave as desired.”
Further development SQIR:
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks, A verified optimizer for Quantum circuits, Proceedings of the ACM on Programming Languages 5 Issue POPL 37 (2021) 1–29 [doi:10.1145/3434318]
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks, Proving Quantum Programs Correct, in 12th International Conference on Interactive Theorem Proving (ITP 2021), Leibniz International Proceedings in Informatics (LIPIcs) 193 (2021) [arXiv:2010.01240]
Kesha Hietala, A verified software toolchain for quantum programming (2022) [pdf, blog]
See also:
Jaap Boender, Florian Kammüller, Rajagopal Nagarajan, Formalization of Quantum Protocols using Coq, EPTCS 195 (2015) 71-83 [doi:10.4204/EPTCS.195.6, doi:10.4204/EPTCS.195.6]
(via Coq)
Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng, Symbolic Reasoning about Quantum Circuits in Coq, Journal of Computer Science and Technology (JCST), 36 6 (2021) 1291-1306 arXiv:2005.11023, doi:10.1007/s11390-021-1637-9
Mingsheng Ying, Model Checking for Verification of Quantum Circuits, in: Formal Methods. FM 2021, Lecture Notes in Computer Science 13047, Springer (2021) arXiv:2104.11359, doi:10.1007/978-3-030-90870-6_2
Mingsheng Ying, Zhengfeng Ji, Symbolic Verification of Quantum Circuits, arXiv:2010.03032
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying, CoqQ: Foundational Verification of Quantum Programs, Proceedings of the ACM on Programming Languages 7 POPL 09 (2023) 29 833–865 [arXiv:2207.11350, doi:10.1145/3554343]
(in Coq)
Via Hoare logic:
Projects:
See also
J. Pau Roth, Hardware Verification, IEEE Transactions on Computers C 26 12 (1977) [doi:10.1109/TC.1977.1674795]
Paolo Camurati, Paolo Prinetto, Formal Verification of Hardware Correctness: Introductions and Survey of Current Research, ComputerVolume 21 7 (1988) [doi:10.1109/2.65, Computer-doi:10.1109/2.65, pdf]
Aarti Gupta, Formal Hardware Verification Methods: A survey, Formal Methods in System Design 1 (1992) 151-238 [doi:10.1007/BF00121125, pdf]
Sharad Malik, Hardware Verification: Techniques, Methodology and Solutions, in Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008, Lecture Notes in Computer Science 4963 [doi:10.1007/978-3-540-78800-3_1]
See also:
Wikipedia, Hardware verification language
Oxford University CS Department: Hardware verification
On hardware verification using proof assistants:
On hardware verification of quantum computing-systems:
Last revised on February 26, 2024 at 12:41:54. See the history of this page for a list of all contributions to it.