Pierpaolo Degano

Lorenzo Ceragioli, Pierpaolo Degano, Letterio Galletta et al.

In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange environments as a formal setting where agents specify and obey exchange policies, which are declarative statements about what resources they offer and what they require in return. Furthermore, we introduce a decidable extension of the computational fragment of linear logic as a fundamental tool for representing exchange environments and studying their dynamics in terms of provability.

Matteo Busi, Job Noorman, Jo Van Bulck et al.

Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features, brings a risk of introducing new such side-channel attacks. This paper studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. We propose to use full abstraction as a formal criterion for the security of a processor extension, and we instantiate that criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility of these enclaves. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor, and evaluate the cost of our design in terms of performance and hardware size.

Matteo Busi, Pierpaolo Degano, Letterio Galletta

Obfuscating compilers protect a software by obscuring its meaning and impeding the reconstruction of its original source code. The typical concern when defining such compilers is their robustness against reverse engineering and the performance of the produced code. Little work has been done in studying whether the security properties of a program are preserved under obfuscation. In this paper we start addressing this problem: we consider control-flow flattening, a popular obfuscation technique used in industrial compilers, and a specific security policy, namely constant-time. We prove that this obfuscation preserves the policy, i.e., that every program satisfying the policy still does after the transformation.

Matteo Busi, Pierpaolo Degano, Letterio Galletta

Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is available to check if a compilation chain meets such requirements. Here, we outline our ongoing research inspired by translation validation, to effectively check one of those principles.

Chiara Bodei, Pierpaolo Degano, Gian-Luigi Ferrari et al.

The Internet of Things (IoT) is smartifying our everyday life. Our starting point is IoT-LySa, a calculus for describing IoT systems, and its static analysis, which will be presented at Coordination 2016. We extend the mentioned proposal in order to begin an investigation about security issues, in particular for the static verification of secrecy and some other security properties.