{'fraction_non_alphanumeric': 0.03896574092232497, 'fraction_numerical': 0.006441491046780008, 'mean_word_length': 4.493494654843789, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Relational Analysis of Sensor Attacks on Cyber-Physical Systems

Cyber-physical systems, such as self-driving cars or autonomous aircraft, must defend against attacks that target sensor hardware. Analyzing system design can help engineers understand how a compromised sensor could impact the system's behavior; however, designing security analyses for cyber-physical systems is difficult due to their combination of discrete dynamics, continuous dynamics, and nondeterminism. This paper contributes a framework for modeling and analyzing sensor attacks on cyber-physical systems, using the formalism of hybrid programs. We formalize and analyze two relational properties of a system's robustness. These relational properties respectively express (1) whether a system's safety property can be influenced by sensor attacks, and (2) whether a system's high-integrity state can be affected by sensor attacks. We characterize these relational properties by defining an equivalence relation between a system under attack and the original unattacked system. That is, the system satisfies the robustness properties if executions of the attacked system are appropriately related to executions of the unattacked system. We present two techniques for reasoning about the equivalence relation and thus proving the relational properties for a system. One proof technique decomposes large proof obligations to smaller proof obligations. The other proof technique adapts the self-composition technique from the literature on secure information-flow, allowing us to reduce reasoning about the equivalence of two systems to reasoning about properties of a single system. This technique allows us to reuse existing tools for reasoning about properties of hybrid programs, but is challenging due to the combination of discrete dynamics, continuous dynamics, and nondeterminism. To evaluate, we present three case studies motivated by real design flaws in existing cyber-physical systems.

Abstract-Cyber-physical systems, such as self-driving cars or autonomous aircraft, must defend against attacks that target sensor hardware. Analyzing system design can help engineers understand how a compromised sensor could impact the system's behavior; however, designing security analyses for cyber-physical systems is difficult due to their combination of discrete dynamics, continuous dynamics, and nondeterminism. This paper contributes a framework for modeling and analyzing sensor attacks on cyber-physical systems, using the formalism of hybrid programs. We formalize and analyze two relational properties of a system's robustness. These relational properties respectively express (1) whether a system's safety property can be influenced by sensor attacks, and (2) whether a system's highintegrity state can be affected by sensor attacks. We characterize these relational properties by defining an equivalence relation between a system under attack and the original unattacked system. That is, the system satisfies the robustness properties if executions of the attacked system are appropriately related to executions of the unattacked system.
We present two techniques for reasoning about the equivalence relation and thus proving the relational properties for a system. One proof technique decomposes large proof obligations to smaller proof obligations. The other proof technique adapts the self-composition technique from the literature on secure information-flow, allowing us to reduce reasoning about the equivalence of two systems to reasoning about properties of a single system. This technique allows us to reuse existing tools for reasoning about properties of hybrid programs, but is challenging due to the combination of discrete dynamics, continuous dynamics, and nondeterminism.
To validate the usefulness of our relational properties and proof techniques, we present three case studies motivated by real design flaws in existing cyber-physical systems.

I. INTRODUCTION
Cyber-physical systems, which consist of both physical and cyber components, are often safety and security critical [1]- [4]. Designing secure cyber-physical systems is difficult because adversaries benefit from a broad attack surface that includes both software controllers and physical components. Sensor attacks often allow an adversary to directly control the system under attack. For example, Cao et al. demonstrate how to manipulate an autonomous vehicle's distance measurements by shining a laser into its Light Detection and This is an extended version of the paper with the same title that appeared in the 2021 Computer Security Foundations Symposium. This version includes a proof of Theorem 3 in Appendix D.
Ranging (LiDAR) sensors [5], Humphreys et al. demonstrate how spoofing Global Positioning System (GPS) signals may allow an attacker to force a yacht autopilot to deviate from a designated course [6], and Davidson et al. demonstrate a GPS-based hijacking attack on unmanned aircraft [7]. The breadth of the cyber-physical attack surface affords adversaries a range of attack modalities even when hijacking control is not possible. For example, Son et al. demonstrate how to crash a quadcopter using a magnetic attack on a quadcopter's gyroscopic sensors [8].
Testing-based approaches are insufficient to guarantee the safety of a cyber-physical system, even when the system is not under attack. In a 2016 study on autonomous vehicles, Kalra et al. conclude that a self-driving fleet would need to drive hundreds of millions or sometimes hundreds of billions of miles to provide a purely testing-based reliability case [9]. Driving these miles in a representative set of road conditions would take tens or hundreds of years depending on the size of the test fleet. The intractability of testing-based approaches is also confirmed by incompleteness results [10]. Establishing security is even more difficult than establishing safety.
The importance and difficulty of ensuring the safety of cyberphysical systems motivate a growing body of work on formal verification for embedded and hybrid systems [11]- [15]. However, relatively little work considers formal verification of such systems in the presence of sensor attacks. Some recent work emphasize timing aspects of sensor-related attacks [16], [17]; however, the work model the system's dynamics as a deterministic discrete time dynamical system, whereas most cyber-physical systems are best modeled with a nondeterministic combination of discrete and continuous dynamics.
It is important for cyber-physical system designers to understand whether a compromised sensor can result in undesired behavior, such as violating a safety property or corrupting a critical state. For example, the designer of an adaptive cruise control system might want to verify that the car's minimum following distance is not affected by a compromised GPS sensor.
Understanding the impact of compromised sensors requires us to reason about relational properties [18], that is, the relationship between executions of the original uncompromised system and executions of the system where some of the sensors have been compromised. Relational properties are often harder to reason about than functional properties, as they require reasoning simultaneously about multiple executions. And there is less tool support for formal verification of relational properties, compared to functional properties.
In this work, we define and explore two relational properties that characterize the robustness of cyber-physical systems under sensor attacks. Our threat model assumes a powerful attacker that may compromise a subset of sensors and arbitrarily manipulate those sensors' values. We do not model or discover the mechanisms by which an attacker manipulates sensor values; we simply assume they are able to do so.
Our first relational property is robustness of safety, which intuitively holds when the compromised sensors are unable to affect whether a given safety property holds in the attacked system. Note that this is not the same as requiring that the attacked system satisfies the safety property. Indeed it may be beyond current verification techniques to determine whether the safety property holds in the uncompromised system, let alone the compromised system. Nonetheless, even in such cases it can be possible to verify that compromised sensors do not affect the safety property. Robustness of safety implies that if the uncompromised system satisfies the safety property then the compromised system will too. Reasoning about robustness of safety separates reasoning about the implications of sensor attacks from reasoning directly about functional properties.
Our second relational property is robustness of high-integrity state, which requires that high-integrity parts of a system cannot be influenced by the attacker. For example, returning to our autonomous vehicle example, parts of the system pertaining to steering and braking should be regarded as high integrity and independent from low-integrity sensors such as the interior thermometer. Robustness of high-integrity state is similar to noninterference [19], [20], which requires that lowintegrity inputs can not influence high-integrity outputs.
We work within the formalism of hybrid programs [10], [21], [22] and their implementation in the theorem prover KeYmaera X [23]. Hybrid programs model cyber-physical systems as hybrid-time dynamical systems, with the discrete time component of the system modeling software components and the continuous time component of the system modeling physical phenomenon.
To define our two relational properties, we introduce the H-equivalence relation over hybrid programs, where H is a set of variables. Intuitively, two hybrid programs are H-equivalent if they agree on the values of all variables in H at appropriate times. In particular, we define our two relational properties as H-equivalence between the original system and the compromised system (for suitable sets of variables H).
We introduce two sound and tractable techniques to reason about H-equivalence (and thus to prove that robustness of safety and robustness of high-integrity state hold). The first technique decomposes reasoning about H-equivalence of two large programs to reasoning about H-equivalence of their subprograms. The second technique reduces reasoning about H-equivalence of two programs A and B to reasoning about safety properties of a single program that represents both A and B. This reduction allows us to prove relational properties using KeYmaera X, an existing theorem prover for hybrid programs that does not directly support relational reasoning. This technique is inspired by the self-composition technique [24] used to prove noninterference in imperative and deterministic programs. A key challenge we faced in adapting the selfcomposition technique for hybrid programs is reasoning about nondeterminism and physical dynamics, and in particular, ensuring that certain nondeterministic choices are resolved the same in both executions.
The main contributions of this paper are the following: 1. We introduce a threat model of sensor attacks in the context of hybrid programs that model cyber-physical systems. We show that these sensor attacks can be formalized in terms of syntactic manipulations of hybrid programs. We introduce robustness of safety and robustness of high-integrity state, two relational properties that express security guarantees in the presence of sensor attacks. (Section III) 2. We introduce H-equivalence, an equivalence relation over hybrid programs, and express our relational properties in terms of H-equivalence. (Section IV) 3. We present two techniques for reasoning about H-equivalence and prove their soundness. (Section V) 4. We validate the approach developed throughout the paper through three case studies of non-trivial cyber-physical systems: an anti-lock braking system, the Maneuvering Characteristics Augmentation System (MCAS) of the Boeing 737-MAX, and an autonomous vehicle with a shared communication bus. (Section VI) We introduce some background about hybrid programs in Section II. Section VII discusses related work.
This is an extended version of the paper with the same title that appeared in the 2021 Computer Security Foundations Symposium. The main addition of this paper is the proof of Theorem 3 in Appendix D.

II. BACKGROUND
Hybrid programs [22] are a formalism for modeling cyberphysical systems, i.e., systems that have both continuous and discrete dynamic behaviors. Hybrid programs can express continuous evolution (as differential equations) as well as discrete transitions. Figure 1 gives the syntax for hybrid programs. Variables are real-valued and can be deterministically assigned (x := θ, where θ is a real-valued arithmetic term) or nondeterministically assigned (x := * ). Hybrid program x ′ = θ&φ expresses the continuous evolution of variables: given the current value of variable x, the system follows the differential equation Computation on terms ⊕ ∈ {+, ×} Hybrid Program α, β, P x := θ Deterministic assignment of real arithmetic term θ to variable x x := * Nondeterministic assignment to variable x x ′ = θ&φ Continuous evolution along the differential equation system x ′ = θ for an arbitrary real duration within the region described by formula φ ?φ Test if formula φ is true at the current state α; β Sequential composition of α and β α ∪ β Nondeterministic choice between α and β α * Nondeterministic repetition, repeating α zero or more times Differential Dynamic Logic φ, ψ θ1 ∼ θ2 Comparison between real arithmetic terms (∼∈ Program necessity (true if φ is true after each possible execution of hybrid program α) x ′ = θ for some (nondeterministically chosen) amount of time so long as the formula φ, the evolution domain constraint, holds for all of that time. Note that x can be a vector of variables and then θ is a vector of terms of the same dimension.
Hybrid programs also include the operations of Kleene algebra with tests [25]: sequential composition, nondeterministic choice, nondeterministic repetition, and testing whether a formula holds. Hybrid programs are models of systems and typically over-approximate the possible behaviors of a system.
Differential dynamic logic (dL) [21], [22], [26] is the dynamic logic [27] of hybrid programs. Figure 1 also gives the syntax for dL formulas. In addition to the standard logical connectives of first-order logic, dL includes primitive propositions that allow comparisons of real-valued terms (which may include derivatives) and program necessity [α]φ, which holds in a state if and only if after any possible execution of hybrid program α, formula φ holds.
The semantics of dL [21], [26] is a Kripke semantics in which the Kripke model's worlds are the states of the system. Let R denote the set of real numbers and V denote the set of variables. A state is a map ω : V → R assigning a real value ω(x) to each variable x ∈ V. The set of all states is denoted by STA. The semantics of hybrid programs and dL are shown in Figure 2. We write ω |= φ if formula φ is true at state ω. The real value of term θ at state ω is denoted ω θ . The semantics of a hybrid program P is expressed as a transition relation P between states. If (ω, ν) ∈ P then there is an We are often interested in partial correctness formulas of the form φ → [α]ψ: if φ is true then ψ holds after any possible execution of α. The hybrid program α often has the form (ctrl;plant) * , where ctrl models atomic actions of the control system and does not contain continous parts (i.e., differential equations); and plant models evolution of the physical environment and has the form of x ′ = θ &φ. That is, the system is modeled as unbounded repetitions of a controller action followed by an update to the physical environment. Consider, as an example, an autonomous vehicle that needs to stop before hitting an obstacle. For simplicity, we model the vehicle in just one dimension. Figure 3 shows a HP model (hybrid program model) of such an autonomous vehicle. Let d be the vehicle's distance from the obstacle. The safety condition that we would like to enforce (φpost) is that d is positive. Let v be the vehicle's velocity towards the obstacle in meters per second (m/s) and let a be the vehicle's acceleration (m/s 2 ). Let t be the time elapsed since the controller was last invoked. The hybrid program plant describes how the physical environment evolves over time interval ǫ: distance changes according to −v (i.e., d ′ = −v), velocity changes according to the acceleration (i.e., v ′ = a), and time passes at a constant rate (i.e., t ′ = 1). The differential equations evolve only within the time interval t ≤ ǫ and if v is non-negative (i.e., v ≥ 0).
The hybrid program ctrl models the vehicle's controller.
Platzer introduces this autonomous vehicle example [22]. Syntax of hybrid programs used in this paper is similar to the syntax used in KeYmaera X, but revised for better presentation. / * cannot change over time * / 2 R ǫ. / * time limit for control * / 3 R A.
/ * braking rate * / 8 HP accel ≡ ?ψ; a := A 9 HP brake ≡ a := −B 10 HP ctrl ≡ ((accel ∪ brake); t := 0)  The vehicle can either accelerate at A m/s 2 or brake at −B m/s 2 . For the purposes of the model, the controller chooses nondeterministically between these options. Hybrid programs accel and brake express the controller accelerating or braking (i.e., setting a to A or −B respectively). The controller can accelerate only if condition ψ is true, which captures that the vehicle can accelerate for the next ǫ seconds only if doing so would still allow it to brake in time to avoid the obstacle.
The formula to be verified is presented on the last line of the HP model. Given an appropriate precondition φpre , the axioms and proof rules dL can be used to prove that the safety condition φpost holds. The tactic-based theorem prover KeYmaera X [23] provides tool support for automating the construction of these proofs.
To present some of our definitions, we need to refer to the variables that occur in a hybrid program [22], [26]. The free variables of hybrid program P , denoted FV(P ), is the variables that may potentially be read by P . Values of FV(P ) won't be modified during executions of program P . The bound variables of program P , denoted BV(P ), is the set of variables that may potentially be written to by P . We write VAR(P ) for the set of all variables of P , and have VAR(P ) = BV(P ) ∪ FV(P ). For example, let P be the hybrid program modeling an autonomous vehicle with sensors shown in Figure 3, then

III. MODELING SENSOR ATTACKS
In this section, we explain how we model the sensor attacks in hybrid programs. In particular, we introduce how sensor readings are modeled and describe our threat model.

A. Modeling Sensor Readings
Hybrid programs typically conflate the values of variables in the physical model and the values ultimately perceived by the sensor. For example, in Figure 3, the hybrid program We follow the naming convention of related work on hybrid programs by using the names of free variables and bound variables [26]. 1 Definitions. 2 R ǫ. / * time limit for control * / 3 R A.
/ * acceleration of the vehicle * / 19 Problem.  Therefore, our analysis begins with a hybrid program P orig in which sensor reads are not explicitly modeled. We construct a program P that is equivalent to P orig but separately represents sensor reads and requires that variables holding sensor reads are equal to the underlying sensor's value. For example, vp may represent the actual physical velocity of a vehicle and it changes according to laws of physics, and vs may represent the variable in the controller into which the sensor's value is read. In model P we have the constraint vs = vp. From P we can derive additional models that allow sensed values to differ from actual physical values. For example, a model that represents the compromise of the velocity sensor would be identical to P except that the constraint vs = vp is removed, allowing vs to take arbitrary values. Similar modifications to P can represent the compromise of other sensors, or of multiple sensors at the same time.
As an example, Figure 4 shows a HP model of an autonomous vehicle introduced in Figure 3 whose hybrid program separates physical and sensed values: vp and dp are physical values of velocity and distance, while vs and ds are the corresponding sensed values. Note that the ctrl program sets the sensed values equal to the physical values (line 10).

B. Threat Model
We allow attackers to arbitrarily change sensed values. We are not concerned with the physical mechanisms by which an attacker compromises a sensor. Instead, we model sensor attacks as assignments to variables that represent sensed values. Let P be a hybrid program, S A ⊆ BV(P ) be a set of distinguished variables corresponding to sensors that may be vulnerable to attacks, the sensor attack on P is defined as follows: Definition 1 (S A -sensor attack). For a hybrid program P of the form (ctrl;plant) * and a set of variables S A ⊆ BV(P ), the S A -sensor attack on program P , denoted ATTACKED(P, S A ), is the program obtained from P by replacing all assignments to variable v ∈ S A with assignment v := * .
For example, let P be the hybrid program (ctrl;plant) * modeling an autonomous vehicle with separate physical and sensed values shown in Figure 4. If the velocity sensor vs is under attack, program ATTACKED(P, {v s }) would be (ctrl ′ ;plant) * where ctrl ′ is the following: v s := * ; d s := d p ; (accel ∪ brake); t := 0. Note that with such a threat model, only the ctrl part of a program (ctrl;plant) * is modified by an attack, i.e., ATTACKED((ctrl; plant), S A ) = (ATTACKED(ctrl, S A )); plant. Intuitively, it means a sensor attack does not directly affect the physical dynamics with which the system interacts.

C. Robustness to Sensor Attacks
We explore the impact of an S A -sensor attack by studying two relational properties that characterize the robustness of the system to the attack: (1) whether a S A -sensor attack affects the safety of the system and (2) whether a S A -sensor attack affects the system's high-integrity state. a) Robust Safety: Safety is critical in many cyber-physical systems, e.g., a vehicle should not collide with obstacles and pedestrians. We first present the definitions of safety and our relational property robust safety, and then show an example.
This definition says P is safe if for any execution of P whose starting state satisfies φ pre , its ending state satisfies safety condition φ post .
A system is robustly safe if compromise of sensors S A does not affect whether the system is safe. Note that robust safety does not require that the attacked system is safe; instead it requires that if the original system is safe, then the attacked system is also safe. The distinction is important: it allows us to separate the task of reasoning about safety from the task of reasoning about sensor attacks. Indeed, as we will see in a case study in Section VI, it is possible to prove robust safety even when it is beyond current techniques to prove safety.
Definition 3 (Robust safety). For a hybrid program P of the form (ctrl;plant) * and a set of variables S A ⊆ BV(P ), P is robustly safe for φ post assuming φ pre under the S A -sensor attack, denoted For example, let P be the hybrid program modeling an autonomous vehicle with sensors shown in Figure 4. P is safe for φ post assuming φ pre (i.e., SAFE(P, φ pre , φ post )). However, P is not robustly safe for φ post assuming φ pre under S A -sensor attack where S A is {v s }, since SAFE(ATTACKED(P, S A ), φ pre , φ post ) doesn't hold.  vs:= vp; ds:= dp; (accel ∪ brake); t := 0 The system can be modified so that it does satisfy robust safety. For example, we can modify the system to use three velocity sensors (perhaps measuring velocity by different mechanisms) and use a voting scheme to determine the current velocity. Figure 5 shows a model of such a modified system. The physical velocity v p is sensed by three sensors (line 2), and voting performed to determine the final reading v s (lines 3-5). The contents elided in Figure 5 are the same as Figure 4.
Let P be the hybrid program modeling an autonomous vehicle with duplicated sensors shown in Figure 5. For any set S A ∈ {{v s1 }, {v s2 }, {v s3 }}, program P is robustly safe under S Asensor attack, i.e., P is robustly safe if at most one of the velocity sensors is compromised. Intuitively, this is because v s = v p holds after running program voting, even if up to one of the velocity sensors is compromised. A systematic approach for proving robustness safety is presented in Section V. b) Robustness of High-Integrity State: Sensors that may be compromised are low integrity: the sensed values might be under the control of the attacker. By contrast, parts of the system state might be deemed to be high integrity: their values are critical to the correct and secure operation of the system. Low-integrity sensor readings should not be able to affect a system's high-integrity state. For example, an attacker with access to a car's interior temperature sensor should not be able to affect the control of the car's velocity.
We can state this requirement as a relational property: we say the high-integrity state is robust if, for any execution of the system with its low-integrity sensors compromised, there is an execution of the non-compromised system that can achieve the same values on all high-integrity variables. We delay formal definition of robustness of high-integrity state to Section IV.
Let's consider an example. Figure 6 presents a HP model of an autonomous vehicle with sensors shown in Figure 4 but added with interior temperature control (elided contents in Figure 6 are the same as Figure 4). The vehicle has sensor readings of interior temperature (temps). The physical temperature (tempp) changes according to thermo that is set by ctrlt after comparing temps with target temperature T (lines 4-6). In this example, the temperature sensor is lowintegrity and may be compromised.
A system designer may want to understand if such an attack can interfere with the vehicle's high-integrity state such as its velocity. Let P be the model of an autonomous vehicle with interior temperature control shown in Figure 6. Intuitively, its velocity (i.e., variable v p ) is robust with respect to sensor temps: for any execution of ATTACKED(P , {temps}), we have an execution of P that can produce the same values of v p at every control iteration. The system does satisfy robustness of high-integrity state, and we will prove it in Section V.

IV. H-EQUIVALENCE
This section introduces H-equivalence, a notion of equivalence that allows us to reason about our relational properties.

A. Equivalence of Hybrid Programs
Intuitively, H-equivalence of two programs means that for every execution of one program, there exists an execution of the other program such that the two executions agree on set H initially and at the end of every control loop iteration, where H is a set of high-integrity variables.
The formal definition of H-equivalence of programs builds on H-equivalence of program states.
Definition 5 (H-equivalence of programs). For hybrid programs P 1 = α * , P 2 = β * , and a set of variables H, P 1 and P 2 are H-equivalent, denoted P 1 ≈ H P 2 , if they satisfy the following: In the definition, the number n corresponds to an arbitrary number of loop iterations, and the last line indicates that the two executions agree on H at the beginning and end of every loop iteration. The definition is symmetric.
This definition can be readily adjusted for loop-free programs.
Definition 6 (H-equivalence of loop-free programs). For two loop-free hybrid programs α and β, and a set of variables H, α and β are H-equivalent, denoted α ≈ H β, if they satisfy the following: Note that Definition 5 is defined in lock-step, i.e., both loops iterate exactly the same number of times [29]. As pointed out by previous work [30], a lock-step approach is sometimes not flexible enough to express and verify some properties, e.g., properties that may hold for two programs that execute for different numbers of iterations. However, such a lockstep definition is reasonable in our setting. According to the threat model, we are comparing a system with compromised sensors and a system with uncompromised sensors and so the attack should not affect the rate of a system's control (i.e., how frequently the system's control loop executes). Thus, the robustness of a system is correctly encoded by a lockstep definition, in which states of a system with and without compromised sensors are consistent after every loop iteration.
An additional benefit of this definition is that it is more tractable for verification, which we will explore in Section V.

