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

[Muhammad Usama Sardar <[e-mail]>]

Hi Colin,

this is a great initiative. Count me in volunteers! Could you set up and share the link for remote participants?


In our experience of complex protocols, the informal protocol descriptions in English are almost always broken (or at least can be interpreted in a way which breaks some guarantees). On a topic related to IETF RATS WG, during the formal specification of the remote attestation protocol in Intel TDX using ProVerif, we found a number of statements that were contradicting [1]. English is simply the best way to camouflage such protocols. At least some kind of formal specification is a necessity.


[1] See section V in https://www.researchgate.net/publication/351699567_Demystifying_Attestation_in_Intel_Trust_Domain_Extensions_via_Formal_Verification


------------------------------------------------------------------------------------------------------------------------------------------
Best Regards,

Muhammad Usama Sardar (M.Sc.)

Research Associate

Technische Universität Dresden


Faculty of Computer Science

Institute of Systems Architecture

Chair of Systems Engineering


Office: APB 3073

Phone: [phone]

Email: [e-mail]

Website: https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar

------------------------------------------------------------------------------------------------------------------------------------------


________________________________
Von: 115attendees <[e-mail]> im Auftrag von Colin Perkins <[e-mail]>
Gesendet: Freitag, 4. November 2022 17:42
An: [e-mail]
Cc: [e-mail]
Betreff: [115attendees] Usable formal methods side meeting at IETF 115


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
     *   (15 mins)
  *   Short presentations (45 mins)
     *   “What are Formal Methods and Why Should We Care?”Jonathan Hoyland
     *   “Formal Specification and Specification-Based Testing of QUIC”, Ken McMillan
  *   Discussion of proposed charter (20 mins)
     *   See Google Doc<https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#>
  *   Next steps (10 mins)
     *   Does this seem appropriate for an RG?
     *   Are there volunteers to work on this topic?
     *   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/