9 ms·

The State of State Machines

426 points by arkadiyt 6y ago

bitcharmer 6y ago
As much as I try to distance myself from Google as a corporation I really appreciate project zero and their write ups. Always learning something new from them.
kache_ 6y ago
That was a really good read. I appreciate the detail that the writer went into describing his investigative process. Let the warning be heard loud and clear: state is the devil
- Jtsummers 6y ago
  State isn't the devil. Nor is it a necessary evil. State is essential to many, if not most, interesting applications. Poorly managed state or ad hoc state machines are the devil. Once you model your system properly as a state machine, many of these issues fall out during the initial design and development (not to say they won't happen anyways, but this mitigates many of the issues). If you design your system so that whatever variables define your state are mutated together to ensure your invariants hold, this helps a lot with addressing poorly managed state. And if you can (you can't always) use a system which is aware of state machines as part of the design then you can mitigate the ad hoc state machine part.
  - bob1029 6y ago
    I would go further and say that the modeling isn't even a big deal (in terms of state machine complexity) as long as you are enforcing immutability at your domain boundary. If only domain methods are able to mutate state, it's a lot easier to find where bugs might be hiding. If any consumer of your domain model can mutate anything in any way it sees fit and then invoke some generic UpdateState(model) method, then you have a much bigger problem. Put differently, as long as you have good accountability of all the things that can change the state and are comfortable with how that set of things operates, then you are probably in a decent position.
    - Jtsummers 6y ago
      That's fair, and is similar to what I would've written if I'd elaborated more on my "poorly managed state" comment. If you apply good modular/OO principles you at least constrain where state is managed in a way that makes writing, maintaining, and testing your system more tenable without an explicit model.
- agency 6y ago
  * her[1] investigative process [1] https://twitter.com/natashenka https://twitter.com/natashenka
  - buckminster 6y ago
    It's an easy mistake to make because the top of the article says > Posted by Natalie Silvanovich but the bottom says > Posted by Ryan The latter is just the blogspot username though. It's quite scruffy.
  - deleted 6y ago
    [deleted]
MaxBarraclough 6y ago
Good analyses, but I was expecting more discussion of how best to work with (conceptual) state machines when writing code. I'm no expert on the matter, but there are code-generative tools out there that help make state machines very explicit: you describe the state machine, and the system generates the code. This should help to avoid issues with transitions that you failed to consider, which may be of real value as such unexpected transitions may pose a serious security issue when implementing the state machine 'by hand' in code. More so than many design patterns, it seems to make good sense to use a code-generative approach for state-machines. This is of course related to how regex works, as regex is implemented with state machines, but state-machine code-generator systems might not make use of the usual regex syntax. Related reading: Turning vaguely reassuring finite-state machines into regular expressions, https://news.ycombinator.com/item?id=25496045 https://news.ycombinator.com/item?id=25496045
- fabian2k 6y ago
  I'm certainly not an expert in this, but the big issues when not using a "real" state machine but e.g. a bunch of separate booleans representing various parts of the state (isLoading, isError, ...) are the following: - you can be in an inconsistent state that should not exist, e.g. isLoading and isError at the same time - state transitions that should not be possible can be performed if you make a mistake The first one you can easily fix without a library by using a state enum instead of a bunch of booleans. The second one is probably better handled by a library that implements a declared state machine or state chart. In Javascript that would be e.g. xstate (https://xstate.js.org/ https://xstate.js.org/). I found that simply thinking about the states and writing them down as a state machine is already very helpful in avoiding certain kinds of issues that arise when you just do this on the fly.
  - taeric 6y ago
    This gets greatly compounded when you have a lot of states. As an easy example, consider the "state machine" for a rubik's cube. All told, this isn't insurmountable, but you are almost certainly not going to write down all of the allowed states with all of the possible transitions. Which is not to say you can't make a program to reason about what the allowed states are. I started a probably bad attempt at that a while back at https://taeric.github.io/cube-permutations-1.html https://taeric.github.io/cube-permutations-1.html. (And, I just noticed the mathjax included on that page isn't loading. Almost certainly my fault... :( )
twoodfin 6y ago
This discussion reminds me of the Alloy[1] language and the associated analyzer. The analyzer transforms an Alloy model and some formal statement about it (e.g. "a caller can never connect to callee without the callee's consent to that caller connecting") into a giant SAT problem, which it feeds to a SAT solver looking for counterexamples, which it can map back to a series of valid state transitions in the original model. Very cool stuff, at least 20 years ago when I was playing with it. [1] http://alloytools.org/about.html http://alloytools.org/about.html
- Jtsummers 6y ago
  It's still useful, though I haven't used it in a while. Alloy was my introduction to properly modeling systems (versus largely paper-based which has limitations on size/scope).
Yeroc 6y ago
It was interesting to me how many of these were related to making async calls to adjust state resulting in race conditions. In many cases the argument was made that async calls were not justified. Many times we follow a particular call pattern in order to keep things consistent without fully considering whether it's necessary and/or safe. Also I wasn't aware of the tool named Frida[0] that she kept referencing so I had look that up. [0] - https://frida.re/ https://frida.re/
- danlugo92 6y ago
  Solution is this: Assign UUID to each async call, including retries. Or disallow retries. Sprinkle in some optimistic update if you want. Keep track of results, mirror lower level timeout (75 seconds for HTTP).
jrochkind1 6y ago
Every time a vulnerability like this comes out, especially if it's a company that has some people with a chip against them (and most companies do), people say "See, that's why you can't trust Company With Vulnerabilty, I never use their software." But if you actually pay attention you'll realize that vulnerabilities happen everywhere. Not all software is created equal, some might be more secure and have fewer vulnerabilities than others. But a single exposed vuln, no matter how severe, is pretty much never enough to judge which software is which. I remember hearing about this exact bug in Facetime, but I had no idea that, as OP demonstrated, an analagous bug effected pretty much every popular similar A/V group chat software. Including the vaunted Signal. Did this one OP find and reveal it in all of them? wow. Also, I really wonder how many of these the NSA knew about before we did, but who can say (except the NSA).
- ehsankia 6y ago
  This extends beyond vulnerabilities to bugs in general too. No company, or programmer for that fact, is immune to making mistakes. Some people like to think that if you're a very good programmer you'll magically write bug-free code, but that just doesn't happen. This is why extensive testing and having multiple eyes look at something is good practice. And even then, with the multiple layers of redundancy and everything, you still see AWS/GCP/Azure having downtimes, you still see bugs and crashes and exploits, from the small startups to the top tech companies.
infogulch 6y ago
I feel like we will continue to run into these kinds of issues to the end of time unless can figure out: 1. How to precisely describe the properties we want the final system to have, 2. How to 'compile' from a higher-level language/layer into a lower-level language while maintaining all those properties. At the least this will require us to: 3. Define the precise semantics of each layer and enforce that every construction in and implementation of that layer adheres to it strictly. Properties like "no private data is accessible until the user consents", "the final result of the algorithm is independent of the order that messages are received", "decryption must be constant-time and the program must not have any observable effect until the message is known to be verified", etc. Obviously these properties as stated are incomplete and imprecise, but that's my point: we have to figure out how to make these kinds of statements precise enough. Layers/languages should verifiably maintain these properties through every translation via paths like: eula/privacy policy, requirements, UX, UI, state machine, source code, AST, IR, ASM, machine code. Every one of these layers should have a well-defined execution model that is isomorphic with other layers, modulo metadata. For example: source code === AST [+ comment/whitespace/filesystem metadata], AST === IR [+ name/desugaring/applied-optimizations metadata]. All undefined behavior at every layer must be exterminated by definition or avoided by construction. One problem is that we throw away too much metadata when moving between layers which makes the task of maintaining these properties through many layers extremely difficult. For example, trying to implement constant time algorithms in a high-level language is nearly impossible to hold over time (robust to changes in source and compiler) because the compiler/optimizer has forgotten (or was never told) what parts must be done in constant time and to not use the partial results of the algorithm until it has completely finished. To implement this, all candidate implementation strategies and optimizations in the lower layer must be identified by whether they preserve constant time execution or not, and optimizer/compilation unit (CU) boundaries inserted to prevent an over-eager optimizer for a non-constant-time CU to observe partial results. Etcetera for every other desirable property and every layer.
- dgb23 6y ago
  A good path to this might be deeper investigation of logic/constraint programming. Its a good tool for formally encoding known, discrete constraints like you described above.
efwfwef 6y ago
That's why I get upset when I look at complex code that doesn't clearly specify a whitelist of state transitions. It's easy god damn it: figure out your protocol state transitions, and write them down in your code somewhere. Now every time you change state, just match it against the whitelist of state transition that you have.
- mumblemumble 6y ago
  One could go so far as to say that a finite state machine with a poorly defined 𝛿 is itself poorly defined.
tedunangst 6y ago
Was hoping to see more than just chat apps. For examples, see also: https://www.libssh.org/security/advisories/CVE-2018-10933.txt https://www.libssh.org/security/advisories/CVE-2018-10933.tx... https://mitls.org/pages/attacks/SMACK https://mitls.org/pages/attacks/SMACK
Mikhail_Edoshin 6y ago
Is there a more detailed description of the logic of these calls to better understand the problem?
kazinator 6y ago
For distributed systems and protocols, you have multiple state machines acting concurrently. Such systems can be modeled by Petri nets: https://en.wikipedia.org/wiki/Petri_net https://en.wikipedia.org/wiki/Petri_net
greggman3 6y ago
I know this is probably what most users want but I hate the why Chrome's camera/mic permissions work. Your options are (1) block a domain from camera/mic access (2) give a domain camera/mic access forever 2 is what people pick. From that point on, that domain, in an iframe, can turn on your camera/mic. That means if messanger.com or meet.google.com or zoom.com wanted to make zoom.com/embed/this/url/as/iframe/to/spy/on/people.html they could, and then sell that service for ads to embed in their ads. They have the permissions needed to turn on the mic/camera whenever they want at that point, no more questions asked. That bugs me. Firefox at least has "allow camera access once". I don't know what a better solution is. One might be mic/camera permission per URL instead of domain. I supposed that's not really any different if you can just append ?dothespything=true Another might just be that it always asks. It's not like the phone feature of a smartphone has the option to just always answer immediately. Instead you choose whether or not the take the call. Does it need to be any different on a webpage? PS: I like that webpages have this feature. I like that I can video chat/conference in a sandboxed environment instead of having to install a native app that can spy on me in other ways too. I just wish this permission issue worked differently.
- deleted 6y ago
  [deleted]
- zitterbewegung 6y ago
  Safari has only two options. One is to block a domain. The other is remember that you allow it to be used for one day. I think this is probably the best way to compromise on this.
- dillondoyle 6y ago
  Doesn't chrome already block 3rd party iframe for those permissions? https://sites.google.com/a/chromium.org/dev/Home/chromium-security/deprecating-permissions-in-cross-origin-iframes https://sites.google.com/a/chromium.org/dev/Home/chromium-se...
  - jazzyjackson 6y ago
    Well I guess it depends on who is controlling the iframe, it just requires an allow="microphone; camera" attribute.
still_grokking 6y ago
No mention of behavior types here in the comments? I'm wondering. Let's add this as it's related. https://www.di.fc.ul.pt/~vv/papers/ancona.bono.etal_behav-types-prog-langs.pdf https://www.di.fc.ul.pt/~vv/papers/ancona.bono.etal_behav-ty... As this above is a very academic viewpoint let's add also some reference to a real world implementation of some of the concepts: https://alcestes.github.io/effpi/ https://alcestes.github.io/effpi/ Enjoy! :-)
deleted 6y ago
[deleted]
ProfHewitt 6y ago
State machines are incompatible with concurrent systems. For example there is no nondeterministic state machine for the following program: IndeterminateLargeNumber:[]→Natural ≡ []↦ aCounting←Counting.[], // Bind aCounting to a newly created Counting aCounting.go||| // Send aCounting a go message while concurrently aCounting.stop // sending aCounting a stop message Counting:[ ]→Interface go→Void, stop→Natural ≡ [] ↦↦ // constructor has no arguments count:=0, // The variable count is initially 0 continue:=False| // The variable continue is initially False go ↦ // When a go message is received: continue cases // Cases for continue are as follows: True then // If continue is True, count:=count+1; // then increment count and afterward Hole (This Counting).go // in a hole in the region of mutual exclusion, send a go message this instance of Counting else Void // If continue is False, then return Void stop ↦ // When a stop message is received: continue:=False; // Assign continue the value False and then count // return the value of count See the following for an explanation: https://papers.ssrn.com/abstract=3459566 https://papers.ssrn.com/abstract=3459566

426 points by arkadiyt 6y ago

As much as I try to distance myself from Google as a corporation I really appreciate project zero and their write ups. Always learning something new from them.

kache_ 6y ago

That was a really good read. I appreciate the detail that the writer went into describing his investigative process. Let the warning be heard loud and clear: state is the devil

Jtsummers 6y ago
State isn't the devil. Nor is it a necessary evil. State is essential to many, if not most, interesting applications. Poorly managed state or ad hoc state machines are the devil. Once you model your system properly as a state machine, many of these issues fall out during the initial design and development (not to say they won't happen anyways, but this mitigates many of the issues). If you design your system so that whatever variables define your state are mutated together to ensure your invariants hold, this helps a lot with addressing poorly managed state. And if you can (you can't always) use a system which is aware of state machines as part of the design then you can mitigate the ad hoc state machine part.
- bob1029 6y ago
  I would go further and say that the modeling isn't even a big deal (in terms of state machine complexity) as long as you are enforcing immutability at your domain boundary. If only domain methods are able to mutate state, it's a lot easier to find where bugs might be hiding. If any consumer of your domain model can mutate anything in any way it sees fit and then invoke some generic UpdateState(model) method, then you have a much bigger problem. Put differently, as long as you have good accountability of all the things that can change the state and are comfortable with how that set of things operates, then you are probably in a decent position.
  - Jtsummers 6y ago
    That's fair, and is similar to what I would've written if I'd elaborated more on my "poorly managed state" comment. If you apply good modular/OO principles you at least constrain where state is managed in a way that makes writing, maintaining, and testing your system more tenable without an explicit model.
agency 6y ago
* her[1] investigative process [1] https://twitter.com/natashenka https://twitter.com/natashenka
- buckminster 6y ago
  It's an easy mistake to make because the top of the article says > Posted by Natalie Silvanovich but the bottom says > Posted by Ryan The latter is just the blogspot username though. It's quite scruffy.
- deleted 6y ago
  [deleted]

MaxBarraclough 6y ago

Good analyses, but I was expecting more discussion of how best to work with (conceptual) state machines when writing code. I'm no expert on the matter, but there are code-generative tools out there that help make state machines very explicit: you describe the state machine, and the system generates the code. This should help to avoid issues with transitions that you failed to consider, which may be of real value as such unexpected transitions may pose a serious security issue when implementing the state machine 'by hand' in code. More so than many design patterns, it seems to make good sense to use a code-generative approach for state-machines. This is of course related to how regex works, as regex is implemented with state machines, but state-machine code-generator systems might not make use of the usual regex syntax. Related reading: Turning vaguely reassuring finite-state machines into regular expressions, https://news.ycombinator.com/item?id=25496045 https://news.ycombinator.com/item?id=25496045

fabian2k 6y ago
I'm certainly not an expert in this, but the big issues when not using a "real" state machine but e.g. a bunch of separate booleans representing various parts of the state (isLoading, isError, ...) are the following: - you can be in an inconsistent state that should not exist, e.g. isLoading and isError at the same time - state transitions that should not be possible can be performed if you make a mistake The first one you can easily fix without a library by using a state enum instead of a bunch of booleans. The second one is probably better handled by a library that implements a declared state machine or state chart. In Javascript that would be e.g. xstate (https://xstate.js.org/ https://xstate.js.org/). I found that simply thinking about the states and writing them down as a state machine is already very helpful in avoiding certain kinds of issues that arise when you just do this on the fly.
- taeric 6y ago
  This gets greatly compounded when you have a lot of states. As an easy example, consider the "state machine" for a rubik's cube. All told, this isn't insurmountable, but you are almost certainly not going to write down all of the allowed states with all of the possible transitions. Which is not to say you can't make a program to reason about what the allowed states are. I started a probably bad attempt at that a while back at https://taeric.github.io/cube-permutations-1.html https://taeric.github.io/cube-permutations-1.html. (And, I just noticed the mathjax included on that page isn't loading. Almost certainly my fault... :( )

twoodfin 6y ago

This discussion reminds me of the Alloy[1] language and the associated analyzer. The analyzer transforms an Alloy model and some formal statement about it (e.g. "a caller can never connect to callee without the callee's consent to that caller connecting") into a giant SAT problem, which it feeds to a SAT solver looking for counterexamples, which it can map back to a series of valid state transitions in the original model. Very cool stuff, at least 20 years ago when I was playing with it. [1] http://alloytools.org/about.html http://alloytools.org/about.html

Jtsummers 6y ago
It's still useful, though I haven't used it in a while. Alloy was my introduction to properly modeling systems (versus largely paper-based which has limitations on size/scope).

Yeroc 6y ago

It was interesting to me how many of these were related to making async calls to adjust state resulting in race conditions. In many cases the argument was made that async calls were not justified. Many times we follow a particular call pattern in order to keep things consistent without fully considering whether it's necessary and/or safe. Also I wasn't aware of the tool named Frida[0] that she kept referencing so I had look that up. [0] - https://frida.re/ https://frida.re/

danlugo92 6y ago
Solution is this: Assign UUID to each async call, including retries. Or disallow retries. Sprinkle in some optimistic update if you want. Keep track of results, mirror lower level timeout (75 seconds for HTTP).

jrochkind1 6y ago

Every time a vulnerability like this comes out, especially if it's a company that has some people with a chip against them (and most companies do), people say "See, that's why you can't trust Company With Vulnerabilty, I never use their software." But if you actually pay attention you'll realize that vulnerabilities happen everywhere. Not all software is created equal, some might be more secure and have fewer vulnerabilities than others. But a single exposed vuln, no matter how severe, is pretty much never enough to judge which software is which. I remember hearing about this exact bug in Facetime, but I had no idea that, as OP demonstrated, an analagous bug effected pretty much every popular similar A/V group chat software. Including the vaunted Signal. Did this one OP find and reveal it in all of them? wow. Also, I really wonder how many of these the NSA knew about before we did, but who can say (except the NSA).

ehsankia 6y ago
This extends beyond vulnerabilities to bugs in general too. No company, or programmer for that fact, is immune to making mistakes. Some people like to think that if you're a very good programmer you'll magically write bug-free code, but that just doesn't happen. This is why extensive testing and having multiple eyes look at something is good practice. And even then, with the multiple layers of redundancy and everything, you still see AWS/GCP/Azure having downtimes, you still see bugs and crashes and exploits, from the small startups to the top tech companies.

infogulch 6y ago

I feel like we will continue to run into these kinds of issues to the end of time unless can figure out: 1. How to precisely describe the properties we want the final system to have, 2. How to 'compile' from a higher-level language/layer into a lower-level language while maintaining all those properties. At the least this will require us to: 3. Define the precise semantics of each layer and enforce that every construction in and implementation of that layer adheres to it strictly. Properties like "no private data is accessible until the user consents", "the final result of the algorithm is independent of the order that messages are received", "decryption must be constant-time and the program must not have any observable effect until the message is known to be verified", etc. Obviously these properties as stated are incomplete and imprecise, but that's my point: we have to figure out how to make these kinds of statements precise enough. Layers/languages should verifiably maintain these properties through every translation via paths like: eula/privacy policy, requirements, UX, UI, state machine, source code, AST, IR, ASM, machine code. Every one of these layers should have a well-defined execution model that is isomorphic with other layers, modulo metadata. For example: source code === AST [+ comment/whitespace/filesystem metadata], AST === IR [+ name/desugaring/applied-optimizations metadata]. All undefined behavior at every layer must be exterminated by definition or avoided by construction. One problem is that we throw away too much metadata when moving between layers which makes the task of maintaining these properties through many layers extremely difficult. For example, trying to implement constant time algorithms in a high-level language is nearly impossible to hold over time (robust to changes in source and compiler) because the compiler/optimizer has forgotten (or was never told) what parts must be done in constant time and to not use the partial results of the algorithm until it has completely finished. To implement this, all candidate implementation strategies and optimizations in the lower layer must be identified by whether they preserve constant time execution or not, and optimizer/compilation unit (CU) boundaries inserted to prevent an over-eager optimizer for a non-constant-time CU to observe partial results. Etcetera for every other desirable property and every layer.

dgb23 6y ago
A good path to this might be deeper investigation of logic/constraint programming. Its a good tool for formally encoding known, discrete constraints like you described above.

efwfwef 6y ago

That's why I get upset when I look at complex code that doesn't clearly specify a whitelist of state transitions. It's easy god damn it: figure out your protocol state transitions, and write them down in your code somewhere. Now every time you change state, just match it against the whitelist of state transition that you have.

mumblemumble 6y ago
One could go so far as to say that a finite state machine with a poorly defined 𝛿 is itself poorly defined.

tedunangst 6y ago

Was hoping to see more than just chat apps. For examples, see also: https://www.libssh.org/security/advisories/CVE-2018-10933.txt https://www.libssh.org/security/advisories/CVE-2018-10933.tx... https://mitls.org/pages/attacks/SMACK https://mitls.org/pages/attacks/SMACK

Mikhail_Edoshin 6y ago

Is there a more detailed description of the logic of these calls to better understand the problem?

kazinator 6y ago

For distributed systems and protocols, you have multiple state machines acting concurrently. Such systems can be modeled by Petri nets: https://en.wikipedia.org/wiki/Petri_net https://en.wikipedia.org/wiki/Petri_net

greggman3 6y ago

I know this is probably what most users want but I hate the why Chrome's camera/mic permissions work. Your options are (1) block a domain from camera/mic access (2) give a domain camera/mic access forever 2 is what people pick. From that point on, that domain, in an iframe, can turn on your camera/mic. That means if messanger.com or meet.google.com or zoom.com wanted to make zoom.com/embed/this/url/as/iframe/to/spy/on/people.html they could, and then sell that service for ads to embed in their ads. They have the permissions needed to turn on the mic/camera whenever they want at that point, no more questions asked. That bugs me. Firefox at least has "allow camera access once". I don't know what a better solution is. One might be mic/camera permission per URL instead of domain. I supposed that's not really any different if you can just append ?dothespything=true Another might just be that it always asks. It's not like the phone feature of a smartphone has the option to just always answer immediately. Instead you choose whether or not the take the call. Does it need to be any different on a webpage? PS: I like that webpages have this feature. I like that I can video chat/conference in a sandboxed environment instead of having to install a native app that can spy on me in other ways too. I just wish this permission issue worked differently.

deleted 6y ago
[deleted]
zitterbewegung 6y ago
Safari has only two options. One is to block a domain. The other is remember that you allow it to be used for one day. I think this is probably the best way to compromise on this.
dillondoyle 6y ago
Doesn't chrome already block 3rd party iframe for those permissions? https://sites.google.com/a/chromium.org/dev/Home/chromium-security/deprecating-permissions-in-cross-origin-iframes https://sites.google.com/a/chromium.org/dev/Home/chromium-se...
- jazzyjackson 6y ago
  Well I guess it depends on who is controlling the iframe, it just requires an allow="microphone; camera" attribute.

still_grokking 6y ago

No mention of behavior types here in the comments? I'm wondering. Let's add this as it's related. https://www.di.fc.ul.pt/~vv/papers/ancona.bono.etal_behav-types-prog-langs.pdf https://www.di.fc.ul.pt/~vv/papers/ancona.bono.etal_behav-ty... As this above is a very academic viewpoint let's add also some reference to a real world implementation of some of the concepts: https://alcestes.github.io/effpi/ https://alcestes.github.io/effpi/ Enjoy! :-)

deleted 6y ago

[deleted]

ProfHewitt 6y ago

State machines are incompatible with concurrent systems. For example there is no nondeterministic state machine for the following program: IndeterminateLargeNumber:[]→Natural ≡ []↦ aCounting←Counting.[], // Bind aCounting to a newly created Counting aCounting.go||| // Send aCounting a go message while concurrently aCounting.stop // sending aCounting a stop message Counting:[ ]→Interface go→Void, stop→Natural ≡ [] ↦↦ // constructor has no arguments count:=0, // The variable count is initially 0 continue:=False| // The variable continue is initially False go ↦ // When a go message is received: continue cases // Cases for continue are as follows: True then // If continue is True, count:=count+1; // then increment count and afterward Hole (This Counting).go // in a hole in the region of mutual exclusion, send a go message this instance of Counting else Void // If continue is False, then return Void stop ↦ // When a stop message is received: continue:=False; // Assign continue the value False and then count // return the value of count See the following for an explanation: https://papers.ssrn.com/abstract=3459566 https://papers.ssrn.com/abstract=3459566