Workshop on Formal Methods for Cryptographic Proofs
12th NASA Formal Methods Symposium (NFM 2020)
Location: Virtual Date: May 15, 2020, 9:15 AM - 3:30 PM Pacific Time Program: Workshop program for 05/15
The recent rapid progress in cryptographic proofs has been driven largely by interest in distributed ledger technology (blockchains). See, for example, SNARKs , Bulletproofs , STARKs , class group accumulators , and DARKs . However, applications of these proof techniques range beyond this area to encompass assurance of proper functioning of components in complex machinery against Byzantine faults, guaranteeing authenticity and validity of distributed sensor readings, enabling decentralized communications, protecting sensitive data while allowing its analysis, and more. While the Boeing 777 and 787 flight control systems, the SpaceX Dragon, and other recent advanced systems incorporate Byzantine fault tolerance into their design, today's newer cryptographic proof techniques enable far more sophistication and space/time efficiency, at the cost of greater software complexity. Formal methods can ensure that the additional complexity does not mean reduced correctness.
Zero knowledge (ZK) proofs comprise one cryptographic proof category of particular interest. A ZK proof allows one party to confirm if another party is aware of a value X without revealing X or any other information besides the other party's awareness of X. The complexity of modern ZK proofs make it hard to detect if the proofs are constructed correctly and if the verification steps of ZK proofs are implemented correctly. An invalid implementation can accept invalid proofs; this can pose serious consequences depending on the application. Correct-by-construction and formally verified implementations are highly desirable.
Recent efforts have successfully brought formal methods to the broader field of cryptography. For instance, the Everest project  implements a formally verified set of cryptographic primitives like ciphers, MACs, elliptic curve signatures, and hash functions exposed via a standard interface. The project may one day provide a drop-in replacement for popular cryptographic toolkits. In the absence of such formal verification, simple implementation bugs have led to severe vulnerabilities in popular cryptographic packages like OpenSSL. The Heartbleed bug  for instance, was a buffer over-read, and a significant number of public facing web-servers were impacted. Efforts to verify memory access allow the full cryptographic stack to be verified.
Even if progress is being made towards verification of cryptographic primitives, higher-level cryptographic proof implementations remain unverified, despite trends accelerating broad adoption of these proofs in the near future. This workshop brings together researchers and practitioners in relevant formal methods—including dependent typing and more—and cryptographic proofs to establish greater interaction between the fields, identify key opportunities of mutual interest, and accelerate the development and adoption of formal methods for cryptographic proofs. Emphasis is further placed on talks and papers that discuss broad cross-cutting themes around cryptographic proofs for Byzantine fault tolerance, data validation, and authentication; practical dependently typed proofs; and other formal methods relevant potentially applicable to cryptographic proofs.REFERENCES:
- : Batching Techniques for Accumulators with Applications to IOPs and Stateless Blockchains IACR Cryptology ePrint Archive: Report 2018/1188. Boneh, Dan. et al.
- : Bulletproofs: Short proofs for confidential transactions and more 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 2018. Bünz, Benedikt et. al.
- : CVE-2014-0160. OpenSSL Heartbleed. Webpage: https://cve.mitre.org/cgi-bin/cvename.cgi?name=cve-2014-0160 Accessed on 11/13/2019
- : Everest: Towards a Verified, Drop-in Replacement of HTTPS Proceedings of the Summit on Advances in Programming Languages (SNAPL). 2017. Bhargavan, Karthikeyan et al.
- : Transparent SNARKs from DARK compilers Cryptology ePrint Archive: Report 2019/1229. Bünz, Benedikt et. al.
- : Scalable, transparent, and post-quantum secure computational integrity IACR Cryptology ePrint Archive 2018 (2018): 46. Ben-Sasson, Eli, et al.
- : Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture 23rd USENIX Security Symposium (USENIX Security 14). 2014. Ben-Sasson, Eli, et al.