Lorenzo Ceragioli
PhD - Research Fellow
lorenzo.ceragioli@phd.unipi.it | |
office room | 383, Dipartimento di Informatica |
telephone | 050 22 3808 |
researchgate | Lorenzo Ceragioli |
github | lceragioli |
corriculum vitae | CV [pdf] |
publications | dblp |
Interests and Activities
I'm a research fellow in Computer Science at the university of Pisa. My research insterests include theoretical computer science and formal methods for computer security.
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.
Slides
- Smart Contracts on Blockchains [pdf]
- Model Checking Quantum Circuits [pdf]
- QWIRE - A Core Language for Quantum Circuits [pdf]
- Access Control Policies Across Abstraction Layers [pdf]
- MuAC - Access Control Language for Mutual Benefits [pdf]
- High Level Management of Firewall Configurations [pdf]
- Are All Firewall Systems Equally Powerful? [pdf]
- From Firewalls to Functions and Back [pdf]
- Computational Fields: SMuC and CFC, two models compared [pdf]
- Epistemic Logic for Security [pdf]
- Mode Systems for Logic Languages, the case of Mercury [pdf] (Italian)
Publications
- From Firewalls to Functions and Back,
(ITASEC 2019), Pisa, Italy, February 13-15, 2019 - Are All Firewall Systems Equally Powerful?,
(PLAS 2019), London, UK, November 15, 2019 - Checking the Expressivity of Firewall Languages,
The Art of Modelling Computational Systems 2019 - Lecture Notes in Computer Science 11760 - MuAC: Access Control Language for Mutual Benefits,
(ITASEC 2020), Ancona, Italy, February 4-7, 2020 - FWS: Analyzing, maintaining and transcompiling firewalls,
Journal of Computer Security 2021 - Volume 29(1) - Can my firewall system enforce this policy?,
Computer & Security 2022 - Volume 117 - IFCIL: An Information Flow Configuration Language for SELinux,
(to appear in - CSF 2022), Haifa, Israel, August 7 - 10, 2022. Extended Version Here
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.