REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency

TL;DR

This paper introduces REAFFIRM, a model-based Matlab toolkit that automates the repair of hybrid system models to enhance resiliency against security threats, reducing the need for complete redesigns.

Contribution

The paper presents a novel methodology and a new model transformation language, HATL, for repairing hybrid system models to meet safety requirements under attacks.

Findings

Successfully repaired models for ACC, SMIB, and missile guidance systems.

Automated synthesis of resilient models reduces manual redesign effort.

Demonstrated effectiveness against various sensor attack scenarios.

Abstract

Model-based design offers a promising approach for assisting developers to build reliable and secure cyber-physical systems (CPSs) in a systematic manner. In this methodology, a designer first constructs a model, with mathematically precise semantics, of the system under design, and performs extensive analysis with respect to correctness requirements before generating the implementation from the model. However, as new vulnerabilities are discovered, requirements evolve aimed at ensuring resiliency. There is currently a shortage of an inexpensive, automated mechanism that can effectively repair the initial design, and a model-based system developer regularly needs to redesign and reimplement the system from scratch. In this paper, we propose a new methodology along with a Matlab toolkit called REAFFIRM to facilitate the model-based repair for improving the resiliency of CPSs. REAFFIRM takes the inputs including 1) an original hybrid system modeled as a Simulink/Stateflow diagram, 2) a given resiliency pattern specified as a model transformation script, and 3) a safety requirement expressed as a Signal Temporal Logic formula, and then outputs a repaired model which satisfies the requirement. The overall structure of REAFFIRM contains two main modules, a model transformation, and a model synthesizer built on top of the falsification tool Breach. We introduce a new model transformation language for hybrid systems, which we call HATL to allow a designer to specify resiliency patterns. To evaluate the proposed approach, we use REAFFIRM to automatically synthesize repaired models for an adaptive cruise control (ACC) system under a GPS sensor spoofing attack, for a single-machine infinite-bus (SMIB) system under a sliding-mode switching attack, and for a missile guidance system under gyroscopes sensor attack.

Figures

Tables

Table 1. Table 1: REAFFIRM performance results for the ACC, SMIB, and MG case studies. BD is the number of blocks in SLSF models. PR is the parameter range. SV is the synthesized value. TT is the transformation time (s). ST is the synthesis time (s).

Model	BD	Attack	Resiliency Pattern		Unknown Condition	PR	SV	TT	ST
ACC	11	GPS spoofing	Ignore GPS, measurement, use wheel encoders value	Pattern 1	When to switch to a safe copy	$\theta \in [0,50]$	7.08515	2	88
				Pattern 2			7.08515	2	88
				Pattern 3	Ratio of GPS/encoders measurements	$\theta \in [0.1,0.9]$	0.1543	1.75	55.78
SMIB	15	Sliding-mode switching	Add a dwell-time to avoid rapid switching	Pattern dwell-time	Minimal dwell-time	$\theta \in [0,0.3]$	0.12	2	45
MG	310	Gyroscopes spoofing	Ignore untrusted, measurements, use the trusted ones	Pattern 1	When to switch to a safe copy	$\theta \in [0,0.5]$	0.06714	2	78
				Pattern 2			0.06714	2	92
				Pattern 3	Ratio of gyroscopes measurements	$\theta \in [0.01,0.1]$	0.01127	1.75	55

Equations

$${\phi }_{ACC}$$

$${\phi }_{SMIB}$$

$${\phi }_{MG}$$

Full text

In this paper, we propose a new methodology along with a MATLAB toolkit called REAFFIRM to facilitate the model-based repair for improving the resiliency of CPSs. REAFFIRM takes as inputs 1) an original hybrid system modeled as a Simulink/Stateflow diagram, 2) a given resiliency pattern specified as a model transformation script, and 3) a safety requirement expressed as a Signal Temporal Logic formula, and outputs a repaired model which satisfies the requirement. The overall structure of REAFFIRM contains two main modules: a model transformation and a model synthesizer built on top of the falsification tool Breach. We also introduce a new model transformation language for hybrid systems, which we call HATL to allow a designer to specify resiliency patterns. To evaluate the proposed approach, we use REAFFIRM to automatically synthesize repaired models for an adaptive cruise control (ACC) system under a GPS sensor spoofing attack, for a single-machine infinite-bus (SMIB) system under a sliding-mode switching attack, and for a missile guidance system under gyroscopes sensor attack.

1 Introduction

A cyber-physical system (CPS) consists of computing devices communicating with one another and interacting with the physical world via sensors and actuators. Increasingly, such systems are everywhere, from smart buildings to autonomous vehicles to mission-critical military systems. The rapidly expanding field of CPSs precipitated a corresponding growth in security concerns for these systems. The increasing amount of software, communication channels, sensors and actuators embedded in modern CPSs make them likely to be more vulnerable to both cyber-based and physics-based attacks [40, 41, 23, 4, 17]. As an example, sensor spoofing attacks to CPSs become prominent, where a hacker can arbitrarily manipulate the sensor measurements to compromise secure information or to drive the system toward unsafe behaviors. Such attacks have successfully disrupted the braking function of the anti-lock braking systems [37, 4], and compromised the insulin delivery service of a diabetes therapy system [27]. Alternatively, attackers can gain access to communication channels to either manipulate the switching behavior of a smart power grid [30] or disable the brake system of a modern vehicle [25]. Generally, constructing a behavioral model at design time that offers resiliency for all kinds of attacks and failures is notoriously difficult.

