TLA+ for parser correctness

[moshe kravchik]

This is a question to the TLA+ experts. I need to write code for network protocol messages' correctness and validity. I want to make sure I get everything correct. Is TLA+/PlusCal the right tool for the job? Are there any examples of applying it to similar tasks?

[Markus Kuppe]

"Code for network protocol messages" is a bit vague, but if your main interest lies in securely parsing data transmitted over networks, you might find https://project-everest.github.io/everparse/ to be useful.

[Aman Shaikh]

Hi Moshe

I have used TLA+ for network protocols - BGP to be specific, so yes, TLA+ can be used for verifying properties of a network protocol. But it depends on what exactly you're trying to achieve. Can you elaborate on what kind of properties you want to check?

aman

[Markus Kuppe]

https://github.com/tlaplus/Examples/blob/master/specifications/tcp/tcp.tla is my TLA+ spec of the abstract state machine defined in RFC 9293 (TCP).

M

[Alex Porter]

If I understand correctly, you want to validate the contents of a message received over the network. TLA+ is more for doing system level design of distributed systems and algorithms. If you want something like a formally verified parser, see EverParse (https://project-everest.github.io/everparse/). 

On Sat, May 11, 2024, 10:39 PM moshe kravchik <moshe.k...@gmail.com> wrote:

This is a question to the TLA+ experts. I need to write code for network protocol messages' correctness and validity. I want to make sure I get everything correct. Is TLA+/PlusCal the right tool for the job? Are there any examples of applying it to similar tasks?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/22e98309-b774-4865-8663-7c3f99f6f9aan%40googlegroups.com.

[moshe kravchik]

Thanks a lot! I will indeed look into EverPArse as it meets my requirements! 

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/5i8FfNmCzZI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CADgQdyJDtUEkqURrU7dWw9iV96aM_y-UV%3DznQ%3DYODjvijmz2cw%40mail.gmail.com.