Systems Security, Modeling and Analysis
SySMA
About us
Mission
Systems Security Modelling and Analysis (SySMA) is the Research Unit at IMT Lucca that focuses on computer science.
SySMA deals with languages and techniques for the analysis, evaluation, and verification of systems. The SySMA unit goal is to use formal methods as methodological and automatic tools for developing high-quality, correct software and systems that are secure, fast, usable, reusable, maintainable, and modular.
We also study algorithms and systems to protect the security and integrity of computer systems, the information they store, and the people who use them. We make large usage of formal methods as enabling technology also for the security-by-design development model.
Research Topics
Artificial Intelligence
Concurrency theory
Cybersecurity
Data science
Machine learning
Modeling and simulation
Programming languages
Software engineering
Software and systems verification
Software performance modeling and control
Recent publications
G. Costa, P. Degano, L. Galletta, S. Soderi: Formally verifying security protocols built on watermarking and jamming. Comput. Secur. 128: 103133 (2023)
L. Di Stefano, R. De Nicola, O. Inverso : Verification of Distributed Systems via Sequential Emulation. ACM Trans. Softw. Eng. Methodol. 31(3): 37:1-37:41 (2022).
S. Soderi, R. De Nicola, 6G Networks Physical Layer Security Using RGB Visible Light Communications. IEEE Access 10: 5482-5496 (2022).
G. Caldarelli, R. De Nicola, M. Petrocchi, M. Pratelli , F. Saracco: Flow of online misinformation during the peak of the COVID-19 pandemic in Italy. EPJ Data Sci. 10(1): 34 (2021).
L. Faggi, A. Betti, D. Zanca, S. Melacci, M. Gori. "Local propagation of visual stimuli in focus of attention". Neurocomputing 560, 2023. doi: 10.1016/j.neucom.2023.126775.
A. Betti, M. Casoni, M. Gori, S. Marullo, S. Melacci and M. Tiezzi. "Neural Time-Reversed Generalized Riccati Equation". Proceedings of the AAAI Conference on Artificial Intelligence, 38(8) (2024), 7935-7942. doi: 10.1609/aaai.v38i8.28630
M. Tiezzi, S. Marullo, L. Faggi, E. Meloni, A. Betti, S. Melacci. "Stochastic Coherence Over Attention Trajectory For Continuous Learning In Video Streams". Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, pp. 3480-3486 (2022). doi: 10.24963/ijcai.2022/483.
S. Soderi and R. De Nicola. “6G Networks Physical Layer Security Using RGB Visible Light Communications”. In: IEEE Access 10 (2022), pp. 5482–5496. doi: 10.1109/access.2021.3139456.
S. Soderi, R. Colelli, F. Turrin, F. Pascucci, and M. Conti. “SENECAN: Secure KEy DistributioN OvEr CAN Through Watermarking and Jamming”. In: IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING 3 (2022), pp. 1–15. doi: 10.1109/TDSC.2022.3179562.
C. Perini Brogi. Curry-Howard-Lambek Correspondence for Intuitionistic Belief. Studia Logica 109 (6), pp. 1441–1461 (2021). doi: 10.1007/s11225-021-09952-3.
S. Soderi, A. Brighente, F. Turrin, and M. Conti. “VLC Physical Layer Security through
RIS-aided Jamming Receiver for 6G Wireless Networks”. In: 2022 19th Annual IEEE International Conference on Sensing, Communication, and Networking (SECON). New York: IEEE, 2022, pp. 370– 378. isbn: 978-1-6654-8643-9. doi: 10.1109/secon55815.2022.9918547.M. Maggesi, C. Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021). doi: 10.4230/LIPIcs.ITP.2021.26.
C. Pugliese, F. Lettich, F. Pinelli, C. Renso. Summarizing Trajectories Using Semantically Enriched Geographical Context, In Proceedings of the 31st ACM International Conference on Advances in Geographic Information Systems (2023). doi: 10.1145/3589132.3625587
C. Pugliese, F. Lettich, C. Renso, F. Pinelli. Semantic Enrichment of Mobility Data: A Comprehensive Methodology and the MAT-BUILDER System. In IEEE Access 11: pp. 90857-90875 (2023). doi: 10.1109/ACCESS.2023.3307824
G.Costa, F. Pinelli, S. Soderi, G. Tolomei. Turning Federated Learning Systems Into Covert Channels. In IEEE Access 10 (2022), pp.130642-130656. doi: 10.1109/ACCESS.2022.3229124
M. Maggesi, C. Perini Brogi. Mechanising Gödel–Löb Provability Logic in HOL Light. Journal of Automated Reasoning 67, 29 (2023). doi: 10.1007/s10817-023-09677-z
G. Garbi, E. Incerto, M. Tribastone. μP: A Development Framework for Predicting Performance of Microservices by Design. IEEE 16th International Conference on Cloud Computing (2023) (pp. 178-188).
E. Incerto, R. Pizziol, M. Tribastone. μOpt: An Efficient Optimal Autoscaler for Microservice Applications. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (2023) (pp. 67-76).
F. Randone, L. Bortolussi, E. Incerto, M. Tribastone. Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. Proceedings of the ACM on Programming Languages, (2024), (pp. 1882-1912).
M. Busi, J. Noorman, J. Van Bulck, L. Galletta, P. Degano, J. T. Mühlberg, F. Piessens. Securing interruptible enclaved execution on small microprocessors. ACM Transactions on Programming Languages and Systems 43:(3), (2021), doi: 10.1145/3470534
L. Ceragioli, L. Galletta, P. Degano, D. Basin. IFCIL: An Information Flow Configuration Language for SELinux. IEEE 35th Computer Security Foundations Symposium (CSF), 2022, pp. 243-259, doi: 10.1109/CSF54842.2022.9919690
L. Galletta, C. Laneve, I. Mercanti, A. Veschetti. 2023. Resilience of Hybrid Casper Under Varying Values of Parameters. ACM Distributed Ledger Technologies. 2(1),(2023), doi:10.1145/3571587
L. Ceragioli, F. Gadducci, G. Lomurno, G. Tedeschi: Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers. Proc. ACM Program. Lang. 8 (POPL) (2024). doi:10.1145/3632885