Traditionally a model of a CPS consists of block diagrams describing the system architecture and a combination of state machines and differential equations describing the system dynamics [5]. Suppose a designer has initially constructed a model of a CPS that satisfies correctness requirements, but at a later stage, this correctness guarantee is invalidated, possibly due to adversarial attacks on sensors, or violation of environment assumptions. Current techniques for secure-by-design systems engineering do not provide a formal way for a designer to specify a resiliency pattern to automatically repair system models based on evolving resiliency requirements under unanticipated attacks.

In this paper, we propose a new methodology and an associated toolkit, called REAFFIRM, to assist a designer in repairing the original model so that it continues to satisfy the correctness requirements under the modified assumptions. The proposed technique relies on designing a collection of potential edits (or resiliency patterns) to the original model to generate the new model whose parameters values can be determined by solving the parameter synthesis problem. Figure 1 shows an overview of REAFFIRM, which contains two mains modules 1) a model transformation, and 2) a model synthesizer built on top of the falsification tool Breach [12]. REAFFIRM takes the following inputs 1) the original system modeled as a Simulink/Stateflow (SLSF) diagram, 2) the resiliency pattern specified by the designer and 3) the safety requirement expressed as a Signal Temporal Logic (STL) [31] formula, and outputs the repaired SLSF model that satisfies the safety requirement.

To allow a designer to specify resiliency patterns we have developed a new model transformation language for hybrid systems, called HATL (Hybrid Automata Transformation Language). A HATL script is a sequence of statements that describe the modifications over the structure of hybrid systems modeled as hybrid automata [5]. Examples of edits to a model include creating new modes of operations, duplicating modes, adding transitions, modifying switching conditions, and substituting state variables in flow equations. The proposed language allows the designer to write a resiliency pattern in a generic manner, and programmatically modify the initial design without knowing the internal structures of a system. The HATL interpreter is implemented in Python with an extensible backend to allow interoperability with different hybrid systems modeling frameworks. The current implementation of HATL supports MATLAB and performs transformations on SLSF models.

For evaluation, we apply REAFFIRM to automatically synthesize the repaired models for three case studies in the domains of automotive control, smart power systems and aerospace applications. The first case study is a simplified model of an adaptive cruise control (ACC) system under a GPS sensor spoofing attack, and the resiliency pattern to fix the model is to ignore the GPS measurement and only use the wheel encoders, which are additional (redundant) sensors for estimating a vehicle’s velocity. REAFFIRM automatically synthesizes the condition that triggers a switch to a copy of the model that ignores the GPS measurement. The second case study is a single-machine infinite-bus (SMIB) model, which is an approximation of a smart power grid, under a sliding-mode attack. In this case, the mitigation strategy is to increase the minimal dwell-time to avoid rapid changes between different operation modes. Thus, the resiliency pattern adds a dwell-time variable in each mode of the model, and the minimal dwell-time can be synthesized automatically by REAFFIRM. The third case study is the missile guidance system (MG) provided by Mathworks, which is a good representative of a practical MG system as it has more than 300 SLSF blocks. The principle of a spoofing attack on the gyroscopes of the MG system is similar to the GPS spoofing attack of the ACC system, and then we can apply the same resiliency pattern used to fix the ACC model for repairing the MG model.

In summary, the main contributions of the paper are as follows.

The methodology to facilitate the model-based repair for improving the resiliency of CPSs against unanticipated attacks and failures, 2. 2.

the design and implementation of an extensible model transformation language for specifying resiliency patterns used to repair CPS models, 3. 3.

the end-to-end design and implementation of the toolkit, which integrates the model transformation and the model synthesis tools to automatically repair CPS models, 4. 4.

the applicability of our approach on three proof-of-concept case studies where the CPS models can be repaired to mitigate practical attacks.

The remainder of the paper is organized as follows. Section 2 presents an overview of our proposed methodology through a simplified example of the ACC system, and introduces the architecture of REAFFIRM. Section 3 describes our model transformation language used to design a resiliency pattern for hybrid systems. Section 4 presents the model synthesizer of REAFFIRM. Section 5 presents three case studies that illustrate the capability of REAFFIRM in automatically repairing the original models of a) the ACC system under a GPS sensor spoofing attack, b) the SMIB system under a sliding-mode attack, and c) the MG system under a gyroscopes sensor attack. Section 6 reviews the related works to REAFFIRM, and  Section 7 concludes the paper.

2 Overview of the Methodology

In this section, we will explain our methodology through a simplified example of the adaptive cruise control (ACC) system. Assume that a designer has previously modeled the ACC system as a combination of the vehicle dynamics and an ACC module, and GPS measurements were considered trusted in the initial design. In the following, we will describe the ACC system as originally designed, an attack scenario, and an example of resiliency pattern to repair the ACC model111We note that the ACC model presented herein is not a representative of the complexity of a true ACC system, but a simplified example in which the dynamics and control equations are chosen for simplicity of presentation.. Then, we present how REAFFIRM can automatically perform a model transformation and synthesis to construct a new ACC model with resiliency.

