1,721,096 research outputs found
Many-to-many information flow policies
No full textInformation flow techniques typically classify information according to suitable security levels and enforce policies that are based on binary relations between individual levels, e.g., stating that information is allowed to flow from one level to another. We argue that some information flow properties of interest naturally require coordination patterns that involve sets of security levels rather than individual levels: some secret information could be safely disclosed to a set of confidential channels of incomparable security levels, with individual leaks considered instead illegal; a group of competing agencies might agree to disclose their secrets, with individual disclosures being undesired, etc. Motivated by this, we study a semantic foundation for such properties based on causal models of computation. We propose a simple language for expressing information flow policies where the usual admitted flow relation between individual security levels is replaced by a relation between sets of security levels, thus allowing to capture coordinated flows of information. The flow of information is expressed in terms of causal dependencies and the satisfaction of a policy is defined with respect to an event structure that is assumed to capture the causal structure of system computations. We also preliminarily explore possibilities for practical applicability of our approach by focusing on systems specified as safe Petri nets, a formalism with a well-established causal semantics. We show how unfolding-based verification techniques for Petri nets can be adopted for solving the problem of checking policy satisfaction
Proceedings 6th Interaction and Concurrency Experience, ICE 2013
No full textThis volume contains the proceedings of ICE 2013, the 6th Interaction and Concurrency Experience workshop, which was held in Florence, Italy on the 6th of June 2013 as a satellite event of DisCoTec 2013. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a Wiki and associated with a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interests. The PC members post comments and questions that the authors reply to. Each paper was reviewed by three PC members, and altogether 6 papers were accepted for publication. We were proud to host two invited talks, Davide Sangiorgi and Filippo Bonchi, whose abstracts are included in this volume together with the regular papers. The workshop also featured a brief announcement of an already published paper
Guest Editorial: Special Issue on Service-Oriented Architectures and Programming
No full textThis special issue includes revised versions of selected papers that were presented at the Special Track
on Service-Oriented Architectures and Programming (SOAP) of the 29th Annual ACM Symposium on
Applied Computing (SAC 2014). SOAP 2014 was held in Gyeongju, Korea, in March 24-28, 2014. Its proceedings were published in a volume edited by Yookun Cho, Sung Y. Shin, Sang-Wook Kim, Chih-Cheng Hung and Jiman Hong and published by ACM in 2014. This special issue was motivated by the quality of the works presented at the conference and by the increasing proliferation of service-oriented systems in our society such as e-governance, e-health and e-commerce systems. We believe that the contributions in this volume provide a valuable example of
current research in this area. We also believe that the published works will contribute to the main aims of
the SOAP track, that is to transform Service-Oriented Programming (SOP) into a mature discipline with
both solid scientific foundations and mature software engineering development methodologies supported
by dedicated tools
A Graph Syntax for Processes and Services
No full textWe propose a class of hierarchical graphs equipped with a simple algebraic syntax as a convenient way to describe configurations in languages with inherently hierarchical features such as sessions, fault- handling scopes or transactions. The graph syntax can be seen as an intermediate representation language, that facilitates the encoding of structured specifications and, in particular, of process calculi, since it provides primitives for nesting, name restriction and parallel composition. The syntax is based on an algebraic presentation that faithfully characterises families of hierarchical graphs, meaning that each term of the language uniquely identifies an equivalence class of graphs (modulo graph isomorphism). Proving soundness and completeness of an encoding (i.e. proving that structurally equivalent processes are mapped to isomorphic graphs) is then facilitated and can be done by structural induction. Summing up, the graph syntax facilitates the definition of faithful encodings, yet allowing a precise visual representation. We illustrate our work with an application to a workflow language and a service-oriented calculus
Graphical Encoding of a Spatial Logic for the pi-Calculus
No full textThis paper extends our graph-based approach to the verification of spatial properties of π-calculus specifications. The mechanism is based on an encoding for mobile calculi where each process is mapped into a graph (with interfaces) such that the denotation is fully abstract with respect to the usual structural congruence, i.e., two processes are equivalent exactly when the corresponding encodings yield isomorphic graphs. Behavioral and structural properties of π-calculus processes expressed in a spatial logic can then be verified on the graphical encoding of a process rather than on its textual representation. In this paper we introduce a modal logic for graphs and define a translation of spatial formulae such that a process verifies a spatial formula exactly when its graphical representation verifies the translated modal graph formula
A Holistic Approach for Collaborative Workload Execution in Volunteer Clouds
Full text linkThe demand for provisioning, using, and maintaining distributed computational resources is growing hand in hand with the quest for ubiquitous services. Centralized infrastructures such as cloud computing systems provide suitable solutions for many applications, but their scalability could be limited in some scenarios, such as in the case of latency-dependent applications. The volunteer cloud paradigm aims at overcoming this limitation by encouraging clients to offer their own spare, perhaps unused, computational resources. Volunteer clouds are thus complex, large-scale, dynamic systems that demand for self-adaptive capabilities to offer effective services, as well as modeling and analysis techniques to predict their behavior. In this article, we propose a novel holistic approach for volunteer clouds supporting collaborative task execution services able to improve the quality of service of compute-intensive workloads. We instantiate our approach by extending a recently proposed ant colony optimization algorithm for distributed task execution with a workload-based partitioning of the overlay network of the volunteer cloud. Finally, we evaluate our approach using simulation-based statistical analysis techniques on a workload benchmark provided by Google. Our results show that the proposed approach outperforms some traditional distributed task scheduling algorithms in the presence of compute-intensive workloads
Replicating Data for Better Performances in X10
Full text linkLinguistic primitives for replica-aware coordination offer suitable solutions to the challenging problems of data distribution and locality in large-scale high-performance computing. The data replication mechanisms that had previously been designed to extend Klaim with replicated tuples are now used to experiment with X10, a parallel programming language primarily targeting clusters of multi-core processors linked in a large-scale system via high-performance networks. Our approach aims at allowing the programmer to specify and coordinate the replication of shared data items by taking into account the desired consistency properties. The programmer can hence exploit such flexible mechanisms to adapt data distribution and locality to the needs of the application, in order to improve performance in terms of concurrency and data access. We investigate issues related to replica consistency and provide a performance analysis, which includes scenarios where replica based specifications and relaxed consistency provide significant performance gains
Asynchronous Distributed Execution of Fixpoint-Based Computational Fields
Full text linkCoordination is essential for dynamic distributed systems whose components exhibit interactive and autonomous behaviors. Spatially distributed, locally interacting, propagating computational fields are particularly appealing for allowing components to join and leave with little or no overhead. Computational fields are a key ingredient of aggregate programming, a promising software engineering methodology particularly relevant for the Internet of Things. In our approach, space topology is represented by a fixed graph-shaped field, namely a network with attributes on both nodes and arcs, where arcs represent interaction capabilities between nodes. We propose a SMuC calculus where µ-calculuslike modal formulas represent how the values stored in neighbor nodes should be combined to update the present node. Fixpoint operations can be understood globally as recursive definitions, or locally as asynchronous converging propagation processes. We present a distributed implementation of our calculus. The translation is first done mapping SMuC programs into normal form, purely iterative programs and then into distributed programs. Some key results are presented that show convergence of fixpoint computations under fair asynchrony and under reinitialization of nodes. The first result allows nodes to proceed at different speeds, while the second one provides robustness against certain kinds of failure. We illustrate our approach with a case study based on a disaster recovery scenario, implemented in a prototype simulator that we use to evaluate the performance of a recovery strategy
Enhancing Threat Model Validation: A White-Box Approach based on Statistical Model Checking and Process Mining
No full textExploiting over- and under-approximations for infinite-state counterpart models
Full text linkSoftware systems with dynamic topology are often infini-testate. Paradigmatic examples are those modeled as graph transformation systems (GTSs) with rewrite rules that allow an unbounded creation of items. For such systems, verification can become intractable, thus calling for the development of approximation techniques that may ease
the verification at the cost of losing in preciseness and completeness. Both over- and under-approximations have been considered in the literature, respectively offering more and less behaviors than the original system. At the same time, properties of the system may be either preserved or
reflected by a given approximation. In this paper we propose a general notion of approximation that captures some of the existing approaches for GTSs. Formulae are specified by a generic quantified modal logic, one that also generalizes many specification logics adopted in the literature for GTSs. We also propose a type system to denote part of the formulae as either reflected or preserved, together with a technique that exploits
under- and over-approximations to reason about typed as well as untyped formula
- …
