Software Engineering and Security

The Department's research in this area covers a rich variety of topics, including: automated static analysis, cryptography, formal language definitions, formal methods, formal security models, formal software verification, logic and verification, malware and its mitigation, massively parallel systems, network security, parallel programming languages, security protocols, security services, semantics, social aspects of security and privacy, software and application security, software architectures, software functional properties, software reverse engineering, software system models, software verification and validation, system description languages, trust frameworks, Unified Modeling Language (UML), web protocol security.

Documents

pdf Brochure di presentazione dell'area  (pdf,  it, 254 KB)
pdf Presentazione Research Day 2017  (pdf,  it, 5121 KB)
Mariano Ceccato
Associate Professor
Matteo Cristani
Associate Professor
Mila Dalla Preda
Associate Professor
Alessandra Di Pierro
Associate Professor
Roberto Giacobazzi
Full Professor
Isabella Mastroeni
Associate Professor
Massimo Merro
Full Professor
Federica Maria Francesca Paci
Associate Professor
Roberto Segala
Full Professor
Nicola Fausto Spoto
Associate Professor
Research interests
Topic People Description
Formal methods and theory of security standard compliant  ACM 2012
Formal methods and theory of security Matteo Cristani
Roberto Segala
Development of formal, and possibly automated, methods for the analysis of the security of software systems
Formal methods for security analysis of cyber-physical systems Massimo Merro
Development of formal, and possibly automated, methods for the security analysis of cyber-physical systems and IoT systems
Probabilistic Analysis of Security Alessandra Di Pierro
Roberto Segala
Static analysis of approximate security properties via Probabilistic Abstract Interpretation
Code protection Mariano Ceccato
Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Development of formal techniques and tools for the protection of software.
Network security standard compliant  ACM 2012
Network security Matteo Cristani
Development of techniques and tools for the security of computer networks
Software and application security standard compliant  ACM 2012
Formal software and application security Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Development of models and analyses, based on abstract interpretation, for the security application verification and for security properties enforcement.
Software and application security Federica Maria Francesca Paci
Development of security methodologies and technologies for the security of software systems and Internet applications
Software creation and management standard compliant  ACM 2012
Code synthesis Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Study and development of techniques for the synthesis of code (or code transformers) from the specification of semantic code properties.
Software creation and management Federica Maria Francesca Paci
Study and development of formal and semi-formal methodologies and technologies for the creation and management of software systems
Software organization and properties standard compliant  ACM 2012
Static Analysis Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Nicola Fausto Spoto
Study of techniques for the static analysis of programming languages. Inference of properties of the heap memory used by programs. Inference of security properties for information manipulated by computer programs.
Quantitative static analysis Alessandra Di Pierro
Study of formal methods for quantitative analysis of programs. Extension of classical program analysis techniques (data-flow, control-flow, abstract interpretation,type systems)to probabilistic and speculative analysis for program optimisation and transformation.
Verification of wireless network protocols Massimo Merro
Semantics-based and model-checking techniques for the verification of wireless network protocols
Gruppi di ricerca
Name Description URL
Blockchain L'attività del gruppo di ricerca riguarda diverse tematiche relative allo sviluppo e all'applicazione della tecnologia blockchain e dell'infrastruttura degli smart contracts.
ForME - Metodi Formali per la Progettazione di Sistemi Ingegneristici Obiettivo del gruppo di ricerca è applicare metodi formali alla modellazione, verifica e sintesi di sistemi ingegneristici. I domini spaziano dai sistemi temporizzati per andare fino ai sistemi ciberfisici non lineari.
Intelligenza Artificiale (IA) Il gruppo svolge ricerche in Intelligenza Artificiale: Ragionamento Automatico, Algoritmi di Ricerca, Rappresentazione della Conoscenza, Apprendimento Automatico, Sistemi Multi-Agenti e applicazioni.
K.Re.Art.I. Rappresentazione della conoscenza tramite tecniche di IJntelligenza Artificiale
Logica Logica in matematica ed informatica. https://www.logicverona.it/
Quantum Informatics Laboratory - QUILAB Laboratorio di Informatica Quantistica https://quilab.github.io
SPY
Projects
Title Managers Sponsors Starting date Duration (months)
Valorizzazione attività di ricerca Matteo Cristani DIGITRONICA.IT SRL 11/8/23 2
Organisation of informative events for the small and medium enterprises of the Veneto region and production of digital contents. Mariano Ceccato UNIONE REGIONALE DELLE CAMERE DI COMMERCIO INDUSTRIA ARTIGIANATO E AGRICOLTURA DEL VENETO 9/1/23 3
Study and formalization of an algorithm for the dynamic determination of the renting price of vehicles. Nicola Fausto Spoto Noleggiare s.r.l. 7/28/23 6
Software as an asset Matteo Cristani Veronesi Holding s.p.a. 7/6/23 4
Automated Testing of REST APIs Mariano Ceccato Muscope Cybersecurity S.r.l. 5/29/23 12
Studio di metodologie per lo sviluppo di strumenti e infrastrutture di trading meccanico Roberto Segala Investivity SA 5/2/23 36
Machine Learning for automated testing of REST APIs Mariano Ceccato Equixely s.r.l. 1/18/23 3
Requirement elicitation for an environmental engineering software framework for modelling the physical processes that control natural water cycle Mariano Ceccato MobyGIS Srl 7/21/22 3
Sviluppo di un motore semantico per l’analisi di descrizioni brevi di prodotti negli ordinativi Matteo Cristani IUNGO s.p.a. 6/8/22 3
Study and implementation of a verified solution in Go for dealing with SPID authentication. Nicola Fausto Spoto Tradenet Services SRL 4/20/22 8
Analisi generale del sistema informativo aziendale Matteo Cristani VENETO AGRICOLTURA - AGENZIA VENETA PER L’INNOVAZIONE NEL SETTORE PRIMARIO 12/20/21 20
Audit Colony Nicola Fausto Spoto Audit Colony SRL 11/1/21 12
SafePKT Nicola Fausto Spoto CJDNS SASU 7/1/21 6
BinTrace: Binary Similarity Analysis based on Execution Traces Mila Dalla Preda RELATECH SPA 10/1/20 12
Study and documentation of the Cosmos SDK for programming blockchains Nicola Fausto Spoto Commerc.io srl 10/1/20 2
Integration between the Takamaka language for smart contracts in Java and the blockchain Takamaka, with user documentation. Nicola Fausto Spoto Ailia SA 6/16/20 6
Software Watermarking Mila Dalla Preda Danieli Automation s.p.a. 6/10/20 14
The SMArt LAbel as a guarantee tool in the WInery-customer trust relationship for Venetian high quality Pgi wines) SMA.LA.WI Roberto Giacobazzi, Mila Dalla Preda Regione Veneto 4/1/19 36
Implementation of a Java Framework for Smart Contracts Nicola Fausto Spoto Ailia SA 1/1/19 12
Computer Engineering for Industry 4.0 Franco Fummi, Alessandro Farinelli MIUR 1/1/18 60
Development of Semantic Analysis Techniques for Java Code Nicola Fausto Spoto Julia s.r.l. 7/1/17 18
Big-code early threat detection by approximate similarity analysis Mila Dalla Preda Joint Projects - assegnato e gestito dal Dipartimento 3/1/17 24
Abstract Interpretation of COBOL Isabella Mastroeni Joint Projects - assegnato e gestito dal Dipartimento 3/1/17 24
Analisi e sviluppo di tecniche di analisi semantica di codice Java industriale Nicola Fausto Spoto Julia s.r.l. 7/1/15 24
La messa a punto di Strumenti innovativi per la ricerca semantica Nicola Fausto Spoto Corvallis S.p.A. 7/1/15 24
Studio e sperimentazione RIA (Rich Internet Application) per soluzioni web e mobile-RIA Nicola Fausto Spoto Add Value S.p.A. 1/16/15 12
TRENDS - Technologies and Resources for Exploiting interNet Documents and Social media - Joint Projects 2014 Nicola Fausto Spoto Techne Media Agency s.r.l. 1/1/15 24
Abstract interpretation based analysis of Scripting Languages - Joint Projects 2014 Isabella Mastroeni Joint Projects - assegnato e gestito dal Dipartimento 12/1/14 24
Interpretation-based design and measurement of code-protecting transformations Roberto Giacobazzi Joint Projects - assegnato e gestito dal Dipartimento 11/1/14 24
Static analysis methods for the static derivation Roberto Giacobazzi Julia s.r.l. 6/5/13 16
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 2/18/13 36
Security Horizons Luca Vigano' MIUR 2/1/13 36
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 1/1/13 30

Activities

Research facilities

Share