2.1 A Simplified Example of ACC System

For simplicity, we assume that the designer initially models the ACC system (including vehicle dynamics) as a hybrid system shown in Figure 2. The original ACC system operates in two modes: speed control and spacing control. In speed control, the host car travels at a driver-set speed. In spacing control, the host car aims to maintain a safe distance from the lead car. The vehicle has two state variables: $d$ is the distance to the lead car, and $v$ is the speed of the host vehicle. The ACC system has two sensors that measure its velocity $v$ via noisy wheel encoders, $v_{enc}=v+n_{enc}$, and a noisy GPS sensor, $v_{gps}=v+n_{gps}$, where $n_{enc}$ and $n_{gps}$ denote the encoder and GPS noises, respectively. Additionally, the ACC system has a radar sensor that measures the distance to the lead vehicle, $d_{rad}=d+n_{rad}$, where $n_{rad}$ captures a corresponding noise. The ACC system decides which mode to use based on the real-time sensor measurements. For example, if the lead car is too close, the controller triggers the transition $g_{sd}$ to switch from speed control to spacing control. Similarly, if the lead car is further away, the ACC system switches from spacing control to speed control by executing the transition $g_{ds}$. The safety specification of the system is that $d$ should always be greater than $d_{safe}$, where $d_{safe}=v+5$. We will describe the ACC model in more details in Section 5.

Safety violation under GPS sensor attack. In this example, we assume that after designing and verifying the initial ACC system, it is determined that the GPS sensor can be spoofed [38, 22]. GPS spoofing occurs when incorrect GPS packets (possibly sent by a malicious attacker) are received by the GPS receiver. In the ACC system, this allows an attacker to arbitrarily change the GPS velocity measurement. Thus, a new scenario occurs when the original assumption of GPS noise, e.g., $|n_{gps}|\leq 0.05$ is omitted, and the new assumption is $|n_{gps}|\leq 50$. As a result, the safety specification could be violated under the GPS sensor attacks, and a designer needs to repair the original model using a known mitigation strategy.

Example of resiliency pattern: ignoring GPS measurement. Since the ACC system has redundancy in the sensory information of its estimated velocity, to provide resilience against the GPS attacks, a mitigation strategy is to ignore the GPS value, and use only the wheel encoders to estimate velocity. Thus, a potential fix is first to create a copy of the original model where the controller simply ignores the GPS reading as it can no longer be trusted. Then, adding new transitions from the modes of the original model to the corresponding instances of the copy that uses only the wheel encoder to measure velocity. We note that this transformation is generic, that is, it can be applied in a uniform manner to any given model simply by creating a duplicate version of each original mode and transition, copying the dynamics in each mode, but without a reference to the variable $v_{gps}$.

Figure 3 illustrates the repaired model in which the transition from the original speeding and spacing control modes to their copies is an expression over $v_{gps}$ and $v_{enc}$. Observe that while it would be possible to use only the wheel encoders all the time, a better velocity estimate can be obtained by using an average velocity measurement (from both the GPS and wheel encoders) when the GPS sensor is performing within nominal specifications. The main analysis question is when should the model switch from the original modes to the copied modes during the spoofing attack. From a practical standpoint, such a transition should occur when the GPS measurement significantly deviates from the wheel encoder measurement, and a transition condition can be specified as $g(v_{gps},v_{enc})=|v_{gps}-v_{enc}|\geq\theta$, where $\theta$ is an unknown parameter. Since $v_{enc}=v+n_{enc}$ and $v_{gps}=v+n_{gps}$, we can rewrite the transition condition as $g(v_{gps},v_{enc})=|n_{gps}-n_{enc}|\geq\theta$. Then, one needs to synthesize the suitable value of the parameter $\theta$ that specifies the threshold for switching from the original copy to the new copy so that the safety requirement is satisfied.

2.2 REAFFIRM Toolkit

Our REAFFIRM prototype for the model-based repair is built in MATLAB and consists of two main modules, corresponding to model transformation and parameter synthesis. To synthesize the model with resiliency to unanticipated attacks, users need to provide the following inputs to REAFFIRM:

• $\bullet$

the initial design of a hybrid system modeled in MathWorks SLSF format,

• $\bullet$

the resiliency pattern specified as a model transformation script that transforms the initial model to the new model with resiliency to unanticipated attacks, and

• $\bullet$

the correctness (safety) requirement of the system specified as an STL formula.

In the case of the ACC example, the inputs of REAFFIRM are the initial SLSF model shown in Figure 2, the resiliency pattern that creates the copied version of the original model without a reference to the variable $v_{gps}$, and the safety requirement encoded as an STL formula,

[TABLE]

The model transformation tool of REAFFIRM takes the initial SLSF model and the resiliency pattern (e.g., the transformation script shown in Figure 4), and then generates the new SLSF model that contains a parameter $\theta$ that appears in the switching condition based on the difference between the GPS measurement and the wheel encoder measurement. Then, the model synthesizer tool of REAFFIRM takes the parametrized ACC model in SLSF and the STL formula $\varphi_{ACC}$ as inputs, and then performs a parameter synthesis to find the desired value of $\theta$ over a certain range, to ensure that $\varphi_{ACC}$ is satisfied. Internally, the model synthesizer of REAFFIRM utilizes an open-source model falsification tool—Breach [12] to synthesize the desired parameters values. If the synthesizer can find the best value of $\theta$ over the given range, then REAFFIRM outputs a competed SLSF model which satisfies $\varphi_{ACC}$ under the GPS attacks. Otherwise, the tool will suggest the designer to either search over different parameter ranges or try different resiliency patterns to repair the ACC model.

