Markdown Version | Session Recording

Session Date/Time: 25 Jul 2024 16:30

ufmrg Meeting Minutes

Summary

The UFMRG session included presentations on usable formal methods. Topics covered included the application of formal methods in protocol review, a tool for debugging designs using lightweight formal methods (Forge), and formal verification of attested TLS. The session explored the challenges and usability aspects of different formal methods tools and approaches.

Key Discussion Points

• Mark Putty's Presentation:

  • Discussion of using formal methods for reviewing IETF specifications.
  • Explanation of proofs, propositions, and the importance of verification.
  • Comparison of pen-and-paper proofs, proof assistants, and the Curry-Howard correspondence.
  • Mark presented how he uses Idris to embed types and proofs directly into IETF drafts.

• Ben Greenman's Presentation:

  • Introduction to Forge, a tool for debugging designs using lightweight formal methods.
  • Example of using Forge to model and analyze cross-site request forgery (CSRF).
  • Discussion of custom visualization, unit testing, and language levels to improve usability.
  • Forge differs because it provides visualization and unit testing, something most formal methods tools do not.

• Samma's Presentation:

  • Discussion on applying formal verification to attested TLS.
  • Exploration of the challenges in using existing formal models and the need for community input.
  • Presentation on vulnerabilities found in existing implementations related to replay attacks.
  • There is a practical need for attested TLS, not just theoretical.

• Chris Wood's Presentation:

  • Discussion about usability of formal methods.
  • Suggestion to focus on software and have that be the base point for the formal models.
  • Proposed that proofs should be software.
  • Talked about Rust and the HACS tool chain

• Robert Merget's Presentation:

  • The use of Tamarin and ProVerif for security.
  • Most RFCs are concerned with message formats.
  • It also permits monitoring which might be a very easy way to double check the specification if it's realistic enough

Decisions and Action Items

• Action Item: Jonathan Hui talk was cancelled because the session was already over time.

Next Steps

• The group will likely discuss potential next steps and future meetings via the mailing list.