Display Omitted Cyber-physical systems need holistic methods to discover relationships between physical and cyber components.Security threats attempt to both physical and cyber elements.Model-driven techniques accounting for joint physical and cyber-security modelling and evaluation are explored.Synergies between physical and cyber security UML profiles remarked in a case study of the railway domain. The multifaceted nature of cyber-physical systems needs holistic study methods to detect essential aspects and interrelations among physical and cyber components. Like the systems themselves, security threats feature both cyber and physical elements. Although to apply divide et impera approaches helps handling system complexity, to consider just one aspect at a time does not provide adequate risk awareness and hence does not allow to design the most appropriate countermeasures. To support this claim, in this paper we provide a joint application of two model-driven techniques for physical and cyber-security evaluation. We apply two UML profiles, namely SecAM (for cyber-security) and CIP_VAM (for physical security), in combination. In such a way, we demonstrate the synergy between both profiles and the need for their tighter integration in the context of a reference case study from the railway domain.

The growing need to find proper countermeasures able to protect critical infrastructures from threats has addressed the definition of quantitative methodologies for risk assessment. One of the most difficult aspects in this topic is the evaluation of the effects of attacks. Attacks Trees represent one of the most used formalisms in the modeling of attack scenarios: notwithstanding some extensions have been proposed to enrich the expressiveness of the original formalism, some effort should be spent on their analyzability. This paper defines a transformational approach that translates Attack Trees into Bayesian Networks. The proposed approach can cope with different Attack Trees extensions; moreover, it allows the quantitative evaluation of combined attacks modelled as a set of Attack Trees

Critical infrastructures as water treatment, power distribution, or telecommunications, provide daily services essential to our lifestyle. Any service discontinuity can have a high impact into our society and even into our safety. Thus, security of these systems against intentional threats must be guaranteed. However, many of these systems are based on protocols initially designed to operate on closed, unroutable networks, making them an easy target for cybercriminals. In this regard, Modbus is a widely adopted protocol in control systems. Modbus protocol, however, lacks for security properties and is vulnerable to plenty of attacks (as spoofing, flooding, or replay, to name a few). In this paper, we propose a formal modeling of Modbus protocol using an extension of hierarchical state-machines that is automatically transformed to a Promela model. This model allows us to find counterexamples of security properties by model-checking. In particular, the original contribution of this paper is the formal demonstration of the existence of man-in-the-middle attacks in Modbus-based systems. Our approach also allows to formally evaluate security properties in future extensions of Modbus protocols.