3 Model Transformation

3.1 Representation of Hybrid System

Hybrid automata [5] are a modeling formalism popularly used to model hybrid systems which include both continuous dynamics and discrete state transitions. A hybrid automaton is essentially a finite state machine extended with a set of real-valued variables evolving continuously over time [5]. The main structure of a hybrid automaton ${\mathcal{H}}$ includes the following components.

• $\bullet$

${\mathcal{X}}$: the finite set of $n$ continuous, real-valued variables.

• $\bullet$

${\mathcal{P}}$: the finite set of $p$ real-valued parameters.

• $\bullet$

${\mathit{Mode}}$: the finite set of discrete modes. For each mode $m\in{\mathit{Mode}}$, $m.{\mathit{inv}}$ is an expression over ${\mathcal{X}}\cup{\mathcal{P}}$ that denotes the invariant of mode $m$, and $m.{\mathit{flow}}$ describes the continuous dynamics governed by a set of ordinary differential equations.

• $\bullet$

${\mathit{Trans}}$: the finite set of transitions between modes. Each transition is a tuple $\tau\mathrel{\stackrel{{\scriptstyle\scriptscriptstyle\Delta}}{{=}}}\left\langle\mathit{source},\mathit{destination},\mathit{guard},reset\right\rangle$, where $\mathit{source}$ is a source mode and $\mathit{destination}$ is a target mode that may be taken when a guard condition $\mathit{guard}$, which is an expression over ${\mathcal{X}}\cup{\mathcal{P}}$, is satisfied, and $reset$ is an assignment of variables in ${\mathcal{X}}$ after the transition.

We use the dot (.) notation to refer to different components of tuples, e.g., ${\mathcal{H}}.{\mathit{Trans}}$ refers to the transitions of automaton ${\mathcal{H}}$ and $\tau.\mathit{guard}$ refers to the guard of a transition $\tau$. Since our goal is to repair a hybrid automaton syntactically, we will not discuss its semantics in this paper, but refer a reader to [5] for details. We note that the model transformation language proposed in this paper transforms a hybrid automaton based on modifying the syntactic components of the hybrid automaton in a generic manner. The transformation tool of REAFFIRM can take a HATL transformation script and translate it into an equivalent script that performs a model transformation for different modeling framework of hybrid automata including a continuous-time Stateflow chart.

Continuous-time Stateflow chart. In this paper, we represent hybrid automata using continuous-time Stateflow chart, which is a standard commercial modeling language for hybrid systems integrated within Simulink. A continuous-time Stateflow chart supplies methods for engineers to quickly model as well as efficiently refine, test, and generate code for hybrid automata. The syntactic description of a continuous-time Stateflow chart is basically a hybrid automaton, with a small few differences. In particular, a mode is a state associated with different types of actions including a) entry action executed when entering the state, b) exit executed when exiting the state, and c) during (or du) action demonstrates the continuous-time evolution of the variables (i.e., ${\mathit{flow}}$ dynamics) when no transition is enabled. A variable can be specified as parameter, input, output, and local variable. Also, an SLSF model which includes a continuous-time Stateflow chart is deterministic since its transition is urgent and executed with priorities [7].

3.2 Hybrid Automata Transformation Language

In our approach, the partial model of the system, which satisfies functional but not necessarily resiliency requirements is originally modeled in the form of hybrid automata. The model transformation that is at the core of the REAFFIRM tool will then attempt to modify the components of the automata such as modes, flows, or switching logic, by applying user-defined resiliency patterns.

In order to specify resiliency patterns for hybrid automata, we introduce a new language for model transformation called HATL (Hybrid Automata Transformation Language). The goal of HATL is to allow a designer to repair an original model in a programmatic fashion. HATL scripts abstract model implementation details so engineers do not need to learn the intricacies of an individual framework. A key use of HATL is to write generic scripts that are applicable to many models, promoting resiliency scripts which are reusable. A script written in HATL is a sequence of statements that specify the changes over the structure of given hybrid automata. HATL’s syntax and semantics are designed to make it intuitive to anyone who is familiar with imperative languages. HATL includes loop statements that iterate over sets of objects, such as modes or transitions of a model. It uses dot references to index into structures to obtain data fields or to call object-specific methods. Assignments are mutable, and scoped within statement blocks. Functions and methods can have variable numbers of arguments which are eagerly evaluated.

The model transformation tool built in REAFFIRM takes a resiliency pattern in the form of a HATL script, and then translates each of the statements of the script into equivalent transformation operations on continuous-time Stateflow models.  Figure 4 shows an example of a HATL script that specifies a transformation from the original ACC model shown in Figure 2 to the parametrized model shown in Figure 3. In this script, we first create a copy of the original model. Next, we iterate over each mode of the model by calling the formode loop, make a copy with replacing the variable $n_{gps}$ by $n_{enc}$, and then add a new transition from the original mode to the copied mode with a new guard condition. This guard condition is a constraint specified over the difference between $n_{gps}$ by $n_{enc}$ (i.e., the difference between $v_{gps}$ and $v_{enc}$) and a new parameter $\theta$, which is added into the model using a function call addParam. Finally, we need to copy all transitions between original modes (stored in a copied version of the original model) and assign them to the corresponding duplicated modes.

