[langsec-discuss] Parallel Systems/Automata
h.lampesberger at cdcc.faw.jku.at
Tue Jun 25 16:42:39 UTC 2013
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,
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
More information about the langsec-discuss