Markdown Version | Session Recording

Session Date/Time: 25 Jul 2023 00:30

ufmrg

Summary

The ufmrg (Usable Formal Methods Research Group) meeting focused on several key topics, including defining sample problems for formal method applications, a presentation on using Isabelle for internet research, and planning for a training session in Prague. The discussion highlighted the need for a range of sample problems with varying complexity and the importance of defining clear questions for each problem. A volunteer was secured to document the dPOP protocol as a sample problem. Gergely presented on Isabelle, discussing its capabilities and limitations for formal verification. Planning for a training session at IETF 118 in Prague was initiated, with a discussion about the level of training (beginner vs. intermediate).

Key Discussion Points

• Sample Problems:
  • The group discussed the need for sample problems of varying complexity to help people learn and apply formal methods.
  • Suggestions for sample problems included: IMAP search, dPOP, HPKE, Quick protocol snippets (packet drops), TCP retransmit timers/slow start, TFTP, TCP Cubic, and SNMP.
  • Defining the specific questions/properties to be proven for each sample problem is crucial (e.g., for IMAP search, defining what properties to prove).
  • The goal is not necessarily to find bugs but to improve the usability of formal methods.
  • One potential target is for a professor to assign the problem to a graduate student.
  • It would be good if at least one problem is related to cryptography, and another one isn't.
• Isabelle Presentation:
  • Gergely presented on using Isabelle for internet research, focusing on definitions and modeling.
  • Isabelle is a software tool that uses formally to basic inferencer.
  • The presentation included an example of modeling TLS certificates using Isabelle.
  • Isabelle automatically creates an induction theorem from definitions that can be used to automatically check corner cases in the models
  • Isabelle can perform code extraction to generate ML, Scala, or Haskell code from a model.
• Training Session in Prague (IETF 118):
  • Planning for a Sunday training session before IETF 118 in Prague.
  • A call will be set up with volunteers in the coming weeks to discuss the content and format.
  • The group needs to decide between beginner-level and intermediate/masterclass level training.

Decisions and Action Items

• Action Item: Hannahs volunteered to document the dPOP protocol as a sample problem.
• Action Item: Chairs to set up a call with training volunteers to plan the Sunday training session before IETF 118.

Next Steps

• Hannahs to begin documenting the dPOP protocol as a sample problem.
• Chairs to organize a call with training volunteers to finalize the plans for the IETF 118 training session and address the beginner vs. intermediate-level content question on the mailing list.
• Consider defining the properties that are expected to be proven for each of the sample problems.