Software security, parametrized model checking, probabilistic model checking, runtime verification & enforcement (RV&E), intrusion & malware detection, machine learning, blockchain
The research focuses on the application of formal methods and artificial intelligence to cybersecurity and software engineering, particularly blockchain-oriented software engineering.
Formal methods include design-time formal verification and runtime formal verification.
Design-time verification involves modeling software as parametric and probabilistic (timed) automata in order to verify their hyperproperties, which are modeled as indexed and probabilistic (timed) temporal logic formulas. On the one hand, the research aims to study and define correct and complete model checking algorithms and cutoff theorems for verifying such systems. On the other hand, the research aims to apply these formal methods to verify complex systems for vulnerabilities and attack patterns. In the latter case, an intrusion model is required. A significant example of a complex system is decentralized applications (i.e., blockchain applications).
Runtime verification involves the synthesis of monitors starting from formal specifications. Monitors can be verification monitors (generating alarms when the monitored system’s execution does not comply with specifications) or enforcement monitors (modifying the monitored system’s execution to ensure compliance with specifications). Monitors can be centralized or decentralized (i.e. blockchain-based). Research aims to define algorithms for synthesizing decentralized monitors.
As for artificial intelligence, in this case machine learning, it can be used to classify the behavior of networks and hosts for malware protection. Research aims to define ensemble architectures and appropriate embedding techniques to detect different classes of malware. In particular, such architectures have been applied to domain name classification, where both feature-based and feature-free classification models are used to search for algorithmically generated domain names. Such architectures have also been applied to traffic analysis in software-defined networks (SDN).
Finally, distributed ledgers (DLTs), particularly blockchains, and smart contracts can be used to notarize, certify, and enforce event compliance.
Regarding certification, the research aims to define trust models for oracles, especially inbound and cross-chain ones.
Regarding enforcement, the research aims to ensure the compliance of a sequence of actions with given choreographies.
Alpen-Adria-Universität Klagenfurt (Austria) – Technische Universität Wien (Austria) – Sintef Ocean Trondheim (Norway) – Sintef Digital Trondheim (Norway) – Katholieke Universiteit Leuven (Belgium) – Université Catholique de Louvain (Belgium) – University of Chieti-Pescara ”G. D’Annunzio” (Italy) – Pegaso University (Italy) – Agenzia per la Cybersicurezza Nazionale (ACN) (Italy)
