TGC 2011 Accepted Papers with Abstracts

Marco Bernardo Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Sequential Processes

Abstract: The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted at steady state between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner's construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. The resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions.

Carme Alvarez, Amalia Duch, Maria Serna and Dimitrios Thilikos On the existence of Pure Nash Equilibria in Strategic Search Games

Abstract: We consider a general multi-agent framework in which a set of n agents are roaming a network (such as Internet or a social network) where m valuable and sharable goods (or resources or services or information) are hidden in m different vertices of the network.
We analyze several strategic situations that arise in this setting by means of game theory. To do so we introduce a class of strategic games tha we call search games. In a search game each agent has to select a simple path starting from a predetermined set of initial vertices. Depending on how the retrieved goods are splitted among the agents we consider two search game types: finders-share in which the agents that find a good split among them the corresponding benefit and first-share in which only the agents that first find a good share the corresponding benefit. We show that finders-share games always have pure Nash equilibria (\PNE). For obtaining this result we introduce the notion of Nash preserving reduction between strategic games. We show that finders-share search games are Nash reducible to single-source network congestion games. This is done through a series of Nash preserving reductions. For first-share search games we show the existence of games with and without \PNE. Furthermore we identify some graph families in which the first-share search game has always a \PNE that is computable in polynomial time.
We conclude with some considerations on variations of the game with regard to the type of strategies and the social benefits that can be of interest to this type of games.

Joaquim Gabarro, Maria Serna and Alan Stewart Orchestrating unreliable services: strategic  and probabilistic approaches to reliability

Abstract: The robustness of orchestrations to service failure  can be analysed  using Angel Daemon games.
The reliability of an orchestration O is found by characterising a users perception of underlying services and by making assumptions about the number of services in the alphabet of O that will fail during an evaluation (uncertainty profiles).
The Nash equilibria of games associated with uncertainty profiles provide a posteriori information about the the probability of orchestration success.  
In this approach probabilities are second class objects since  they are  derived  from calculated Nash equilibria.
Alternatively, probabilistic characterisations of failing services can be given  from the outset (probabilistic profiles).
Uncertainty profiles and probabilistic profiles provide complementary  techniques for investigating the robustness of web-based orchestrations.  
In this paper the relationship between the two approaches is investigated.
A means of adding probabilistic information to an uncertainty profile is proposed -- hybrid profiles give rise to  bayesian variations of angel-daemon games.

Liliana D'Errico and Michele Loreti Compositional specification of distributed systems

Abstract: Distributed and mobile systems are typically composed of heterogeneous computational units that interact with each other following a predefined protocol.
Process algebras and modal logics have been largely used as tools for specifying and verifying such kind of systems.
However, to use these tools, a complete system description has to be provided. This is not always possible. Indeed, even if the protocol governing the interactions among the system components is completely specified, the precise implementation of each component, as well as the number of network elements, is generally unknown.
In this paper we present a set of formal tools that permits specifying systems by means of "mixed specifications": a system is not considered in isolation, but under the assumption that the enclosing environment satisfies a given set of properties.
A model-checking algorithm is also defined to verify whether considered specifications satisfy or not the expected properties. In the case,  it is also guaranteed that whenever the context is instantiated with components satisfying the assumptions, property satisfaction is preserved.

Liqun Chen, Ming-Feng Lee and Bogdan Warinshi Security of the Enhanced TCG Privacy-CA Solution

Abstract: The privacy-CA solution (PCAS) designed by the Trusted Computing Group (TCG) was
specied in TCG Trusted Platform Module (TPM) Specication Version 1.2 in 2003 and allows a TPM to obtain from a certication authority (CA) certicates on short term keys. The PCAS protocol is a lighter alternative to the Direct Anonymous Attestation (DAA) scheme for anonymous platform authentication.
The first rigorous analysis of PCAS was recently performed by Chen and Warinschi who focus on an unforgeability property (a TPM cannot obtain a certicate without the CA knowing its identity). The analysis in that paper holds only when no TPM is corrupt as, otherwise, an attack can be easily mounted. The authors also propose a stronger protocol (which we refer to as the enhanced PCAS or ePCAS) intended to withstand attacks of corrupt TPMs, but the protocol had never been formally analyzed.
The contribution of this paper is two-fold. We formalize three security properties desired from the ePCAS protocol. Unforgeability renes the earlier model for the case where TPMs may be corrupted. Deniability is the property that a CA cannot prove to a third party that he engaged in a run of the protocol with a certain TPM. Finally, anonymity is the property that third parties cannot tell the identity of TPMs based on the certicates that the TPM uses. The second contribution are proofs that the ePCAS protocol does indeed satisfy the security requirements that we formalize in this paper.

