[jwmullally]

They should have pasted this diagram all over the document: https://en.wikipedia.org/wiki/Automata_theory

I'm disappointed that the "Formal Methods" section makes only a passing reference to Finite State Machines. FSMs are arguably the easiest to understand and use formal methodology, and probably the most prevalent. Especially worth emphasizing given how difficult and opaque a lot of formal methods remain to even people with 4 year CS bachelor degrees.

This old thread https://news.ycombinator.com/item?id=2949543 had lots of interesting discussions on FSMs, particularly their current widespread use in (sometimes mission-critical) embedded systems. An ongoing problem seems to be a lack of robust first-class support for FSMs in every day programming languages, which can limit debugging, static analysis, standard tools etc.

Disclaimer: I know nothing about security or formal methods.

[schoen]

People making arguments about automata theory in security are often affiliated with the LANGSEC program/project/movement.

http://langsec.org/

There are lots of compelling ideas there (and LANGSEC researchers would tend to agree that if a functionality can be implemented correctly as an FSM, that would be a safer option).

A related phenomenon that people talk about is the unexpected Turing-completeness (where people have been able to prove that so many different parts of computing are Turing-complete -- things that were never intended to be programming languages). LANGSEC people and others refer to the negative security implications of some of this as "weird machines", where you really didn't want Turing-completeness but you got it by accident or by default anyway, and it might be possible for an attacker who can corrupt control flow or other kinds of state to then perform arbitrary operations. For security people an example may be return-oriented programming, but there are evidently others that can be thought of in the same way.

[ngneer]

Glad someone mentioned this. LANGSEC encourages you to think about computational power as privilege, and the principle of least privilege will guide you to constructing machines that are easier to reason about, leaving less room for ambiguity.

[triplesec]

This is fascinating. Do you have any examples or stories of such 'weird machines'?

[schoen]

The concept is presented in

http://www.langsec.org/papers/Bratus.pdf

I think people have found a number of other, well, weird examples. I found

https://www.usenix.org/conference/woot15/workshop-program/pr...

via Google Scholar and there are more papers on this theme if you search for "weird machines" there. It seems like a helpful way to think about this issue!

[ChoHag]

At a higher level than the other guy, and not precisely the same thing:

http://blog.checkpoint.com/2016/02/02/ebay-platform-exposed-...

[lawnchair_larry]

https://www.usenix.org/system/files/conference/woot13/woot13...

[triplesec]

many thanks, peoples

[nickpsecurity]

High-assurance security from 80's-90's used them too in both formal specifications and coding approach. It was more like looking at the kernel as a giant, state machine but you can do protocols or app components, too. Many will complain about unreadability of C code. However, a proper spec or DSL for state machines makes them extremely readable with the C code autogenerated. They're also extremely easy to formally verify as you pointed out.

On page 15, you can see Rockwell-Collins combining model-driven development with Z, SPARK, and state-machines. It's a nice example of power of interacting, state machine approach combined with some other elements.

https://www.nsa.gov/resources/everyone/digital-media-center/...

[nitrogen]

If each state is a function that simply waits for events and returns the next state, the C code doesn't look that bad.

[nickpsecurity]

It doesn't look bad versus regular C. You still have the C-specific risks in the module and at module interfaces that other language reduce. It's also harder to parse, analyze, and compile in a secure way. With SPARK & formal tools, one can get a strong analysis that the code will always meet the spec. The ability to fully do that for C has only come online in the past few years. It appears to take more work, too.

[ArkyBeagle]

"Lack of robust first-class support" is no reason not to become well-versed in them. Static analysis is just as possible with them as with any other style in the chosen toolset.

Debugging is particularly straightforward - events cross states, yo. :) All you need is logging. Event detection code is particularly amenable to rigorous verification.

Toolchains like ObjecTime and Rational Rose had direct support for "coding using graphic representations of FSM" but the tools themselves were somewhat unwieldy and expensive and they sort of dinosaured.