Committee

  • Andrew Appel (advisor)
  • Aarti Gupta
  • Kyle Jamieson

Title

Verified Forward Erasure Correction with Coq and VST

Abstract

Most methods of data transmission and storage are prone to errors, leading to data loss. Error-correcting codes encode the data with redundant parity information to allow the original data to be recovered even in the presence of a small number of errors. An erasure code uses an ECC to correct erasures, errors where the location is known. There are dozens of classes of error-correcting and erasure codes, many based on sophisticated mathematics, making them difficult to verify using automated tools.

These erasure codes can be implemented in networks as Forward Erasure Correction, in which a sender encodes a block of input packets using an ECC, and the receiver decodes if errors were detected. In this talk, I will describe my verification of a real-world C implementation of FEC using Coq and the Verified Software Toolchain for verifying C programs. This verification includes both a purely-mathematical proof that the underlying algorithm (a form of Reed-Solomon erasure coding) is correct and the VST proof that the C code, over 25 years old and including many modifications and optimizations, correctly implements this algorithm.

Reading List

Papers

Automated Verification of Network Functions

  • Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. Verifast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, Berlin, Heidelberg, 2011. (link)
  • Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea. A Formally Verified NAT. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM ’17, New York, NY, USA, 2017. (link)
  • Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea. Verifying Software Network Functions with No Verification Expertise. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP ’19, New York, NY, USA, 2019. (link)
  • Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. Automated Verification of Customizable Middlebox Properties with Gravel. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), Santa Clara, CA, February 2020. (link)

Reed-Solomon Erasure Codes

  • A. J. McAuley. Reliable Broadband Communication Using a Burst Erasure Correcting Code. In Proceedings of the ACM Symposium on Communications Architectures & Protocols, SIGCOMM ’90, New York, NY, USA, 1990. (link)
  • James S. Plank. A Tutorial on Reed-Solomon Coding for Fault-Tolerance in RAID-like Systems. Software Practice & Experience, 27(9), Sep 1997. (link)

Verification of Error-Correcting Codes

  • Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. In 2016 International Symposium on Information Theory and Its Applications (ISITA), 2016. (link)
  • Manabu Hagiwara, Kyosuke Nakano, and Justin Kong. Formalization of coding theory using lean. In 2016 International Symposium on Information Theory and Its Applications (ISITA), 2016. (link)
  • Mahum Naseer, Waqar Ahmed, and Osman Hasan. Formal Verification of ECCs for Memories Using ACL2. Journal of Electronic Testing, 36, 10 2020. (link)

Textbooks

  1. Software Foundations
    • Volume 1. Logical Foundations (link)
    • Volume 2. Programming Language Foundations (link)
    • Volume 3. Verified Functional Algorithms (link) (through ADT)
    • Volume 5. Verifiable C (link) (through Verif_hash)
  2. Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. (chapters 1-6)

Slides

They can be found here in PDF format.

Questions

(including follow-up questions)
  1. (Appel) What is the Curry-Howard correspondence and how does it relate to Coq? (after I gave some info about proof terms) Can you give an example of a part of a proof term in Coq?
  2. (Jamieson) How does your work (FEC verification) compare to existing projects in Coq? What new techniques, if any, does your project involve? Are there similar efforts related to ECCs or in other domains? Could Gravel verify FEC written using Click? Why or why not? In general, how do these verification methods (Coq + VST) compare with static analysis techniques? When would you want to use one vs another?
  3. (Gupta) How do you know that your FEC specification is correct? In general, how do you know when a specification is complete?
  4. (Appel) Explain what covariance and contravariance are in the context of subtyping with an example. (After I talked about functions in STLC) Go through the same with product types.
  5. (Gupta) What is a first-order theory? Can you give an example? How are these theories used in SMT solvers? (After I gave the theory of equality with uninterpreted functions) What is a decision procedure for this theory?