Gian-Luigi Ferrari

Paolo Bernardi, Antonio Brogi, Gian-Luigi Ferrari et al.

Quantum computing is a disruptive technology that is expected to offer significant advantages in many critical fields (e.g. drug discovery and cryptography). The security of information processed by such machines is therefore paramount. Currently, modest Noisy Intermediate-Scale Quantum (NISQ) devices are available. The goal of this work is to identify a practical, heuristic methodology to evaluate security properties, such as secrecy and integrity, while using quantum processors owned by potentially untrustworthy providers.

Rocco De Nicola, Gianluigi Ferrari, Rosario Pugliese et al.

We review some results regarding specification, programming and verification of different classes of distributed systems which stemmed from the research of the Concurrency and Mobility Group at University of Firenze. More specifically, we examine the distinguishing features of network-aware programming, service-oriented computing, autonomic computing, and collective adaptive systems programming. We then present an overview of four different languages, namely Klaim, Cows, Scel and AbC. For each language, we discuss design choices, present syntax and semantics, show how the different formalisms can be used to model and program a travel booking scenario, and describe programming environments and verification techniques.

Stefano Forti, Gian-Luigi Ferrari, Antonio Brogi

Assessing the security level of IoT applications to be deployed to heterogeneous Cloud-Edge infrastructures operated by different providers is a non-trivial task. In this article, we present a methodology that permits to express security requirements for IoT applications, as well as infrastructure security capabilities, in a simple and declarative manner, and to automatically obtain an explainable assessment of the security level of the possible application deployments. The methodology also considers the impact of trust relations among different stakeholders using or managing Cloud-Edge infrastructures. A lifelike example is used to showcase the prototyped implementation of the methodology.

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.