6 ms·

I guess a related question would be, is anyone aware of a common protocol that does have a formally defined state machine to review?

scott_karana 9y ago
TCP's might not be formally defined (unsure), but it's pretty well understood to the point of having de facto ones, at least.
- userbinator 9y ago
  There are state diagrams in the TCP RFC --- in ASCII art, so the authors clearly really wanted to have one.
  - scott_karana 9y ago
    Nice! Good to know. That must be the origin of all the useful but unofficial SVG ones I'd seen :)
lsh123 9y ago
SSL
- tom_mellior 9y ago
  Here is really cool work on state machines in TLS: https://www.smacktls.com/smack.pdf https://www.smacktls.com/smack.pdf Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS" From the abstract: "mplementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes and key exchange methods, where each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years ..." Based on this work you might say that there are formal state machines for TLS, but they aren't in the standard.
chrismorgan 9y ago
HTML parsing is, from the HTML 5 spec onwards, defined as a state machine.
tonyhb 9y ago
JSON, but it isn't that pretty.
- chrismorgan 9y ago
  JSON is actually not well or consistently specified, and definitely not to the rigour of a state machine; it’s specified in half a dozen places and ways, with inconsistencies and fuzzy details; see http://seriot.ch/parsing_json.php http://seriot.ch/parsing_json.php.
yxhuvud 9y ago
RADIUS.
mhandley 9y ago
When we designed DCCP, I did a formal model using LTSA to prove liveness and safety properties. Mostly I did it for fun (I got landed with teaching concurrency, and the previous professor had used this tool). As formal models go, LTSA is rather simple. I was pretty surprised when it found a previously unknown deadlock state. To my chagrin, a decade or so earlier, I'd observed a very similar deadlock in the Solaris TCP stack when running SMTP, which is unusual in that it requires the server to send first. I shared the LTSA model with a few others at the time, but no-one else seemed very interested in doing anything with it. https://www.doc.ic.ac.uk/ltsa/ https://www.doc.ic.ac.uk/ltsa/ https://tools.ietf.org/html/rfc4340 https://tools.ietf.org/html/rfc4340 Edit: I dug through my old backups, and I think this is probably the model I used: http://nrg.cs.ucl.ac.uk/mjh/dccp.lts http://nrg.cs.ucl.ac.uk/mjh/dccp.lts It's nothing fancy, but my point is that even simple modelling can spot errors that a whole standards group of smart people miss.

scott_karana 9y ago

TCP's might not be formally defined (unsure), but it's pretty well understood to the point of having de facto ones, at least.

userbinator 9y ago
There are state diagrams in the TCP RFC --- in ASCII art, so the authors clearly really wanted to have one.
- scott_karana 9y ago
  Nice! Good to know. That must be the origin of all the useful but unofficial SVG ones I'd seen :)

lsh123 9y ago

SSL

tom_mellior 9y ago
Here is really cool work on state machines in TLS: https://www.smacktls.com/smack.pdf https://www.smacktls.com/smack.pdf Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS" From the abstract: "mplementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes and key exchange methods, where each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years ..." Based on this work you might say that there are formal state machines for TLS, but they aren't in the standard.

chrismorgan 9y ago

HTML parsing is, from the HTML 5 spec onwards, defined as a state machine.

tonyhb 9y ago

JSON, but it isn't that pretty.

chrismorgan 9y ago
JSON is actually not well or consistently specified, and definitely not to the rigour of a state machine; it’s specified in half a dozen places and ways, with inconsistencies and fuzzy details; see http://seriot.ch/parsing_json.php http://seriot.ch/parsing_json.php.

yxhuvud 9y ago

RADIUS.

mhandley 9y ago

When we designed DCCP, I did a formal model using LTSA to prove liveness and safety properties. Mostly I did it for fun (I got landed with teaching concurrency, and the previous professor had used this tool). As formal models go, LTSA is rather simple. I was pretty surprised when it found a previously unknown deadlock state. To my chagrin, a decade or so earlier, I'd observed a very similar deadlock in the Solaris TCP stack when running SMTP, which is unusual in that it requires the server to send first. I shared the LTSA model with a few others at the time, but no-one else seemed very interested in doing anything with it. https://www.doc.ic.ac.uk/ltsa/ https://www.doc.ic.ac.uk/ltsa/ https://tools.ietf.org/html/rfc4340 https://tools.ietf.org/html/rfc4340 Edit: I dug through my old backups, and I think this is probably the model I used: http://nrg.cs.ucl.ac.uk/mjh/dccp.lts http://nrg.cs.ucl.ac.uk/mjh/dccp.lts It's nothing fancy, but my point is that even simple modelling can spot errors that a whole standards group of smart people miss.