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.

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

Attacks against Supervisory Control and Data Acquisition (SCADA) systems operating critical infrastructures have increased since the appearance of Stuxnet. To defend critical infrastructures, security researchers need realistic datasets to evaluate and benchmark their defense mechanisms such as Anomaly Detection Systems (ADS). However, real-world data collected from critical infrastructures are too sensitive to share openly. Therefore, testbed datasets have become a viable option to balance the requirement of openness and realism. This study provides a data generation framework based on a virtual testbed with a commercial SCADA system and presents an openly available dataset called RICSel21, with packets in IEC-60870-5-104 protocol streams. The dataset is the result of performing 12 attacks, identifying the impact of attacks on a power management system and recording the logs of the seven successful attacks.

The edge computing paradigm comes with a promise of lower application latency compared to the cloud. Moreover, offloading user device computations to the edge enables running demanding applications on resource-constrained mobile end devices. However, there is a lack of workload models specific to edge offloading using applications as their basis.In this work, we build upon the reconfigurable open-source mixed reality (MR) framework MR-Leo as a vehicle to study resource utilisation and quality of service for a time-critical mobile application that would have to rely on the edge to be widely deployed. We perform experiments to aid estimating the resource footprint and the generated load by MR-Leo, and propose an application model and a statistical workload model for it. The idea is that such empirically-driven models can be the basis of evaluations of edge algorithms within simulation or analytical studies.A comparison with a workload model used in a recent work shows that the computational demand of MR-Leo exhibits very different characteristics from those assumed for MR applications earlier.

Recent advances in machine learning and artificial intelligence are now beingconsidered in safety-critical autonomous systems where software defects maycause severe harm to humans and the environment. Design organizations in thesedomains are currently unable to provide convincing arguments that their systemsare safe to operate when machine learning algorithms are used to implement theirsoftware.

In this paper, we present an efficient method to extract equivalence classes from decision trees and tree ensembles, and to formally verify that their input-output mappings comply with requirements. The idea is that, given that safety requirements can be traced to desirable properties on system input-output patterns, we can use positive verification outcomes in safety arguments.

This paper presents the implementation of the method in the tool VoTE (Verifier of Tree Ensembles), and evaluates its scalability on two case studies presented in current literature. We demonstrate that our method is practical for tree ensembles trained on low-dimensional data with up to 25 decision trees and tree depths of up to 20.Our work also studies the limitations of the method with high-dimensionaldata and preliminarily investigates the trade-off between large number of trees and time taken for verification.