Antoine Ferlin

Simon Collart-Dutilleul

Philippe Bon

Virginie Wiels

Trace analysis from ERTMS engineering

Keywords: Dynamic Analysis, Runtime Verification, trace, Linear Temporal Logic, statistical information, pattern

Interoperability of railway systems is a major concern in the European Union. Therefore, ERTMS (European Railway Train Management System) has been defined. Nevertheless, ERTMS has to be paired with national track rules. The Perfect project studies the implementation of ERTMS on the French territory. We use an ERTMS 3D Simulator framework which is able to simulate trains, track and communication between the trains and the RBC. The simulator records all events that occur in a sequence of states called trace. Each event is timestamped, so the sequence of events can be temporally analysed. We propose a methodology to analyse the results of a scenario performed on this platform, using temporal properties. One of the strengths of this method is the computation of statistical information on the trace during its analysis, according to a dedicated pattern of property. An automatic analysis of a trace can be used in several domains. In safety, verification of critical temporal property makes sense in ensuring that a program is compliant with its specification. An analysis of an accident or near accident using temporal properties can provide a safety problem detection and a first level diagnosis. It can also be a interesting tool to evaluate the efficiency of an operator according to several criteria such as tiredness, expertise, repetitiveness of an event.

Introduction

When a border is crossed by a train, the modification of the embedded signalling system generates an additional cost which is not desirable. Interoperability is vital for the competitiveness of the European railway field, and aims to provide a safe and coutinious railway system. Any rupture of train charge is allowed to ensure the performence of the railway lines. This ability is based on the fact that the train system is compliant with the essential requirements. This paper provides a feedback about the Perfect1 project. It aims to contribute to the validation and the implementation of the interoperable railway signalling systems, and in particular ERTMS, the European Rail Trafic Management System.

The signalling system is managed according to national rules which are proper to each European country. Therefore, the evaluation of the safety requirements is difficult. In the Perfect project, we provide tools and methodologies based on Runtime Verification2 to evaluate the global consistency of the specification and the operating rules from the safety point of view. Even if this problem is critical for industries, the academic world does not concentrate too much attention on it.

The project is composed of three steps. In the first one, a formal model of a part of the railway rules has been proposed. This model allows the study of the merger of national rules and European specification, in particular in a scenario of a movement authority (MA). The second one provides a methodology using existing formal tools to ensure the complience of the scenario with the specification.

This paper focuses on the last part of the project. It consists in endding the study throughout the use of the ERTMS simulator 3 . After this intruction, some related works are presented in order to position our works according to the specification language and the proposed analysis method. Then, the ERTMS simulator used by the Perfect project is described. The following section focuses on the proposed methodology. Finally, we conclude and propose some future works.

Related works

Runtime Verification works are classifiable in two main categories : On-line and a posteriori methods.

On-line verification consists either in adding assertions to the programme to express the properties to be monitored during the execution, or in executing, in parallel to the programme, an automaton representing the property and taking as inputs data from the programme execution. A lot of work exists for on-line verification, especially for Java programmes and in the aspect-oriented programming community [START_REF] Patricko | An overview of the mop runtime verification framework[END_REF][START_REF] Stolz | Temporal assertions using aspectj[END_REF][START_REF] Havelund | A rewriting-based approach to trace analysis[END_REF][START_REF] Havelund | Monitoring programs using rewriting[END_REF][START_REF] Drusinsky | The temporal rover and the atg rover[END_REF].

We work on a proprietary railway platform which records events on a database. Because it is not possible to interface an on-line monitoring system, we are restricted to the a posteriori verification method. In addition, because the platform can be used in a certification context, it is preferable to use an a posteriori method to replay a verification scenario as a justification. Existing works can be ordered using several criteria.

The first one is the choice of the specification language used to express the properties. It depends on the application domain, on the complexity of the properties and on the user-friendliness of the langage. Even if several porposals already exist, we defined a language tuned to the industrial needs inspired by existing works. Indeed, language such as SALT [START_REF] Bauer | Salt-structured assertion language for temporal logic[END_REF] and PSL [START_REF]The accelera psl language reference manual[END_REF] are complex because they multiply the different temporal operators. Other languages such as LogScope [START_REF] Barringer | Formal analysis of log files[END_REF] are specialised to a specific context and are not compatible with our requirements. Eagle [START_REF] Barringer | Eagle does space efficient ltl monitoring[END_REF] and its HAWK System extension [START_REF] Amorim | Event-based runtime verification of java programs[END_REF] propose a means to handle finite traces but are not sufficient in term of expressiveness.

The second criterion is the nature of the considered execution traces. In several existing works, complete execution traces can be obtained by listening to all the variables of the programme [START_REF] Pnueli | Psl model checking and run-time verification via testers[END_REF][START_REF] Barringer | Eagle does space efficient ltl monitoring[END_REF]. In our case, traces are automatically generated by the simulator without any possible customization. The size of the trace depends on the scenario duration and on the number of events that occur. A way to limit the size of the handled trace is to filter the relevant information. Actually, if the property is about a type of message, the limitation of the trace to all messages with that type is a good slicing method.i

The third issue is the implementation of an efficient verification technique on the traces obtained that can be very large. Existing works are based on rewriting techniques [START_REF] Havelund | Monitoring programs using rewriting[END_REF] or specific techniques, such as translation of LTL formula into state machines [12] [6]. We propose to use an existing tool called Ltl2Ba to transform LTL properties into Büchi automaton and propose specific techniques to handle sequence properties using regular expression. Then the Büchi automaton is executed to perform the analysis.

