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

[Colin Perkins <[e-mail]>]

Thank you – yes, we’re working on remote attendance.
Colin



On 6 Nov 2022, at 18:41, Muhammad Usama Sardar wrote:

> 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/