3.3 Implementation

Our current implementation dynamically interprets HATL scripts in Python and translates them into SLSF model transformations via the MATLAB Engine. Our interpreter checks argument values at runtime to ensure only valid transformed models are produced. If a malformed program statement is detected, HATL will throw a verbose error message and roll back any changes it has applied already before exiting. Additionally, these error messages are reported in terms of generic HATL models, so an engineer writing a resiliency pattern does not need to worry about the underlying implementation.

Currently, HATL provides enough programming abstraction to express concise model transformations that function as valid resiliency patterns, and more examples of these scripts will be introduced in Section 5. There is room for future improvement, such as adding language constructs like type checking to verify the type correctness of the model before and after repair.

4 Model Synthesis

In this section, we present the model synthesizer incorporated in REAFFIRM which takes a parameterized model produced by the model transformation, and a correctness requirement as inputs, and then generates a completed model with parameter values instantiated to satisfy the correctness requirements. Since the structure of the completed model is already determined after the model transformation, the model synthesis problem then reduces to the parameter synthesis problem. Let ${\mathcal{P}}_{s}$ be the set of parameters of the transformed model $\tilde{{\mathcal{H}}}$, given a safety specification $\varphi$ and sets of parameter values $\bar{{\mathcal{P}}_{s}}$ , find the best instance values of ${\mathcal{P}}_{s}$ over $\bar{{\mathcal{P}}_{s}}$ so that $\tilde{{\mathcal{H}}}\models\varphi$. For example, the transformation of the ACC model shown in Figure 3 introduces a new parameter $\theta$ whose value needed to be determined so that the completed model will satisfy the safety requirement with respect to the same initial condition of the state variables and parameters domains of the original model.

4.1 Overview of Breach

We incorporated Breach into the model synthesizer of REAFFIRM as an analysis mechanism to perform the falsification and parameter synthesis for hybrid systems. Given a hybrid system modeled as an SLSF diagram, an STL specification described the safety property, and specific parameter domains, Breach [12] can perform an optimized search over the parameter ranges to find parameter values that cause the system violating the given STL specification. The parameter mining procedure is guided by the counterexample obtained from the falsification, and it terminates if there is no counterexample found by the falsifier or the maximum number of iterations specified by a user is reached. On the other hand, Breach can compute the sensitivity of execution traces to the initial conditions, which can be used to obtain completeness results by performing systematic simulations. Moreover, Breach provides an input generator for engineers to specify different testing input patterns such as step, pulse width, sinusoid, and ramp signals. This input generator is designed to be extensible, so users can write a specific input pattern to test their model against particular attack scenarios.

We note that although Breach cannot completely prove the system correctness, it can efficiently find bugs existing in the initial design of CPS that are too complex to be formally verified [21]. These bugs are essential for an engineer to specify resiliency patterns to repair the model. Moreover, the general problem of verifying a CPS modeled as a hybrid system is known to be undecidable [18]. Instead, the falsification algorithms embedded within Breach are scalable and work properly for black-box hybrid systems with different classes of dynamics. Thus, in practice, engineers prefer to use counterexamples obtained by a falsification tool to refine their design. Our prototype REAFFIRM utilizes the advantages of SLSF modeling framework and the falsification tool Breach to design a resiliency pattern and perform the model synthesis for a repaired CPS model with resiliency.

4.2 Model Synthesis using Breach

Next, we describe how REAFFIRM uses Breach to synthesize parameters values for the parametrized model returned from the model transformation tool. The parameter synthesis procedure consists of following steps.

We first specify the initial conditions of state variables and parameters, the set of parameters ${\mathcal{P}}_{s}$ that need to be mined, the sets of parameter values $\bar{{\mathcal{P}}_{s}}$, and the maximum time (or number of iterations) for the optimization solver of Breach. 2. 2.

Next, we call the falsification loop within Breach to search for a counterexample. For each iteration, if the counterexample is exposed, the unsafe values of ${\mathcal{P}}_{s}$ will be returned. Based on these values, the tool will automatically update the sets of parameter values $\bar{{\mathcal{P}}_{s}}$ to the new sets of parameter values $\bar{{\mathcal{P}}^{\prime}_{s}}\subset\bar{{\mathcal{P}}_{s}}$, and then continue the falsification loop. 3. 3.

The process repeats until the property is satisfied that means the falsifier cannot find a counterexample and the user-specified limit on the number of optimized iterations (or time) for the solver expires. 4. 4.

Finally, the tool returns the best (and safe) values of ${\mathcal{P}}_{s}$, updates the parametrized model with these values, and then exports the completed model. If the synthesizer fails to find the values of ${\mathcal{P}}_{s}$ over the given sets of parameter values $\bar{{\mathcal{P}}_{s}}$ so that the safety requirement is satisfied, it will recommend a designer to either search over different parameter ranges or try another resiliency pattern.

Monotonic Parameters. The search over the parameter space of the synthesis procedure can be significantly reduced if the satisfaction value of a given property is monotonic w.r.t to a parameter value. Intuitively, the satisfaction of the formula monotonically increases (respectively decreases) w.r.t to a parameter $p$ that means the system is more likely to satisfy the formula if the value of $p$ is increased (respectively decreased). In the case of monotonicity, the parameter space can be efficiently truncated to find the tightest parameter values such that a given formula is satisfied. In Breach, the check of monotonicity of a given formula w.r.t specific parameter is encoded as an STM query and then is determined using an STM solver. However, the result may be undecidable due to the undecidability of STL [20]. In this paper, the synthesis procedure is based on the assumption of satisfaction monotonicity. If the check of monotonicity is undecidable over a certain parameter range, a user can manually enforce the solver with decided monotonicity (increasing or decreasing) or perform a search over a different parameter range.

5 Model Repair for Resiliency

In this section, we demonstrate the capability of REAFFIRM to repair CPSs models under unanticipated attacks. We first revisit the ACC example and evaluate three resiliency patterns that can be applied to repair the ACC model under the GPS sensor spoofing attack. Second, we investigate a sliding-mode switching attack that causes instability for a smart grid system and how REAFFIRM can use a dwell-time pattern to repair the model under this attack automatically. Finally, we apply the three resiliency patterns used to fix the ACC model to repair the MG system under gyroscopes sensor attacks.

REAFFIRM was tested using MATLAB 2018a and MATLAB 2018b executed on an x86-64 laptop with 2.8 GHz Intel(R) Core(TM) i7-7700HQ processor and 32 GB RAM. All performance metrics reported were recorded on this system using MATLAB 2018a. In Breach, we choose the CMAES solver, and the maximum optimization time is 30 seconds for each iteration of the falsification loop. REAFFIRM and all case studies investigated in this paper are available to download at https://github.com/LuanVietNguyen/reaffirm. The overall performance222The transformation time reported in the table is the actual time required for the model transformation by neglecting the overhead of loading the MATLAB Engine in Python. of REAFFIRM in repairing the initial models of three case studies to mitigate their corresponding attacks is summarized in Table 1. Next, we will describe three case studies in more details.

5.1 Adaptive Cruise Control System

Original SLSF model. We previously introduced the simplified example of the ACC system in Section 2 to illustrate our approach. In this section, we present the ACC system in more details. The ACC system can be modeled as the SLSF model shown in Figure 5. The model has four state variables where $d$ and $e_{d}$ are the actual distance and estimated distance between the host car and the lead vehicle, $v$ and $e_{v}$ represent the actual velocity and estimated velocity of the host car, respectively. In this model, we assume that the lead vehicle travels with a constant speed $v_{l}$. The transition from speed control to spacing control occurs when the estimate of the distance is less than twice the estimated safe distance, i.e., $e_{d}<10+2e_{v}$. A similar condition is provided for switching from spacing control to speed control, i.e., $e_{d}\geq 10+2e_{v}$. In this case study, we assume that the designer has verified the initial SLSF model of the ACC system against the safety requirement $\varphi_{ACC}$ under the scenario when $d(0)\in[90,100]$, $v(0)\in[25,30]$, $|d(0)-e_{d}(0)|\leq 10$, $|v(0)-e_{v}(0)|\leq 5$ , $v_{l}=20$, $|n_{rad}|\leq 0.05$, $|n_{enc}|\leq 0.05$ and $|n_{gps}|\leq 0.05$.

GPS sensor attack. To perform a spoofing attack on the GPS sensor of the ACC model, we continuously inject false data to manipulate its measurement value. In this case, we omit the original assumption $|n_{gps}|\leq 0.05$, and employ the new assumption as $|n_{gps}|\leq 50$. Using the input generator in Breach, we can specify the GPS spoofing attack as a standard input test signal such as a constant, ramp, step, sinusoid or random signal. The following evaluations of three different resiliency patterns used to repair the ACC model are based on the same assumption that the GPS spoofing occurs at every time point, specified as a random constant signal over the range of [-50, 50] during 50 seconds.

Model Repair for the ACC system. Under the GPS sensor spoofing attack, the original SLSF model does not satisfy its safety requirement and a designer needs to apply a certain resiliency pattern to repair the model. The first resiliency pattern for repairing the ACC system has been introduced in Section 2, which makes the copy of the original model where the controller ignores the GPS reading as it can no longer be trusted. However, we need to determine the best switching condition from the original model to the copy. Figure 11 in Appendix 0.A shows the completed model, where the switching condition is determined by synthesizing the value of $\theta$ over the range of [0, 50] using Breach.

The second resiliency pattern for the ACC model is the extended version of the first one where it includes a switching-back condition from the copy to the original model when the GPS sensor attack is detected and mitigated. An example of such a switching-back condition is when the difference between the $n_{enc}$ and $n_{gps}$ are getting smaller, i.e., $|n_{gps}-n_{enc}|<\theta-\epsilon$, where $\epsilon$ is a positive user-defined tolerance. For this pattern, the model transformation script can be written similar to the one shown in Figure 4 with adding the addTransition function from the copy mode to the original mode with the guard condition labeled as $|n_{gps}-n_{enc}|<\theta-\epsilon$ in the formode loop. The performance of REAFFIRM for the second pattern is similar to the first pattern with the same synthesized value of $\theta=7.08515$ and $\epsilon=0$.