The ERTMS simulator

The ERTMS simulator allows the replay of a given scenario. A scenario is an illustration of a real situation. The framework is able to reproduce the railway track including the signalling systems, the Radio Block Centres (RBC), the trains and the communications between the RBC and the trains. In addition, it is possible to command one of the simulated trains as a real driver.

Figure 1b is a screen of the simulated DMI. The driver is able to switch on/off the machine, to define the identifier of the train, the phone number of the RBC, to select the ERTMS level, to receive the movement authority . . . as in a real train. The simulator is able to automatically manage up to 10 trains during a simulation. Each automated train is piloted using a specific interface presented in figure 1a. The Route Map Controller simulator is able to open a train section, define a journey on a map which synthetizes the network. This map is displayed on the screen as in figure 2. The strength of this simulator is to provide a real time 3D simulation of what a driver sees in the cabin. This ability of the simulator is useful to consider scenario which may be irreleant or relevant for the human factor point of view. Indeed the different systems (RBC and driver cabin) can be spread over several machines and the dialogues between the driver and the authority can be reproduced as exactly as possible, as shown in figure 3. Finally, one of the needs of this project is to simulate the limit of the authority of two RBCs. The solution consists in pairing two simulators across the Network. This system is still under developpment and should be used to treat scenario on a boarder between two European countries.

When a scenario is played, all events are timestamped and recorded in a database as a sequence of states. The goal is to automatically verify a temporal property on this trace. Therefore, we propose a methodology based on Runtime Verification to achieve this goal.

A methodology to analyse traces

The methodology used, synthesised in figure 4, is composed of three steps detailed in the next sections: definition of properties on a given scenario, generation of trace during the execution of the scenario and the automated trace analysis. The process coloured in grey is not managed by the proposed methodology. Indeed, the proprietary simulator receives as input the scenario defined for the methodology and gives the execution traces to be verified.

Definition of the property to be verified

Propositional logic is well adapted to verify a property at a given state of a program or at a given instant. When a property has to be verified over several instants, then a temporal logic has to be used. Because we handle a sequence of states, the natural logic to use to formalise a temporal specification is a linear logic. An extended version of LTL was chosen for different reasons [START_REF] Ferlin | Vérification de propriétés temporelles sur des logiciels avioniques par analyse dynamique formelle[END_REF]. Indeed, the methodology was initially defined for verifying avionics softwares. A non-publishable analysis of several avionics softwares led to the gathering of temporal properties to be verified. The approach of this analysis consisted of gathering complex properties, classifying them according to the Dwyer [START_REF] Dwyer | Property patterns for finite-state verification[END_REF] classification, and defining the best logic to express them. During our investigation, Dwyer classification was extended to take into account specific temporal properties. Actually, some properties belonged to frequency class, duration class or a merge with Dwyer classes. Because it is possible to handle numeric variable by defining a boolean operator using numeric comparator, LTL was chosen. In addition, because definition of a sequence properties is a complex task, a regular language was aggregated with LTL. Hence, the syntax of our language is:

property ::= φ|reg
The syntax of a LTL property follows:

φ ::=2 φ|φ 1 Uφ 2 |φ 1 ∧ φ 2 | ¬ φ|⊥| |p
where φ, φ i are temporal properties and p is a boolean variable or a comparison of numeric variables, 2 is the global operator and U the until operator. When the property is written in regular expression, the syntax will be:

reg ::=seq|seq * |seq + |seq(b) (1)
seq ::= (p)list|list (2)

list ::= [list of p] (3)
|(list of p)

A regular expression is a sequence of p (1). This sequence can be unique, repeated as much as possible or repeated until a condition is reached. A sequence can begin immediately at the beginning of the trace or after an event [START_REF] Barringer | Formal analysis of log files[END_REF]. A sequence can be stuttered [START_REF] Barringer | Eagle does space efficient ltl monitoring[END_REF] or not (4).

Generation of the trace to be analysed

The next step consists in executing the scenario to be analysed and gathering the information required to verify the temporal properties. The difficulty of this step is to define the data to be collected. Indeed, gathering every state of the execution is not desirable, because it can slow down the simulation and endanger temporal results. The impact of the gathering method has to be limited as much as possible to preserve the realism of the scenario in comparison with reality. In addition, the gathering of every state during the execution of the scenario can overflow the memory capacity of a computer. Actually, there are several variables in a state and the size of the trace depends on the duration of the scenario. An execution trace can go over more than several billion of states. Therefore, a strategy has to be established to be sure that necessary states are collected. A state is necessary when an operand of the property to be verified is modified. The modification of a variable which does not depend on the property has no impact on the property.

In our case, because the ERTMS simulator is proprietary, we can express properties only on variables which are collected. As a hypothesis, the modification of each variable collected by the simulator is recorded. In previous works, the simulator was parametrisable. In other words, it collected only the required variables in defined programme point. In this case, the solution consists in using static analysis to collect all points of the programme where a variable is modified. The interested reader can find more information about this method in [START_REF] Ferlin | Combination of static and dynamic analyses for the certification of avionics software[END_REF] . The impact of the trace recording on the chronology of the events is presumed to be limited for both platforms.

Automated analysis of the trace

