Markdown Version | Session Recording

Session Date/Time: 24 May 2023 15:00

UFMRG

Summary

The UFMRG interim meeting focused on initial presentations of formal methods research and tools, discussing their applicability and usability within the IETF context. Key discussions included a tool for verifying state-separating proofs, an engineer's experience applying formal methods to a DNS component, the proposal of IMAP SEARCH as a sample problem for the research group, and a detailed exploration of usability challenges in formal methods. A sense of those present indicated strong support for developing and documenting sample problems and training materials to improve tool accessibility and adoption.

Key Discussion Points

• SSP verif (Jan):

  • Presented SSP verif, a tool for modularizing computational cryptographic security proofs, specifically for State-Separating Proofs (SSP).
  • Aims to bridge modular SSP proofs with monolithic security definitions (e.g., HPKE).
  • The tool takes pseudocode-like input and user invariants, generating SMT-LIB code for solvers, performing type and composition checks.
  • Current challenges include user fluency in SMT-LIB, error reporting, and providing better proof insights.
  • SSP verif is designed for large protocols, contrasting with other tools that focus on smaller, detailed systems.
  • Discussion highlighted the tool's invariant-based approach to state passing, and potential for integrating with other formal methods backends.

• Rosette Experiments on DNS (Bob):

  • Bob, an engineer without formal methods training, shared his positive experience using Rosette (a Racket/Scheme augmentation with Z3 SMT solver) to verify a critical component.
  • He applied Rosette to the FullCompare method in DNS Python's Name object, which compares DNS names.
  • By simplifying the DNS name representation and rewriting the function, Rosette proved consistency properties for the entire (simplified) input space, which Bob found significantly stronger than unit tests.
  • Key takeaways: Formal methods can be highly valuable for day-to-day engineering, even for small, critical fragments. Rosette's interface (symbolic variables, verify/solve) was user-friendly and helped identify bugs.
  • Discussion emphasized the value of small, self-contained examples for learning and architectural exploration.

• Sample Problems for UFMRG (Stephen):

  • Proposed the concept of creating IETF-oriented, relatively simple, non-cryptographic, and tractable sample problems for the research group.
  • These problems would help individuals learn and apply formal methods, improve tool usability, and potentially uncover insights about the problem itself.
  • IMAP SEARCH (a simplified subset of RFC 1951) was proposed as a candidate problem, citing its familiarity, stateful nature, and potential for concurrency issues (e.g., message UID changes during parallel operations).
  • Discussion covered the need for a crisp, expert-extracted problem definition to make it accessible for students, and the potential value of including problems with known bugs to facilitate tool comparison and demonstration.
  • A poll of the room indicated a strong sense (21 of 33 present) that the research group should spend time identifying and documenting a sample problem.

• Usability Issues in Formal Methods (Jonathan):

  • Identified key areas hindering the usability of formal methods: Tooling (UI/UX), Pen and Paper (PnP) Proofs, Publishability, Training, and Verifiability.
  • Tooling: Many tools have powerful functionality but poor UI/UX (e.g., non-semantic color schemes, slow rendering).
  • PnP Proofs: While useful for initial sketches, long PnP proofs become assertions, lacking machine-checkable rigor. The goal should be for tools to be so good that they are preferred over PnP for final proofs.
  • Publishability: It's often difficult to publish "positive" results (e.g., "protocol found to be secure"), even though such results are valuable to the community.
  • Training: A significant gap exists between trivial tool examples and expert-level usage with complex hacks, making it hard for newcomers to learn. Intermediate-difficulty examples are needed.
  • Verifiability: Running and checking large mechanized proofs can be time-consuming and costly (e.g., TLS 1.3 proof takes days). Research into cheap verification artifacts (e.g., using zero-knowledge proof concepts) could address this.
  • Another point raised was the "low-levelness" of many formal methods input languages, which require engineers to think at a very mathematical level rather than matching their system intuitions, highlighting a need for better abstractions.

Decisions and Action Items

• Bob (Rosette Experience): Bob volunteered to write up his experience applying Rosette to the DNS FullCompare problem and share it with the mailing list.
• Sample Problems Discussion: The Chairs will initiate a discussion on the mailing list to identify and document one or more sample problems for the research group to collectively address. This discussion will also consider different classes of problems (e.g., correctness, security).
• Training Materials:
  • Felix volunteered to help put together training materials for Rosette for the November IETF meeting (Prague).
  • Jonathan will aim to contribute training for Rosette for November.
  • The Chairs will coordinate training plans and opportunities for the November IETF, including exploring hackathon sessions or tutorials.
• Protocol/Technique Lists: The research group will work on updating the wiki to capture lists of protocols that could benefit from formal methods input and a compendium of formal methods techniques.

Next Steps

• The Chairs will drive the mailing list discussions regarding sample problems and training initiatives.
• The research group plans to request a session for the IETF 117 meeting in July.
• Further efforts will be made to update and utilize the UFMRG wiki as a repository for relevant protocols, techniques, and shared resources.