Re: [irtf-discuss] Usable formal methods side meeting at IETF 115

[Buday Gergely <[e-mail]>]

Formal methods is a broad term, what did people actually suggest?

Model checking has a long track record of verifying protocols, 
especially the Spin model checker by Gerald Holzmann.

Theorem provers were also used, e.g. for security protocols, the work of 
Larry Paulson and Giampaolo Bella and others.

I think English should augment formal specifications as it could ignite 
debate whether the formalisation is correct and unambigous.

Unfortunately I cannot attend this meeting as I will give a talk exactly 
this time.

I do not have a voting right but I certainly support setting up such a 
research group, and I am willing to volunteer working on it.

My research is at the intersection of concurrency and formal 
verification, and doing that for Internet-wide deployed protocols is 
indeed a good case study.

Cheers

- Gergely

11/4/2022 5:42 PM keltezéssel, Colin Perkins írta:
>
> Hi,
>
> How should we describe and specify protocols?
>
> How can we ensure that network protocol specifications are consistent 
> and correct, and verify that implementations match the specification?
>
> The IETF community has long used natural language, English, to 
> describe and specify its protocols, with occasional use of formal 
> languages and a some limited amounts of formal verification. One of 
> the sessions in the Applied Networking Research Workshop at IETF 114 
> [1] started to discuss whether this is the right approach, and to what 
> extent formal methods, structured specification languages, and natural 
> language processing techniques can help describe network protocols.
>
> Chris Wood and I are organising a side meeting at IETF 115 to continue 
> this discussion, and to assess interest in forming a new IRTF research 
> group to explore usable formal methods for protocol specification.
>
> This will takes place on Thursday lunchtime, 10 November, from 
> 11:30-13:00 UK time in room Richmond 5 of the IETF meeting hotel (the 
> IAB breakout room).
>
> The draft agenda is as follows:
>
>   * Welcome, Goals, Motivation, Introductions
>       o (15 mins)
>   * Short presentations (45 mins)
>       o “What are Formal Methods and Why Should We Care?”Jonathan Hoyland
>       o “Formal Specification and Specification-Based Testing of
>         QUIC”, Ken McMillan
>   * Discussion of proposed charter (20 mins)
>       o See Google Doc
>         <https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#>
>   * Next steps (10 mins)
>       o Does this seem appropriate for an RG?
>       o Are there volunteers to work on this topic?
>       o What, if anything, have we missed?
>
> if you’re interested in this topic, please review the draft charter 
> <https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#> 
> and come along to the side meeting to give your feedback.
>
> Hope to see you in London!
>
> Colin
>
> [1] https://www.youtube.com/watch?v=tCsiB87s-f4
>
> --
> Colin Perkins
> https://csperkins.org/
>