Modeling Adversaries with TLA+
hillelwayne.com
Modeling Adversaries with TLA+
1–10 of 14 posts
Re: Modeling Adversaries with TLA+
#2this 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).
Re: Modeling Adversaries with TLA+
#3Anyone have a similar how-to for applying this to decision-making (eg. game theory) in TLA+, Python or similar?
Re: Modeling Adversaries with TLA+
#4The author mentions the World and the Machine by Michael Jackson, I am guessing that is a reference to this paper?
Re: Modeling Adversaries with TLA+
#5> 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.
Re: Modeling Adversaries with TLA+
#6this 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).
Use of Formal Methods at Amazon Web Services
https://lamport.azurewebsites.net/tla/formal-methods-amazon....
Re: Modeling Adversaries with TLA+
#7Used 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.
Re: Modeling Adversaries with TLA+
#8The 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
I got the terms from _Software Requirements and Specifications_, which is a fun, if fluffy and meandering, read. I only skimmed the paper you linked but it seems to be a more thorough treatment than the book was.
https://www.amazon.com/Software-Requirements-Specifications-...
Re: Modeling Adversaries with TLA+
#9Used 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 inte…
> Didn't find it added more value than other formal methods with less scope and ambition
For my own future reference, can you list a few other formal methods?
Re: Modeling Adversaries with TLA+
#10Anyone have a similar how-to for applying this to decision-making (eg. game theory) in TLA+, Python or similar?
I don't know any game theory so can't say much about the landscape, but I know people've modified PRISM to model games: http://www.prismmodelchecker.org/games/
Fair warning though: PRISM is... weird. You can analyze some crazy complex properties in it but you don't get basic affordances like "strings", "lists", or "functions that take parameters".