Maria Grazia Buscemi, Mario Coppo, Mariangiola Dezani-Ciancaglini and Ugo Montanari Constraints for Service Contracts

Abstract: This paper focuses on client-service interactions distinguishing between three phases: negotiate, commit and execute. The participants negotiate their behaviours, and if an agreement is reached they commit and start an execution which is guaranteed to respect the interaction scheme agreed upon. These ideas are materialised through a calculus of contracts enriched with semiring-based constraints, which allow clients to choose services and to interact with them in a safe way. A concrete representation of these constraints with logic programs is straightforward, thus reducing constraint solution (and consequently the establishment of a contract) to the execution of a logic program.

Gilles Barthe and Exequiel Rivas Static enforcement of information flow policies for a concurrent  object-oriented language

Abstract: An essential security goal of mobile code platforms is to protect confidential data against untrusted third-party applications; yet, prevailing mechanisms for ensuring confidentiality of mobile code are limited to sequential programs, whereas existing applications are generally concurrent. To bridge this gap, we develop a sound information-flow type system for a JVM-like, low-level concurrent object-oriented language. The type system builds upon existing solutions for object-oriented languages and concurrency, solving a number of intricate issues in their combination. Moreover, we connect the type system for bytecode programs to a type system for Java programs, extending the results of type-preserving compilation developed in earlier works.

Rocco De Nicola, Andrea Margheri and Francesco Tiezzi Orchestrating Tuple-based Languages

Abstract: The World Wide Web can be thought of as a global computing architecture supporting the deployment of distributed networked applications. Currently, such applications can be programmed by resorting mainly to two distinct paradigms: one devised for orchestrating  distributed services, and the other designed for coordinating distributed (possibly mobile) agents. In this paper, the issue of designing a programming language aiming at reconciling orchestration and coordination is investigated. Taking as starting point the orchestration calculus Orc and the tuple-based coordination language Klaim, a new formalism is introduced combining concepts, patterns and primitives of the original calculi. To demonstrate feasibility and effectiveness of the proposed approach, a prototype implementation of the new formalism is described and it is then used to tackle a simple case study dealing with a simplified but realistic electronic marketplace, where a number of on-line stores allow client applications to access information about their goods and to place orders.

Chenyi Zhang Unwinding Theorems for Conditional Information Flow Policies

Abstract: In this paper, we present a framework of information flow security policies, following the works of Goguen and Meseguer on the notions of noninterference and unwinding theorems. The framework allows actions to act as controlling channels on the availability of sensitive information, which subsumes intransitive noninterference policies. We propose sound and complete characterisation of such policies by unwinding, which we believe will benefit verification of the security properties defined in the framework.

Dominic Duggan and Ye Wu Transactional Correctness for Secure Nested Transactions

Abstract: Secure Nested Transactions are an adaptation of traditional nested transactions to support the synergy of language-based security and multi-level database security.  They have application in security for enterprise applications, where transactional semantics are a critical feature in middleware systems.  This article considers  correctness in terms of transactional properties for secure nested transactions.  Correctness is expressed in terms of a labeled transition system, the TauZero calculus.

Hernan Melgratti and Christian Roldan On correlation sets and correlation exceptions in ActiveBPEL

Abstract: Correlation sets are a programming primitive that allows instance identification in orchestration languages. A correlation set is a set of properties (i.e., values carried on by messages) that are used to associate each received message with a process instance: every time a service receives a message, it explores its content and determines a service instance that should handle the received message.  Based on a concrete implementation, this paper proposes a formal model for correlation sets accounting for correlation exceptions. We also investigate different type systems aimed at ensuring that orchestrators are free from some kind of correlation exceptions.