Session Date/Time: 29 Mar 2023 00:30

ufmrg

Summary

This was the first meeting of the Usable Formal Methods Research Group (ufmrg). The session included introductory material, presentations on formal analysis and ongoing work, and an open discussion about the group's goals and future directions. Key themes revolved around tool usability, knowledge sharing, and integrating formal methods into the IETF workflow.

Key Discussion Points

Tool Usability: Making formal methods tools more accessible to a broader audience, including protocol designers and implementers. Reducing the barrier to entry beyond PhD-level expertise.
Knowledge Sharing: Creating a repository of knowledge, including tools, training materials, examples, and documented negative results (i.e., cases where formal methods did not find vulnerabilities).
IETF Integration: Finding ways to integrate formal methods into the IETF process, including working group activities and protocol specification. Avoiding "parachuting in" and instead engaging as part of the working group activity.
Security Analysis and Proofs: Discussions on different types of security analysis (symbolic vs. computational), machine-checked proofs, and pen-and-paper proofs. Concerns raised about the level of scrutiny pen-and-paper proofs receive.
Scope of Formal Methods: The scope of the group covers not just protocol analysis but also information modeling and other formal methods relevant to network protocols.
Privacy and Formal Methods: Discussion on privacy aspects of formal methods.

Decisions and Action Items

Knowledge Repository: Start building a knowledge repository on the wiki, including tools, training materials, and examples.
- ACTION: Document existing tools, and their use cases.
Small Sample Problem: Consider developing a small, understandable sample problem that can be used to demonstrate different formal methods.
Outreach to Working Groups: Identify specific working groups within the IETF that could benefit from formal methods and initiate discussions about their needs.
Publication Venue: Pursue publication of research, including negative results, in venues such as the Applied Networking Research Workshop (ANRW). Colin Perkins to assist.

Next Steps

Send a mail to the mailing list to continue the discussion and propose additional action items.
Schedule a call in one or two months for further discussion.
Organize an in-person meeting in San Francisco.