Biblio

In control systems, the operation of the system after an incident occurs is important. This paper proposes to design a whitelist model that can detect anomalies and identify locations of anomalous actuators using finite automata during multiple actuators attack. By applying this model and comparing the whitelist model with the operation data, the monitoring system detects anomalies and identifies anomaly locations of actuator that deviate from normal operation. We propose to construct a whitelist model focusing on the order of the control system operation using binary search trees, which can grasp the state of the system when anomalies occur. We also apply combinatorial compression based on BDD (Binary Decision Diagram) to the model to speed up querying and identification of abnormalities. Based on the model designed in this study, we aim to construct a secured control system that selects and executes an appropriate fallback operation based on the state of the system when anomaly is detected.

Industrial Control Systems (ICS) are not secure by design–with recent developments requiring them to connect to the Internet, they tend to be highly vulnerable. Additionally, attacks on critical infrastructures such as power grids and nuclear plants can cause significant damage and loss of lives. Since such attacks tend to generate anomalies in the systems, an efficient way of attack detection is to monitor the systems and identify anomalies in real-time. An automated anomaly detection tool is introduced in this paper. Additionally, the functioning of the systems is viewed as Finite State Automata. Specific sensor measurements are used to determine permissible transitions, and statistical measures such as the Interquartile Range are used to determine acceptable boundaries for the remaining sensor measurements provided by the system. Deviations from the boundaries or permissible transitions are considered as anomalies. An additional feature is the provision of a finite state automata diagram that provides the operational constraints of a system, given a set of regulated input. This tool showed a high anomaly detection rate when tested with three types of ICS. The concepts are also benchmarked against a state-of-the-art anomaly detection algorithm called Isolation Forest, and the results are provided.

This work-in-progress paper proposes a design methodology that addresses the complexity and heterogeneity of cyber-physical systems (CPS) while simultaneously proving resilient control logic and security properties. The design methodology involves a formal methods-based approach by translating the complex control logic and security properties of a water flow CPS into timed automata. Timed automata are a formal model that describes system behaviors and properties using mathematics-based logic languages with precision. Due to the semantics that are used in developing the formal models, verification techniques, such as theorem proving and model checking, are used to mathematically prove the specifications and security properties of the CPS. This work-in-progress paper aims to highlight the need for formalizing plant models by creating a timed automata of the physical portions of the water flow CPS. Extending the time automata with control logic, network security, and privacy control processes is investigated. The final model will be formally verified to prove the design specifications of the water flow CPS to ensure efficacy and security.

A considerable portion of computing power is always required to perform symbolic calculations. The reliability and effectiveness of algorithms are two of the most significant challenges observed in the field of scientific computing. The terms “feasible calculations” and “feasible computations” refer to the same idea: the algorithms that are reliable and effective despite practical constraints. This research study intends to investigate different types of computing and modelling challenges, as well as the development of efficient integration methods by considering the challenges before generating the accurate results. Further, this study investigates various forms of errors that occur in the process of data integration. The proposed framework is based on automata, which provides the ability to investigate a wide-variety of distinct distance-bounding protocols. The proposed framework is not only possible to produce computational (in)security proofs, but also includes an extensive investigation on different issues such as optimal space complexity trade-offs. The proposed framework in embedded with the already established symbolic framework in order to get a deeper understanding of distance-bound security. It is now possible to guarantee a certain level of physical proximity without having to continually mimic either time or distance.

Industrial Control System (ICS) communication transmits monitoring and control data between industrial processes and the control station. ICS systems cover various domains of critical infrastructure such as the power plants, water and gas distribution, or aerospace traffic control. Security of ICS systems is usually implemented on the perimeter of the network using ICS enabled firewalls or Intrusion Detection Systems (IDSs). These techniques are helpful against external attacks, however, they are not able to effectively detect internal threats originating from a compromised device with malicious software. In order to mitigate or eliminate internal threats against the ICS system, we need to monitor ICS traffic and detect suspicious data transmissions that differ from common operational communication. In our research, we obtain ICS monitoring data using standardized IPFIX flows extended with meta data extracted from ICS protocol headers. Unlike other anomaly detection approaches, we focus on modelling the semantics of ICS communication obtained from the IPFIX flows that describes typical conversational patterns. This paper presents a technique for modelling ICS conversations using frequency prefix trees and Deterministic Probabilistic Automata (DPA). As demonstrated on the attack scenarios, these models are efficient to detect common cyber attacks like the command injection, packet manipulation, network scanning, or lost connection. An important advantage of our approach is that the proposed technique can be easily integrated into common security information and event management (SIEM) systems with Netflow/IPFIX support. Our experiments are performed on IEC 60870-5-104 (aka IEC 104) control communication that is widely used for the substation control in smart grids.