The next step consists in verifying the properties on the generated finite execution trace. The approach is implemented in a prototype called AnTarES. In order to verify a temporal property φ on an execution trace σ, we use two main transformations. Firstly, the temporal formula is translated into a Büchi automaton B φ . Secondly, because temporal properties have a semantics on infinite traces, the finite trace σ is transformed into an infinite one σ ∞ by looping over the last element. The transformation of the LTL properties into a Büchi automaton is ensured by [START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF], whereas the transformation of the regular expression is provided in [START_REF] Ferlin | Vérification de propriétés temporelles sur des logiciels avioniques par analyse dynamique formelle[END_REF]. We focus in this section on the way to handle infinite traces. We firstly recall the classic algorithm to analyse the main part of the trace. Then, we provide the end of trace algorithm. Finally, we use a pragmatic approach to handle border effect caused by the transformation of the finite trace.

Büchi automaton execution

Execution of the Büchi automaton is performed in two steps: nominal case and end of trace. The nominal case consists in computing the set of next current states by evaluating the formulas for each possible transition. The nominal case is composed of 6 steps:

1. The next state of the trace is loaded, if there is one. 2. If the next state does not exist, then the nominal case algorithm ends and the end-of-trace algorithm starts. 3. The formula of each transition for all states of the Büchi automaton in the set of current states is evaluated. If the formula is true, then the state following the transition is added to the new set of current states. 4. The new set of current states becomes the set of current states. In this set, each state only occurs once to avoid combinatorial explosion. 5. If the current state is empty, then the property is false. The nominal case algorithm ends. 6. Loop to the first step. σ is an execution trace. E A (i) is the set of current states of the Büchi automaton A at state i of σ. The initial state of A is singleton I A . For a given state , T is the set of transitions with as origin. ν(σ i , T ) returns the set of next states pointed by the transition where the formula is evaluated to true.

The formalized algorithm is, for all n in 0, |σ| -1 :

E A (0) = I A ; E A (n) = ∈E A (n-1) ν(σ i , T )
When there is no next state in the trace, we switch to the end of trace algorithm, defined to handle the execution of the Büchi automaton at the end of the trace. This algorithm answers the following question: is there an infinitely often accessible final state? This algorithm performs:

1. Computing the strongly connected components of the Büchi automaton, by only taking into account transitions where the formula is true. 2. Defining a direct acyclic graph (dag), equivalent to the Büchi automaton, from the strongly connected components computation. 3. Browsing the direct acyclic graph for each element of the current state. 4. Determining for each state of the dag accessed from an element of the current state if it is a final state of the Büchi automaton. Because of the looping over the last state of the trace, the Büchi automaton is equivalent to a graph. Then verifying a property on this end of trace is equivalent to looking for a cycle in the graph with acceptant states. And finally, looking for a cycle with accepting states is equivalent to browsing the associated direct acyclic graph and to finding an equivalent accepting state during this process. Consequently, the algorithm is validated.

Pattern 23 (P )

2 (P ⇒ Q) 2 (P ⇒3 Q) Metric

Computation of additional statistical information

This method allows the treatment of big traces and gives a result of an analysis depending on a temporal property. However, the expected result is only true or f alse. When the property is f alse, this result is not enough, because the origin of the problem is not always obvious. Therefore, we propose to compute additional statistical information to target the origin of the property invalidation. These metrics can be used to detect if the property is f alse because of a border effect. We propose two kins of statistical information:

• for each kind of properties, providing the number of the state and the timestamps where the error occurs, • for some pattern of properties, providing specific metrics In the previous non-publishable analysis, three kinds of pattern of properties were often used :

• 23 (P ) which means that propositional property P often occurs on a trace ; • 2 (P ⇒ Q) which means that when propositional property P occurs then propositional property Q occurs at the same time ; • 2 (P ⇒3 Q) which means that when propositional property P occurs, propositional property Q will occur. The interest of this approach is to provide to the verifier a quantitative aspect related to the trace and the property. Indeed, this kind of information is helpful to detect an anomaly even if the property is true. For instance, the fact that 2 (P ⇒ Q) is true does not mean that P occurs several times. Perhaps P never occurs. The statistical information ensures that P will occur a reasonable number of times. Table 1 defines the different statistical information computed, when a pattern is recognized. This position paper is focused on the last part of the Perfect project which aims to study the ERTMS implementation on the French territory troughouth the LGV-Est line. In this last part is studied the collaboration between the formal validation and tests in an integrated approach. Tests are performed on an ERTMS railway 3D simulator which records all events of the scenario played into a trace. In this paper, we define a method to automatically analyse the execution traces. The method consists in verifying temporal properties throughout the formalism of Büchi automata. Temporal properties are expressed using LTL or regular expression for sequence properties. In addition, this approach provides a method to compute metrics about the verified trace according to a specific pattern of properties.

Experiments have to be performed on the platform to provide trace to be analysed. Firstly, we hope to analyse trace coming from a scenario that simulates a normal journey. Secondly we will focus on an accident scenario. As a future work, we propose to couple the system of metric computation to a study related to the human factors. Indeed, it is possible to study the behaviours of a driver using the 3D simulator. In addition, computation of statistical information could be performed using a specific automaton instead of a "hard encoding solution".

  (a) for automated trains (b) for the driver

Figure 1 :

 1 Figure 1: The DMI

Figure 2 :

 2 Figure 2: The Route Map Controller