Alternatively, the third resiliency pattern, where we do not need to modify the structure of the original model, is to model the redundancy in the sensory information as a linear combination of different sensor measurements. For example, instead of taking the average of $n_{gps}$ and $n_{enc}$, we can model their relationship as $\theta n_{gps}+(1-\theta)n_{enc}$, and then synthesize the value of $\theta$ so that the safety property is satisfied. The transformation script of this resiliency pattern is given in Figure 6. For this pattern, we assume that a designer still wants to use all sensor measurements even some of them are under spoofing attacks and would like to search for the value of $\theta$ over the range of [0.2, 0.8] (instead of [0, 1]). Given the same attack model for the other patterns, the synthesizer in REAFFIRM fails to find the value of $\theta$ within the given range to ensure that the safety property is satisfied. However, if we enlarge the range of $\theta$ to [0.1, 0.9], the synthesizer successfully finds the safe value $\theta=0.1543$.

5.2 Single-Machine Infinite-Bus System

Next, we study a class of cyber-physical switching attacks that can destabilize a smart grid system model, and then apply REAFFIRM to repair the model to provide resilience. A smart power grid system such as the Western Electricity Coordinating Council (WECC) 3-machine, 9-bus system [36], can be represented as a single-machine infinite-bus (SMIB) system described in [14]. The SMIB system is considered as a switched system in which the physical dynamics are changed between two operation modes based on the position of the circuit breaker. The system has two states, $\delta_{1}$ and $\omega_{1}$, which are the deviation of the rotor angle and speed of the local generator $G_{1}$ respectively. The stability (safety) property of the system can be specified as the following STL formula,

[TABLE]

where $T$ is a simulation duration.

Original SLSF Model. In this paper, we model the SMIB system as the SLSF model displayed in Figure 7. The model contains two operation modes whose nonlinear dynamics characterize the transient stability of the local generator $G_{1}$ presented in [14]. The transitions between two operation modes depend on the status of the circuit breaker which is connected or disconnected to the load. In the model, $\delta_{1}$ and $\omega_{1}$ are represented by $delta$ and $omega$, respectively; and the initial conditions are $delta0\in[0,1.1198]$ and $omega0\in[0,1]$. The discrete variable $load$ captures the open and closed status of the circuit breaker.

Sliding-mode attack. The SMIB system has an interesting property known as a sliding mode behavior. This behavior occurs when the state of the system is attracted and subsequently stays within the sliding surface defined by a state-dependent switching signal $s(x)\in\mathbb{R}$ [11, 29]. When the system is confined on a sliding mode surface, its dynamics exhibit high-frequency oscillations behaviors, so-called a chattering phenomenon, which is well-known in the power system design [35]. At this moment, if an attacker forces rapid switching between two operation modes, the system will be steered out of its desirable equilibrium position. As a result, the power system becomes unstable even each individual subsystem is stand-alone stable [29]. The sliding-mode attack model of the SMIB system in SLSF format and the unstable behavior of the system under the attack are described in more details in Appendix 0.A.

Model Repair for the SMIB system. A potential strategy to mitigate a sliding-mode attack is to increase the minimum switching time of the circuit breakers. Indeed, the designer can repair the original model by including a minimum dwell time in each mode of the system to prevent rapid switching. Figure 8 shows a resiliency pattern written as a HATL script that introduces the clock variable as a timer, and the switching time relies on the value of $\theta$.

The model transformation of REAFFIRM takes the dwell-time pattern shown in Figure 8, and then convert the model to a new version that integrates the pattern with the unknown parameter $\theta$. Then, the model synthesis of REAFFIRM calls Breach to search for the best (i.e., minimum) value of $\theta$ over and the range of $[0,0.3]$ that ensures the final model satisfies $\varphi_{SMIB}$ (with $T=10$ seconds) under the sliding-mode attack. The final model, which is stable, is displayed in Figure 9, where the synthesized value of $\theta$ equals to $0.12$.

5.3 Missile Guidance System

Original SLSF Model. We consider the example of the missile guidance system (MG) provided by Mathworks, which is a good representative of a practical MG system. The original SLSF model has more than 300 blocks. The details of the model can be found at https://www.mathworks.com/help/simulink/examples/designing-a-guidance-system-in-MATLAB-and-simulink.html. In our study, we make a slight modification in the Sensors of the Airframe $\&$ Autopilot subcomponent of the original MG model. In the modified version, we model the missile body rate measurements as an array of two different gyroscopes, and the body rate estimation is obtained by using the average of the measurements obtained from the two gyroscopes. Such modification is reasonable as a practical MG system usually uses an array of gyroscopes to estimate the body rate of a missile. The correctness requirement of the model is that the missile will eventually approach the target where their distance is less than 10. This requirement can be formulated as an STL formula

[TABLE]

In the original setting, the MG model satisfies the STL requirement and the noisy levels of two gyroscopes are assumed as $|n_{gyro1}|\leq 0.05$ and $|n_{gyro2}|\leq 0.05$, respectively.

