Modeling Wazuh rules with Weighted Timed Automata

at EUSPN 2024

with Anass Haydar

In the rapidly evolving landscape of cybersecurity, Endpoint Detection and Response (EDR) systems have emerged as a critical advancement in cybersecurity, providing organizations with enhanced capabilities to detect, investigate, and mitigate sophisticated attacks. The open-source EDR platform Wazuh is specifically highlighted as an attractive option for organizations and provides comprehensive security monitoring, threat detection, and incident response capabilities without the burden of licensing costs. A critical component of the Wazuh system is its rules set, which are predefined or custom-written conditions that analyze log data and system events to identify potential security threats, anomalies, or policy violations. These rules, typically written in XML format, form the core of Wazuh's threat detection capabilities. However, in complex architectures, the set of rules can be challenging to understand and update, and different rules can overlap, preempt, or cancel each other. To address this issue, we propose to model Wazuh rules as Weighted Timed Automata, which helps to verify that rules are well-triggered by verifying the reachability of the corresponding state in the automaton using the model checker Uppaal.

Parametric verification to ensure safe behaviour of connected devices

at AMDE 2024

With the surge of IoT devices, these systems must provide reliable services and make trustworthy decisions based on fast and accurate data analytics. Effective data analysis is crucial for IoT systems to make rapid decisions, gain insights, uncover hidden patterns, and interact with users and other systems efficiently. This work in progress aims to model connected devices as Parametric Timed Automata, allow them to share operating data on a blockchain and verify its good behaviour with this data. Operating data are seen as unknown constraints in Parametric Timed Automata and can be used to verify or improve models of connected devices, along with providing safety. We propose a framework to model simple connected devices, upload and download parameter through smart contracts and verify the safety of the produced behaviour.

Parametric analyses of attack-fault trees

in Fundamenta Informaticae, Volume 182, Issue 1, 2021, at ACSD 2019, pdf

with Étienne André, Didier Lime and Mariëlle Stoelinga

Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e., absence of unintentional failures) and security (i. e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree- based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parametrize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure.

Parametric updates in parametric timed automata

in Logical Methods in Computer Science, Volume 17, Issue 2, 2021, at FORTE 2019, pdf

with Étienne André, Didier Lime

We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.

On the expressive power of invariants in parametric timed automata

at ICECCS 2019

with Étienne André, Didier Lime

The verification of systems combining hard timing constraints with concurrency is challenging. This challenge becomes even harder when some timing constants are missing or unknown. Parametric timed formalisms, such as parametric timed automata (PTAs), tackle the synthesis of such timing constants (seen as parameters) for which a property holds. Such formalisms are highly expressive, but also undecidable, and few decidable subclasses were proposed. We propose here a syntactic restriction on PTAs consisting in removing guards (constraints on transitions) to keep only invariants (constraints on locations). While this restriction preserves the expressiveness of PTAs (and therefore their undecidability), an additional restriction on the type of constraints allows to not only prove decidability, but also to perform the exact synthesis of parameter valuations satisfying reachability. This formalism, that seems trivial at first sight as it benefits from the decidability of the reachability problem with a better complexity than Timed Automata (TAs), suffers from the undecidability of the whole TCTL logic that TAs, on the contrary enjoy. We believe our formalism allows for an interesting trade-off between decidability and practical expressiveness and is therefore promising. We show its applicability in a small case study.

TCTL model checking lower/upper-bound parametric timed automata without invariants

at FORMATS 2018

with Étienne André, Didier Lime

We study timed systems in which some timing features are unknown parameters. We consider Upper-bound Parametric Timed Automata (U-PTAs), one of the simplest extensions of timed automata with parameters, in which parameters are only used as clock upper bounds in the constraints. Up to now, there have been several decidability results for the existence of parameter values in U-PTAs such that non-nested TCTL formulas are satisfied. We prove here that this does not extend to the full logic and that only one level of nesting leads to undecidability. This provides, to the best of our knowledge, the first problem that is decidable for Timed Automata with an undecidable parametric emptiness version for U-PTAs.

Timed automata with parametric updates

with Étienne André, Didier Lime

at ACSD 2018