Figure 3 Figure 4 :

 34 Figure 3: The 3D rendering

Table 1 :

 1 Statistical information computed with the three patterns.

	Number of P Number of P Number of P, Number of Q,
	min/max Number of P before an
	occurrence of Q

http://perfect.ifsttar.fr/Site

http://www.runtime-verification.org/

http://www.ersa-france.com

Acknowledgement

The work is funded by the French national research agency (ANR) in the context of the Perfect project and Re(H)STRAIN project. Perfect is also supported by the French I-TRANS competitive pole.


M Sghiar
email: msghiar21@gmail.com

TURBULENT FUNCTIONS AND SOLVING THE NAVIER-STOKES EQUATION BY FOURIER SERIES

Keywords: Navier-Stokes, Fourier, Séries de Fourier. I . Introduction

The Navier-Stokes equations is considered to be the first step to understanding the elusive phenomenon of turbulence, the Clay Mathematics Institute in May 2000 made this problem [2] one of its seven Millennium Prize problems in mathematics.

In this article I will prove that the Navier-Stokes equation have a solutions and I will give techniques to resolve this beautiful equation.

The Navier-Stokes equation, established in the nineteenth century by the French Navier and the British Stokes. It is an equation that describes the velocity field of a fluid. More specifically, it is a differential equation whose velocity field is unknown.

The Navier-Stokes equation is also used to predict the weather, the oceans simulate, optimize aircraft wings ... Knowing that a link between the Boltzmann equation and the Navier-Stokes equation was established, by studying the latter problem, I found that for to solve it we can reduce the problem of the heat-equation which is known can be solved by several methods : one of the first methods of solving the heat-equation was proposed by Joseph Fourier in his treatise analytical Theory of heat [START_REF] Fourier | Théorie analytique de la chaleur[END_REF] in 1822 .

After giving a specific solutions to the Navier-Stokes equation, I will demonstrate how to find all solutions of this equation if they exist, and I give the necessary and sufficient conditions for their existence. M. SGHIAR

It will be seen in a remark that if the turbulence function is negligible, then the fluid will tend to behave like an ideal gas.

II. Recall, notations and definitions

Here are the Navier-Stokes equation:

ρ ( ∂u ∂ t +(u . ∇ u ) ) =-∇ p+μ ∇ 2 u div u=0
Where u is the velocity field, p is the pressure ,the density of the fluid , and μ its viscosity.

And :

∇= ( ∂ ∂ x 1 , … , ∂ ∂ x n ) (u . ∇ u)= ∑ 1 n u i ∂u ∂ x i ∇ 2 u= ∑ 1 n ∂ 2 u ∂ x i 2 div u= ∑ 1 n ∂ u ∂ x i
In the following, by dividing by ρ , the Navier-Stokes equations is of the form :

∂u ∂ t +(u . ∇ u )=α ∇ p + β ∇ 2 u div u=0

III-Existence of the solutions for the Navier-Stokes equation :

On each axis i, try to find the solutions of the form :

(IJEAT)', ISSN: 2249-8958 (Online), Volume-6 Issue-1, Page No.: 79-80, October 2016. M. SGHIAR

∂u i ∂ t + ( u i ∂ u i ∂ x i ) =α ∂ p i ∂ x i + β ∂ 2 u i ∂ x i 2
This is equivalent to:

∂u i ∂ t + ∂ ( 1 2 u i 2 -α p i ) ∂ x i =β ∂ 2 u i ∂ x i 2
If u i is a solution of the equation :

∂u i ∂ t =β ∂ 2 u i ∂ x i 2
Such solutions u i exist because the equation is analogous to the heat-equation which is resolvable by the Fourier series [START_REF] Fourier | Théorie analytique de la chaleur[END_REF].

If p i is such 1 2 u i 2 -α p i =f i (t) , then ∂ ( 1 2 u i 2 -α p i ) ∂ x i =0
, and the equation is solved.

We do the same for all axes i until i=n -1 .

For the axe i=n :

Let be u n =-∑ 1 n -1 u i .
We have :

∂u n ∂ t = β ∂ 2 u n ∂ x i 2 ,
( 1 2 u n 2 -α p n ) ∂ x n =0
, and the equation is solved for the axe n.

It is clear that if e i is the vector for the axes i, then u= ∑ 1 n u i e i is one solution of the Naviers-Stokes equation if div u=0 .

Else, to have div u=0 , we take u i of the form :

u i =e β t + ( ∑ 1 n x i ) , ∀ i∈ {1, … , n-1}
So we have solutions of the Navier-Stokes equation.

IV-Necessary conditions :

Any solution (u , p ) of the Navier-Stokes equation verifies that :

u i 2 -α p i =f i (t ), ∀ i∈ {1, … , n } Indeed : If (u , p
) is a solution of the Navier-Stokes equation , we must have :

∂u i ∂ t + ∂ ( 1 2 u i 2 -α p i ) ∂ x i =β ∂ 2 u i ∂ x i 2
Therefore :

(IJEAT)', ISSN: 2249-8958 (Online), Volume-6 Issue-1, Page No.: 79-80, October 2016. M. SGHIAR

- ∂ u i ∂ t = ∂ ( 1 2 u i 2 -α p i -β ∂u i ∂ x i ) ∂ x i
And :

-