Gyroscopes Sensor Attack. The principle of a spoofing attack on the gyroscopes of the MG system is similar to the GPS spoofing attack of the ACC system. In this case, we omit the original assumption $|n_{gyro2}|\leq 0.05$, and employ the new assumption as $|n_{gyro2}|\leq 1$. As a result, the MG model no longer satisfies the STL requirement under this assumption.

Model Repair for the MG System under Gyroscopes Sensor Attack. To repair the MG model under the gyroscope spoofing attack, we can reuse the three different patterns used to fix the ACC model under GPS spoofing attack. Figure 10 shows the original gyroscope noise estimator which is vulnerable to the spoofing attack and three different repaired versions generated using the three resiliency patterns, respectively. For each resiliency pattern, the synthesized values of $\theta$ and the performance of our Reaffirm toolkit is reported in Table 1.

6 Related Work

Model-based design of resilient CPSs. Examples of model-based approaches to ensure resiliency include the approach proposed in [15] that can be used to design a resilient CPS through co-simulation of discrete-event models, a modeling and simulation integration platform for secure and resilient CPS based on attacker-defender games proposed in [26] with the corresponding testbed introduced in [33], the resilience profiling of CPSs presented in [19], and the recent works of the design, implementation, and monitor of attack-resilient CPSs introduced in [42, 34]. Although these approaches can leverage the modeling and testing for a resilient CPS, they do not offer a model repair mechanism or a generic approach to design a resiliency pattern when vulnerabilities are discovered. Our proposed method is complementary to these efforts as we provide a generic, programmable way for a designer to specify a potential edit that can effectively repair the model for improving resiliency.

Formal analysis of hybrid systems. Our approach utilizes Breach to synthesize an SLSF model due to its advantages in performing falsification, systematic testing and parameter synthesis for hybrid systems. However, Breach cannot give a formal proof of the system correctness. Depending on different types of hybrid systems, other automatic verification tools can be considered to perform a reachability analysis or formally prove whether a system satisfies a given safety property. For examples, d/dt [6] and SpaceEx [16] are well-known verification tool for linear/affine hybrid systems; Flow*[10] and dReach[24] can be used to compute a reachable set of nonlinear hybrid automata; and C2E2 is a verification tool for Stateflow models [13]. We choose Breach as it is more scalable.

Model transformation languages of hybrid systems. In the context of the model transformation, GREAT is a metamodel-based graph transformation language that can be used to perform different transformations on domain-specific models [2, 1]. GREAT has been used to translate SLSF models to Hybrid Systems Interchange Format (HSIF) [3]. Such a translation scheme is accomplished by executing a sequence of translation rules described using UML Class Diagram in a specific order. Other approaches that also perform a translation from Simulink diagrams to hybrid systems formalisms such as Timed Interval Calculus [9], Hybrid Communicating Sequential Processes [28], Lustre [39], and SpaceEx [32]. HYST [8] is a conversion tool for hybrid automata which allows the same model to be analyzed simultaneously in several hybrid systems analysis tools. However, the problem of designing a scripting language to facilitate transforming models of hybrid systems has not been addressed before.

7 Conclusion

In this paper, we have presented a new methodology and the toolkit REAFFIRM that effectively assist a designer to repair CPS models under unanticipated attacks automatically. The model transformation tool takes a resiliency pattern specified in the transformation language HATL and generates a new model including unknown parameters whose values can be determined by the synthesizer tool such that the safety requirement is satisfied. We demonstrated the applicability of REAFFIRM by using the toolkit to efficiently repair CPS models under realistic attacks including the ACC models under the GPS sensor spoofing attack, the SMIB models under the sliding-model attack, and the MG system under gyroscopes spoofing attack.

Appendix 0.A Appendix: Additional Experimental Results

The repaired ACC models. Figure 11, Figure 12, and Figure 13 show the repaired models of the ACC system using the first, second and third resiliency patterns, respectively.

The SMIB system.

Figure 14 represents the general structure of the SMIB system. In this system, $G_{\infty}$ and $G_{1}$ correspondingly represent the SMIB and local generators; $B_{\infty}$ and $B_{1}$ denote the infinite and local bus, respectively; $E_{\infty}$ is the infinite bus voltage; $E_{1}$ is the internal voltage of $G_{1}$; $B_{1\infty}$ is the transfer susceptance of the line between $B_{1}$ and $B_{\infty}$; and $P_{M}$ is the mechanical power of $G_{1}$. The local load $P_{L}$ is connected or disconnected to the grid by changing a circuit breaker status.

Sliding-mode attack model of the SMIB system. To perform the sliding-mode attack on the original SMIB model, we model the attack as the SLSF model shown in Figure 15. In this model, we assume that the attacker selects a sliding surface $s(x)=\delta_{1}+\omega_{1}=0.2$, and the local variable $t$ captures a simulation duration. We note that two transitions from the first mode to the second mode are executed with priorities such that the load is permanently disconnected at some instance where $t\geq 2.5$ seconds. More details of the stages to construct the sliding-mode attack can be found in [14].

Figure 16 illustrates the examples of stable (i.e., without an attack) and unstable (i.e., a counterexample appearing under the sliding-model attack) behaviors of the SMIB system returned by running the falsifier of Breach, respectively. The red box defines the stable (safe) operation region of the SMIB system that can be formalized by the STL formula $\varphi_{SMIB}$.