Session Date/Time: 08 Nov 2023 12:00

ufmrg

Summary

The Universal Formal Methods Research Group (ufmrg) meeting covered several topics, including formal methods usage at Google, a new language (Owl) for verifying security protocols, and the HTTP/2 record reset vulnerability. There was also a discussion about sample problems for bridging research with IETF working groups and feedback on the formal methods training session held on Sunday.

Key Discussion Points

Formal Methods at Google: Chris presented on the use of formal methods at Google, highlighting projects like Open Titan, Project Oak, and the verification of cryptographic code in BoringSSL. A key challenge is the usability of formal methods tools and toolchains, requiring specialized expertise and better documentation. Performance improvements were seen when formally verified elliptic curve operations were implemented in BoringSSL. The team is interested in exploring protocols and ways to make the tooling useful in their security review processes, but the tools are not easy to use.
Owl: Verified Security Protocols: Joshua presented Owl, a new language for developing verified security protocols. Owl uses a type-based analysis to guarantee computational security and can extract verified Rust code. A large-scale application currently being worked on is WireGuard.
HTTP/2 Record Reset Vulnerability: Lucas discussed a recently discovered vulnerability related to the HTTP/2 protocol's record reset feature. The vulnerability isn't a bug in the protocol itself but arises from interactions with implementation details and deployment architectures. The question was posed whether formal methods could help in modeling such system-wide effects. Modeling this was seen as potentially possible using CSP (Communicating Sequential Processes).
Sample Problems: Corey provided an update on the effort to define sample problems for bridging the gap between formal methods research and IETF working groups. The focus is currently on the TIP protocol for trusted execution environment provisioning. Draft models are being developed in Proverif and Tamarin.
Formal Methods Training Feedback: Participants provided feedback on the formal methods training session. A hands-on, exercise-based approach with experts present was valued. Some attendees favored security tool-focused training, while others suggested more general tools or intermediate level training based on previous surveys.

Decisions and Action Items

Action Item: The chairs will discuss the feedback from the training session and incorporate it into planning future training events. Further suggestions can be sent via email.
Action Item: Stephen will revisit the I'm up search case.

Next Steps

Further discussion on training formats and tool choices for future sessions.
Continued development of the TIP model as a sample problem.
Meet at the next IETF meeting.