∂ x i ∂ u i ∂ t =∂ ( 1 2 u i 2 -α p i -β ∂ u i ∂ x i )
When the fluid flows in one direction, then the space-time flows in the opposite direction with the same speed value:

We deduce that :

-u i ∂ u i =∂ ( 1 2 u i 2 -α p i -β ∂ u i ∂ x i ) Therefore : 0=∂ ( u i 2 -α p i -β ∂ u i ∂ x i )
And : We deduce therefore that :

u i 2 -α p i -β ∂u i ∂ x i =f i (t ) So : ∑ 1 n u i 2 -α p i -β ∂ u i ∂ x i =f (t ) (
u i 2 -α p i =h i (t ) , ∀ i ∈{1, … , n} because : ∀ i ∈ {1, … , n} , u i 2 -α p i =l i (x i , t
) , and we must have

∂(u i 2 -α p i ) ∂ x j =0 ∀ j∈ {1, … , n} .

V-Conclusion :

Theorem:

The Navier-stokes equation have a solution, Moreover, any solution (u, p) must check:

u i 2 -α p i =f i (t ) and ∂u i ∂ t =β ∂ 2 u i ∂ x i 2 , ∀ i ∈ {1, … , n} . where u= ∑ 1 n u i e i and p= ∑ 1 n p i e i .
Conversely any pair (n, p) satisfying these conditions with div u=0 is solution of the Navier-Stokes equation.

Remarks :

1-We note in the above equations the dependence between pressure, density, speed vector fields and viscosity 2-By dividing by α in the equation u i 2 -α p i =f i (t ) we deduce that :

ρ u i 2 -p i =ρ f i (t )
where 1 α =ρ is the density of the fluid.

Let's ρ= m V , we will have :

mu i ² -Vp i =mf i (t) .
And the equation mu i ² -Vp i =mf i (t) is linking energy, mass, pressure, temperature, volume and time ... This may not be surprising since a link between the Boltzmann equation and the When f i (t ) tends to 0, we will have mu i ² ≃ Vp i , there is therefore a tendency towards the law of an ideal gas, and the function f i (t ) can be regarded as a turbulent function.

(

  IJEAT)', ISSN: 2249-8958 (Online), Volume-6 Issue-1, Page No.: 79-80, October 2016.

  IJEAT)', ISSN: 2249-8958 (Online), Volume-6 Issue-1, Page No.: 79-80, October 2016. p i =g (t ) because div u=0 .

(

  IJEAT)', ISSN: 2249-8958 (Online), Volume-6 Issue-1, Page No.: 79-80, October 2016. M. SGHIAR Navier-Stokes has been established.


Chad Arnold

Jonathan Butts

Krishnaprasad Thirunarayan

Detecting Integrity Attacks on Industrial Control Systems

Keywords: Control systems, integrity attacks, Byzantine Generals Problem Low Open

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

On June 26, 1996, an oil pipeline operator in Fork Shoals, South Carolina acted on erroneous data that conflicted with the true state of the pipeline system [START_REF]Pipeline Accident Report, Pipeline Rupture and Release of Fuel Oil into the Reedy River at Fork Shoals, South Carolina, Report[END_REF]. To relieve pressure in the pipeline, the operator sent a remote signal to start a pump. Although the operator's console revealed that the pump had started, it was a faulty indication and the pump had not been activated. As the pressure readings continued to increase, the operator was confused by the anomaly and took actions that exacerbated the problem. The pipeline ultimately ruptured, spilling 957,600 gallons of oil into a nearby river and surrounding areas, and causing more than 20 million dollars in damage.

Industrial control systems monitor and control infrastructure assets that are vital to society -the electric power grid, oil and gas pipelines, transportation systems and water treatment and supply facilities. Attacks that impact the operations of these critical assets can have devastating consequences. The complexity and interconnectivity of control systems have introduced vulnerabilities and attack surfaces that previously did not exist, resulting in a significant increase in security incidents during the past few years [START_REF] Rashid | ICS-CERT: Response to cyber "incidents" against critical infrastructure jumped 52 percent in 2012[END_REF]7]. Indeed, researchers have demonstrated that a number of critical infrastructure systems have been exposed to malicious process manipulation [START_REF] Finkle | Irrational" hackers are growing U.S. security fear[END_REF][START_REF] Zorz | Company's industrial heating system hacked via backdoor, Help Net Security[END_REF].

Industrial control devices inherently trust system inputs for proper operation [START_REF] Macaulay | Cyber Security for Industrial Control Systems[END_REF]. Few, if any, advanced decision support systems are available to assist operators in identifying anomalous data and determining the best course of action in the presence of conflicting information about process systems. As a result, accidental or malicious manipulations of system parameters can cascade to produce incorrect functionality and possibly induce system failures.

The Byzantine Generals Problem (BGP) [START_REF] Lamport | The Byzantine Generals Problem[END_REF] is a classic problem in distributed computing that seeks to determine the appropriate course of action when there is no consensus among the actors. Indeed, this problem is relevant to industrial control systems where operators often have to make important process control and management decisions in the presence of bad data. This paper considers a formulation of the Byzantine Generals Problem in the context of industrial control systems. The goal is to draw inferences from the physical state of a system to help determine integrity compromises.

Byzantine Generals Problem

The Byzantine Generals Problem was originally introduced as an abstract problem for understanding the reliability of computer systems and failures stemming from conflicting information [START_REF] Lamport | The Byzantine Generals Problem[END_REF]. The problem is described in the context of malicious actors who can modify messages to create discontinuity and conflict. In the classical formulation of the problem, Byzantine generals communicate with each another by messenger and must decide on a common course of action: attack or retreat. Messages can be manipulated by senders or while they are in transit from senders to receivers. Each receiver must gather and compare messages from all the neighboring generals before making a final decision to attack or retreat.

The original work by Lamport, et al. [START_REF] Lamport | The Byzantine Generals Problem[END_REF] evaluated solutions for resolving conflicting data. Each solution assumes different requirements, features and constraints when evaluating the overall reliability of a system. In the Byzantine Generals Problem, traditional oral messages sent between the generals correspond to the messages sent between computer systems. A common plan of action guarantees that a small number of "traitors" cannot negatively impact the system by enforcing a bad plan.

Valid solutions require more than two-thirds of the generals to be loyal. A valid solution enables generals to reach consensus or an agreed upon decision that cannot be negatively influenced by a limited number of traitors. Thus, when there are only three generals, no solution exists in the presence of even a single traitor. Lamport, et al. [START_REF] Lamport | The Byzantine Generals Problem[END_REF] proved that consensus can be reached when there are at least 3m + 1 generals in the presence of at most m traitors. More generally, with 3m + 1 total nodes, at most m nodes can suffer from Byzantine faults. That is, for m = 1, only one of the four nodes can be malicious for the solution to be valid.

Figure 1 shows a traditional Byzantine Generals Problem scenario where the commander C1 sends a consistent value (message v) to three lieutenants, L1, L2 and L3, where L3 is a traitor. L2 receives conflicting data from the commander and the other two lieutenants, C1, L1 and L3, and evaluates the values provided by C1, L1 and L3. Specifically, L2 identifies the inconsistency using a majority function that considers the three inputs (v, v, x). The inconsistent data source is identified and, in this case, L3 is identified as the traitor based on the set of three messages. Note that the majority function is the basis for conflict resolution in the Byzantine Generals Problem [START_REF] Lamport | The Byzantine Generals Problem[END_REF].

Control Systems and Byzantine Failures

An industrial control system is a hierarchical, distributed system with operators, controllers and sensors, often many miles apart. The control system enables an operator at a distant location to assess the current status of a process and to perform the appropriate control actions to manage the process. This activity can be automated or semi-automated and, depending on the situation, can require frequent, regular or immediate intervention. Effective communications with field devices are critical for the proper operation of an industrial control system. This section demonstrates how the Byzantine Generals Problem applies to an industrial control environment. Instead of the generals passing messages, field devices in an industrial control system pass messages to a control layer. Each field device collects state values from sensors and transmits the values to the control layer. The decision authority in the control layer executes an algorithm that compares the inputs received from the field (device) layer. The algorithm identifies malicious nodes and presents the current state of the system to enable an operator to make an informed decision when conflicting data is received. This may require the operator to modify system parameters for better performance or to restore the system to a stable state if it has become unstable as a result of a data integrity compromise.

Basic Notions

In the Byzantine Generals Problem, a contributing node is defined as a node that produces a state value to pass directly to other available nodes. In the original formulation of the problem, all the nodes are contributing nodes, including the lead commander and the lieutenants. However, in an industrial control system, only field layer devices are contributing nodes.

A decision authority is defined as a node that evaluates inputs and decides on the state of the system. In the original Byzantine Generals Problem, all the nodes with the exception of the lead commander are decision authorities. However, an industrial control system has a single decision authority that resides in the control layer.

In an industrial control system, all the nodes are generally known and trusted. However, a node can be compromised and its data may be manipulated in an integrity attack.

Figure 2 shows the major components of an industrial control system corresponding to the Byzantine Generals Problem framework. The framework has the following types of nodes: Decision Component Node: This corresponds to a control layer node. A single decision component node, also known as a decision authority, is present. The decision component node receives state values from field device nodes and executes an algorithm to identify inconsistencies.

PLC Node: This corresponds to a field layer node. Multiple PLC (programmable logic controller) nodes, also known as contributing nodes, are present. The PLC nodes send state values to the single decision component node. Note that only PLC devices are considered in this paper. However, the approach is applicable to any type of industrial control device that reports status information to a central authority.

Sensor/Actuator Node: This corresponds to a physical layer node. Multiple sensor (S i ) and actuator (A i ) nodes are present to monitor the process system and perform control actions on the process system, respectively. In an industrial control environment, the physical layer provides ground truth of the system state.

Industrial Control System Attributes

A Byzantine algorithm designed for an industrial control system must incorporate ground truth in order to correlate interdependencies between nodes. The ground truth is the actual state of a physical system. Given the state of one PLC, the decision component must infer the state of neighboring components. Inference is enabled by interdependent relationships between nodes. When neighboring components report state values, the decision component compares the reported state values with the anticipated state values.

Figure 3 shows a system with three nodes. Direct links exist from PLC nodes P 1 and P 2 to decision component node D1. Nodes P 1 and P 2 are contributing nodes.

To clarify the concepts, a simplified diagram of the original Byzantine Generals Problem is presented in Figure 4. The figure has three contributing nodes, C1, L1 and L2. The directional arrows in Figures 3 and4 show the information flow between nodes. The solid lines in the two figures correspond to direct links along which messages are passed directly from one node to another; the messages may be manipulated by integrity attacks. The simplified industrial control system in Figure 3 uses a dotted line to represent an indirect link. The indirect link is not a physical link -it indirectly ties the two nodes together, enabling inferences to be made about the device state. Note that an indirect link cannot be compromised because it not a physical (actual) link.