This paper studies the use of Supervisory Control Theory to design and implement post-fault restoration schemes in a HVDC grid. Our study focuses on the synthesis of discrete controllers and on the management of variable control rules during the execution of the protection strategy. The resulting supervisory control system can be proven "free of deadlocks" in the sense that designated tasks are always completed.

Modern SoC applications include a variety of sensitive modules in which data must be protected against malicious access. Security vulnerabilities, when exercised during the SoC operation, lead to denial of service or disclosure of protected data. Hence, it is essential to undertake security validation before and after SoC fabrication and make provisions for continuous security assessment during operation. This paper presents a methodology for optimized post-deployment monitoring of SoC's security properties by migrating pre-fab design security assertions to post-fab run-time security monitors. We show that the method is scalable for large systems and complex properties by optimizing the hardware monitors and applying it to a large SoC design based on a OpenRISC-1200 SoC. About 40 security assertions were specified in System Verilog Assertions (SVA). Following formal verification, the assertions were synthesized into finite state machines and cross optimized. Following code generation in Verilog, commercial logic and layout synthesis tools were used to generate hardware monitors which were then integrated with the SoC design ready for fabrication.

In quantum cryptography research area, quantum digital signature is an important research field. To provide a better privacy for users in constructing quantum digital signature, the stronger anonymity of quantum digital signatures is required. Quantum ring signature scheme focuses on anonymity in certain scenarios. Using quantum ring signature scheme, the quantum message signer hides his identity into a group. At the same time, there is no need for any centralized organization when the user uses the quantum ring signature scheme. The group used to hide the signer identity can be immediately selected by the signer himself, and no collaboration between users.Since the quantum finite automaton signature scheme is very efficient quantum digital signature scheme, based on it, we propose a new quantum ring signature scheme. We also showed that the new scheme we proposed is of feasibility, correctness, anonymity, and unforgeability. And furthermore, the new scheme can be implemented only by logical operations, so it is easy to implement.

The article discusses new models and methods for timely identification and blocking of malicious code of critically important information infrastructure based on static and dynamic analysis of executable program codes. A two-stage method for detecting malicious code in the executable program codes (the so-called "digital bombs") is described. The first step of the method is to build the initial program model in the form of a control graph, the construction is carried out at the stage of static analysis of the program. The article discusses the purpose, features and construction criteria of an ordered control graph. The second step of the method is to embed control points in the program's executable code for organizing control of the possible behavior of the program using a specially designed recognition automaton - an automaton of dynamic control. Structural criteria for the completeness of the functional control of the subprogram are given. The practical implementation of the proposed models and methods was completed and presented in a special instrumental complex IRIDA.

Supervisor synthesis enables the design of supervisory controllers for large cyber-physical systems, with high guarantees for functionality and safety. The complexity of the synthesis problem, however, increases exponentially with the number of system components in the cyber-physical system and the number of models of this system, often resulting in lengthy or even unsolvable synthesis procedures. In this paper, a new method is proposed for reducing the model of the system before synthesis to decrease the required computational time and effort. The method consists of three steps for model reduction, that are mainly based on symmetry in dependency graphs of the system. Dependency graphs visualize the components in the system and the relations between these components. The proposed method is applied in a case study on the design of a supervisory controller for a road tunnel. In this case study, the model reduction steps are described, and results are shown on the effectiveness of model reduction in terms of model size and synthesis time.

The industrial Internet of Things (IIoT) can facilitate industrial upgrading, intelligent manufacturing, and lean production. Industrial control system (ICS) is a vital support mechanism for many key infrastructures in the IIoT. However, natural defects in the ICS network security mechanism and the susceptibility of the programmable logic controller (PLC) program to malicious attack pose a threat to the safety of national infrastructure equipment. To improve the security of the underlying equipment in ICS, a model checking method based on timed automata is proposed in this work, which can effectively model the control process and accurately simulate the system state when incorporating time factors. Formal analysis of the ICS and PLC is then conducted to formulate malware detection rules which can constrain the normal behavior of the system. The model checking tool UPPAAL is then used to verify the properties by detecting whether there is an exception in the system and determine the behavior of malware through counter-examples. The chemical reaction control system in Tennessee-Eastman process is taken as an example to carry out modeling, characterization, and verification, and can effectively detect multiple patterns of malware and propose relevant security policy recommendations.

With the explosion of Industry 4.0, industrial facilities and critical infrastructures are transforming into “smart” systems that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of industrial control systems. We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.'s edit automata, to enforce specification compliance in networks of potentially compromised controllers, formalised in Hennessy and Regan's Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet P and complying with the property e. Our monitors correct and suppress incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the synthesis, deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers.

When using digital signatures, we need to deal with the problem of fairness of information exchange. To solve this problem, Chen, etc. introduced a new conception which is named concurrent signatures in Eurocrypt'04. Using concurrent signatures scheme, two entities in the scheme can generate two ambiguous signatures until one of the entities releases additional information which is called keystone. After the keystone is released, the two ambiguous signatures will be bound to their real signers at the same time. In order to provide a method to solve the fairness problem of quantum digital signatures, we propose a new quantum concurrent signature scheme. The scheme we proposed does not use a trusted third party in a quantum computing environment, and has such advantages as no need to conduct complex quantum operations and easy to implement by a quantum circuit. Quantum concurrent signature improves the theory of quantum cryptography, and it also provides broad prospects for the specific applications of quantum cryptography.

Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.

A common way to characterize security enforcement mechanisms is based on the time at which they operate. Mechanisms operating before a program's execution are static mechanisms, and mechanisms operating during a program's execution are dynamic mechanisms. This paper introduces a different perspective and classifies mechanisms based on the granularity of program code that they monitor. Classifying mechanisms in this way provides a unified view of security mechanisms and shows that all security mechanisms can be encoded as dynamic mechanisms that operate at different levels of program code granularity. The practicality of the approach is demonstrated through a prototype implementation of a framework for enforcing security policies at various levels of code granularity on Java bytecode applications.

Deep Packet Inspection (DPI) is an essential building block implementing various services on data plane [5]. Usually, DPI engines are centered around efficient implementation of regular expressions both from the required memory and lookup time perspectives. In this paper, we explore and generalize original approaches used for packet classifiers [7] to regular expressions. Our preliminary results establish a promising direction for the efficient implementation of DPI engines.

A popular countermeasure against IP piracy relies on obfuscating the Finite State Machine (FSM), which is assumed to be the heart of a digital system. In this paper, we propose to use a special class of non-group additive cellular automata (CA) called D1 * CA, and it's counterpart D1 * CAdual to obfuscate each state-transition of an FSM. The synthesized FSM exhibits correct state-transitions only for a correct key, which is a designer's secret. The proposed easily testable key-controlled FSM synthesis scheme can thwart reverse engineering attacks, thus offers IP protection.

In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.

Mobile AdHoc Networks (MANET) can be fast implemented, and it is very popular in many specific network requirements, such as UAV (Unmanned Aerial Unit), Disaster Recovery and IoT (Internet of Things) etc. However, MANET is also vulnerable. AODV (Ad hoc On-Demand Distance Vector Routing) protocol is one type of MANET routing protocol and many attacks can be implemented to break the connections on AODV based AdHoc networks. In this article, aim of protecting the MANET security, we modeled the AODV protocol with one type of Automata and analyzed the security vulnerabilities of it; then based on the analyzing results, we proposed an enhancement to AODV protocol to against the Black Hole Attacks. We also implemented the proposed enhancement in NS3 simulator and verified the correctness, usability and efficiency.

