Modeling Adversaries with TLA+

Used TLA+ for security/availability modeling at a previous venture. Didn't find it added more value than other formal methods with less scope and ambition when it came to implementation, but I had very limited resources and we were greenfield so the experience probably wasn't generally applicable.

IMHO (from an implementation perspective): (1) If state is a pain to model, this may be a symptom you aren't placing interfaces in the right places (ie. scope is too broad). (2) If your system behavior departs from known models (ie. expected behavior under rigorously analyzed and easy to model consensus algorithms) then this may be a symptom of larger issues such as unrecognized state or edge cases, which are better tackled first. (3) A practical alternative to the theoretical model of 'safe' machines within the post would be an implementation model with a functional approach ... ie. if in doubt, reset to known state. (4) To model "bad" actors practically, you have to define them. To do so within meaningfully any complex (black box) multi-agent (networked) system, you need a good model of known "good" behavior for any given node. Building this is IMHO more useful than pie-in-sky theoretical modeling, because it allows the efficient (~fully automatic) deployment of practical countermeasures (anomaly detection on resource utilization, communication, etc.). To do this for near-arbitrary systems requires a tight CI/CD pipeline with above-average full stack security insight, for-purpose infrastructure and management level commitment to the additional resources it will cost. Only when all that is done, model for concurrently compromised nodes at this level, because you've surpassed more immediate/pragmatic requirements.

The author mentions the World and the Machine by Michael Jackson, I am guessing that is a reference to this paper?

http://mcs.open.ac.uk/mj665/icse17kn.pdf

> In the TLA+ formulation, and we can think of an adversary as an agent in the system who can take a superset of the actions everybody else can.

Sounds a lot like a Dolev-Yao adversary, which is used in protocol verification tools like Tamarin.

An review of the post is at https://lemmster.de/tla-liveness-review.html

Anyone have a similar how-to for applying this to decision-making (eg. game theory) in TLA+, Python or similar?

this is the kind of dark magic that is fascinating to read about and I hope there are people actually using it in the described way to design and implement safe systems and protocols. I haven't heard of any (not that I looked much).