scholarly journals A User-Friendly Verification Approach for IEC 61131-3 PLC Programs

Electronics ◽  
2020 ◽  
Vol 9 (4) ◽  
pp. 572 ◽  
Author(s):  
Jiawen Xiong ◽  
Gang Zhu ◽  
Yanhong Huang ◽  
Jianqi Shi
Keyword(s):  
Control Systems ◽  
Real Life ◽  
Programmable Logic ◽  
Proof Of Concept ◽  
Industrial Control ◽  
Industrial Control Systems ◽  
Specification Mining ◽  
Plc Program ◽  
User Friendly

Programmable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. In this paper, we present a specification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires users to review specifications mined from the program behaviors instead of model checking for specified specifications, which can greatly improve the efficiency of safety verification and is much easier for control system engineers to use. Moreover, we implement a proof-of-concept tool named PLCInspector that supports directly mining LTL specifications and data invariants from PLC programs. Two examples and one real-life case study are presented to illustrate its practicability and efficiency. In addition, a comparison with the existing verification approaches for PLC programs is discussed.

scholarly journals Analysis of Cyber Threats in the Connection Section of the Control System and Countermeasures Required

2021 ◽  
Vol 12 (6) ◽  
pp. 412-417
Author(s):  
Yangha Chun
Keyword(s):  
Control System ◽  
Control Systems ◽  
Real Life ◽  
Information Storage ◽  
Control Network ◽  
Security Measures ◽  
Industrial Control ◽  
Industrial Control Systems ◽  
Cyber Threats ◽  
Cyber Threat

In the past, the general practice for the control system network that manages and controls industrial facilities such as electric power, gas, oil, water, chemicals, automobiles, etc. was to install and operate this as an independent system, but over time the practice has gradually shifted toward the use of an open and standardized system. Until recently, most industrial control systems consisted of an independent network, and the possibility of cyber threat infringement was very low. As information storage media such as laptops or USB are connected to the control system for maintenance or management purposes, the possibility of cyber infringement is increasing. When the use of the control system's operational information increases due to beingVinked with the internal business system network or the Internet, countermeasures against external cyber threats must be provided.This paper analyzes and organizes the cyber threat factors that exist in the linking section connected to the industrial control system and other networks, examining domestic and foreign incidents of hacking of control systems to identify the vulnerabilities and security measures for each scenario in the control system network linkage section. Through this analysis, a method is suggested for establishing a control network that secures both availability and security, which are important in the control system, as well as the safe relay system in the configuration of the linkage between the control network and the business network, while addressing the vulnerabilities in the structure due to long-term use of the control system.This study analyzes cyber threat factors and real-life examples of infringements with the aim of providing approaches that will ensure industrial control systems can be operated safely and the risk of cyber hacking threats that occur in connection with other networks can be managed, and suggesting cyber security measures for the control system connection sections.

Ασφάλεια βιομηχανικών συστημάτων και εφαρμογών

2020 ◽  
Author(s):  
Κωνσταντίνος Κατσιγιάννης
Keyword(s):  
Control Systems ◽  
Industrial Control ◽  
Industrial Control Systems ◽  
Fuzz Testing

Στην παρούσα διατριβή αντιμετωπίζουμε το πρόβλημα της ασφάλειας των βιομηχανικών συστημάτων ελέγχου (Industrial Control Systems, ICS) και ειδικότερα των δικτυωμένων κόμβων τους, όπως τα συστήματα SCADA και PLC. Η διατριβή εστιάζει στην ανάπτυξη και υλοποίηση μεθοδολογίας ελέγχου που αφορά τον έλεγχο τρωτότητας υλοποιήσεων πρωτοκόλλων βιομηχανικών δικτύων. Οι μέθοδοι που προτείνονται, βασίζονται στην τεχνική fuzz testing, καθώς η τεχνική αυτή είναι ιδιαίτερα αποτελεσματική μέχρι σήμερα στην αποκάλυψη σφαλμάτων σε ένα ευρύ φάσμα εφαρμογών λογισμικού και πρωτοκόλλων. Προτείνουμε μια μεθοδολογία fuzz testing για έλεγχο ασφάλειας υλοποιήσεων πρωτοκόλλων ICS που επεκτείνει τις ήδη υπάρχουσες προσεγγίσεις και εργαλεία. Η προσέγγιση που ακολουθούμε προσαρμόζεται δυναμικά προσδιορίζοντας τις λειτουργίες και χαρακτηριστικά της ελεγχόμενης υλοποίησης. Στη συνέχεια αναπτύσσει συστηματικά δοκιμαστικές ακολουθίες, μειώνοντας τον χώρο δοκιμών μέσω διαμερισμού του εύρους τιμών σε κάθε πεδίο και εστιάζοντας στην εξέταση τιμών που έχουν αυξημένη πιθανότητα να προκαλέσουν σφάλματα. Προς αποτίμηση της μεθοδολογίας, παρουσιάζεται ως μελέτη περίπτωσης (case study) ο MTF-Storm, ένας προσαρμοσμένων χαρακτηριστικών (custom) πλήρως αυτοματοποιημένος ελεγκτής (tester, fuzzer), για έλεγχο σε βιομηχανικές συσκευές που υποστηρίζουν το πρωτόκολλο Modbus/TCP. Εξετάζονται πειραματικά ένας αριθμός υλοποιήσεων του πρωτοκόλλου και παρουσιάζονται τα αποτελέσματα και ευρήματα από την αποτίμηση του εργαλείου. Η διατριβή ολοκληρώνεται με την παρουσίαση συγκριτικών αποτελεσμάτων με άλλες προσεγγίσεις (εργαλεία fuzzing) που αναδεικνύουν τα πλεονεκτήματα της προτεινόμενης μεθοδολογίας.

scholarly journals MODELING AND VALIDATING A SECURE INTERCONNECTION BETWEEN INDUSTRIAL CONTROL SYSTEM AND CORPORATE NETWORK USING COLORED PETRI NET

2020 ◽  
Vol 12 (2) ◽  
pp. 45-61
Author(s):  
Adriano Borrego ◽  
Adilson Eduardo Guelfi ◽  
Anderson Aparecido Alves da Silva ◽  
Marcelo Teixeira de Azevedo ◽  
Norisvaldo Ferraz Jr ◽  
...  
Keyword(s):  
Best Practices ◽  
Control Systems ◽  
Process Improvement ◽  
Proof Of Concept ◽  
Industrial Control ◽  
Industrial Control Systems ◽  
Corporate Networks ◽  
Level Of Automation ◽  
Corporate Network ◽  
High Level

Industrial Control Systems (ICS) networks offer a high level of automation combined with high levels of control, quality,and process improvement. Since network corporate users have to access the ICS environment, these networks have to be interconnected. However, this interconnection can introduce risks to the systems and manufacturing processes, which leads to the need to ensure the interconnection is done safely. The objective of this paper is to perform modeling and validation of a proposed secure interconnection between ICS and corporate networks using Colored Petri Networks (CPN). In addition to the best practices published in related works, this paper recommends some integrated features like the use of terminal server service, secure manual uplinks, and unidirectional security gatewayto enhance environmental security. However, our main contribution is the validation process performed in a CPN, which made it possible to execute queries in the state space resulting from the simulation -that works as a proof of concept. As a result, thepaper presents a secure and validated model of interconnection between ICS and corporate networks, capable of being applied to any interconnection environment

Sign in / Sign up

Export Citation Format

Share Document