Current Research Interests

  • Safety and Security in autonomous robots
  • Verification of security policies within ROS2-based applications
  • Verification of functional behavior of ROS-based applications
  • Verification of Access Control policies over low-level OS code
  • Applying formal methods for the verification of real-time operating systems
  • Schedulability Analysis

    • Scientific activities

    PhD students:
  • Iliass Mellal, FS - UM5, "Security verification within V2X communication system"
    • Interns:
  • Amine Nasri, ENSIAS - UM5, "Access control analyses using Frama-C"
  • Mohammed Amine Layachi, FS - UIT, "Aided formal verification using neural networks"
    • Master projects:
  • EDRISI: an AI-based real-time traffic management system
  • Implementing the confidentiality between nods communications in ROS2

    • Postdoc Project

    In the context of H2020 ENSURESEC european project, we to use Frama-C for detecting security threats in operating systems. The projects aims to enhance privacy and/or security by checking their properties at the code level. To do so, a dedicated language is proposed to express allow expressing of such properties over the code of the target OS.

    PhD Project

    Implementing a new scheduling policy within a real-time operating system is a real challenge. Moving from an abstract literary specification of a policy to an implementation within a real platform requires the consideration of several constraints. Consequently, a scheduler implementation work shall imperatively be supported by a verification effort to give it a level of confidence to validate the compliance of the implemented scheduler behavior with its literary specification. In our thesis project, we investigate the use of formal methods for the verification of real-time scheduler implementations. We propose a model-checking based approach, which we conduct on global scheduler implementations carried out on an OSEK/VDX-compliant real-time operating system. Accordingly, for each implementation, a model describing its behavior is elaborated with finite state and timed machines. This model is stimulated by generators producing indeterministic scenarios of scheduling events in order to observe the reaction of the implementation under various situations. Based on these situations, the verification is then conducted by examining the satisfaction of a set of specified requirements according to the expected behavior of the implementation as stipulated in the literature. This approach allowed the verification of the functional correction of the behavior of two implementations of global schedulers in a real-time operating system: G-EDF and EDF-US. It may also be used to verify other implementations on other systems.

    Projects

    H2020 - ENSURESEC (2020 - 2021): Extensive Code Security Analyses for Frama-C

    Events

  • ICECOCS 2022 - PC member
    • JRWRTC 2018 - PC member