[langsec-discuss] Parallel Systems/Automata
Meredith L. Patterson
clonearmy at gmail.com
Tue Jun 25 16:54:21 UTC 2013
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> 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.
> On 25.06.2013 17: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
> > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss