Current Projects - Selected

AI4VET4AI : AI-powered Next Generation of VET

Funding : ERASMUS Lump Sum Grant

Duration : 2023-2027

Role : Consultant

The objective of AI4VET4AI is to form a transnational European platform of VET excellence that will help bridge the current AI-related non-IT skills gap, which is actively obstructing stronger deployment of AI solutions in the EU. In doing so, we will empower VET providers to acknowledge and embrace their share of the AI transformation effort. Our project partnership is composed of policy makers, VET providers, research institutions, and AI occupational sector organizations representing AI companies. We will map the AI-related skills gap for non-IT experts on the job market, in particular in industries health, tourism, agriculture, business management and smart city planning (they could hugely profit from higher acceptance rates of AI). Based on this, we will create 10 high-tech MOOC courses for VET students (IVET) and adult on-the-job training, ready to be deployed in modular form by VET providers. We will ensure support for VET teachers and trainers in form of teacher training materials. We will launch 8 AI VET campuses and 7 VET innovation incubators, in which VET learners will learn how to use AI for strengthening their problem-solving skills. In total, more than 1.000 VET learners will go through our programmes in the course of project, with many more to profit in its aftermath. In 2018 the European Union has vowed to become the world-leading region for developing and deploying cutting-edge, ethical and secure AI. Our project will bring us one step closer to this goal.

The project is funded by Erasmus LS Grant and costs approx. 5 Mio €.

ASM2S : Automated Synthesis of Runtime Monitors for Safe & Secure Distributed Industrial Systems

Funding : HFRI

Duration : 2022-2025

Role : Co-I

ASM2S aims at developing methods and tools for the automated synthesis of runtime security monitors for distributed applications of industrial processes. The monitor will detect computational and false data injection attacks, combining verification techniques for computational attacks and fault diagnosis techniques for dynamic systems in order to detect false data injection attacks. The objectives are (1) the development of behavior‐based methods for detecting deviations of a distributed application execution from the specified behavior of a correct application specification, (2) the development of fault detection and diagnosis methods for false data injection attacks in distributed industrial applications, (3) the development of a unified monitoring methodology that combines the above methods, and (4) the development of a method and a tool the automatically synthesizes a monitor using the unified monitoring framework.

The project is funded by HFRI and I am serving as an expert in cyber security jointly with world leading cyber security researchers including Howard Shrobe from MIT CSAIL who is currently a program manager at DARPA and Marilyn Wolf from the University of Nebraska-Lincoln. For current activities of the project, please visit here

RESCUER : first RESponder Centred support toolkit for operating in adverse and infrastrUcture-less EnviRonments

Funding : H2020

Duration : 2021-2024

Role : Co-I

RESCUER aims to design and develop an FR-centered technology toolkit that will empower the next-generation of First Responders by enhancing their operational capacity and safety, specifically in adverse conditions, both environmental and infrastructure-wise. RESCUER will deliver a toolkit offering (1) sense augmentation through enhanced sensorial input, (2) precise and infrastructure-less self-positioning, (3) cognitive support and multi-sense AR interfaces, improving their focus and capability to utilise information and (4) robust ad-hoc intra-team communications for both verbal and data exchanges, all delivered over enhanced power and communication autonomy features. Extending the above capabilities, through the concept of a building black box, RESCUER will also introduce the capability of extracting environment information “in situ and infrastructure-wise”, during a disaster.

The project is funded by H2020 and costs approx. 8 Mio €. For current activities of the project, please visit here

SEEROSE : Responsible Safe and Secure Robotic Systems Engineering

Funding : Karl Popper Kolleg

Duration : 2021-2024

Role : Foreign Expert

Robot ethics demands programmers to write code that is not only functionally correct but also secure and safe to disallow any intended or accidental harm to humans. Hence, programmers bear a responsibility w.r.t. several instances (e.g., system customers, providers, end-users, etc.), for which awareness is required (likewise for questions of liability, which is a complex matter of contemporary research and legislation). SEEROSE aims at achieving usable robotic security by jointly addressing process ethical, psychological, and technical aspects of developing safe and secure robotics systems.

The project is funded by Karl Popper Kolleg. For current activities of the project, please visit here

