The State of State Machines
googleprojectzero.blogspot.com
googleprojectzero.blogspot.com
(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.
The browsers are over trusted for things like this and should never have direct access. Google Meet after a crash or the browser was shutdown and restarted with all the old tabs would open up your meeting again hidden behind a bunch of other tabs. No one was ever on them long after the meeting but it was freaky. This isn't the behaviour that I've seen recently thankfully.
This isn’t a difficult feature to design and a pretty simple one to implement at the OS level.
https://sites.google.com/a/chromium.org/dev/Home/chromium-se...
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
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
}
}
* 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.
ADT's + pattern matching make it a very easy pattern to implement. If your language supports exhaustive pattern matching it's also a very easy way to leverage the compiler to find bugs in your logic.
- 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.
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... :( )
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.
Basically, there's a finite group that acts on the Rubik's cube, and every finite group is a subgroup of a permutation group if you squint at it right. (what's a 'finite group action?' The 'group' is a set of composable and reversible "moves." The 'action' means that the group moves are effectively state transitions acting on a set of states, and that the action is nice and associative: g(hs) = (gh)s. And 'finite' just says that there's only so many states possible...)
Really nice demo, by the way! Very fun to see the squares go flying.
Glad others found the squares flying as much fun to watch as I did. :D
Granted. In context of this story, I'm in complete agreement with you.
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.
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.
[1] https://www.colm.net/open-source/ragel/
[2] https://blog.cloudflare.com/incident-report-on-memory-leak-c...
J's sequential machine builtin[0] implements something similar to this. It doesn't generate code, but it executes a state machine based purely on descriptions of states and transitions.
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.
Not true - (pure) functional programming also enforces that you do exactly that. Even more, its rule-set also enforces that time must be an input.
The ones that aren't state machines are very limited and often enough way too verbose.
In particular, FRP is worth noticing as being exactly a set of states that change by means of events. It's a nice idiom for composing very complex state machines, but isn't even disguised.
FRP goes further than state machines, in that it forbids any side effects.
E.g. you could build a state machine that, when in a certain state and getting a certain event, responds or acts by printing the current time. A classical state machine will thus behave different, depending when it receives the event. However, in FRP you _must_ either parametrize the event with the current time, or you need to have something _outside_ of the statemachine (such as an effect interpreter) which handles effects such as printing the current time. A classic state machine does not have these restrictions.
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).
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.
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.
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.
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/
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).
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
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/
Enjoy! :-)
https://www.libssh.org/security/advisories/CVE-2018-10933.tx...
Let the warning be heard loud and clear: state is the devil
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.
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.
> Posted by Natalie Silvanovich
but the bottom says
> Posted by Ryan
The latter is just the blogspot username though. It's quite scruffy.