[HN Gopher] The State of State Machines
___________________________________________________________________
The State of State Machines
Author : arkadiyt
Score : 234 points
Date : 2021-01-19 17:57 UTC (5 hours ago)
(HTM) web link (googleprojectzero.blogspot.com)
(TXT) w3m dump (googleprojectzero.blogspot.com)
| efwfwef wrote:
| 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 wrote:
| One could go so far as to say that a finite state machine with
| a poorly defined is itself poorly defined.
| kazinator wrote:
| 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
| tedunangst wrote:
| Was hoping to see more than just chat apps. For examples, see
| also:
|
| https://www.libssh.org/security/advisories/CVE-2018-10933.tx...
|
| https://mitls.org/pages/attacks/SMACK
| MaxBarraclough wrote:
| 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
| tyingq wrote:
| One of those code-generative tools is Ragel[1], which was in
| the middle of an issue at CloudFlare[2]. Though CF did note
| that it was a bug in how they used Ragel, not Ragel itself.
|
| [1] https://www.colm.net/open-source/ragel/
|
| [2] https://blog.cloudflare.com/incident-report-on-memory-
| leak-c...
| monocasa wrote:
| That's one of the reasons I love ADTs and pattern matching in
| systems code so much.
|
| For instance in rust where both self and Event are enums
| fn on_event(&mut self, event: Event) { *self = match
| (self, event) { (State1(data), Event1(args)) => {
| .... processing event1 State2(new_data)
| } // All other events in State1 are ignored
| (State1(data), _) => State1(data),
| (State2(data), Event1(args)) => { .... processing
| event2 State3(new_dat) }
| ..... pattern match the rest of the matrix } }
|
| will do a great job highlighting missing transitions of the
| state machine's transition matrix.
| __jem wrote:
| My favorite rust state-machine-ism is consuming self by value
| when you transition. In combination with generics and From,
| this allows you to ensure that states are only ever entered
| into via the transitions you encode by implementing the
| trait, and because the previous state is totally consumed it
| makes the transitions super clear.
| pdimitar wrote:
| I'd love to read a blog post detailing exactly how is this
| done.
| __jem wrote:
| Here! https://hoverbear.org/blog/rust-state-machine-
| pattern/
| pdimitar wrote:
| Much appreciated, thank you!
| tangjurine wrote:
| Could you explain a little more? That sounds really cool.
| __jem wrote:
| Here's a good blog on the topic:
| https://hoverbear.org/blog/rust-state-machine-pattern/.
| The last implementation of Raft uses this pattern.
| monocasa wrote:
| I started off by doing that, but ultimately didn't like it
| for my use cases.
|
| * It didn't seem to grant a lot of benefits over pattern
| matching (errors were pushed to compile time checks in both
| cases).
|
| * It had larger cognitive overhead since the allowed
| transitions were either all over the place in the source
| instead of in one match statement or weren't colocated with
| their structs.
|
| * It didn't seem nearly as good at attacking the
| combinatorial complexity you see in these matrices as
| pattern matching is.
| __jem wrote:
| It's definitely not a great fit if you have a ton of
| different state transitions, since the From impls add a
| lot of boiler plate. But I've found it perfect for
| situations where there's only a few very well defined
| transitions, like the Raft implementation suggested in
| the blog post I linked in parent reply.
| astrange wrote:
| Ragel is a good tool for this: http://www.colm.net/open-
| source/ragel/
|
| This can be built into languages as "typestate" but noone ever
| seems to get around to doing it. It's unfortunate because I
| think it's the only acceptable way to do OOP.
| MaxBarraclough wrote:
| Heh, I mentioned Ragel in that other thread I linked to,
| although I see I messed up the link and linked to GraphViz
| instead.
|
| I have to admit I've only very briefly dabbled with Ragel but
| yes it does seem a pity that this approach is so rarely used.
| rwmj wrote:
| To be honest I wouldn't bother with an existing code generator.
| However I would definitely consider modelling your state
| machine and generating code from that. Also model your state
| machine hierarchically, especially if it has any kind of
| complexity. We did that with our NBD client, which has 96
| states in 17 groups, generating C code:
| https://github.com/libguestfs/libnbd/tree/master/generator
| bsder wrote:
| tl;dr Software programmers continue to fail to grasp that
| "protocol" means "state machine". News at 11.
|
| Even beyond just "use an _actual_ state machine ", programmers
| don't grasp that you need to think about:
|
| 1) What is my state _now_?
|
| 2) What are my inputs _now_?
|
| 3) What are my outputs _now_?
|
| 4) What is my state _next_?
|
| 5) Where/when do I transition from state _now_ to state _next_
| and does it need to be atomic?
|
| Conflating any of these results in bugs. And not using state
| machines explicitly _always_ results in conflating these.
|
| One of the most important overlooked concepts in protocols is
| that "time" is an input (interestingly, Carmack talks about
| this in game development, too). Timeouts and errors are a state
| like anything else.
| minitoar wrote:
| This is what Interana does. You define the states and the
| transition rules, and what you want to compute (eg how many
| times was this pattern matched, what was the p50 duration
| between steps 2 and 5, etc.) It then compiles this into machine
| code to actually scan the column store using llvm.
| fabian2k wrote:
| 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/).
|
| 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 wrote:
| 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. (And, I just noticed the mathjax
| included on that page isn't loading. Almost certainly my
| fault... :( )
| fabian2k wrote:
| State charts avoid that problem to some extent, you don't
| explode the number of state like in a simple finite state
| machine. But that's a point where you certainly want to use
| a library.
| taeric wrote:
| Right. My assertion would then be that many things are
| modeled on a ton of possible states.
|
| Granted. In context of this story, I'm in complete
| agreement with you.
| Jtsummers wrote:
| Might be worth reposting that link, it's an interesting
| topic on its own. Rubik's cube transformations as
| permutations is one of those "obvious" things that had
| never occurred to me before, plus the neat interactive demo
| at the bottom.
| taeric wrote:
| Would love to see feedback on it. I posted back when I
| wrote it. I think it was mostly lost to the noise.
| madpata wrote:
| I think your answer boils down to "pick the right tool for
| the job". Of course state machines are cumbersome for
| systems with loads of different states and transitions.
|
| But state machines are really useful when designing safety-
| critical systemsfor aeronautical, automotive or train
| components, especially if one uses timed automata for
| modelling.
|
| It's possible to either generate the code from the model or
| use the model to automatically generate a complete test
| suite for the modelled system. Very useful for verification
| purposes.
| taeric wrote:
| Completely agree. I did not mean my post as an argument
| against state machines.
| Yeroc wrote:
| 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/
| bitcharmer wrote:
| 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.
| jrochkind1 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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.
| infogulch wrote:
| IMO an interesting project in this space is: mm0 / MetaMath
| Zero - Closing the loop in proof verification down to
| verifying the machine code of the verifier. Goes from first-
| order logic to peano arithmetic to a model of x86 to a model
| of the verifier written in x86. Interestingly, it
| demonstrates that verification of a compact proof can be
| performed in linear time (!) if the proof is structured
| correctly. -- https://github.com/digama0/mm0
|
| The fact that proof checking can take linear time (though not
| proof-finding), and the fact that it incorporates so many
| 'layers' has emboldened my opinion that such a thing as I
| described above is possible and has enormous potential.
| infogulch wrote:
| Agreed! I've been paying attention to constraint/logic
| programming (CLP) recently, but I haven't found the right
| thing yet / haven't invested enough time into it to find the
| right thing. In my very-layman opinion, CLP-based systems
| need three things to properly take off: 1. some kind of 'type
| system'-like thing that enables robust symbolic reasoning
| over pure relations in any mode, 2. a critical mass of
| defined layers that is 'deep enough' to reach the hardware,
| 3. a way to express verified alternatives and preference in
| the order they are applied.
| twoodfin wrote:
| 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
| Jtsummers wrote:
| 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).
| Mikhail_Edoshin wrote:
| Is there a more detailed description of the logic of these calls
| to better understand the problem?
| kache_ wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| That's fair, and is similar to what I would've written if
| I'd elaborated more on my "properly 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 wrote:
| * _her_ [1] investigative process
|
| [1] https://twitter.com/natashenka
| buckminster wrote:
| 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]
___________________________________________________________________
(page generated 2021-01-19 23:00 UTC)