30 November 2022
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
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
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:
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.