To elaborate, the Byzantine Generals Problem in Figure 4 has direct links C1 → L1, C1 → L2, L1 → L2 and L2 → L1. The contributing nodes (bold circles) are C1, L1 and L2; the decision authorities are L1 and L2. The simplified industrial control system in Figure 3 has links P 1 → D1 and P 2 → D1. It has two contributing nodes, P 1 and P 2, which pass data to decision authority D1. Note that D1 is not a contributing node because it does not produce a state value that is sent to the other nodes.

The indirect link in Figure 3 is formed as a consequence of a direct physical relationship between the field devices. While direct links from contributing nodes can be compromised, an inferred link cannot be compromised; this reduces the attack surface. However, the interdependency captured by the inferred link enables the control layer to infer a change in state of a neighboring device. The interdependency arises from the ground truth of the system and the properties of dependent control system components.

As a practical example, consider a scenario where two sensors are attached to a bucket. One sensor detects the flow of water into the bucket while the other measures the weight of the bucket. If water does not leave the bucket as new water enters, the weight sensor should continually report an increase. The two sensors are, in fact, indirectly linked and their readings will always correlate if the system operates normally. However, if the system has an integrity error, the two sensors would not correlate; this inconsistency can lead to an unstable or undesired state. In the case of the bucket, the water will eventually overflow; in the Fork Shoals incident described above, the oil pipeline ruptured.

Algorithm

In order to detect integrity errors, the decision authority in an industrial control system executes an algorithm after it receives local state values from the contributing nodes. A total of (l + m) state values exist, one from each of the l loyal contributing nodes and the m malicious contributing nodes. By using inferred data, the algorithm identifies the m malicious nodes, where m ≥ 1 and the total number of nodes n ≥ 4, as long as there are a majority of l > m loyal nodes. To assist in identifying loyal and malicious nodes, the function CONSISTENT is invoked. This function evaluates the state values to identify the inconsistent nodes. After the inconsistent nodes are identified, the integrity of the entire system is evaluated by comparing the number of malicious nodes with the number of loyal nodes.

Each contributing node receives an input from a physical device that represents ground truth; however, the contributing nodes can be loyal or malicious. It is assumed that physical devices work properly and have no faults, and all the inconsistencies are due to the malicious nodes. It is also assumed that the decision node has complete information about the design of the physical system. Specifically, it can determine if the contributing nodes are reporting consistent values or inconsistent values.

The algorithm uses two primary functions. After all the state values are collected, the function CONSISTENT is executed for each pair of contributing nodes to determine consistency. After all the nodes are analyzed for consistency, the function MAJORITY is executed to determine if the majority of nodes are consistent or inconsistent.

The input to the CONSISTENT function is (s i , s i+1 ) where s i and s i+1 are state values for PLCs P i and P i+1 , respectively. There are two possible return values for the CONSISTENT function, True or False, which reflect whether the state values are consistent or inconsistent, respectively. If both the state values are consistent, then the state determination t i is assigned the consistent value C; if the values are inconsistent, the inconsistent value I is assigned. Note that, if the values are consistent, then the nodes are either both loyal or both malicious. If the values are inconsistent, then one of the nodes is malicious.

The MAJORITY function evaluates the results generated by the CONSIS-TENT function. The function returns an overall state for the system. The system is consistent if, over all the t i , the number of C values is greater that the number of I values; otherwise, the system is inconsistent.

Evaluation

The algorithm, shown in Figure 5, begins by acquiring local state values from all the l + m contributing nodes. If there are at least three contributing nodes, the first value is labeled as consistent; otherwise, the algorithm terminates because of the lack of a sufficient number of loyal nodes required to evaluate system state. Next, pairs of state values are evaluated for consistency in sequential order. Nodes are labeled for consistency based on their relationship to previous evaluations. After all the nodes are evaluated for consistency, the majority operation is performed. If the majority of the nodes are consistent, then the first node is loyal. As a result, all the consistent nodes are labeled as loyal and all the inconsistent nodes are labeled as malicious. Alternatively, if the majority of the nodes are inconsistent, the first node is malicious. These results hold as long as there are more loyal nodes than malicious nodes (i.e., l > m).

Figure 6 shows a three-node system with P 1 as a malicious node and flagged with an integrity error t 1 = I. In the example, decision authority D1 receives inputs from PLC field devices P 1 and P 2. P 1 reports a local state value s 1 = b, where b is the value of a system parameter. Meanwhile, P 2 reports a local state value s 2 = d. D1 can infer, based on the state value reported by P 1, that the state value reported by P 2 should correlate with the state c. Likewise, D1 can infer, based on the state value reported by P 2, that the state value reported by P 1 should be e. This discrepancy is caused by conflicting values from the two reporting field devices. An inconsistency is identified because CONSISTENT(s 1 , s 2 ) = False. However, because of the small number of contributing nodes, D1 cannot determine the node that caused the integrity error.