ENSURESEC : End-to-end Security of the Digital Single Market’s E-commerce and Delivery Service Ecosystem

Funding : H2020

Duration : 2020-2022

Role : P.I.

ENSURESEC will be a sociotechnical solution for safeguarding the Digital Single Market’s e-commerce operations against cyber and physical threats. It provides an automatic, rigorous, distributed and open-source toolkit for protecting the e-commerce infrastructure, with monitoring of the impact of threats in physical space and a campaign for training SMEs and citizens aimed at creating awareness and trust. It addresses the whole gamut of modern e-commerce, from standard physical products purchased online and delivered via post, to entirely virtual products or services delivered online.

The project is funded by H2020 and costs approx. 10 Mio €. For current activities of the project, please visit here

Software :

Following software were developed in the frame of this project.

Security-by-Design using Ladder Logic

Funding : Independent

Duration : 2020-Date

Role : Lead I.

The details will be added later.

 

Prospective Projects - Selected

Synthesizes of Runtime Security Monitoring for Distributed Applications

Funding : Independent

Duration : 2020-Date

Role : Lead I.

The details will be added later.

 

Past Projects - Selected

Ex Machina: The Emergence of the Legal Tech Industry and Future of the Legal Profession

Funding : HEIF (Higher Education Innovation Fund) UK

Duration : 2021-2021

Role : Co-I

The proposed project aims to provide a study on the emerging legal-tech industry, addressing the legal and technical aspects of innovative data-driven tools in the legal profession.

The project is funded by HEIF UK and costs approx. 25K £. For current activities of the project, please visit here

Runtime Security Monitoring

Funding : MIT CSAIL and QCRI

Duration : 2016-2018

Role : Lead I.

The goal of the project was to develop a system which allows target applications to continue rendering useful services even after successful (known or unknown) attack happens. The project is lead by Howard Shrobe (AIRE research group) and is an extension to AWDRAT middleware which is funded by DARPA's SRS (Self-Regenerative System) program. The motivation here is that today' cybersecurity tools are very limited as they are retrospective (i.e. catch things we have already seen) and focus on individual exploits instead of complex and multi-stage full campaign of an APT.

Software :

Following software was developed in the frame of this project.

Formal Verification of Computer Algebra Software

Funding : FWF, Austria

Duration : 2009-2014

Role : Project Assistant

In this project, we have developed a novel framework for the formal specification and verification of MiniMaple programs and its application to a non-trivial program package. MiniMaple is a substantial subset of the language of the computer algebra system Maple; in contrast to Maple (which is dynamically typed), we have equipped MiniMaple with a static type system. The main goal of the thesis is the application of light-weight formal methods to MiniMaple programs (annotated with types and behavioral specifications) for finding internal inconsistencies and violations of methods preconditions by employing static program analysis. This task is more complex for a computer algebra language like Maple as it supports non-standard types of objects and also requires abstract data types to model algebraic concepts and notions. As a starting point, we have defined and formalized the syntax, semantics, type system and specification language for MiniMaple. For verification, we automatically translate the annotated MiniMaple program into (a semantically equivalent program in) the intermediate language Why3ML of the verification tool Why3; from the translated program, Why3 generates verification conditions whose correctness can be proved by various automatic and interactive theorem provers (e.g. Z3 and Coq). Furthermore, we have defined a denotational semantics of MiniMaple and proved the soundness of the translation with respect to the operational semantics of Why3ML. Finally, we discuss the application of our verification framework to the Maple package DifferenceDifferential developed at our institute to compute bivariate difference-differential dimension polynomials using relative Groebner bases.
Further details of the project are available here.

 

Formal Verification of Space Mission Communication Protocols

Funding : University of Leicester, UK

Duration : 2007-2008

Role : Project Assistant

This research was carried out in the frame of project "Space Link Extension Service Management", which was sponsored and run by various space agencies, e.g. NASA, USA. The goal of the project was to study the (space mission communication protocols) specification documents provided by NASA and to

  1. find ambiguities and inconsistencies in the requirements of the protocols
  2. devise a unified protocol resolving the identified ambiguities
  3. specify the behavior of the proposed protocol and finally
  4. to verify various properties of the protocol, e.g. absence of dead-lock and information inconsistencies.

Further details of the project are available here.