[langsec-discuss] Parallel Systems/Automata
Carter Tazio Schonwald
carter.schonwald at gmail.com
Thu Jul 4 05:27:07 UTC 2013
one of the reasons why TLA / TLA+ or something similar are worth using seriously as tools is model checking!
you take care specifying the required "liveness" or "progress properties", and then write the "algorithm" or "decision rule " specification,
and I believe that under fairly general conditions, if your properties aren't true, you will get an explicit counter example!
That is a powerful thing! Its like a type check or parser generator giving you a helpful error message that shows you whats probably wrong, but for a protocol!
http://en.wikipedia.org/wiki/Temporal_logic and its sibling pages http://en.wikipedia.org/wiki/Linear_temporal_logic and http://en.wikipedia.org/wiki/Computation_tree_logic
these all basically work by virtue of the specs having a finite state space, or so via some abstraction, and enumerating them.
on a more "concrete" bent than TLA+ that is perhaps handy for experimentation is https://github.com/aphyr/timelike, which is meant as a way of writing a computational model then running it!
the point being: counter example driven refinement is a great learning / feedback tool! Especially if you care about liveness/correctness
On Tue, Jun 25, 2013 at 12:54 PM, Meredith L. Patterson <clonearmy at gmail.com (mailto:clonearmy at gmail.com)> wrote:
> I have indeed been meaning to forge ahead into the process calculi when I have a few more things off my plate. (Hammer is taking a lot of my time right now, and we're putting together a funding proposal for a standard library for it.) Len was particularly interested in Lamport's temporal logic of actions, though he never really explained why; it seems to me like whatever calculus suits the system ought to be appropriate. (Is there an analogy to the Chomsky hierarchy for the process calculi? Should there be? Much as langsec models input handling vulnerabilities as a failure to implement the formal model of an input syntax correctly, what sorts of vulnerabilities stem from bad assumptions about the model of a distributed system? Node.js has been bugging me for a while, and I think it has something to do with this.)
> The observation about parsing being a function from messages to actions is really nicely phrased.
> On Jun 25, 2013 6:43 PM, "Harald Lampesberger" <h.lampesberger at cdcc.faw.jku.at (mailto:h.lampesberger at cdcc.faw.jku.at)> wrote:
> > Hey Fabian,
> > one method to model distributed systems is process calculus. The
> > simplest calculi is "basic process algebra" (BPA). It looks similar to
> > regular expressions but is extended with additional operators for
> > interleaving, recursion and synchronization. The symbols in terms are
> > from a finite set and represent atomic actions.
> > There are many process calculi around that extend/restrict BPA, for
> > example Pi-calculus, CSP, CCS, pBPA, ambient calculus, ...
> > What can you do with this: By reducing a term that "describes" one or
> > more parallel processes you see whether the process(es) terminate(s) or
> > is free of deadlocks. Note that reduction is only the application of
> > syntactic rules and therefore computable!
> > Another thing you can do is bisimulation: show whether two terms,
> > representing two processes over a set of actions, are the same.
> > What are the effects of the langsec-view? Parsing a message sent between
> > processes is basically a function from messages to actions. Process
> > calculi assume that the set of actions is finite. But practical parsing
> > problems could lead to a situation, where a malicious message maps to an
> > action that is not in the action set of your formal process model. Or
> > worse, there might be infinite messages that map to infinite actions
> > outside the action set. Doh.
> > Langsec guarantees that the mapping (parsing) from messages to actions
> > (in the sense of a formal process) is precise and bounded. I lack the
> > experience to see if there is fruitful research hidden in combining the
> > langsec view and process calculi. Let me know if you pursue this further!
> > Hope that helps.
> > Cheers,
> > Harald
> > On 25.06.2013 17 (tel:25.06.2013%2017):25, Fabian Fäßler wrote:
> > > Thank you very much for your thoughts. I took the comments and thought about it again.
> > > So what he basically meant was about the distributed systems. Synchronization, deadlocks, race conditions, ...
> > >
> > > So what I am thinking is. In langsec we try to treat input languages, such as protocols as formal languages. But with a protocol in a network, you introduce even more problems. For example a deadlock - two correct deterministic automata on their own, are waiting for a message from eachother. So when you try to proof if a protocol is correct, you also have to proof that the state machines of the participants of the protocol can't run in the known problems of distributed systems. Am I wrong?
> > >
> > > Can anybody point me two well known papers about the problems with distributed systems?
> > >
> > > kind regards,
> > > Fabian
> > > _______________________________________________
> > > langsec-discuss mailing list
> > > langsec-discuss at mail.langsec.org (mailto:langsec-discuss at mail.langsec.org)
> > > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> > >
> > _______________________________________________
> > langsec-discuss mailing list
> > langsec-discuss at mail.langsec.org (mailto:langsec-discuss at mail.langsec.org)
> > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org (mailto:langsec-discuss at mail.langsec.org)
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss