Since machine learning components are now being considered for integration in safety-critical systems, safety stakeholdersshould be able to provide convincing arguments that the systems are safe for use in realistic deployment settings. In the caseof vision-based systems, the use of tree ensembles calls for formal stability verification against a host of composite geometricperturbations that the system may encounter. Such perturbations are a combination of an affine transformation like rotation,scaling, or translation and a pixel-wise transformation like changes in lighting. However, existing verification approachesmostly target small norm-based perturbations, and do not account for composite geometric perturbations. In this work,we present a novel method to precisely define the desired stability regions for these types of perturbations. We propose afeature space modelling process that generates abstract intervals which can be passed to VoTE, an efficient formal verificationengine that is specialised for tree ensembles. Our method is implemented as an extension to VoTE by defining a new propertychecker. The applicability of the method is demonstrated by verifying classifier stability and computing metrics associatedwith stability and correctness, i.e., robustness, fragility, vulnerability, and breakage, in two case studies. In both case studies,targeted data augmentation pre-processing steps were applied for robust model training. Our results show that even modelstrained with augmented data are unable to handle these types of perturbations, thereby emphasising the need for certifiedrobust training for tree ensembles.

Intrusion Detection Systems (IDSs) can help bolster cyber resilience in high-risk systems by promptly detecting anomalies and thwarting security threats which could have catastrophic consequences. While Machine Learning (ML) techniques like Tree Ensembles are well suited for tasks like detecting anomalies, the widespread adoption of these techniques in IDSs faces barriers due to the threat of evasion attacks. Moreover, ML-based IDSs are susceptible to producing a high rate of false positive alerts during detection, causing alert fatigue. To alleviate these problems, we present a method that uses counterexample regions to detect evasion attacks in tree-ensemble-based IDSs. We generate these counterexample regions by defining a modified mapping checker in VoTE, a fast & scalable formal verification tool specialized for tree ensembles. Our method also provides quaternary annotations, empowering security managers with nuanced insights to better handle alerts in the triage queue. Our approach does not require training a separate model and displays good detection performance (≥98 %) in both adversarial & non-adversarial scenarios in four real-world case studies when compared to several approaches in the literature. The prototype system we implement based on our method called Iceman has a very low prediction latency, making it 5-115x faster than the current state-of-the-art in evasion detection for tree ensembles. Finally, empirical evaluations show that Iceman can correctly re-annotate the samples in the presence of evasion attacks for alert management purposes with an accuracy of more than 98 % .

Safety-critical functions in modern vehicles rely on electronic control units that communicate using the controller area network (CAN) protocol, which lacks vital security features. In this context, machine learning (ML) based intrusion detection systems (IDSs) were proposed as a solution to improve cyber resilience through real-time attack detection. However, these ML-IDSs must also withstand evasion attacks that could compromise vehicular safety. To this end, this paper addresses such attacks in misuse-based tree ensemble IDSs and proposes a method that detects evasion attempts. It uses the ordered set of reached leaf nodes activated by correctly classified training samples as a normality baseline. An autoencoder-based detector then identifies deviations as likely evasion attempts. Our approach does not modify the protected tree ensemble IDS, assumes no knowledge of the process for generating adversarial examples (ensuring generalisability), and works with any additive tree ensemble. We also prove that it is mathematically equivalent to the state-of-the-art, which we advance in terms of detection speed by replacing its Hamming distance-based deviation search with an autoencoder-based model of typical predictive behavior trained using our custom loss function. This enhancement results in a detection process that is orders of magnitude faster. Additionally, our method offers nuanced insights regarding the pre-evasion attack signature prior to the adversarial perturbation, thereby enriching the security analysis of the features targeted during evasion attempts. The prototype system we present, called Maverick, has a very low prediction latency, making it 85-563x faster than the current state-of-the-art while maintaining identical detection accuracy. Finally, Maverick predicts the pre-evasion attack signatures of the evasion samples with an accuracy of more than 93% and has an average prediction time well below the message transmission rate for CAN 2.0 and CAN FD, thereby satisfying the criteria for an evasion-hardened & real-time automotive IDS.