Deep packet inspection via regular expression (RE) matching is a crucial task of network intrusion detection systems (IDSes), which secure Internet connection against attacks and suspicious network traffic. Monitoring high-speed computer networks (100 Gbps and faster) in a single-box solution demands that the RE matching, traditionally based on finite automata (FAs), is accelerated in hardware. In this paper, we describe a novel FPGA architecture for RE matching that is able to process network traffic beyond 100 Gbps. The key idea is to reduce the required FPGA resources by leveraging approximate nondeterministic FAs (NFAs). The NFAs are compiled into a multi-stage architecture starting with the least precise stage with a high throughput and ending with the most precise stage with a low throughput. To obtain the reduced NFAs, we propose new approximate reduction techniques that take into account the profile of the network traffic. Our experiments showed that using our approach, we were able to perform matching of large sets of REs from SNORT, a popular IDS, on unprecedented network speeds.

Hardware Trojan Horses and active fault attacks are a threat to the safety and security of electronic systems. By such manipulations, an attacker can extract sensitive information or disturb the functionality of a device. Therefore, several protections against malicious inclusions have been devised in recent years. A prominent technique to detect abnormal behavior in the field is run-time verification. It relies on dedicated monitoring circuits and on verification rules generated from a set of temporal properties. An important question when dealing with such protections is the effectiveness of the protection against unknown attacks. In this paper, we present a methodology based on automatic generation of monitoring and formal verification techniques that can be used to validate and analyze the quality of a set of temporal properties when used as protection against generic attackers of variable strengths.

Cloud Computing is the most suitable environment for the collaboration of multiple organizations via its multi-tenancy architecture. However, due to the distributed management of policies within these collaborations, they may contain several anomalies, such as conflicts and redundancies, which may lead to both safety and availability problems. On the other hand, current cloud computing solutions do not offer verification tools to manage access control policies. In this paper, we propose a cloud policy verification service (CPVS), that facilitates to users the management of there own security policies within Openstack cloud environment. Specifically, the proposed cloud service offers a policy verification approach to dynamically choose the adequate policy using Aspect-Oriented Finite State Machines (AO-FSM), where pointcuts and advices are used to adopt Domain-Specific Language (DSL) state machine artifacts. The pointcuts define states' patterns representing anomalies (e.g., conflicts) that may occur in a security policy, while the advices define the actions applied at the selected pointcuts to remove the anomalies. In order to demonstrate the efficiency of our approach, we provide time and space complexities. The approach was implemented as middleware service within Openstack cloud environment. The implementation results show that the middleware can detect and resolve different policy anomalies in an efficient manner.

A new approach of a formalism of hybrid automatons has been proposed for the analysis of conflict processes between the information system and the information's security malefactor. An example of probability-based assessment on malefactor's victory has been given and the possibility to abstract from a specific type of probability density function for the residence time of parties to the conflict in their possible states. A model of the distribution of destructive informational influences in the information system to connect the process of spread of destructive information processes and the process of changing subjects' states of the information system has been proposed. An example of the destructive information processes spread analysis has been given.

Cryptographic hash functions play a crucial role in information security. Cryptographic hash functions are used in various cryptographic applications to verify the message authenticity and integrity. In this paper we propose a Cellular Automata Based Hashing Algorithm (CABHA) for generating strong cryptographic hash function. The proposed CABHA algorithm uses the cellular automata rules and a custom transformation function to create a strong hash from an input message and a key.

SCADA control systems use programmable logic controller to interface with critical machines. SCADA systems are used in critical infrastructures, for instance, to control smart grid, oil pipelines, water distribution and chemical manufacturing plants: an attacker taking control of a SCADA system could cause various damages, both to the infrastructure but also to people (for instance, adding chemical substances into a water distribution systems). In this paper we propose a method to detect attacks targeting SCADA systems. We exploit model checking, in detail we model logs from SCADA systems into a network of timed automata and, through timed temporal logic, we characterize the behaviour of a SCADA system under attack. Experiments performed on a SCADA water distribution system confirmed the effectiveness of the proposed method.