Lorenzo Ceragioli

PhD - Assistant Professor at IMT Lucca

IMT
unipi
My face
mail lorenzo.ceragioli@imtlucca.it
office San Ponziano Library, Lucca
researchgate Lorenzo Ceragioli
github lceragioli
corriculum vitae CV [pdf]
publications dblp

Interests and Activities

I'm an assistant professor at IMT Lucca, and part of the SySMA research group. My research interests include modeling and verification of quantum systems and formal methods for computer security, in particular applied to Access Control.

Short Bio

I obtained a master degree “cum laude” in Computer Science at the University of Pisa, in 2018. In the same year I started a Ph.D course in computer science in Pisa, which I dedicated to language-based security as a student of Pierpaolo Degano and Letterio Galletta. In collaboration with research groups from Ca’ Foscari, ETH Zurich and King’s College, I focused on the application of formal methods to real-world scenarios of security, targeting widespread technologies for access control: firewalls, operating systems and collaborative distributed environments. After receiving my Ph.D in 2022, I started working as a research fellow with Fabio Gadducci on assessing behavioural equivalence for quantum processes. I am a co-supervisor of Giuseppe Lomurno and Gabriele Tedeschi (in Pisa), and of Edoardo Lunati (IMT Lucca).

Teaching

Slides

Selected Publications

  • C. Bodei, L. Ceragioli, P. Degano, R. Focardi, L. Galletta, F. L. Luccio, M. Tempesta, L. Veronese,
    FWS: Analyzing, maintaining and transcompiling firewalls,
    Journal of Computer Security 2021 - Volume 29(1)
  • L. Ceragioli, P. Degano, L. Galletta,
    Can my firewall system enforce this policy?,
    Computer & Security 2022 - Volume 117
  • L. Ceragioli, L. Galletta, P. Degano, D. Basin,
    IFCIL: An Information Flow Configuration Language for SELinux,
    CSF 2022. Extended Version Here
  • L. Ceragioli, F. Gadducci, G. Lomurno, G. Tedeschi,
    Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers,
    POPL 2024. Extended Version Here
  • L. Ceragioli, F. Gadducci, G. Lomurno, G. Tedeschi,
    Effect Semantics for Quantum Process Calculi,
    CONCUR 2024.

Preprints

Thesis

Automi Cellulari, una rassegna

My bachelor thesis, in italian, is an overview on cellular automata and their computational power. We give a general definition of the model and recap the main classical results of cellular automata theory, we briefly introduce their characterization as topological dynamical systems, and define reversibility and conservation laws. Then we present the problem of the definition of computation cellular auomata and the indirect way of proving universality through simulation. Finally we give some examples by presenting various cellular automata that simulates turing equivalent models both in two and one dimension.

Transcompilazione fra Linguaggi di Firewall, sintesi e generazione di configurazioni

My master thesis, in italian, is an extention of a previous work that proposes a transcompilation pipeline between firewall configuration languages. It is composed by three steps: (i) encoding of the source configuration into a common intermediate language having a formal semantics, (ii) synthesis of an abstract and handy representation of the behaviour of the configuration, and (iii) generation of a configuration for the target system having the desired semantics. In the manuscript, we propose a new intermediate representation based on a denotational semantic for the intermediate language, and a pair of more general algorithm for the stages (ii) and (iii). We also study the expressivity of firewall languages, surprisingly discovering that they have different expressive power.

Access Control Policies Across Abstraction Layers

My PhD thesis analyses the management of Access Control systems where the low level representation of the actual enforcing mechanisms is paired with a high level representation that abstract away from implementation details and allow the administrator to easily read and write their policies. These two different representations must be coherent. For granting this we develop different theoretical solutions and apply them to different contexts: firewalls, operating systems and collaborative environments, obtaining usable tools that bridge theory and real-world application of computer security.

Others

Two very basic web applications for cellular automata follow. They where used for avoiding to draw at hand figures for my bachelor thesis. The first one allow you to fill some cells of a grid and then to export the picture as TikZ code. The second one simulates for you an elementary cellular automaton (you can choose which rule); as before you can export the resulting picture as TikZ code.