Proposing an IRTF Usable Formal Methods Research Group
30 November 2022
/ protocol-standards
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.
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.