Workshop on Formal Methods for Cryptographic Proofs
12th NASA Formal Methods Symposium (NFM 2020)
Location: NASA Ames Research Center, Moffett Field, CA, USA
Conference Dates: May 15, 2020
COVID-19 AND ONLINE PARTICIPATION UPDATE:
In view of the COVID-19 situation, we are moving this workshop to a primarily online format. We realize attendees, particularly those traveling internationally, need to finalize travel plans and so we want to be proactive about this decision. Here are the possible routes we will take based on what happens with the parent NFM2020 Symposium:
IF NFM2020 PROCEEDS AS SCHEDULED: If the parent NFM2020 proceeds normally, then we will still have an in-person component to our workshop for those that wish to meet up. But, regardless, we will have an online platform and support video participation from anywhere.
IF NFM2020 IS CANCELLED: We'll still hold our online workshop as planned.
IF NFM2020 IS DELAYED TO LATER THIS YEAR: We may delay the workshop to match the new NFM dates.
Recent and emerging cryptographic proof techniques allow proofs of sufficiently complicated properties that it has become desirable to formally verify that the proofs indeed prove what they intend. This is an exciting new application area for verification. This workshop brings together practitioners from formal methods and cryptography, exploring opportunities and challenges at the intersection of formal methods and cryptographic proofs.
- Mar. 19, 2020: Submission deadline (by email to firstname.lastname@example.org)
- Mar. 26, 2020: Notification of acceptance
- May 15, 2020: NFM 2020
- Non US Citizens and Non Permanent Residents must allow minimum 4 weeks for a background check. Register and provide your visa information ASAP.
Call for Papers:
We invite paper submissions potentially relevant to the application of formal methods to cryptographic proofs. This workshop is held in conjunction with the NASA Formal Methods conference in May 2020. Workshop focus areas include, but are not limited to, the following. Submissions are single-blind.
- Formal methods that can assist construction of cryptographic proofs.
- Practical dependently typed proofs.
- Emerging cryptographic proof techniques that will benefit from formal methods.
- Implementations, opportunities, and urgent focus areas.
Submissions are due 19-Mar-2020 by email (to email@example.com) in PDF format. Accepted submissions will be notified by email on 26-Mar-2020.
Accepted papers will be displayed in a poster session. Select papers will be chosen for an oral presentation.
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.