[langsec-discuss] Parallel Systems/Automata
Harald Lampesberger
h.lampesberger at cdcc.faw.jku.at
Wed Jun 26 07:13:39 UTC 2013
What I know so far is that process calculi und temporal logics have the same goal to specify concurrency but from different standpoints. This is from the abstract in [1]:
"""
Research in the specification and verification of concurrent systems falls into two general categories. The temporal logic school advocates temporal logic as a language for formulating system requirements, with the semantics of the logic being used as a basis for determining whether or not a system is correct. The process-algebraic community focuses on the use of “higher-level” system descriptions as specifications of “lower-level” ones, with a refinement relation being used to determine whether an implementation conforms to a specification. From a user’s perspective, the approaches offer different benefits and drawbacks. Temporal logic supports “scenario-based” specifications, since formulas may be given that focus on single aspects of system behavior. On the other hand, temporal logic specifications suffer from a lack of compositionality, since the language of specifications differs from the system description language. In contrast, compositional specification is the hallmark of process algebraic reasoning, but at the expense of requiring what some view as overly detailed specifications.
"""
Regarding expressiveness, basically all full-blown process calculi are Turing complete [2], therefore no hierarchy.
I think the distributed nature of software brings some interesting attack vectors. For example, the cloud hype promotes software architectures where distributed components implement different parts of the underlying business process and extensively use message queues for interaction. Yes, it allows scalability and availability BUT we lose consistency according to Brewer's CAP theorem. The question is, where exactly do we loose the consistency? I think hidden race-conditions between the distributed components are a good example. Or, even better, what if there is a weird machine over distributed components?
Personally, I would be interested in this topic and it's on my agenda but not for this year. Currently, I am tied up with another topic on grammatical inference for langsec. For the interested ones: I just uploaded my paper "A Grammatical Inference Approach to Language-Based Anomaly Detection in XML" [3]. Let me know what you think about it!
Cheers,
Harald
[1] http://link.springer.com/chapter/10.1007%2F3-540-48320-9_1
[2] http://www.brics.dk/NS/03/2/BRICS-NS-03-2.ps.gz
[3] http://arxiv.org/abs/1306.5898
On 25.06.2013, at 18:54, Meredith L. Patterson <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.
>
> Cheers,
> --mlp
>
> 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.
>
> Cheers,
> Harald
>
>
> 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
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
More information about the langsec-discuss
mailing list