Abstract
Large-scale distributed systems appear as the major infrastructures for supporting planet-scale services. These systems call for appropriate management mechanisms and protocols. Slicing is an example of an autonomous, fully decentralized protocol suitable for large-scale environments. It aims at organizing the system into groups of nodes, called slices, according to an application-specific criteria where the size of each slice is relative to the size of the full system. This allows assigning a certain fraction of nodes to different task, according to their capabilities. Although useful, current slicing techniques lack some features of considerable practical importance. This paper proposes a slicing protocol, that builds on existing solutions, and addresses some of their frailties. We present novel solutions to deal with non-uniform slices and to perform online and dynamic slices schema reconfiguration. Moreover, we describe how to provision a slice-local Peer Sampling Service for upper protocol layers and how to enhance slicing protocols with the capability of slicing over more than one attribute. Slicing is presented as a complete, dependable and integrated distributed systems primitive for large-scale systems.

Abstract

Abstract
Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper, we extend previous results supporting the practicality of self-composition proofs of non-interference and generalizations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We formalize these policies and propose a formal verification approach based on self-composition, extending the range of security policies that could previously be handled using this technique. We demonstrate our results by addressing compliance with the NaCl security policies in real-world cryptographic code, highlighting the potential for automation of our techniques.

Abstract
We present work in progress on the development of EasyBV, a specialized theorem prover for fixed-size bit-vector arithmetic. © 2013 Authors.

Abstract
A central issue in program verification is the generation of verification conditions (VCs): proof obligations which, if successfully discharged, guarantee the correctness of a program vis-a-vis a given specification. While the basic theory of program verification has been around since the 1960s, the late 1990s saw the advent of practical tools for the verification of realistic programs, and research in this area has been very active since then. Automated theorem provers have contributed decisively to these developments. This paper establishes a basis for the generation of verification conditions combining forward and backward reasoning, for programs consisting of mutually-recursive procedures annotated with contracts and loop invariants. We introduce also a visual technique to verify a program, in an interactive way, using Verification Graphs (VG), where a VG is a Control Flow Graph (CFG) whose edges are labeled with contracts (pre- and postconditions). This technique intends to help a software engineer to find statements that are not valid with respect to the program's specification.

Abstract
Searching for resources over unstructured networks is usually supported by broadcast communication primitives. Ideally, the broadcast process should be cancelled as soon as possible after a successful discovery, to avoid flooding the entire network. However, cancelling an ongoing broadcast is challenging and may increase the number of exchanged messages. In this paper, we compare the cancellation mechanisms used by BERS and BERS* with new proposed cancellation approaches BCIR and BCIR*. The formulation of a simplified analytical model and the simulation results show that: i) it is possible to reduce the number of retransmitted messages, without increasing the latency observed in BERS*; and ii) BCIR is more energy efficient, which can contribute to extend the availability of mobile battery powered devices. Copyright 2013 ACM.