Although awareness is constantly rising, that industrial computer networks (in a very broad sense) can be exposed to serious cyber threats, many people still think that the same countermeasures, developed to protect general-purpose computer networks, can be effectively adopted also in those situations where a physical system is managed/controlled through some distributed Information and Communication Technology (ICT) infrastructure. Unfortunately, this is not the case, as several examples of successful attacks carried out in the last decade, and more frequently in the very recent past, have dramatically shown. Experts in this area know very well that often the peculiarities of industrial networks prevent the adoption of classical approaches to their security and, in particular, of those popular solutions that are mainly based on a detect and patch philosophy. This paper is a contribution, from the security point of view, to the assessment of the current situation of a wide class of industrial distributed computing systems. In particular, the analysis presented in this paper takes into account the process of ensuring a satisfactory degree of security for a distributed industrial system, with respect to some key elements such as the system characteristics, the current state of the art of standardization and the adoption of suitable controls (countermeasures) that can help in lowering the security risks below a predefined, acceptable threshold.

Testing equivalence is a powerful means for expressing the security properties of cryptographic protocols, but its formal verification is a difficult task because of the quantification over contexts on which it is based. Previous articles have provided insights into using theorem-proving for the verification of testing equivalence of spi calculus specifications. This article addresses the same verification problem, but uses a state exploration approach. The verification technique is based on the definition of an environment-sensitive, labeled transition system representing a spi calculus specification. Trace equivalence defined on such a transition system coincides with testing equivalence. Symbolic techniques are used to keep the set of traces finite. If a difference in the traces of two spi descriptions (typically a specification and the corresponding implementation of a protocol) is found, it can be used to automatically build the spi calculus description of an intruder process that can exploit the difference.

The availability of performance studies and simple models for firewalls able to deal with industrial application-layer communication protocols, like Modbus/TCP, is crucial when the impact of these devices has to be estimated, even roughly, before their actual deployment in industrial networks. Unfortunately, most manufacturers do not provide this kind of information for COTS available products. Thus, a viable solution is the development and experimental validation of simple models that can be used by designers to predict those firewall characteristics not explicitly related to their security capabilities. As an example, latency introduced on message forwarding is an aspect of significant interest in many industrial control systems, where delays and jitters in data delivery can severely impact on the effectiveness of the control actions. This paper reports on our experience in developing a performance model for a commercial device able to perform advanced application-layer filtering, in particular of Modbus/TCP traffic. A set of ad-hoc designed experiments, performed by means of a purposely-developed laboratory testbed, enabled both model development and validation, confirming a good correspondence of the estimated performance with the device actual behavior.

In modern factories, personal computers are starting to replace traditional programmable logic controllers, due to cost and flexibility reasons, and also because their operating systems now support programming environments even suitable for demanding real-time applications. These characteristics, as well as the ready availability of many software packages covering any kind of needs, have made the introduction of PC-based devices at the factory field level especially attractive. However, this approach has a profound influence on the extent of threats that a factory computing infrastructure shall be prepared to deal with. In fact, industrial personal computers share the same kinds of vulnerabilities with their office automation counterparts. Then, their introduction increases the risk of cyber-attacks. As the complexity of the network grows, the problem rapidly becomes hard to tackle by hand, due to the subtle and unforeseen interactions that may occur among apparently unrelated vulnerabilities, thus bearing the focus on the full automation of the analysis. Going into this direction, this paper presents a software tool that, given an accurate and machine-readable description of vulnerabilities, detects whether or not they are of concern and evaluates consequences in the context of a factory network.