Computer Science

Software Security and Security Software
 
Description
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 PersonLuca Spalazzi
Collaborations:
  • Alpen-Adria-Universität Klagenfurt
  • Technische Universität Wien
    Projects:
    • Safe Round-Trip Software Engineering for Improving the Maintainability of Legacy Software Systems (Safe RTSE) - Funding: FFG Austria, Bridge 1, project number 850757 - Duration: November 2015 - April 2019
      People:
      • Luca Spalazzi
      • Francesco Spegni (technical staff)
      • Lucia Pepa (research fellow)