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

[Buday Gergely <[e-mail]>]

post scriptum: in the draft chapter, there is a sentence:

"Technical limitations include formalisms that cannot fully describe the 
complexity of modern protocols or the network environment."

Knowing the expressivity of various theorem provers this seems to be an 
unfounded statement.

May I get examples of these overly complex protocols and network 
environments, and the formalisms that that cannot handle these complexities?

This might be a challenge for new research.

- Gergely

11/6/2022 6:13 PM keltezéssel, Buday Gergely írta:
>
> 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/
>>