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

Background:

The recent rapid progress in cryptographic proofs has been driven largely by interest in distributed ledger technology (blockchains). See, for example, SNARKs [6], Bulletproofs [1], STARKs [5], class group accumulators [0], and DARKs [4]. 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 [3] 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 [2] 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: