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.

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 % .

The evolution of the fifth-generation network (5G) increases the demand and use of Internet of Things (IoT) devices extensively. The increased number of IoT devices increases the possibility of new attack surfaces, and thus even resource-constrained IoT devices need secure communication. In this work, we consider the Julia Key Agreement (JKA) protocol, which has been proposed as a secure and efficient protocol for communication among resource-constrained IoT devices. We formally model two variants of the JKA protocol and verify the intended security requirements, such as mutual authentication, forward secrecy, backward secrecy, and resilience to key impersonation attacks, using the Tamarin prover. Our formal analysis shows that the JKA protocol is susceptible to replay attacks under the Dolev-Yao threat model. We also expand the threat model by including several strong threat assumptions to discover interesting attack vectors.

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.

The term "digital twin" (DT) has become a key theme of the cyber-physical systems (CPSs) area, while remaining vaguely defined as a virtual replica of an entity. This article identifies DT characteristics essential for enhancing CPS security and discusses indicators to evaluate them.

Deciding where to handle services and tasks, as well as provisioning an adequate amount of computing resources for this handling, is a main challenge of edge computing systems. Moreover, latency-sensitive services constrain the type and location of edge devices that can provide the needed resources. When available resources are scarce there is a possibility that some resource allocation requests are denied. In this work, we propose the VioLinn system to tackle the joint problems of task placement, service placement, and edge device provisioning. Dealing with latency-sensitive services is achieved through proximityaware algorithms that ensure the tasks are handled close to the end-user. Moreover, the concept of spare edge device is introduced to handle sudden load variations in time and space without having to continuously over-provision. Several spare device selection algorithms are proposed with different cost/performance tradeoffs. Evaluations are performed both in a Kubernetes-based testbed and using simulations and show the benefit of using spare devices for handling localized load spikes with higher quality of service (QoS) and lower computing resource usage. The study of the different algorithms shows that it is possible to achieve this increase in QoS with different tradeoffs against cost and performance.

In this paper, we apply a grammar-based approach to generate computation and communication platforms for avionic applications with mixed classes of time-sensitive communication messages. Then, we propose an evolutionary algorithm to schedule communication in the platform considering the interaction between timetriggered and bandwidth-constrained traffic. Together, the platform generation approach and the scheduling algorithm support the exploration of avionic systems at the concept level.

Supervisory and Data Acquisition (SCADA) systems control and monitor modern power networks. As attacks targeting SCADA systems are increasing, significant research is conducted to defend SCADA networks including variations of anomaly detection. Due to the sensitivity of real data, many defence mechanisms have been tested only in small testbeds or emulated traffic that were designed with assumptions on how SCADA systems behave. This work provides a timing characterization of IEC-104 spontaneous traffic and compares the results from emulated traffic and real traffic to verify if the network characteristics appearing in testbeds and emulated traffic coincide with real traffic. Among three verified characteristics, two of them appear in the real dataset but in a less regular way, and one does not appear in the collected real data. The insights from these observations are discussed in terms of presumed differences between emulated and real traffic and how those differences are generated.

Analyzing the resource adequacy of complex cyber-physical systems at concept development stage can be a challenging task since there are a lot of uncertainties about the system at this stage. In Integrated Modular Avionics (IMA) systems, with a life-cycle over several decades and potential functionality changes, we need to estimate resource needs at the early stage but leave capacity to absorb future modifications. Given an envisaged set of functions and a mapping to a candidate platform, one needs to assure that the selected network configuration will provide adequate resources to meet communication timeliness. In particular, whether the set of switches, the topology, and the available bandwidth are sufficient to meet the envisaged needs. In this paper, timeliness requirements are expressed as constraints on the freshness of data and a strict bounding of end-to-end latency. We support generation of UML/MARTE-based specifications by creating a domain-specific meta-model for IMA systems and a resource modelling approach for the study of time-critical systems. The instances of this model then specify the application requirements and various network configurations that can be formally analyzed. We present a tool, M2NC, for automatic derivation of a network calculus model through model transformation, and use the state-of-art NC tools for deriving the bounds for end-to-end timeliness. The approach is illustrated on an example avionics case study, consisting of 91 computational processes that exchange 629 different types of messages. The results of the analysis show that our approach can efficiently provide feedback on configurations that are compliant with the requirements imposed by the application and the toolchain provides a systematic mechanism to quickly identify potential future bottlenecks.

n/a