Abstract
Gossip-based protocols have been gaining an increasing interest from the research community due to the high resilience to node churn and high scalability, thus making them suitable to modern large-scale dynamic systems. Unfortunately, these properties come at the cost of redundant message transmissions to ensure bimodal delivery to all interested peers. In systems with high message throughput, those additional messages could pose a significant burden on the excess of required bandwidth. Furthermore, the overlays upon which message dissemination takes place are oblivious to the underlying network, or rely on posterior optimizations that bias the overlay to mimic the network topology. This contributes even more to the required bandwidth as 'undesirable' paths are chosen with equal probability among desired ones. In a Cloud Computing scenario, nodes tend to be aggregated in sub-nets inside a data-center or in multiple data-centers, which are connected by costlier, long-distance links. The goal of this work is, therefore, to build an overlay that approximates the structure of the physical network, while ensuring the connectivity properties desirable to ensure reliable dissemination. By having each node judiciously choose which nodes are in its dissemination list at construction time, i.e. by giving preference to local nodes, we are able to significantly reduce the number of messages traversing the long-distance links. In a later stage, this overlay shall be presented as a service upon which data dissemination and management protocols could be run. Copyright 2009 ACM.

Abstract
The current exponential growth of data calls for massive-scale capabilities of storage and processing. Such large volumes of data tend to disallow their centralized storage and processing making extensive and flexible data partitioning unavoidable. This is being acknowledged by several major Internet players embracing the Cloud computing model and offering first generation remote storage services with simple processing capabilities. In this position paper we present preliminary ideas for the architecture of a flexible, efficient and dependable fully decentralized object store able to manage very large sets of variable size objects and to coordinate in place processing. Our target are local area large computing facilities composed of tens of thousands of nodes under the same administrative domain. The system should be capable of leveraging massive replication of data to balance read scalability and fault tolerance. Copyright 2009 ACM.

Abstract

Abstract

Abstract
This paper presents techniques developed to check program equivalences in the context of cryptographic software development, where specifications are typically reference implementations. The techniques allow for the integration of interactive proof techniques (required given the difficulty and generality of the results sought) in a verification infrastructure that is capable of discharging many verification conditions automatically. To this end, the difficult results in the verification process (to be proved interactively) are isolated as a set of lemmas. The fundamental notion of natural invariant is used to link the specification level and the interactive proof construction process.

Abstract