B. Reasoning about Robustness using H-equivalence
The H-equivalence relation can be used to reason about our two relational properties.
a) Reasoning about Robustness of Safety: Robustness of safety can be established by proving H-equivalence with the help of the following theorem, which states that if program P is H-equivalent to ATTACKED(P, S A ) where H is the free variables of formulas φ pre and φ post , then P is robustly safe for φ post assuming φ pre under the S A -sensor attack.
Theorem 1 (H-equivalent programs are robustly safe). For a hybrid program P of the form (ctrl;plant) * , a set of variables S A ⊆ BV(P ), and formulas φ pre and φ post , if P ≈ FV(φpre∧φpost) ATTACKED(P, S A ), then A proof is in Appendix B. Intuitively, the theorem holds because if there were an execution of attacked program such that φ pre held at the beginning but φ post did not hold at the end of a loop, then there must be an execution of P where the same is true, contradicting the assumption that P is safe.
Note that the converse of Theorem 1 does not hold, i.e., if ROBUST(P, φ pre , φ post , S A ), it is not always true that P ≈ FV(φpre∧φpost) ATTACKED(P, S A ). For example, let P be the program (b := 1; a := b) * , formula φ pre be a > 0, φ post be b > 0, and S A be {a}. Then ROBUST(P, φ pre , φ post , S A ) holds, but P ≈ {a,b} ATTACKED(P, S A ) does not hold since some executions of ATTACKED(P, S A ) (i.e., (b := 1; a := * ) * ) do not have a matching execution of P .
Theorem 1 reduces proving robustness of safety to proving H-equivalence, which can be achieved by the techniques introduced in Section V.

V. PROVING H-EQUIVALENCE
We present two sound techniques for reasoning about H-equivalence.

A. Decomposition Approach
Our first approach proves H-equivalence of programs by decomposing the proof obligation into simpler obligations for components of the programs. This relies on various compositional properties of H-equivalence, stated here and proven in Appendix B.
Theorem 2. For all loop-free hybrid programs A, B, C, D and sets H and H ′ of variables, the following properties hold: Sequential composition (Property 4) is particularly useful. The condition FV(C) ∪ FV(D) ⊆ H ensures that H includes all variables that might affect the evaluation of programs C and D. We use this property when considering H-equivalence of ctrl; plant and ATTACKED(ctrl; plant, S A ) = ATTACKED(ctrl, S A ); plant. In particular, if H includes the actuators by which the controller interacts with the physical environment, then ctrl ≈ H ATTACKED(ctrl, S A ) ensures that the physical dynamics (i.e., program plant) can evolve identically in both the attacked and unattacked systems.

B. Self-Composition Approach
The second approach toward proving H-equivalence is inspired by self-composition [24], [31], a proof technique often used for proving noninterference [19], [20]. Noninterference is a well-known strong information security property that, intuitively, guarantees that confidential inputs do not influence observable outputs, or dually guarantees that low-integrity inputs of a system do not affect high-integrity outputs. Noninterference is a relational property: it compares two executions of a program with different low-integrity inputs.
To develop an intuition for how the self-composition technique is used to prove noninterference, consider the problem of checking whether low-integrity inputs of a deterministic program affect high-integrity outputs. Construct two copies of the program, renaming the program variables so that the variables in the two copies are disjoint. Set the high-integrity inputs in both copies to identical values but allow the lowintegrity inputs to take different values. Now, sequentially compose these two programs together. If the composed program can terminate in a state where the corresponding highintegrity outputs differ, then the original program does not satisfy noninterference; conversely, if in all executions of the composed program, the high-integrity outputs are the same, then the original program satisfies noninterference. Intuitively, the composition of the two copies allows a single program to represent two executions of the original program, reducing checking a relational property of the original problem to checking a safety property of the composed program.
Using the same insights, we develop a self-composition technique for hybrid programs, allowing us to use existing verification tools such as KeYmaera X (which can reason about safety properties of hybrid programs) to reason about H-equivalence of two hybrid programs.
It is non-trivial to adapt the self-composition approach to hybrid programs due to the nondeterminism in hybrid programs. In particular, to show that two executions of the same hybrid program are in an appropriate relation, it may be necessary to force (some of) the nondeterminism in the two executions to resolve in the same way. For example, a nondeterministic choice in a hybrid program may represent a decision by a driver to brake or accelerate; the driver's decision is assumed to be a high-integrity input, and so the resolution of the nondeterministic choice should be the same in both executions.
The self-composition must somehow couple the nondeterministic choices to ensure this. Nondeterministic assignment must be similarly handled, i.e., resolution of high-integrity nondeterminism must be coupled in the two executions.
An additional source of nondeterminism in hybrid programs is the duration of physical evolution. The program construct for physical dynamics, x ′ = θ&φ, specifies that the variable(s) evolve according to the differential equation system x ′ = θ for an arbitrary duration within the region described by formula φ. The duration is chosen nondeterministically.
Our self-composition technique takes as input a program P and set of sensor variables S A and creates a program that represents an execution of each of P and ATTACKED(P, S A ). We ensure that the composed program (1) resolves high-integrity nondeterministic choices and assignments the same in both executions; and (2) has the same duration for corresponding physical evolutions.
To ensure that the two executions are appropriately related, we produce a formula that encodes that the two executions have the same values for high-integrity variables; we assume this formula holds at the beginning of the executions, and require the formula to hold at the end of every control iteration. If we can prove that this is the case, then we have proved that if the two executions (1) have the same values for highintegrity inputs at the beginning of their executions, (2) follow the same decisions on high-integrity nondeterminism during their executions, and (3) evolve for the same duration, then the two executions have the same values for high-integrity variables at the end of every control iteration.
Our self-composition approach has some limitations on the hybrid programs to which it applies. First, it is applicable only for hybrid programs of the form (ctrl; plant) * . Second, it is applicable only for hybrid programs that have total semantics for low-integrity inputs. Intuitively, it means if a program has a valid execution for an input state ω (i.e., exists a state ν such that (ω, ν) ∈ P ), then the program has a valid execution for every input state that differs with ω only on low-integrity inputs. The reason for this requirement is that self-composition uses a single program to represent two executions; this composed program has a valid execution only if both executions are valid. Since the two executions differ only on low-integrity inputs, our technique works only if semantics of the unattacked program is total on low-integrity inputs. A straightforward syntactic checker can be developed to check whether a hybrid program meets this requirement. More discussion about the limitation and the syntactic checker can be found in Appendix C.
The rest of this section describes in detail our self-composition approach: how to construct a single program that represents an execution of P and ATTACKED(P, S A ), and then prove it correct. At a high level, our approach works by (1) converting program P to a canonical form P canon that makes highintegrity nondeterministic choices and assignments explicit;  The goal of the canonical form is to make it easier to share the same nondeterministic choices and assignments between the two executions: when we compose the two programs, they will essentially share the same choices program.
For example, Figure 7 shows the previously presented model of an autonomous vehicle with interior temperature control shown in Figure 6 whose hybrid program is rewritten to the canonical form (elided contents in Figure 7 are the same as Figure 6). The program has a nondeterministic choice variable c that represents a decision to brake or accelerate. This choice is considered high-integrity. b) Hybrid Program with Renaming: Note that program P and ATTACKED(P, S A ) have the same set of variables. To compare executions of P and ATTACKED(P, S A ) in a composition, we need to rename bound variables in one of the two programs. Renaming is needed only for bound variables, since their values may differ during executions. Other variables are readonly and their values will be the same for executions of program P and ATTACKED(P, S A ). Thus, these variables can be shared by both programs, and renaming is not needed.
To help us with renaming, we define renaming functions that map all and only the bound variables of a program to fresh variables.
We write ξ(P ) for the program identical to P but whose variables have been renamed according to function ξ. We also apply renaming functions to states and formulas, with the obvious meaning. c) Interleaved Composition: We develop an interleaved composition that composes two programs so their executions have the same values for high-integrity nondeterministic choices and assignments, and last the same evolution duration.
For example, let P be the previously presented hybrid program (in canonical form) of an autonomous vehicle with interior temperature control shown in Figure 7. Figure 8 shows IC(P, {temp s }, ξ), where function ξ renames bound variables in ATTACKED(P, S A ) with subscript 1. Program ctrl ′ and Plant ′ compose two programs as described in Definition 9 (lines 27-30). Line 18 shows the effect of function SUB(choices, ξ): substituting c = * with c1 = c in choices. The choice represents a decision to accelerate or brake, which is high-integrity. The resolution of this choice should be the same in both executions.

d) Proving H-equivalence with an Interleaved Composition:
Given an interleaved composition IC(P, S A , ξ), to prove that two programs are H-equivalent on a set H, we need to first identify a set η of high-integrity variables on which the evaluation of variables in H depend. Then we construct a formula to express that the two program executions have the same values for variables in set η, and finally prove that, for any execution of the composition, if the formula holds initially, it would hold at the end of every control loop iteration of the execution.
/ * time limit of control * / 3 R A.
/ * clock variables * / 34 R dp, dp 1   formula of η and ξ, denoted eq ξ η , is defined as: Then the desired property is, for any execution of the composition, if the equivalence formula holds at the beginning of an execution, it holds at the end of every control loop iteration of the execution. That means, we want to prove the following: eq ξ η → [IC(P, S A , ξ)]eq ξ η For example, eq η in Figure 8 (line 6) encodes that the two executions have the same position (d p = d p1 ) and velocity (v p = v p1 ). The desired property is shown at line 43.
We have proven this property using Keymaera X. Intuitively, proving this property means that for any execution of the autonomous vehicle model, whether or not its temperature sensor is compromised, if the vehicle starts with the same position and velocity, makes the same control decisions for acceleration and brake, and runs for the same duration, it would end with the same position and velocity. e) Soundness: The soundness theorem links the selfcomposition approach with proving H-equivalence. Proof of this theorem is based on trace semantics of hybrid programs [33], [34] and can be found in Appendix D.
Theorem 3 (Soundness of the self-composition approach). For hybrid program P and P c , a set S A ⊆ BV(P ), a renaming function ξ of P c , a set of variables η ⊆ BV(P ), and a set H ⊆ η, if P c is P in canonical form, S A ∩ η = ∅, and eq ξ η → [IC(P c , S A , ξ)]eq ξ η , then P ≈ H ATTACKED(P, S A ).
Note that the condition S A ∩ η = ∅ indicates that the adversary cannot compromise high-integrity variables. f) Applicability: Our self-composition technique applies to a subset of problems of interest rather than general problems. In particular, our technique requires that two executions having the same duration at every control iteration for the plant, and identical values for high-integrity nondeterministic assignments. Our self-composition technique cannot be applied to compare two executions that evolve for different durations or that resolve high-integrity nondeterministic choices and highintegrity nondeterministic assignments differently. However, these restrictions arise naturally for many systems. First, requiring the same duration of evolution for both executions corresponds to the control system having the same frequency of operation. That is, the rate of the the system's control can't be influenced by the attacker. Second, high-integrity non-deterministic choices and high-integrity non-deterministic assignments are used to model exactly the nondeterminism that cannot be influenced by the attacker. As such, they should be resolved the same in both executions. For example, when considering how a corrupted temperature sensor can affect a (non-autonomous) vehicle, the driver's decisions (i.e., whether to accelerate or brake) would be modeled with a highintegrity nondeterministic choice, since we are concerned with understanding the relationship between two executions where the driver makes the same decisions but in one execution the sensor is corrupted. If in the two executions the driver is making different choices, the two executions might diverge almost arbitrarily, even if the corrupted sensor has no security impact. If, on the other hand, we want to use this technique to determine whether an autonomous vehicle's driving subsystem can be influenced by a corrupted temperature sensor, we would need a more precise model of the system that does not use nondeterministic choice between accelerating and braking to model the driving subsystem's decisions. That is, highintegrity nondeterministic choices are by assumption choices that cannot be influenced by the attacker.

VI. CASE STUDIES
To demonstrate the feasibility and efficacy of our approach, we conduct three case studies of non-trivial systems. The first two case studies analyze robustness of safety with the

A. Case Study: an Anti-lock Braking System
System designers may wonder if the system is robustly safe against sensor attacks or if their countermeasures are effective. This case study demonstrates analyzing robustness of safety with the decomposition approach in an Anti-lock Braking System (ABS). An ABS is a safety braking system used on aircraft and vehicles. It operates by preventing the wheels from locking up during braking, thereby maintaining tractive contact with the road surface. ABS monitors the speed of wheels using the wheel-speed sensors. If the controller sees that one wheel is decelerating at a rate that couldn't possibly correspond to the vehicle's rate of deceleration, it reduces the brake pressure applied to that wheel, which allows it to turn faster. Once the wheel is back up to speed, it applies the brake again [35]. a) Modeling ABS: Figure 9 shows a model of an ABS system [36], [37]. The model assumes a single wheel and uses a simple controller that turns on and off maximum braking torque. Intuitively, ABS systems are designed to achieve the maximum friction under certain circumstances (e.g., braking on icy road surface). They achieve this by maintaining an ideal slip ratio (e.g., λ ref in Figure 9). Our controller switches the brake on and off based on the calculated slip ratio (λc) and reference slip ratio (lines 5-7). The calculated slip ratio is computed using sensed wheel speed and vehicle speed (lines 2-3). The physical slip ratio (λp) depends on physical wheel speed (v p ) and vehicle speed (w p ), which are affected by braking torque (T b ) and adhesion coefficient (µp) that depends on the physical slip ratio (line 4).
The initial condition of the ABS system (φ pre ) is that the vehicle is moving at a high speed and its wheel speed is not negative (line 10). The safety condition (φ post ) is that the vehicle's wheel should not lock if the current vehicle speed is large (line 11) [38].

b) Modeling Non-invasive Attack on ABS:
Previous research has demonstrated attacks on ABS through physical channels [39]. By placing a thin electromagnetic actuator near the ABS wheel-speed sensors, an attacker can inject magnetic fields to both cancel the true measured signal and inject a malicious signal, thus spoofing the measured wheel speeds. Such an attack is a S A -sensor attack, where S A = {ω s }, on the wheel-speed sensor. Let P be the hybrid program modeling an ABS system shown in Figure 9. Then ATTACKED(P, {ω s }) is program P with line 2 changed into the following: ctrl ≡ ω s := * ; v s := v p Program P is not robustly safe when the sensor ω s is compromised: assuming SAFE(P, φ pre , φ post ) holds, SAFE(ATTACKED(P, {ω s }), φ pre , φ post ) doesn't necessarily hold, since ω s can be an arbitrary value. c) Designing Robustly Safe ABS System: System designers, in attempts to make ABS system modeled in Figure 9 safer, would be confident in their design if the system with countermeasures can be proven to be robustly safe against the attack.
Assume that designers deploy three wheel-speed sensors and a majority voting scheme in the ABS system modeled in Figure 9. The countermeasure can be modeled by changing line 2 in Figure 9 into the ctrl ≡ voting;vs := vp;, where voting is the following: voting ≡ ω s1 := ω p ; ω s2 := ω p ; ω s3 := ω p ; then ω s := ω s1 else ω s := ω s2 Using the decomposition approach, we can prove that such an ABS system is robustly safe if only one wheel-speed sensor is compromised. The proof can be found in Appendix B.

B. Case study: Boeing 737-MAX
Robustness of safety is a relational property: if the original system is safe then the attacked system will be safe too. Importantly, this separates reasoning about the implications of sensor attacks from reasoning directly about safety properties. Proving a system's safety is often labor-intensive and may even be epistemically problematic. For example, many systems must be verified and validated empirically because their correctness properties are not possible to state in a formal language. However, when it is not easy or even impossible to formally verify safety, it is often still possible to prove that compromised sensors do not affect the safety property.
To demonstrate this advantage of relational reasoning, we present a case study inspired by the Boeing 737-MAX Maneuvering Characteristics Augmentation System (MCAS) [40]. The 737-MAX's dynamics are extremely complicated, and proving properties about similar stabilization systems is an  open challenge in hybrid systems verification [41]. Nonetheless, we are able to analyze robustness of safety against faults or attacks on the angle of attack (AOA) sensor used by the 737-MAX MCAS, even without an analysis of the system's overall safety property or the MAX's flight dynamics.

a) Modeling MCAS:
The MCAS caused at least two deadly crashes in 2019 [42]. MCAS was added to compensate for instability induced by the 737-MAX's new engines. Adding new engines to an existing airframe resulting in an aircraft whose nose tended to pitch upward, risking stalls. The MCAS adjusts the plane's horizontal stabilizer in order to push the nose down when the aircraft is operating in manual flight at an elevated angle of attack (AOA). In many 737-MAX planes, the MCAS is activated by inputs from only one of the airplane's two angle of attack sensors. In both 2019 crashes, the MCAS was triggered repeatedly due to a failed AOA sensor. These false readings caused the MCAS software to repeatedly push the plane's nose down, ultimately interacting with manual inputs in a way that caused violently parabolic flight paths terminating in lost altitude and an eventual crash. On each control iteration, one of the two AOA sensors is randomly chosen (ctrlaoa) and the MCAS is activated using the value of the chosen sensor (line 9). In this model, we intentionally omit details about the flight controller, MCAS system, and flight dynamics. Even with a high-fidelity model [43], proving correctness for the 737-MAX MCAS requires advances in state-of-the-art reachability analysis for hybrid time systems; fortunately, relational reasoning allows us to nonetheless analyze robustness of the system against faults or attacks on the AOA sensors. b) Reasoning for Robustness of Safety: Program ctrlaoa is not robustly safe if either of the AOA sensors is compromised, since aoa s can have false readings. Therefore, the system is not robustly safe for attacks on AOA sensors. Boeing's proposed fix to MCAS includes a requirement that the controller should compare inputs from both AOA sensors [44], which can 15 HP ctrl ≡ choices; ctrlv; ctrl bus ; ctrlr; t:= 0 18 ProgramVariables. 19 R busV . / * value on the bus * / 20 R busH. / * header indicating the type of information * / 21 ... 22 Problem. (?s L = s R ) ∪ (?¬(s L = s R ); aoa s := 0) We can prove that the system with this fix is robustly safe. Let ctrl ′ aoa be ctrlaoa with this simple fix. Then aoa is robustly safe by the decomposition approach. The proof is included in Appendix B. Figure 8 shows the self-composition approach with a model of an autonomous vehicle with interior temperature control. However, the model doesn't account for any internal communication mechanisms. In modern vehicles, Electronic Control Units (ECUs) oversee a broad range of functionality, including the drivetrain, lighting, and entertainment. They often communicate through an internal bus [45].

