csperkins.org

Proposing an IRTF Usable Formal Methods Research Group

How should we describe and specify protocols? And how can we ensure that network protocol specifications are consistent and correct, and that implementations match the specification?

The IETF community has long used natural language to describe and specify protocols, with occasional use of formal languages and some limited amount of formal verification. In many ways this is clearly a successful approach. After all, the Internet exists as an interoperable, global, multi-vendor, network in large part due to the protocol standards the IETF develops. It is clearly possible to build interoperable implementations from IETF standards.

But is this the right approach to developing protocol specifications? The way the IETF describes protocols has changed little over the years. It may be time to consider whether new techniques have been developed that might change how protocols are specified, and possibly improve the process.

With help from Chris Wood, I organised a side meeting at IETF 115 to discuss whether there could be benefits to more systematic use of formal methods in the IETF, what are the factors limiting the adoption of such techniques, and whether it would make sense to create an IRTF research group to explore such topics.

Jonathan Hoyland discussing why formal methods might be useful in the IETF

The meeting was structured around three short presentations, plus time for discussion of the scope of the proposed work and draft charter. The presentation slides used were as follows:

Introduction, Agenda, and Proposed Charter (Colin Perkins)
I introduced the meeting, described the goals and motivation for the work, and outlined the proposed charter and the process by which new IRTF Research Groups are formed and the questions the IRSG and IAB consider when deciding whether to approve new research group proposals: 1) Is the research area that the Research Group plans to address clear and relevant for the Internet community? 2) Will the formation of the Research Group foster work that would not be done otherwise? 3) Do the Research Group’s activities overlap with those of another Research Group? 4) Is there sufficient interest and expertise in the Research Group’s topic, with at least several people willing to expend the effort that is likely to produce significant results over time?
A Bird's Eye View of Formal Methods? And Why We Should Care (Jonathan Hoyland)
Jonathan Hoyland introduced the group to formal methods, a group of techniques that use mathematical methods to prove that a system is correct. He outlined the difference between formal analysis and formal verification, how these might be used as part of the protocol specification process, and why such techniques are difficult to use. He then gave some examples of the benefits that can be realised by the use of these techniques, to show why they might be worth using despite being hard.
Formal Specification and Specification-based Testing of QUIC (Ken McMillan)
Ken McMillan outlined work to formally specify some properties of the QUIC Transport Protocol using the Ivy formal specification language. Ken's talk outlined the approach taken to understanding the QUIC specification, motivating why and how to develop a formal model of the protocol, and describing some of the properties of implementations that were verified against that model. The approach found 27 errors in implementations of QUIC, that were not found by the automated interoperability tests run by the QUIC working group, including several security vulnerabilities.
Formal Security Analysis of OAuth and OpenID Connect (Daniel Fett)
Finally, Daniel Fett gave a short presentation on work to develop A Comprehensive Formal Security Analysis of OAuth 2.0. This helped uncover new and unexpected problems with OAuth, and led to the creation of OAuth Security Best Current Practices and RFC9207. Again, the goal was to briefly highlight how formal methods can be used to find problems with protocol specifications that are not found by the usual IETF process.

There were around 35 people attending in-person with maybe another 15 people joining via video conference. Due to limitations of the in-room equipment, the meeting was not recorded but Stephen McQuistin took comprehensive minutes. The associated chat log was also saved.

The meeting concluded with a discussion of the proposed research group charter, and whether is seems appropriate for an RG, if there are topics that have been missed, and if there are people interested in working on these topics in the IRTF. Feedback on the charter and proposed work was strongly positive, and a significant number of people expressed interest in working on these topics.

Given this interest, next steps will be to revise the charter taking into account the feedback received during the meeting, then to take it to the IRSG and IAB for approval for formation of the new research group.

The Proposed Usable Formal Methods Research Group Mailing List has been created for further discussion of these topics -- please consider subscribing.