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: TBA (1-day workshop during May 11-15, 2020)

Summary:

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.

Important Dates:

  • Mar. 06, 2020: Submission deadline (by email to fmcp@onai.com)
  • Mar. 11, 2020: Notification of acceptance
  • May 11-15, 2020: NFM 2020

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 06-Mar-2020 by email (to fmcp@onai.com) in PDF format. Accepted submissions will be notified by email on 11-Mar-2020.

Accepted papers will be displayed in a poster session. Select papers will be chosen for an oral presentation.

Links:

Contact:

fmcp@onai.com

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: