Rayna Dimitrova

Maciej Gazda

Mohammad Reza Mousavi

Sebastian Biewer

Holger Hermanns

Conformance-Based Doping Detection for Cyber-Physical Systems

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

System doping, in our terminology, is an intentional intervention causing a change in the system's normal behaviour against the interests of the user or other stakeholders (such as the society at large). Examples of system doping are widespread and range from vendors' enforcing a monopoly on chargers and spare parts (by checking for and refusing third-party chargers and spare parts, respectively) to tampering with exhaust emission in order to detect and pass emission tests. Doping can be the result of embedding a piece of code or smuggling a piece of electronic circuit into the system and it can be caused by the original developers or by hackers. Software and system doping has been studied in the past couple of years and rigorous theories for it have been developed [START_REF] Barthe | Facets of software doping[END_REF][START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF][START_REF] Biewer | Cyber-physical doping tests[END_REF]. These theories were subsequently adopted in order to detect doping, or formally, to check system cleanness [START_REF] Hermanns | Verification, testing, and runtime monitoring of automotive exhaust emissions[END_REF][START_REF] Biewer | Doping tests for cyber-physical systems[END_REF] (corresponding to the absence of doping).

In the present paper, we extend the theory of doping to the setting of cyberphysical systems (CPS) by exploiting the notions of conformance testing for CPS [START_REF] Abbas | Formal property verification in a conformance testing framework[END_REF][START_REF] Deshmukh | Quantifying conformance using the Skorokhod metric[END_REF][START_REF] Khakpour | Notions of conformance testing for cyber-physical systems: Overview and roadmap[END_REF]. The existing theories of software doping define doping in terms of drastic deviations in output as a result of minor deviations in input, where the term "deviation" refers to differences in validity of propositions or values of variables. However, the current notions come short of properly dealing with the issues of retiming and delays, which are commonly present in the signals of CPS. We observe that this is an essential aspect of detecting doping for cyber-physical systems: often the traces to be tested for doping have subtly different timing behaviour, e.g., due to measurement and calibration errors or due to the slight deviations of human actors in acting upon the planned scenarios. The insufficient treatment of retiming and delays can both lead to false negatives, i.e., missing cases of doping, as well as false positives, i.e., reporting spurious doping cases.

To address these issues, we exploit the notion of conformance to devise a general theory of being clean from doping and instantiate that theory with some existing notions of conformance for hybrid systems. We show how these notions can account for retiming and lead to more precise notions of cleanness.

We illustrate the usefulness of our theory by empirical analysis of diesel engine exhaust emissions in the context of one of the official test cycles, the New European Driving Cycle (NEDC) [START_REF]UN Vehicle Regulations -1958 Agreement[END_REF]. In particular, we show that catering for retiming is essential in effectively exploiting the actual driving cycles for performing doping analysis. We thus demonstrate that our new theory remedies a major shortcoming in the existing notions from the literature. To facilitate the presentation, we use throughout the remainder of this paper the following simple running example, which is inspired by our case study.

Example 1. Fig. 1.(a) shows two test cycles (evolution of speed over time), designed to detect whether the exhaust emission control of a particular vehicle is doped. The test cycle i st , depicted with a black solid line, is the standard one prescribed by the (fictitious) official regulation, while test cycle i dev , depicted by a red dotted line, is a slight deviation thereof. If the exhaust emissions measured during the test cycle i dev turn out to be significantly higher than the ones measured in test cycle i st , then we can conclude that the exhaust emission system is potentially doped, since it appears tailored to the standard test cycle.

Fig. 1.(b) addresses a notorious problem of testing cars: a human tester is supposed to drive the car as just described, however, she can do this only up to a certain imprecision. Assume her driving of i dev exhibits a slight time shift τ relative to the test cycle, as in i ddev , while i st is being driven as intended.

The result of a test is the emission footprint measured at the exhaust pipe of the car. The contributions for this paper can be summarized as follows:

-We define a general notion of conformance that can express different ways of comparing execution traces by allowing deviations both in value and in time.

-We define a general notion of cleanness for hybrid systems, and show that it subsumes the existing notion of robust cleanness [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF]. -We demonstrate the usefulness of the proposed generic framework by applying it to software doping tests in the automotive domain, where we show that the new cleanness definition is able to flag a case of software doping that goes unnoticed when robust cleanness is used.

Related Work

The term "software doping" was coined around 2015 [START_REF] Hapke | Schummeln auch in Europa[END_REF] in media uncovering the diesel exhaust emissions scandal. An informal problem formulation [START_REF] Barthe | Facets of software doping[END_REF] pointed out the general phenomenon of intentionally added hidden software behaviour, which is not in the interest of the consumer. Shortly after, this observation has been complemented by a set of formal cleanness definitions [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF] laying the theoretical foundations upon which formal methods to detect such software behaviour can be used. It is possible to detect missing functionality and undesired existing functionality. The definitions support both sequential programs and non-deterministic reactive programs. To check satisfaction of the definitions, it is necessary to compare two (or more) execution traces of the same system. Such properties are called hyperproperties [START_REF] Clarkson | Hyperproperties[END_REF] (whereas classical properties are trace properties). Tool support for analysing hyperproperties typically requires high computational effort [START_REF] Clarkson | Temporal logics for hyperproperties[END_REF][START_REF] Finkbeiner | Algorithms for model checking HyperLTL and HyperCTL[END_REF]. There exist several temporal logics for analysing satisfaction of trace properties of various kinds of systems, one of them being Linear Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] for systems producing outputs in discrete time steps and properties that do not consider the time passing between outputs. LTL has been extended to the logic HyperLTL, which can express hyperproperties by allowing explicit quantification of execution traces in front of an LTL formula [START_REF] Clarkson | Temporal logics for hyperproperties[END_REF]. Tools for model-checking boolean circuits, satisfiability and monitoring of HyperLTL specifications have been developed [START_REF] Agrawal | Runtime Verification of k-Safety Hyperproperties in HyperLTL[END_REF][START_REF] Brett | Rewriting-Based Runtime Verification for Alternation-Free HyperLTL[END_REF][START_REF] Finkbeiner | Algorithms for model checking HyperLTL and HyperCTL[END_REF][START_REF] Finkbeiner | Deciding hyperproperties[END_REF][START_REF] Finkbeiner | EAHyper: Satisfiability, implication, and equivalence checking of hyperproperties[END_REF][START_REF] Finkbeiner | Monitoring hyperproperties. RV[END_REF][START_REF] Finkbeiner | RVHyper: A runtime verification tool for temporal hyperproperties[END_REF][START_REF] Hahn | Constraint-based monitoring of hyperproperties[END_REF].

Signal Temporal Logic (STL) [START_REF] Maler | Monitoring temporal properties of continuous signals[END_REF] is an extension of LTL that adds support for time constraints and real-valued signals. Tools exist that automatically try to falsify STL formulas [START_REF] Donzé | Breach, A toolbox for verification and parameter synthesis of hybrid systems[END_REF][START_REF] Annpureddy | S-taliro: A tool for temporal logic falsification for hybrid systems[END_REF]. There has been an extension of STL to HyperSTL in a similar fashion as it was done for HyperLTL [START_REF] Nguyen | Hyperproperties of real-valued signals[END_REF]. The syntax of HyperSTL, however, is not able to express the cleanness definitions (for deterministic systems) in a way that allows (efficient) falsification. Robust cleanness is defined for distance functions on inputs and outputs [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF]. When used with temporal logics the distance functions are restricted to those compatible with the logics. To be fully independent, robust cleanness analysis has been embedded into the theory of model-based testing [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF] with input-output conformance [START_REF] Tretmans | A formal Approach to conformance testing[END_REF][START_REF] Tretmans | Conformance testing with labelled transition systems: Implementation relations and test generation[END_REF].

Notions of conformance for discrete event systems have been discussed for almost a century. The earliest work on this topic dates back to 1960's when researchers studied model-based testing of digital circuits using Finite State Machine models [START_REF] Hennie | Fault detecting experiments for sequential circuits[END_REF][START_REF] Lee | Principles and methods of testing finite-state machinesa survey[END_REF]. Concurrency theory contributed ideas to this field, such as decoupling (i.e., removing the synchronised assumption between) inputs and outputs and observing failures to engage in a communication (and more specifically quiescence) [START_REF] De Nicola | Testing equivalences for processes[END_REF][START_REF] Tretmans | A formal Approach to conformance testing[END_REF]. A theory of conformance testing for systems with continuous dynamics was developed by Michiel van Osch [START_REF] Van Osch | Hybrid input-output conformance and test generation[END_REF]; this theory did not gain much popularity in practice, partly because of its insufficient treatment of approximation (e.g., differences in values and retiming). Pappas and Girard [START_REF] Girard | Approximate simulation relations for hybrid systems[END_REF][START_REF] Girard | Approximate bisimulation: A bridge between computer science and control theory[END_REF] proposed the use of Metric Bisimulation for conformance checking in dynamical systems and Pappas and Fainekos [START_REF] Fainekos | Robustness of temporal logic specifications for continuous-time signals[END_REF] developed a falsification framework for the same purpose. This ressearch led to two notions of conformance used in the present paper, namely hybrid conformance by Abbas and Fainekos [START_REF] Abbas | Formal property verification in a conformance testing framework[END_REF] and Skorokhod conformance by Deshmukh, Majumdar, and Prabhu [START_REF] Deshmukh | Quantifying conformance using the Skorokhod metric[END_REF].

Preliminaries

Semantic domain. In this section, we provide definitions regarding semantic domain, conformance, and robust cleanness. We begin with the definition of our semantic domain, called generalised timed traces [START_REF] Gazda | Logical characterisation of hybrid conformance[END_REF]. This definition subsumes both discrete-time state sequences and continuous-time trajectories. A generalised timed trace is a function with a discrete or continuous domain (called time domain) and a co-domain which is a metric space. Intuitively, a generalized timed trace maps each element of its time domain to a state. We require that the set of possible states is a metric space since we study conformance notions that compare traces based on the distance between the states of the traces. For a GTT µ : T → Y and time t 0 ∈ T , by µ[. . . t 0 ] we denote the prefix of µ up to t 0 , i.e., the restriction µ| t∈T :t≤t0 ; likewise, by µ[t s . . . t e ], we shall denote the restriction µ| t∈T :ts≤t≤te

A hybrid system is a mapping from generalised (input) traces to sets of generalised (output) timed traces.

Definition 2. A Y-valued hybrid system is a function H : GTT (Y) → P(GTT (Y)) such that for all µ ∈ GTT (Y) and all µ ∈ H (µ) it holds that dom(µ ) = dom(µ). We define H(Y) to be the set of all Y-valued hybrid systems.

In addition, we distinguish deterministic hybrid systems whose output values range over singleton sets only. In what follows, we identify deterministic hybrid systems with functions of the type GTT (Y) → GTT (Y).

For simplicity, we assume that the input and output domain are defined on the same metric spaces. The generalisation to different spaces is straightforward.

Conformance relations. Recently, a number of notions of conformance for cyberphysical systems have been proposed [START_REF] Aerts | Model-based testing of cyber-physical systems[END_REF][START_REF] Khakpour | Notions of conformance testing for cyber-physical systems: Overview and roadmap[END_REF]. It turns out that these notions, two of which are quoted below, can provide a rigorous basis for doping detection.

Note that throughout the paper, the variables τ and (with possible subscripts) always range over non-negative real numbers. Definition 3. We say that Y-valued GTTs µ 1 : T 1 → Y and µ 2 : T 2 → Y are:

trace conformant with tolerance threshold for signal value , notation

TraceConf (µ 1 , µ 2 ), if T 1 = T 2 and for all t ∈ T 1 , d Y (µ 1 (t), µ 2 (t)) ≤ -hybrid conformant with thresholds τ and , denoted HybridConf τ, (µ 1 , µ 2 ), if: • ∀t 1 ∈ T 1 ∃t 2 ∈ T 2 : |t 2 -t 1 | ≤ τ ∧ d Y (µ 2 (t 2 ), µ 1 (t 1 )) ≤ • ∀t 2 ∈ T 2 ∃t 1 ∈ T 1 : |t 1 -t 2 | ≤ τ ∧ d Y (µ 1 (t 1 ), µ 2 (t 2 )
) ≤ -Skorokhod conformant with tolerance thresholds τ and , notation SkorConf τ, (µ 1 , µ 2 ), if T 1 and T 2 are intervals and there is a strictly increasing continuous bijection r : T 1 → T 2 called retiming, such that:

• for all t ∈ T 1 , |r(t) -t| ≤ τ , and

• for all t ∈ T 1 , d Y (µ 1 (t), µ 2 (r(t))) ≤ .
We show in the proposition below and also in our generalisation results in Section 4, that these notions are closely related. However, they also have some fundamental differences, that can be illustrated using the example in Fig. 1.

Example 2. Consider again the example shown in Fig. 1. We can see that in The outputs o (i st ) and o (i ddev ) in Fig. 1.(d) illustrate the fundamental difference between hybrid and Skorokhod conformance: although the order of rising and falling signals are reversed in the two trajectories, they are still hybrid conformant, because hybrid conformance disregards the order. However, Skorokhod conformance requires an order-preserving retiming, and hence distinguishes these two trajectories. On the other hand, such retiming exists, e.g., for i st and i ddev in Fig. 1.(b), witnessing their Skorokhod conformance.

We shall use the following notation. We write Conf 1 Conf 2 whenever for all µ 1 : T 1 → Y and µ 2 :

T 2 → Y, we have Conf 1 (µ 1 , µ 2 ) =⇒ Conf 2 (µ 1 , µ 2 ). We write Conf 1 Conf 2 whenever Conf 1 Conf 2 and ¬ Conf 2 Conf 1 .
Proposition 1. For any τ, ∈ R ≥0 , the following relations hold:

TraceConf SkorConf τ, HybridConf τ,
Robust cleanness. We shall now state the original definition of robust cleanness from [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF], adapted to our framework of hybrid systems. It is based on Definition 7 and Proposition 19 from [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF]; the phrasing below abstracts from the so-called parameters of interest and standard inputs. Moreover it is cast in the setting of generalised timed traces rather than discrete-step programs, and stated using trace conformance with different thresholds for inputs and outputs, κ I and κ O . Intuitively, a hybrid system is robustly clean if for every pair of input prefixes on which no difference in the inputs exceeding κ I has occurred so far (i.e., all sub-prefixes are trace conformant), the corresponding sets of output prefixes are also conformant with respect to κ O . As we consider nondeterministic systems, Hausdorff distance is used to compare sets of outputs (see [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF] for details).

Definition 4. A hybrid system H is robustly clean, denoted RobustClean(κ I , κ O ), whenever: ∀i 1 , i 2 ∈ GTT (Y) : ∀t ∈ dom(i 1 ) ∪ dom(i 2 ) : ∀t ≤ t : TraceConf κ I (i 1 [. . . t ], i 2 [. . . t ]) =⇒ (∀o 1 ∈ H (i 1 ) ∃o 2 ∈ H (i 2 ) : TraceConf κ O (o 1 [. . . t], o 2 [. . . t])) ∧ (∀o 2 ∈ H (i 2 ) ∃o 1 ∈ H (i 1 ) : TraceConf κ O (o 1 [. . . t], o 2 [. . . t]))
Note that in the above definition we do not require that dom(i 1 ) = dom(i 2 ). In practice, robust cleanness is typically applied to pairs of traces that are both defined over N. Here, however, for the sake of generality we impose no such restriction. In particular, when the time domains of two traces are different, for example disjoint, the predicate RobustClean will trivially evaluate to true. Example 3. Consider the traces depicted in Fig. 1. The input prefixes i st and i ddev are given in Fig. 1.(b), and the corresponding pair of outputs is shown in Fig. 1.(c). The trace i st results in output o(i st ) and i ddev results in o(i ddev ). Suppose that < |i st (t 0 ) -i ddev (t 0 )| and < |o(i st )(t 1 ) -o(i ddev )(t 1 )| at some time t 1 . Thus, the left-hand side of the implication in the Def. 4 instantiated with κ I = κ O = does not hold for any t . Hence, regardless of the outputs, this pair of inputs satisfies the condition of RobustClean( , ), and, if these are the only traces in a hybrid system H then we can conclude that H is RobustClean( , ).

Conformance-Based Cleanness

We now define a general notion of conformance-based cleanness and provide two instantiations based on the conformance notions defined in the previous section.

The need for considering disturbance in time as well as in value is motivated by our running example from Fig. 1. One of the challenges in performing doping tests for cyber-physical systems is that in such systems timing is rarely perfectly precise, due to imprecision in measurements, or caused by the interaction with the physical world. As illustrated in Example 1, for instance, when checking for software doping in a car [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF], the input to the system is the value of the car's speed over time, which is under the control of a driver, and can thus vary from one execution to the other, even if the driver is trying to execute the same input sequence. Clearly, those variations can be in value, as well as in time.

Example 4. Consider the test setup sketched in Fig. 1. There, i st and i ddev , depicted in Fig. 1.(b) define speed of a car as a function of time. These two input sequences follow a trajectory of values differing by a small margin (the difference in value allowed by the standard defining the doping tests), but also shifted by a small unit of time τ . Observe further that |i st (t 0 ) -i ddev (t 0 )| . Thus, without allowing for deviations in time when comparing these input sequences, they will be considered sufficiently different, and as a result their respective exhaust emission outputs will fall out of the comparison when checking for doping according to Def. 4, even if the NO x emission values in the corresponding outputs H (i st (t)) and H (i ddev (t)) are vastly different, as depicted in Fig. 1.(c). This results in a false negative, i.e., failing to detect a clearly doped system.

In the above example, we demonstrated that not accounting for timing disturbances when relating input trajectories can result in false negatives in doping detection. Dually, using the traditional comparison for output traces can result in false positives by requiring overly strict matching of outputs.

The above example motivates the need to account for timing deviations in trajectories. Intuitively, for input trajectories this relaxation results in considering more traces as conforming, and thus enforcing more comparisons when checking if a system is clean. For output trajectories this means relaxing the conformance requirement by considering two output sequences as conforming even if their values are not perfectly aligned in time. Furthermore, different types of timing deviations need to be considered in different scenarios, for example, depending on whether the order in which values occur is important or not.

Example 5. Consider the testing workflow from Example 1 and Fig. 1, where inputs i st and i ddev are passed to a car. In the second experiment, depicted in Fig. 1.(d), the car outputs o (i st ) and o (i ddev ), which are hybrid conformant for and τ . Hence this observation of the system is classified as clean under hybrid output conformance. However, the output o (i ddev ) is clearly suspicious, as the values in o (i ddev ) and o (i st ) are reversed. This motivates considering conformance notions that require retimings to be order-preserving. Indeed, using Skorokhod conformance we can detect that the system is doped.

The above examples show that in order to be useful in a diverse set of applications, a software cleanness theory should allow for using a variety of conformance notions. To this end, we next take a more general view on conformance notions, in order to be able to develop a generic conformance-based cleanness framework.

So far, we have defined three specific notions of conformance which either coincide, or are closely inspired by ones that have appeared in the literature. In order to define a general framework for cleanness, we also wish to treat notions of conformance in a more generic manner. To this end, we propose an abstract definition of conformance predicates. As conformance predicates admit variations in time, as well as in value, our definition is based on retimings, a device that will play a key role in the context of this work. In its general form a retiming is a pair of functions between two time domains. Intuitively, given two GTTs, a retiming will define a mapping from points in each of the traces to points in the other trace. Note that in general the mappings are not required to be injective; this way we can cater for notions of conformance allowing for the so-called local disorder phenomenon (in particular hybrid conformance -see Proposition 2). Definition 5. A retiming is a pair of functions between two time domains, i.e., a pair of the form (r 1 , r 2 ), where r 1 : T 1 → T 2 and r 2 : T 2 → T 1 , with time domains T 1 , T 2 ⊆ R ≥0 .Given two time domains T 1 and T 2 , we denote the set of all retimings between T 1 and T 2 with RET (T 1 , T 2 ).

Retiming is explicitly present in the definition of Skorokhod conformance; there, each Skorokhod retiming is required to be a strictly increasing continuous bijection. We can express a Skorokhod retiming r as an instance of our definition as the pair (r, r -1 ). In fact, one can also define hybrid conformance, as well as a whole class of conformance notions, using a suitable family of retimings.

A family of retimings Ret can be further constrained by τ to a subset Ret τ of Ret containing only functions that shift time by at most τ time units. In order to use a family of retimings for concrete sequences µ 1 and µ 2 , it is necessary to consider only functions that match the domains of the sequences. This leads to a generic notion of conformance associated with a given family of retimings Ret, a given time threshold τ and a given value threshold . Definition 6. Let Ret be a family of retimings, and let

Ret τ = {(r 1 , r 2 ) ∈ Ret | ∀t ∈ dom(r i ) : |r i (t) -t| ≤ τ (i = 1, 2)}, Ret τ (T 1 , T 2 ) = Ret τ ∩ RET (T 1 , T 2 ).
A conformance notion with time threshold τ and value threshold induced by Ret is a predicate Conf Ret τ, on pairs of GTTs such that, for µ 1 :

T 1 → Y, µ 2 : T 2 → Y: Conf Ret τ, (µ 1 , µ 2 ) ⇐⇒ ∃(r 1 , r 2 ) ∈ Ret τ (T 1 , T 2 ) : ∀t ∈ T 1 : d Y (µ 1 (t), µ 2 • r 1 (t)) ≤ ∧ ∀t ∈ T 2 : d Y (µ 2 (t), µ 1 • r 2 (t)) ≤ .
Using the above definition, we can easily express the specific notions of conformance defined in the previous section by selecting a suitable family of retimings.

Proposition 2. The conformance predicates below coincide with the notions of conformance induced by the corresponding families of retimings:

-TraceConf is induced by the family of retimings containing only identity functions: Ret id = {(id, id) | id : T → T is the identity on some T ⊆ R ≥0 }. -SkorConf τ, is induced by the family of retimings Ret = {(r, r -1 ) | r is a strictly increasing continuous bijection}. -HybridConf τ, is induced by pairs of arbitrary functions.

Definition 6 also enables us to define other notions of conformance, such as, for instance a "shift conformance", which, intuitively, shifts all time points by a given constant c ∈ R, i.e., Ret c = {(r, r -1 ) | r(t) = t + c}.

Next, we define a generic notion of cleanness, parametrised by conformance predicates for the input and for the output traces. Instantiating these predicates with existing or new conformance notions, yields different conformance-based notions of cleanness that can capture a variety of cleanness specifications.

We now extend the notion of robust cleanness [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF] to allow for "small" variations in time, in addition to the variations in value. To this end, the new notion makes use of two conformance predicates, one that postulates when two input traces should be considered close enough, and another one that specifies when two output traces are close enough.

Our starting point, the notion of robust cleanness in Definition 4, is based on comparison of matching prefixes of a pair of input traces and the corresponding prefixes of the associated output traces. As we now want to accommodate for distance in time, we (1) compare prefixes using a conformance relation, and (2) allow for variation in the length of the compared prefixes that is within the corresponding time-distance threshold. More precisely, when comparing two prefixes, we allow for discarding start and end segments of length at most τ .

This intuition is formalized by the predicate PrefConf for relaxed comparison of GTT prefixes using a notion of conformance Conf with tolerance threshold τ for time disturbance. We use cascaded notation to define PrefConf as a higher-order function taking Conf as its first argument. The predicate PrefConf compares two prefixes µ 1 and µ 2 by requiring that there exist traces µ 1 [t s 1 . . . t e 1 ] and µ 2 [t s 2 . . . t e 2 ] obtained from them, that are conformant with respect to Conf. These traces are obtained by possibly removing a sub-prefix of length at most τ , and/or removing extending with a suffix of length at most τ . Definition 7. Let Conf be a notion of conformance on GTTs with tolerance threshold τ for time disturbance. For any pair of GTTs µ 1 : T 1 → Y, µ 2 : T 2 → Y, and t ∈ T = T 1 ∪ T 2 , the predicate PrefConf is defined as:

PrefConf(µ 1 , µ 2 , t)⇐⇒∃t s 1 ∈ [0, τ ] ∩ T 1 , ∃t e 1 ∈ [t -τ, t + τ ] ∩ T 1 , ∃t s 2 ∈ [0, τ ] ∩ T 2 , ∃t e 2 ∈ [t -τ, t + τ ] ∩ T 2 : Conf(µ 1 [t s 1 . . . t e 1 ], µ 2 [t s 2 . . . t e 2 ]
). The predicate PrefConf provides a generic notion of prefix-conformance. By instantiating it with conformance relations Conf I and Conf O for input and output traces respectively, we define the notion of (Conf I , Conf O )-cleanness.

For deterministic systems (Conf I , Conf O )-cleanness requires that for all pairs of input prefixes for which all sub-prefixes are prefix-conformant w.r.t. Conf I , the corresponding pair of output prefixes are prefix-conformant w.r.t.

Conf O . Definition 8. A deterministic system H is (Conf I , Conf O )-clean if ∀i 1 , i 2 ∈ GTT (Y) : ∀t ∈ dom(i 1 ) ∪ dom(i 2 ) : (∀t ≤ t : PrefConf I (i 1 , i 2 , t ) =⇒ PrefConf O (H (i 1 ), H (i 2 ), t).
The above definition naturally generalises to nondeterministic hybrid systems, by comparing sets of possible output prefixes using Hausdorff distance as in [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF].

Definition 9. A system H is (Conf I , Conf O )-clean if ∀i 1 , i 2 ∈ GTT (Y) : ∀t ∈ dom(i 1 ) ∪ dom(i 2 ) : ∀t ≤ t : PrefConf I (i 1 , i 2 , t ) =⇒ (∀o 1 ∈ H (i 1 ) ∃o 2 ∈ H (i 2 ) : PrefConf O (o 1 , o 2 , t)) ∧ (∀o 2 ∈ H (i 2 ) ∃o 1 ∈ H (i 1 ) : PrefConf O (o 1 , o 2 , t)) .
Robust cleanness [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF] can be now formulated as conformance-based cleanness, which establishes that (Conf I , Conf O )-cleanness is a generalisation. Using hybrid conformance, we define hybrid-conformance cleanness, and similarly, plugging in Skorokhod conformance, we define Skorokhod-conformance cleanness. Formally: We will now establish some key relations between the cleanness notions defined previously. We begin by lifting the implication between conformance relations to implication between cleanness notions defined using those relations.

-A hybrid system H is robustly clean, denoted RobustClean(κ I , κ O ), if and only if H is (TraceConf κ I , TraceConf κ O )-clean. -A hybrid
Proposition 3. Suppose that Conf 1 I Conf 2 I and Conf 1 O Conf 2 O . Then for any system H: H is (Conf 1 I , Conf 1 O )-clean =⇒ H is (Conf 2 I , Conf 2 O )-clean.
The proposition above has two important corollaries. The first one explains the relationships between the original robust cleanness, and notions of cleanness based on Skorokhod conformance and hybrid conformance, in particular stating the conservative generalisation property for the latter notions. The second corollary compares cleanness notions with different conformance thresholds. Hence, the system tested in Fig. 1.(c) is not HybridClean( , τ, , τ ).

We now discuss testing and falsification of conformance-based cleanness.

For systems with discrete time domains the existing methods for verifying [START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF] or testing [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF] robust cleanness can be readily applied.

In the case of hybrid cleanness, existing methods for testing hybrid conformance, such as [START_REF] Abbas | WiP abstract: Conformance testing as falsification for cyber-physical systems[END_REF] and [START_REF] Araujo | Sound conformance testing for cyber-physical systems: Theory and implementation[END_REF] can be extended to testing and falsification of hybrid cleanness of hybrid systems consisting of traces with finite time domains. Methods for checking Skorokhod conformance were presented in [START_REF] Deshmukh | Quantifying conformance using the Skorokhod metric[END_REF]. Due to the quantification over all time-points t in our Definition 8 and Definition 9, it is not clear how to directly extend them to testing Skorokhod cleanness.

Case Study

In this section we evaluate the proposed notion of hybrid cleanness in the context of doping detection in relation to the recent Diesel Emissions Scandal.

Conducting software doping tests for cyber-physical systems has a range of applications. A prominent example is the body of recent work [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF][START_REF] Hermanns | Verification, testing, and runtime monitoring of automotive exhaust emissions[END_REF][START_REF] Köhl | Efficient monitoring of real driving emissions[END_REF][START_REF] Biewer | Cyber-physical doping tests[END_REF][START_REF] D'argenio | Is your software on dope? -formal analysis of surreptitiously "enhanced" programs[END_REF][START_REF] Contag | How they did it: An analysis of emission defeat devices in modern automobiles[END_REF][START_REF] Barthe | Facets of software doping[END_REF] that gives insights into the Diesel Emissions Scandal. This is a world-wide scandal where millions of diesel cars have been equipped with defeat devices reducing the effectiveness of emission cleaning systems during real-world usagein contrast to the regulator-defined driving scenarios on a chassis dynamometer, where the amount of emitted pollutants are well below the applicable limits.

Assuming the existence of a contract that formalizes when software is considered to be doped, recent work demonstrates how doping tests can be generated automatically and how the characteristic challenges arising with these kinds of tests can be tackled [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF]. A major challenge is the distortion of inputs that can occur during test execution. As doping tests have to be conducted on the final product, i.e., a vehicle such as a passenger car, a human driver has to provide the inputs to the car by driving it. It is far from trivial to provide the inputs exactly as defined by the test case. Official regulations, that define the approval process for new car models, precisely specify test cycles for which they allow tolerances in the input of up to 2 km/h (in car speed). But even driving a car within this tolerance requires a very experienced driver. To strengthen the position of consumers against manufacturers, it is necessary to allow manufacturer-independent methods to check the compliance of a car model with the applicable regulations, i.e., the absence of defeat devices. These methods are supposed to require a reasonable amount of effort, and training a driver over months so that she has enough experience to stay within the tolerance of 2 km/h is way beyond reasonable effort. This means that the responsibility for accounting for the driver's imprecision must be shifted to the techniques for checking for software doping.

In this section we give a short summary of recent doping tests with a diesel car and demonstrate how the theory developed in this paper addresses the above challenge. More precisely, it allows us to overcome the imprecise timing leading to minor input distortions, by appropriately accounting for the effect of retiming on the input value error. We further show how using our theory one of the tests reveals strong indications for a defeat device in the car under test -despite a very inexperienced driver conducting the test. This doping detection would not have been possible using the cleanness notions existing prior to this work.

Physical set-up of the experiment. Before a car model can be sold, it must meet the requirements defined in the official regulations. The type approval procedure requires the car to be placed on a chassis dynamometer. Cars have to follow certain standardized test cycles, each defined as a function from time to speed. One of the test cycles, involved in the diesel scandal, was the New European Driving Cycle (NEDC) [START_REF]UN Vehicle Regulations -1958 Agreement[END_REF] shown in Fig. 2. For the tests here, we consider the speed of the car as input, since this is the parameter defining a test cycle. The total amount of NO and NO 2 (abbreviated as NO x ) is the only output of interest. The car under test is a Nissan NV200 Evalia, with Renault 1.5 dci (110hp) diesel engine and approved w.r.t. regulation Euro 6b. The test set-up is shown in Fig. 2.

In order to perform a check for defeat devices using a cleanness test, we consider, in addition to the original NEDC, two manually synthesized tests. These test cycles, denoted PowerNEDC and SineNEDC were proposed in previous work [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF] and are defined as follows. PowerNEDC is based on the NEDC but slightly deviates from it by enforcing higher accelerations (1.5 m s 2 instead of 0.94 m s 2 ) after 56s, 251s, 446s and 641s. The maximum input deviation from NEDC is κ I = 10km/h. SineNEDC is defined as the NEDC superimposed by a sine curve, formally SineNEDC(t) = max{0, NEDC(t) + 5 sin(0.5t)}, with a maximum input deviation from NEDC of κ I = 5km/h. These test cycles are defined by specifying the input value (the speed) in each second. Both test cases are shown by the red dotted lines in Fig. 3.

Conformance-based cleanness tests for NEDC. We have applied our theory of conformance-based cleanness to check for doping, i.e., the presence of a defeat device, in the car under test. For this, we have at our disposal the raw data obtained from three test drives: (1) Test drive dNEDC is the result of NEDC cycle driven by a human driver. It serves as the reference behaviour of the car, to which we will compare the executions of the other two test cycles. (2) Test drive dPowerNEDC is the trajectory that is produced as the result of a human driver driving PowerNEDC. (3) Test drive dSineNEDC is the trajectory that is produced as the result of a human driver driving SineNEDC.

The values of the actual sequences of inputs executed by driving the car are sampled in steps of 0.05s. As mentioned earlier, the human in the loop makes testing considerably more challenging. The maximum deviation of inputs compared to the test specification for NEDC is just below 10 km/h, for PowerNEDC is almost 12 km/h, and for SineNEDC it approaches 16 km/h. This shows that the perturbation introduced by the human driver is clearly noticeable. The amount of NO x measured for dNEDC is 180mg/km, for dPowerNEDC and dSineNEDC the measurements revealed 204mg/km and 584mg/km, respectively.

In order to detect doping (by falsifying cleanness), the input sequences of dPowerNEDC and dSineNEDC have to be each compared to dNEDC, and if the input sequences in the corresponding pair are conforming, then the respective outputs (the total NO x emission values) have to be checked for conformance.

As we desire for our doping tests to be as strict as possible, we identify hybrid conformance HybridConf τI , I , i.e., the weakest of the conformance relations discussed in Section 3, as the most suitable conformance relation for the comparison of input traces. As the outputs are just single values, the choice of output conformance relation is immaterial in this case, so we take HybridConf 0, O .

Formally, we consider the deterministic hybrid system H defined by the input GTTs dNEDC, dPowerNEDC, and dSineNEDC, and check whether H is HybridClean(τ I , I , 0, O )-clean for given values of τ I , I and O . The driver's imprecision has a significant effect on the values in the input sequences and their timing. This can lead to dismissing pairs of sequences if they are incorrectly deemed too far apart, and thus missing some indications of doping. For instance, a too strict comparison of dSineNEDC to dNEDC will dismiss this pair of executions; however, the measured NO x emission during the dSineNEDC drive is three times more than the one measured during dNEDC.

Testing HybridClean(τ I , I , 0, O ) allows us to perform a realistic comparison by taking into account the two possible sources of driving errors: the over-or undershooting of the speed, and the timing offsets, where the driver accelerates or decelerates too fast or too slowly. In comparison, prior doping tests based on Robust Cleanness, considered only the former, i.e., the point-wise offset in speed. As we demonstrate, depending on the specified value threshold, there are cases when this is insufficient to identify doping. Indeed, looking into the official regulations, we can see that they allow for a timing variation of one second [START_REF]UN Vehicle Regulations -1958 Agreement[END_REF][START_REF][END_REF]. Thus, essentially, the regulations allow for hybrid conformance with τ I = 1s. Hybrid cleanness testing. In order to test HybridClean(τ I , I , 0, O ) we have to examine the conformance relations HybridConf τI , I (dNEDC, dPowerNEDC) and HybridConf τI , I (dNEDC, dSineNEDC) between the corresponding input sequences. Recall that since the output of the system measured in each test is the total amount of NO x emitted during the test, i.e., a single value for the whole execution, timing plays no role when quantifying the value error for the output.

In order to evaluate the power of using hybrid cleanness for detecting doping, we consider different values for I and τ I , and perform two types of analysis of the results of testing HybridClean(τ I , I , 0, O ), which we describe below. Effect of τ I on the minimal I for which inputs are conforming. First, we fix a maximum value that we allow for the time offset τ I . For this τ I we analyse our dataset to find the minimal I such that for the combination τ I and I the input traces under consideration satisfy hybrid conformance. For τ I = 0 we get exactly the I for which the two traces are trace conformant. Table 1 (left side) shows the computed I values for τ I = 0, 0.5, 1, 2, 5, 10.

As expected, when we increase τ I , the minimal I decreases. At some point (at τ I = 2 for PowerNEDC and τ I = 5 for SineNEDC) the decrease in the value error reduces notably. This happens because the error is only partially caused by the incorrect timing of the driver.

From the values reported in Table 1 (left) we see that if, for example, we allow deviation for the input τ I = 1, as per the official regulation, and set I = 15, then we have that both HybridConf τI , I (dNEDC, dPowerNEDC) and HybridConf τI , I (dNEDC, dSineNEDC) are true, while, for τ I = 0 both are false. Thus, under hybrid conformance these pairs of traces will be considered in the cleanness test, while under trace conformance they will be dismissed.

Since the difference between the outputs measured during dSineNEDC and during dNEDC is vast, we establish that HybridClean(1, 15, 0, 180) does not hold. Effect of I on the minimal τ I for which inputs are conforming. Second, we fix the maximum value error I and examine what minimal τ I results in a combination τ I and I for which the analysed data is hybrid conformant. For the synthesized test cases we study the error tolerance I set to the respective input thresholds κ I . As discussed above, this is 10km/h for PowerNEDC and 5km/h for SineNEDC. We also consider the scenario where the error tolerance allowed by the official regulation for the test cycle is added, that is, we also consider I = κ I + 2km/h. The two rightmost columns of Table 1 show the necessary time shifts to achieve these value errors. As apparent, they reduce by approximately 84% and 94% when adding the error tolerance of 2 km/h. These values for τ I give us the minimal tolerance threshold for time, for which HybridClean(τ I , I , 0, 180) is violated in H for the given I ; the value of O is fixed at 180mg/km according to the standard [START_REF] Biewer | Doping tests for cyber-physical systems[END_REF].

Evaluation and discussion. The analysis of the data shows that it is indeed necessary to not only consider a deviation of value, but to also allow for timing deviations, especially when the quality of the studied driving tests suffers from the human-caused input distortions. In terms of the theory established in this paper, this means that in scenarios like this one, employing HybridClean is more adequate than using prior notions such as RobustClean, and without this, the cases of doping we have detected would go unnoticed. Allowing a retiming of up to 10.8s (for PowerNEDC) and of 4.05s (for SineNEDC) makes both inputs conformant to the NEDC input, so we are able to detect the violation of SineNEDC for the hybrid cleanness for the specified desired value error tolerance. While these time deviations appear large given the test cycle timeline, they are acceptable when we recall that the tests are executed by human drivers.

If, on the other hand, we want to restrict the tolerance in time to one second, we are able to consider both tests for the hybrid cleanness for value error tolerance of 12.41km/h for PowerNEDC and 14.24km/h for SineNEDC.

This demonstrates how conformance-based cleanness notions like HybridClean allow us to some extent to account for human-caused errors related to timing.

Finally, while hybrid cleanness is arguably the appropriate notion for the case study considered here, our generic theory of conformance-based cleanness allows for using other conformance notions as appropriate for the CPS under test.

Conclusions

In this paper, we presented a theory of doping detection and cleanness based on the notions of conformance for cyber-physical systems. Our new notion accounts for possible "deviations" of the system output, upon "perturbing" its inputs, both in time and in values. Both notions of "deviation" and "perturbation" turn out to be expressible using a generic notion of retiming. We instantiate our definition with specific notions of retiming from the conformance testing literature. We apply our notions to a case study from the automotive domain and demonstrate how our generalised notions are useful in using actual driving cycles for doping detection according to the New European Driving Cycle (NEDC) [START_REF]UN Vehicle Regulations -1958 Agreement[END_REF].

We intend to turn our theory into an automatic tool for doping detection, using hybrid systems models. We intend to use the HyConf tool [START_REF] Araujo | Sound conformance testing for cyber-physical systems: Theory and implementation[END_REF] as the starting point and use our search-based testing implementation in HyConf [START_REF] Araujo | Multi-objective Search for Effective Testing of Cyber-Physical Systems[END_REF] to automate the process of test-case generation and test-case selection. Once this process is automated, one can generate test-cases that can go beyond a specific standard and detect intelligent defeat devices that cheat the standards and the tests prescribed by them.

We also intend to organise widespread experiments regarding emission detection to put our theory into practice. Our experimental set-up involves instrumenting a large number of cars using low-cost equipments, constructing models of emission behaviour, and generating realistic driving scenarios that are more likely to detect doping.

Fig. 1 .

 1 Fig. 1. Running Example: Specified (a) and Actual (b) Test Cycles and Emission Footprints obtained from Different (Fictitious) Vehicles (c) and (d).

Fig. 1 .

 1 Fig.1.(c) provide significant evidence for doping -a slightly different test cycle has resulted in significantly larger footprint. However, due to the time shift on the input side Fig.1.(b) the point-wise difference of the two driven test-cycles has grown very large. As we show in the remainder of this paper, the existing theory of doping fails to detect such a clear evidence, due to the minor delay during the execution of the driving cycle. The emission footprint in Fig.1.(d) is another (synthetic) example of a significant deviation which cannot be detected for the input in Fig.1.(b) using existing theories; this latter footprint sheds some light on the intricate design decisions in the theory we develop in this paper.

Definition 1 .

 1 Let (Y, d Y ) be a metric space. A Y-valued generalised timed trace (GTT) is a function µ : T → Y such that T ⊆ R ≥0 . We call T the time domain of µ, denoted dom(µ). GTT (Y) is the set of all Y-valued generalised timed traces.

Fig. 1 .

 1 (a) i st and i dev are trace conformant with value threshold , as they only exhibit point-wise deviations by values less than . In contrast, i st and i ddev in Fig.1.(b) are not trace conformant, yet they are hybrid conformant with time and value margins τ and , respectively. The key difference is that the inputs depicted in Fig.1.(b) are very different if compared point-wise, but if one allows for retiming, they are close enough in value after retiming.

Corollary 1 .Corollary 2 . 1 .Example 6 .

 1216 For all τ I , τ O , I , O ∈ R ≥0 , the following implications hold: 1. RobustClean( I , O ) =⇒ SkorClean(0, I , τO, O ) =⇒ HybridClean(0, I , τO, O ), 2. HybridClean(τI , I , 0, O ) =⇒ SkorClean(τI , I , 0, O ) =⇒ RobustClean( I , O ). Also, RobustClean( I , O ) = SkorClean(0, I , 0, O ) = HybridClean(0, I , 0, O ) and hence SkorClean and HybridClean are conservative extensions of robust cleanness. For all I , I , O , O , τ I , τ I , τ O , τ O that satisfy the inequalities I ≤ I , τ I ≤ τ I , O ≥ O , τ O ≥ τ O the following implications hold: RobustClean( I , O ) =⇒ RobustClean( I , O ); 2. HybridClean( I , τ I , O , τ O ) =⇒ HybridClean( I , τ I , O , τ O ); 3. SkorClean( I , τ I , O , τ O ) =⇒ SkorClean( I , τ I , O , τ O ). Consider the testing workflow in Fig. 1. The inputs passed to a car are i st and i ddev , depicted in Fig. 1.(b

Fig. 2 .

 2 Fig. 2. Left: New European Driving Cycle (NEDC); Right: Test Setup with Nissan NV200 Evalia on a chassis dynamometer attached to a PEMS.

Fig. 3 .

 3 Fig. 3. Initial 200s of PowerNEDC (left) and SineNEDC (right) planned test cycles (red, dotted) and actually driven (black).

10 I

 10 = κ I I = κ I +2 Power I = 15.88 I = 15.03 I = 12.41 I = 10.10 I = 10.07 I = 10.07 τI = 67.35 τI = 10.8 Sine I = 16.17 I = 15.46 I = 14.24 I = 12.91 I = 11.67 I = 11.37 τI = 72.4 τI = 4.05

  ). One of the test results is presented in Fig.1.(c), where i st reveals output o(i st ) and i ddev reveals o(i ddev ). We assume that < |i st (t 0 ) -i ddev (t 0 )| and < |o(i st )(t 1 ) -o(i ddev )(t 1 )| at some time t 1 .-For inputs i st and i ddev , any output is immediately deemed RobustClean( , ), as the left-hand side of the implication in Def. 8 does not hold for any t . Note, that for other inputs the car used for testing might not be RobustClean( , ). -As explained in Example 2, i st and i ddev are hybrid conformant for and τ , i.e., the predicate PrefConf I on the left-hand side of the implication in Def. 8 holds. PrefConf O , however, fails at time t 1 for signals o(i st ) and o(i ddev ).

Table 1 .

 1 Value thresholds for fixed τI (left) and time thresholds for fixed I (right). Values are given as mg/km and time in seconds.

This work is partly supported by the ERC Grant 695614 (POWVER) by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) grant 389792660 as part of TRR 248, see https://perspicuous-computing.science, by the Saarbrücken Graduate School of Computer Science, and by the Sino-German CDZ project 1023 (CAP).


Christian Bartolo Burlò
email: christian.bartolo.16@um.edu.mt

Adrian Francalanza
email: adrian.francalanza@um.edu.mt

Alceste Scalas
email: a.scalas@aston.ac.uk

Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)

Keywords: Session types, Static and dynamic verification, Monitors

We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).

Introduction

Session Types [START_REF] Takeuchi | An interaction-based language and its typing system[END_REF][START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] have emerged as a central formalism for the verification of concurrent and distributed programs. Session-types-based analysis ensures that a program correctly implements some predetermined communication protocol, stipulating the desired exchange of messages [16,[START_REF] Ancona | Behavioral types in programming languages[END_REF]. The analysis is typically performed statically, via type checking, before the programs are deployed. However, full static analysis is not always possible (e.g., when the source code of third-party programs and components is unavailable); in such cases, session types are checked at runtime via monitors [START_REF] Demangeon | Practical interruptible conversations: distributed dynamic verification with multiparty session types and python[END_REF][START_REF] Jia | Monitors and blame assignment for higher-order session types[END_REF]6,[START_REF] Neykova | Let it recover: multiparty protocol-induced recovery[END_REF]. We view these approaches as two extremes on a continuum: our aim is to develop practical hybrid (static and dynamic) verification methodologies and tools for distributed programs in open settings. In particular, our aim is to verify distributed systems where: (i) we make no assumptions on how messages are delivered between components; (ii) the components available prior-deployment are checked statically; and (iii) the components that are unavailable for checking prior-deployment are verified at runtime, by deploying autogenerated, type-checked monitors. To achieve this aim, we present a methodology with three key features, presented as contributions in this paper: F1. Open systems are prone to malicious attacks and data corruption. Thus, we describe protocols via augmented session types including runtime data assertions (reminiscent of interaction refinements [START_REF] Neykova | A session type provider: Compiletime api generation of distributed protocols with refinements in f#[END_REF]), and synthesise monitors that automate such data checks. Unlike [START_REF] Neykova | A session type provider: Compiletime api generation of distributed protocols with refinements in f#[END_REF]6], our monitors are independent, type-checked processes, that can be deployed over any network. F2. We develop a tool that, given a session type S, can synthesise the Scala code of (1) a type-checked monitor that verifies at run-time whether an interaction abides by S (aim (iii)), and (2) the signatures usable to implement a process that interacts according to S, in a correct-by-construction manner (aim (ii)). F3. Our monitor synthesis can abstract over low-level communication protocols, bridging across a variety of message transports (e.g., TCP/IP, REST, etc.): this is key to facilitate the interaction with third-party (untyped) components in open systems (aim (i)); this is also unlike previous work on session monitoring (theoretical [6] or practical [START_REF] Neykova | Let it recover: multiparty protocol-induced recovery[END_REF]) that focus on a specific technology and runtime system, or assume a centralised message routing medium.

Binary Sessions with Assertions

A session type defines the intended behaviour of a participant that communicates with another over a channel. Our work is based on session types with assertions:

Assertions A ::= v 1 == v 2 | v 1 >= v 2 | A 1 && A 2 | !A | . . . Base types B ::= Int | Str | Boolean | . . . Session types R, S ::= & i∈I ?l i (V i : B i )[A i ].S i | ⊕ i∈I !l i (V i : B i )[A i ].S i | rec X.S | X | end (with I = ∅, li pairwise distinct)
We assume a set of base types B, and introduce payload identifiers V (with their types) and assertions A (i.e., predicates on payload values). Branching (or external choice) & i∈I ?l i (V i : B i )[A i ].S i requires the participant to receive one message of the form l i (v i ), where v i is of (base) type B i for some i ∈ I; the value v i (i.e., the message payload) is bound to the variable V i in the continuation. If the assertion A i [ vi /Vi] holds, the participant must proceed according to the continuation type S i [ vi /Vi], but if the assertion fails, a violation is raised. Selection (or internal choice)

⊕ i∈I !l i (V i : B i )[A i ]
.S i requires the participant to choose and send one message l i (v i ) where v i is of (base) type B i for some i ∈ I; a violation is raised if the assertion A i [ vi /Vi] does not hold, otherwise the protocol proceeds as S i [ vi /Vi]. The recursive session type rec X.S binds the recursion variable X in S (we assume guarded recursion), while end is the terminated session. For brevity, we often omit ⊕ and & for singleton choices, end, and trivial assertions (i.e., true). A process implementing a session type S can correctly interact with a process implementing the dual type of S, denoted S -where each selection (resp. branching) of S is a branching (resp. selection), with the same choices:

& i∈I ?l i (V i : B i )[A i ].S i = ⊕ i∈I !l i (V i : B i )[A i ].S i end = end X = X ⊕ i∈I !l i (V i : B i )[A i ].S i = & i∈I ?l i (V i : B i )[A i ].S i rec X.S = rec X.S Example 1.
The type S login below describes the protocol of a server handling authorised logins. Notice that the type uses two assertion predicates:

-validAuth() checks if an OAuth2-style token [START_REF]RFC 6749: OAuth 2.0 framework[END_REF] authorises a given user; -validId() checks whether an authentication id is correct for a given user. The server waits to receive Login(uname:Str, pwd :Str, tok :Str), where tok is a token obtained by the client from an authorisation service. Once received, the values of uname and tok are passed to the the predicate validAuth() which checks whether tok contains a desired cryptographically-signed authorisation for uname: if it evaluates to true, the server can either send Success including an id , or Retry. If the server chooses the former, then id and uname must be validated by validId (): if it succeeds, the message is sent and the server continues along session type R. If the server chooses to send Retry, the session loops.

Design and Implementation

We now give an overview ( §3.2) and an example-driven tour ( §3.3) of our methodology; but first, we summarise the toolkit underlying its implementation ( §3.1).

3.1 Background: Session Programming with lchannels lchannels [START_REF] Scalas | Lightweight session programming in scala[END_REF][START_REF] Scalas | Lightweight session programming in scala (artifact)[END_REF][START_REF] Scalas | lchannels[END_REF] is a library implementation of session types in the Scala programming language. Its API is inspired by the continuation-passing encoding of session types into the linear π-calculus [START_REF] Dardha | Session types revisited[END_REF]. (2) the library provides run-time linearity enforcement: e.g., if a "one-shot" channel object is used twice to send messages, then the program is not advancing along S, hence lchannels discards the message and raises an error.

lchannels

Hybrid Verification via Static and Dynamic Checking

Srv C

S login

We now illustrate how our methodology is implemented, as a tool [START_REF] Burlò | STMonitor implementation[END_REF] targeting the Scala programming language. Consider the scenario on the right: a client C exchanges messages with a server Srv over a network. Srv implements the session type S login outlined in Example 1, and expects each client C to follow the dual, S login . However, in an open system, we cannot guarantee that C abides by S login . The messages sent from Srv to C (and vice versa) must pass through the monitor Mon. As Srv and Mon use lchannels to interact, they are statically typed according to S login and S login ; instead, there is no assumption on the interaction between Mon and C: it is handled by a user-supplied connection manager (CM), which acts as a translator and gatekeeper by transforming messages from the transport protocol supported by C to the Mon's CPSP classes, and vice versa. Hence, CM provides a message transport abstraction for Mon and Srv: to support new clients and message transports, only CM needs extending.

Srv

When the monitor is initialised, it invokes CM to set up the communication channel with client C, through a suitable message transport: e.g., in the case of TCP/IP, CM creates a socket and initialises the I/O buffers. Each message sent from Srv to Mon via lchannels is analysed by Mon, and if it conforms to S login and its assertions, it is translated by CM and forwarded to C. Dually, each message sent from C to Mon is translated by CM and analysed by Mon, and if it conforms to S login and its assertions, it is forwarded to Srv. Mon's assertion checks provide additional verification against incorrect values from Srv or C.

A Step-by-step Example

To illustrate our approach and implementation, we now follow the message exchanges prescribed by S login , showing how they engage with the elements of our design. Roughly, Mon acts as a state machine: it transitions by receiving and forwarding messages between Srv and CM, abiding by the type S login and its dual. CM, in turn, provides a send/receive interface to Mon, and delivers messages to/from client C. The monitor also maintains a mapping, called payloads, that associates the payload identifiers of S login to their current values. We begin with the login request sent from a client over TCP/IP. The client's message is initially handled by the connection manager CM, which provides a receive method like the one shown above: it is invoked by Mon to retrieve messages. When invoked, receive checks the socket input buffer inBuf: if a new supported message is found (line 3, where the message matches the regex loginR), the corresponding CPSP class is returned to the monitor; otherwise, the unaltered message is returned (line 4). On the left is the synthesised code of Mon that handles the server's response to the client. According to S login , the server can choose to send either Success or Retry; correspondingly, the monitor waits to receive either of the options from Srv, using the function ? from lchannels (line 2).

-If the server sends Success, including the value id as specified in S login , the first case is selected (line 3). The monitor evaluates the assertion on id and uname (stored in receiveLogin above, and now retrieved from the payloads mapping): if it is satisfied, the message is sent to the client (line 5) via CM's send method (explained below), and the monitor continues according to session type R. Otherwise, the monitor logs a violation and halts (line 8). -Instead, if the server sends Retry (line 10), the message is forwarded directly to the client using the method send of the CM (see below); notice that there are no dynamic checks at this point, as there is no assertion after Retry in S login . The monitor then goes back to the previous state receiveLogin.

Notably, unlike the synthesised code of receiveLogin (that handles the previous external choice), there is no catch-all case for unexpected messages from Srv. In fact, here we assume that Srv is written in Scala and lchannels, hence statically checked, and conforming to S login ; hence, it can only send one of the expected messages (as per §3.1). The monitor only checks the assertions on Srv's messages. Finally, we review the send method of CM: it translates messages from a CPSP class instance to the format accepted by the client's transport protocol. In this case, the format is a textual representation of the session type. The catch-all case (lines 4-5) is for debugging purposes.

Conclusion

We presented our preliminary work on the hybrid verification of open distributed systems, based on session types with assertions and automatically syntehsised monitors -with a supporting tool [START_REF] Burlò | STMonitor implementation[END_REF] based on the Scala programming language. Future work. Our approach adheres to the "fail-fast" design methodology: if an assertion fails, the monitor logs the violation and halts. In the practice of distributed systems, "fail-fast" is advocated as an alternative to defensive programming [START_REF] Cesarini | ERLANG Programming[END_REF]; it is also in line with existing literature on runtime verification [START_REF] Bartocci | Introduction to runtime verification[END_REF]. Our further rationale for this design choice is that we intend to investigate monitorability properties of session types, along the lines of recent work [START_REF] Francalanza | Monitorability for the hennessymilner logic with recursion[END_REF][START_REF] Aceto | Adventures in monitorability: from branching to linear time and back again[END_REF][START_REF] Aceto | An operational guide to monitorability[END_REF], and identify any limits, in terms of what can be verified at runtime. We plan to extend our approach to multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF], in connection to existing work [START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF][START_REF] Scalas | A linear decomposition of multiparty sessions for safe distributed programming (artifact)[END_REF] based on lchannels and Scribble [START_REF]Scribble homepage[END_REF][START_REF] Yoshida | The Scribble protocol language[END_REF]. Finally, we plan to investigate how to handle assertion violations by adding compensations to our session types, formalising how the protocol should proceed whenever an assertion fails. Related Work. The work in [6] formalises a theory of monitored (multiparty) session types, based on a global, centralised router providing a safe transport network that dispatches messages between participant processes. The main commonality with our work is that session types are used to synthesise monitors. The main differences (besides our focus on a tool implementation) are that (1) we do not assume a centralised message routing system, and consider the network adversarial (as per contribution F1) and use monitors to also protect typed participants; (2) our monitors can enforce data constraints, through assertions; and

(3) in our setting, if a participant sends an invalid message, the monitor will flag violations (and stop computation) whereas [6] drops the invalid message, but will continue forwarding the rest, akin to runtime enforcement via suppressions [3]. Our protocol assertions are reminiscent of interaction refinements in [START_REF] Neykova | A session type provider: Compiletime api generation of distributed protocols with refinements in f#[END_REF], that are also statically generated (by an F# type provider), and dynamically enforced when messages are sent/received. However, we enforce our assertions by synthesising well-typed monitoring processes that can be deployed over a network, whereas [START_REF] Neykova | A session type provider: Compiletime api generation of distributed protocols with refinements in f#[END_REF] injects dynamic checks in the local executable of a process.

S

  login = rec X.?Login(uname:Str, pwd :Str, tok:Str)[validAuth(uname, tok )]. ⊕ !Success(id :Str)[validId (id , uname)].R , !Retry().X

lchannels

  Our approach is outlined on the left. The accessible participant Srv is statically checked, and the behaviour of the inaccessible participant C is dynamically monitored at runtime. Given S login , the synthesiser Synth generates (1) the Continuation-Passing-Style Protocol classes (CPSPc) for representing S login in Scala and lchannels (see §3.1), and (2) the source code of a runtime monitor (Mon), based on the CPSPc above. Below are the CPSPc generated from S login by our synthesiser: notably, they can be used to write a type-checked version of Srv.

1

  case class Login(uname: String, pwd: String, tok: String)(val cont: Out[Choice1]) 2 sealed abstract class Choice1 3 case class Success(id: String)(val cont: Out[R]) extends Choice1 4 case class Retry()(val cont: Out[Choice1]) extends Choice1 5 case class R(...) // This is the continuation of the session (omitted)

1 4 case other => other 5 }

 45 val loginR = """LOGIN (.+) (.+) (.+)""".r 2 def receive(): Any = inBuf.readLine() match { 3 case loginR(uname, pwd, tok) => Login(uname, pwd, tok)(null)

1

  def receiveLogin(srv: Out[Login], client: ConnManager): Unit = { 2 client.receive() match { 3 case msg @ Login(_, _, _) => 4 if (validateAuth(msg.uname, msg.tok)) { 5 val cont = srv !! Login(msg.uname, msg.pwd, msg.tok)_ 6 payloads.Login.uname = msg.uname receiveLogin(msg.cont, Client) 13 } }

1 2 case

 2 def send(msg: Any): Unit = msg match { Success(id) => outB.write(f"SUCCESS ${id}\n") 3 case Retry() => outB.write(f"RETRY\n")4 case _ => { close();5 throw new Exception("Invalid message") } 6 }

The research was partly supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No 778233.

On the left is the synthesised code for Mon that handles the beginning of S login . The monitor invokes CM's method receive (shown above) to retrieve the latest message (line 2). Depending on the type of message, the monitor will perform a series of actions. By default, a catch-all case (line 9) handles any messages violating the protocol. If Login is received, the monitor initially invokes the function validateAuth() with the values of uname and tok; i.e., the assertion predicate in S login corresponds to a Scala function (imported from a user-supplied library). If the function returns true, the message is forwarded to the server Srv (line 5), otherwise the monitor logs the violation and halts. The function used to forward the message (!!), which is part of lchannels, returns a continuation channel that is stored in cont. The value of uname is stored in a mapping (line 6) since it is used later on in S login . Finally, the monitor moves to the next state, by calling the synthesised method sendChoice1, passing cont to continue the protocol.