|Software Security and Security Software|
The research focuses on applying formal methods and artificial intelligence to cybersecurity and to blockchain-oriented software engineering. Concerning formal methods, they consist in modeling software as as Parameterized and Probabilistic (Timed) Automata in order to verify their hyperproperties modeled as indexed and probabilistic (timed) temporal logic formulas. On the one hand, the research aims at studying and defining sound and complete model checking algorithms and cutoff theorems for verifying such systems. On the other hand, the research aims at applying such formal methods to the verification of complex systems looking for vulnerabilities and attack patterns. In the latter case, an intruder model is required. A notable example of complex system is represented by decentralized applications (i.e. applications on blockchain). Concerning artificial intelligence, in this case machine learning, it can be used to classify network and host behavior searching for malware. In particular, both feature-based and featureless classification techniques are used to classify domain names, searching for algorithmically generated domain names.
|Laboratory DAISY at DII|
|Contact Person: Luca Spalazzi|