Software security, runtime verification & enforcement (RV&E), malware detection, machine learning, blockchain
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. The research aims to define appropriate ensemble architectures and embedding techniques to detect different classes of malware. In particular, both feature-based and featureless classification techniques are used to classify domain names, searching for algorithmically generated domain names.
Finally, distributed ledgers (DLTs), blockchains in particular, and smart contracts can be used to enforce compliance of choreographies and processes, to issue immutable certifications (soulbound tokens) and to trace activities.
Alpen-Adria-Universität Klagenfurt (Austria) – Technische Universität Wien (Austria) – Sintef Ocean Trondheim (Norway) – Agenzia per la Cybersicurezza Nazionale (ACN) (Italy)
Safe RTSE – FFG Austria, Bridge 1, project no. 850757 – Safe Round-Trip Software Engineering for Improving the Maintainability of Legacy Software Systems – Duration: November 2015 – April 2019