The algorithm can accurately identify malicious nodes when there are a majority of loyal nodes (l > m). To demonstrate how the algorithm works, consider the basic case with n = 4. In this scenario, there are three contributing nodes and, as a result, l > 1 and m < 2 must be true for the algorithm to be successful. Consider the case where P 3 is flagged for an integrity problem. In the first step, D1 receives the state values: s 1 = b from P 1, s 2 = c from P 2 and s 3 = f from P 3. In the second step, since there are least three contributing nodes (P 1, P 2 and P 3), the first node is labeled consistent (t 1 = C).

Next, the state values from P 1 and P 2 are compared for consistency. Specifically, CONSISTENT(s 1 , s 2 ) = True. As a result, the integrity flag of P 2 is set to the same value as P 1 (t 2 = C). Next, CONSISTENT(s 2 , s 3 ) = False. As a result, the integrity flag of P 3 is set appropriately (t 3 = I).

Finally, the MAJORITY function is executed. Since MAJORITY(C, C, I) = C, the first node is loyal. As a result, all the nodes with t i = C are identified as loyal and all the nodes with t i = I are identified as malicious.

At this stage, using visual observations only, a control system operator may fail to identify the node with the integrity problem and could act on the invalid data, as in the case of the Fork Shoals pipeline rupture. Implementing this algorithm would have identified the faulty alert that led the pipeline operator to believe that the pump had started, when, in fact, it had not.

Application

The algorithm identifies integrity problems and a means for evaluating conflicting data. From a cyber security perspective, the integrity of field devices can be manipulated when components are networked to the Internet and targeted compromises or accidental manipulations occur. A field device can, thus, become compromised and report false data. If this occurs, the integrity of the data can be compromised. The following example highlights a scenario where devices provide inconsistent data, but the malicious device can be identified.

Figure 7 represents a notional oil pipeline with its associated connectivity and interdependencies. The physical layer components are several miles apart In the example, a field device P 1 monitors pressure, a field device P 2 monitors a control valve and a field device P 3 monitors flow. A change in state at P 1 changes the physical layer and the corresponding states of the subsequent field devices P 2 and P 3. This is an important property, which enables the decision authority to infer the state of the subsequent field devices. For simplicity, pressure can be High or Low, the valve position can be Open or Closed, and the flow sensor shows a flow state of Yes or No. Each field device reports either the accurate local state or the false local state.

Data reported by each field device is evaluated for consistency to allow the decision component D1 to make decisions. Integrity problems are present if the field devices P 1, P 2 and P 3 report conflicting state values. Table 1 lists various combinations of sensor readings that represent consistent and inconsistent states in the notional example. The table values are used for evaluating the CONSISTENT function and enabling inference.

When the pressure at P 1 is Low, the valve position at P 2 should be Open and the flow rate at P 3 should be Yes. When the valve position at P 2 is Closed, the pressure at P 1 is High and the flow rate at P 3 is No. Inconsistent sequences of the reported state values are detected by the algorithm.

For example, consider the second row in Table 1. In the first step, the decision component receives state values from field devices P 1, P 2 and P 3. P 1 reports the pressure as High, P 2 reports the valve as Open and P 3 reports the flow rate as Yes. In the second step, P 1 is labeled as consistent (t 1 = C). In the third step, values from P 1 and P 2 are compared for consistency. CONSISTENT(s 1 , s 2 ) = False, meaning that High pressure at P 1 does not infer an Open valve position at P 2. Since P 1 and P 2 are inconsistent, P 2 is labeled as inconsistent (t 2 = I). Next, values from P 1 and P 3 are compared for consistency. CONSISTENT(s 1 , s 3 ) = False, meaning a High pressure at P 1 does not imply a flow rate of Yes at P 3 and, therefore, t 3 = I. The comparison of state values from P 2 and P 3 reveals consistency. Since MAJORITY(C, I, I) = I, P 1 is identified as malicious.

Conclusions

Human operators and automated decision components in industrial control environments often must make rapid decisions to react to system integrity errors. The application of the Byzantine Generals Problem to industrial control systems provides a formal mechanism for recognizing the presence of anomalous data and potentially identifying its sources. Using physical system properties, the resulting algorithm enables a decision authority to infer the system state and identify integrity compromises. A key constraint is that, when more than three field devices report the physical state of a system and when there are more trusted devices than compromised devices, it is possible to identify the specific devices that are compromised. The gas pipeline example demonstrates how the algorithm can identify and resolve conflicting data. As demonstrated, solutions to the Byzantine Generals Problem in the context of industrial control environments facilitate the resolution of inconsistent data that can result from cyber attacks against field devices and communications links.

Figure 1 .

 1 Figure 1. Byzantine Generals Problem.

Figure 2 .

 2 Figure 2. Industrial control system components.

Figure 3 .

 3 Figure 3. Industrial control system.

Figure 4 .

 4 Figure 4. Byzantine Generals Problem.

Figure 5 .

 5 Figure 5. Algorithm for detecting integrity errors.

Figure 6 .

 6 Figure 6. Impossibility of a solution for a system with less than four nodes.

Figure 7 .

 7 Figure 7. Oil pipeline representation.

Table 1 .

 1 Sample oil pipeline data.and the components are managed by multiple PLCs that report to a single decision component. The distribution of PLCs makes it difficult for an operator to manually or visually verify the current state of every device. Nonetheless, the operator must rely on the system for situational awareness prior to making decisions or taking actions. Previous examples have demonstrated the negative effects of conflicting data.

	Pressure Valve Flow Consistent Malicious
	P1	P2	P3	Yes/No	Node