C. Case Study: An Autonomous Vehicle with an Internal Bus
In this case study, we explore how to use the self-composition approach to analyze robustness of high-integrity state in a model of an autonomous vehicle with an internal bus that communicates both low-integrity messages (sensed temperature) and a high-integrity messages (sensed velocity). We are interested in whether the high-integrity state (i.e., velocity) is robust when the temperature sensor is compromised. Figure 11 shows a model (in canonical form) of such a system (elided contents are the same as in the model previously presented in Figure 8). We model the bus using two variables: a value variable (busV ), which indicates the current value that sits on the bus, and a header variable (busH), which indicates the type of information that sits on the bus: busH = 0 for acceleration, busH = 1 for temperature. Exactly one message is communicated via the bus at each control loop iteration. Acceleration messages have higher priority over thermostat messages. Program (ctrlv) first sets the bus value to the next acceleration value. Program ctrl bus then checks if the value has changed from the existing acceleration value. If not, it activates temperature control (ctrlt) to set the bus value to desired thermostat value (line 11). Otherwise, busH is sent to 0 to indicate that a new acceleration value has arrived (line 12). Program ctrlr reads a value off the bus and sets corresponding values based on the header (lines 13-14).

a) Modeling a Vehicle with an Internal Bus:
b) Robust High-Integrity State: We are interested in whether the vehicle's high-integrity state-v p , the velocity of the vehicle-is robust when its low-integrity sensor (temp s ) is compromised. Specifically, we wonder whether P ≈ {vp} ATTACKED(P, {temp s }), where P is the model shown in Figure 11. We can prove this using the self-composition approach. Figure 12 shows IC(P, {temp s }, ξ), where ξ renames variables in BV(P ) with a subscript 1 (we elide the descriptions of program variables introduced in Figure 11). By choosing the equivalence formula as vp = vp 1 ∧ dp = dp 1 ∧ a = a1 (line 3), we are able to prove the desired property at line 40. Proving this property means for this vehicle, its high-integrity variable v p , d p , and a are robust when its temperature sensor is compromised. We have proven the model in Figure 12 using KeYmaera X.
Note that the decomposition approach and self-composition approach may work well in different settings. The decomposition approach is easy to apply and works well when the sensor attack affects a small portion of the system, as in our first two case studies; by constrast, the self-composition approach can handle cases where the effect of the attack may be complicated-as in our third case study-but requires more effort to use. It is possible to combine the two techniques to prove robustness properties of complicated cases. For example, if we can identify that only a single component of a large system is affected by an attack, the self-composition approach can be used to prove robustness of this component, while the decomposition approach delivers the robustness proof of the whole system.

VII. RELATED WORK
Formal analysis of sensor attacks Lanotte et al. [16], [17] propose formal approaches to model and analyze sensor attacks with a process calculus. The threat model allows attacks that manipulate sensor readings or control commands to compromise state. Their model of physics is discrete and it focuses on timing aspects of attacks on sensors and actuators. In comparison, we analyze relational properties in systems whose dynamics are modeled with differential equations and we introduce techniques to establish proofs of these properties.
Bernardeschi et al. [46] introduce a framework to analyze the effects of attacks on sensors and actuators. Controllers of systems are specified using the formalism PVS [47]. The physical parts are assumed to be described by other modeling tools. Their threat model is similar to ours: the effect of an attack is a set of assignments to the variables defined in the   Figure 11 controller. Simulation is used to analyze effects of attacks. By contrast, we focus on formal analysis for the whole system and propose concrete proof techniques for relational properties.
Analyzing relational properties of cyber-physical systems Akella et al. [48] use trace-based analysis and apply model checking to verify information-flow properties for discrete models based on process algebra. Prabhakar et al. [49] introduce a type system that enforces noninterference for a hybrid system modeled as a programming language. Nguyen et al. [50] propose a static analysis that checks noninterference for hybrid automata. Liu et al. [51] introduce an integrated architecture to provide provable security and safety assurance for cyber-physical systems. They focus on integrated codevelopment: language-based information-flow control using Jif [52] and a verified hardware platform for information-flow control. Their focus is not on sensor attacks.
Bohrer et al. [53] verify nondeducibility in hybrid programs, a noninterference-like guarantee. To do this, they introduce a very expressive modal logic that can explicitly express that formulas hold in a given world (i.e., state). By contrast, we use an existing logic (that has good tool support) to express and reason about a specific threat model.
Closely related to our work is that of Kolčák et al. [54] which introduces a relational extension of dL. A key contribution of their work is a new proof rule to combine two dynamics, allowing existing inference rules of dL to be applied in a relational setting. Similar to their work, our self-composition technique expresses relational properties by leveraging a composition of two programs whose variables are disjoint. Unlike their work, our self-composition technique aims to prove relational properties that require some of the nondeterministic choices to be resolved in the same way in both executions. For instance, our example shown in Figure 8 is not directly expressible in their setting. We believe that the work by Kolčák et al. [54] is orthogonal to ours, and the two can be combined to express and prove more complicated relational properties.
Security analysis for CPSs Much work have focused on the security of cyber-physical systems (CPS), but primarily from a systems security perspective rather than using formal methods. Various attacks (and mitigations of these attacks) have been identified, including false data injection [55], replay attacks [56], relay attacks [57], spying [58], and hijacking [59]. Our work focuses on formal methods for CPS security, ruling out entire classes of attacks.
Mitigating sensor attacks Some work propose attack-resilient state estimation to defend against adversarial sensor attacks in cyber-physical systems [60], [61]. These methods model systems with bounded sensor noises as an optimization problem to locate potentially malicious sensors. Our work has a different formal model of sensor attacks and focuses on formal guarantees of robustness of systems under sensor attacks.

VIII. CONCLUSION
We have introduced a formal framework for modeling and analyzing sensor attacks on cyber-physical systems. We formalize two relational properties that relate executions in the original system and a system where some sensors have been compromised. The relational properties express the robustness of safety properties and the robustness of high-integrity state.
Both relational properties can be expressed in terms of an equivalence relation between programs, and we presented two approaches to reason about this equivalence relation, one based on decomposition and the other based on using a single program to represent executions of the original system and the attacked system. We have shown both of these approaches sound, and used them on three case studies of non-trivial cyber-physical systems.
This work focuses on sensors, but our approach can also be used to model and analyze attacks on actuators. Proof. By the definition of ≈ H and lemma 4 from [26].
Proof of Property 4 of Theorem 2. We prove that for any execution of A; C, there exists an execution of B; D that agrees with it on H. The other direction can be proven similarly. For any execution σ ac of A; C, let ω ac f and ω ac l be its first and last state respectively. Then there exists a state ω acm such that (ω ac f , ω acm ) ∈ A and (ω acm , ω ac l ) ∈ C .
Proof of Property 5 of Theorem 2. By induction on the number of iterations of α * and β * . Base case is trivial. For the induction case, assume α k ≈ H β k is true, we can prove α k ; α ≈ H β k ; β using Property 4 by letting A be α k , B be β k , C be α, and D be β. Thus, α * ≈ H β * holds. Similarly, we can prove ROBUST(P, φ pre , φ post , {s R }).

APPENDIX C LIMITATIONS OF THE SELF-COMPOSITION APPROACH
One limitation of our self-composition approach is that it applies only for hybrid programs that have total semantics for all low-integrity inputs. It means if a program has a valid execution on an input state ω (i.e., exist state ν such that (ω, ν) ∈ P ), then for any state ω ′ that differs with ω only in low-integrity inputs, there exists ν ′ that (ω, ν) ∈ ATTACKED(P, S A ) .
A program may have partial (not total) semantics on lowintegrity inputs for two reasons: (1) some low-integrity inputs fail test conditions in all execution paths, for example, if a is a low-integrity variable, then ?a > 0 is a program whose semantics are partial on low-integrity inputs; (2) the program's evolution constraint depends on low-integrity inputs. For example, if a is a low-integrity variable, (x ′ = θ&a > 0 ) is a program whose semantics are partial on low-integrity inputs.
Fortunately, there is a relatively simple way to check that hybrid programs meet this requirement. First, given a set of low-integrity sensor variables, a straightforward program analysis can identify all variables that might depend on a lowintegrity sensor variables; call these the low-integrity variables. Second, check that all evolution constraints do not include any low-integrity variables. Third, check that any test ?φ i that includes a low-integrity variable occurs as part of a construct ?φ 1 ; α 1 ∪ · · · ∪?φ n ; α n such that φ 1 ∨ · · · ∨ φ n is valid (i.e., the tests are exhaustive and so at least one of the branches of the nondeterministic choice will be true).
Well-designed hybrid program models should have total semantics on low-integrity inputs, except in specific situations that rarely depend on low-integrity sensor variables. Models that do not have total semantics on low-integrity inputs typically do not correspond to actually implementable control strategies, and are therefore only vacuously safe.

APPENDIX D SOUNDNESS PROOF OF THE SELF-COMPOSITION APPROACH
We use trace semantics of hybrid programs [33], [34] to prove Theorem 3. The trace semantics of hybrid programs assigns to each program α a set of traces τ (α). A state is a map from the set of variables to real numbers. The set of all variables is denoted V. The set of all states is denoted STA. A separate state Λ (not in STA) denoting a failure of the system.
A trace is a (non-empty) finite or infinite sequence σ = (σ 0 , σ 1 , ...) of trace functions σ i : [0, r i ] → STA with duration r i ∈ R. A position of σ is a pair (i, ι) with i ∈ N and ι in the interval [0, r i ]; the state of σ at (i, ι) is σ ι i . For a state ω ∈ STA,ω: 0 → ω is a point flow at ω with duration 0. A trace terminates if it is a finite sequence σ = (σ 0 , σ 1 , ...σ n ) and σ n = Λ. In that case, the last state is denoted as σ n (r n ). The first state of σ, denoted FST σ, is σ 0 (0). The set of all traces is TRA.
We denote by ω[x → r] the valuation assigning variable x to d ∈ R and matching with ω on all other variables.
We refer to finite traces that end with failure state Λ as failure traces, and other traces as normal traces. We denote τ ⊲ (P ) the set of normal traces of a program P : τ ⊲ (P ) = {σ ∈ τ (P ) | LST σ = Λ ∨ σ does not terminate} Now, we formalize the H-equivalence of states, trace functions, traces, and programs. Compare with Definition 5, these formal definitions are more general (can be applied on programs with different variable sets) and uses a mapping function between variables in two states (instead of using just a set).
Definition 15 (H-equivalence of states). We define ω i ∼ ∼ ∼ζ ω j , for states ω i and ω j that agree on corresponding variables that are related by function ζ, i.e., Here the domain of ζ corresponds to the H in Definition 5. And ζ is often a subset of the renaming function of the program of concern.
Definition 16 (H-equivalence of trace functions). We define σ i ∼ ∼ ∼ζ σ j , for trace functions σ i and σ j that have the same domain and H-equivalent states at all domain values: dom(σ i ) = dom(σ j ) and ∀p ∈ dom(σ i ), σ i (p) ∼ ∼ ∼ζ σ j (p) Definition 17 (H-equivalence of traces). We define σ a ∼ ∼ ∼ζ σ b , for trace σ a and σ b that agree on (1) the first state (2) Figure 13 shows the formal definition.
We write ω 1 ∼ ∼ ∼id H ω 2 to mean that ω 1 and ω 2 are H-equivalence with respect to an identity function defined on set H and undefined otherwise (i.e., id H ). We write σ a ∼ ∼ ∼id H σ b to indicate traces σ a and σ b are equivalent on id H . We write σ a ∼ ∼ ∼id σ b to mean that σ a and σ b are equivalent with all variables, i.e., the two traces use the same set of variables and they are H-equivalent.
Definition 18 (H-equivalence of two programs by traces). For two hybrid programs P 1 and P 2 of the canonical form, a function ζ maps variables in P 1 to variables in P 2 , P 1 ∼ ∼ ∼ζ P 2 is defined as follows: ∀σ a ∈ τ ⊲ (P 1 ), ∃σ b ∈ τ ⊲ (P 2 ) such that σ a ∼ ∼ ∼ζ σ b To help express the agreement between executions composed in a self-composition, we introduce the notion of projections on states, trace functions, and traces.
Definition 19 (Projection). For state ω and a set V of variables such that V ⊆ VAR(ω), the V projection of state ω, denoted ω ⇓ V , is a map {x → ω(x)} for all x ∈ V .
For a trace function σ i : [0, r i ] → STA and a set V of variables such that V ⊆ VAR(σ i ), the V projection of σ i , denoted σ i ⇓ V , is {ι → (σ i (x) ⇓ V )} for all ι ∈ dom(σ i ).
The soundness theorem (Theorem 3) has a list of promises: a program P and P c (P in canonical form), a set S A of variables, a set η of variables such that S A ⊆ BV(P ), η ⊆ BV(P ), and S A ∩ η = ∅. We assume but elide these promises in the following definitions and lemmas.
Proof. By induction on P .
Proof. By induction on P .
Lemma 11 (Choice part of composition preserve equivalence).
Lemma 13 (Projections of a sequence).