Introduction

Contact tracing protocols, e.g., smartphone apps, are aimed at investigating who could have been contaminated by a positively diagnosed person and alert them, see e.g. [1]. After the COVID-19 pandemic, several protocols have been proposed as an automated support for this task su as PEPP-PT, DP3T, ROBERT4 and NTK5. In general the system architecture is based on a smart app, a notification server as in Publish/Subscribe architectures, and a possibly trusted server. In order to reduce the risk of a malicious use of user data (see e.g. the attacks described in [2,1]), the protocols are based on frequent rotations of identifiers emitted via bluetooth. In centralized versions of the protocol ephemeral identifiers are downloaded from a trusted server. In decentralized versions ephemeral identifiers are generated by user apps. The user app installed on the user device (e.g. Immuni in Italy) broadcasts the currently valid ephemeral identifier. The same user app also collects all identifiers emitted in the same bluetooth range and stores them locally. When users are diagnosed to be infected, they release a report to the server. One possible implementation consists in sending the report to a central log database. Users can then consult the database to check if they crossed their way with infected users, i.e., they share some ephemeral identifier with one of them.

Based on a preliminary study present at Overlay 2020 [3], in this paper we present an automatabased formal model of distributed systems specifically devised to formalise abstractions of Contact Tracing Protocols that combine Bluetooth and network communication. The model combines pure names, read/write operations on first-order and higher-order variables and synchronous communication primitives. The transition system models the interaction between devices in the same physical location and between a single device and a notification server. Violations of safety properties for this kind of protocols typically require universally quantified conditions on global configurations (e.g. one user detects a contact while no user is positive).

To automatically validate protocols in our formalism, we resort to an extension of the Cubicle SMT-based infinite-state model checker. Cubicle is a model checker that can be applied to verify safety properties of array-based systems, a syntactically restricted class of parameterized transition systems with states represented as arrays indexed by an arbitrary number of processes [4,5]. Cubicle integrates the SMT solver Alt-Ergo [6]. Cubicle input language is a typed version of Mur𝜑 [7]. A system is describe in Cubicle by: a set of type, variable, and array declarations; a formula for the initial states; and a set of transitions. A system execution is defined by an infinite loop that at each iteration non-deterministically chooses a transition instance whose guard is true in the current state; and updates state variables according to the action of the fired transition instance.

To validate instances of our model, we will exhibit a general encoding in the Cubicle arraybased language and propose to refine the overapproximation of universally quantified preconditions applied in the Cubicle backward procedure by introducing abstract predicates obtained via Counting Abstraction.

Contact Tracing Systems

In this section we introduce a possible general formal model for contact tracing protocol. To specify the protocol rules and behavior (computation), we will use a transition system defined on configurations consisting of a set of states of individual users. User configurations contain a local memory needed to store the list of emitted and received identifiers. System configurations contain a global memory that can be used to gather and a set of user states that corresponds to the current number of registered indivuals.

We will use the following general definitions: ℐ is a denumerable set of pure names (identifiers) containing the undefined label ⊥; 𝑀 is a finite set of message labels (𝑎, 𝑏, 𝑐, . . . ); 𝑉 is a finite set of first order variables (identifiers) that are part of the local state of users (𝑥, 𝑦, . . . ); 𝑆 is a finite set of second order variables (set of identifiers) that are part of the local state of users (𝑠, 𝑡, . . . ). We then define Act(𝑀, 𝑉, 𝑆) the set of actions defined as follows: 𝑒𝑞(𝑥, 𝑦) and 𝑛𝑜𝑡𝑒𝑞(𝑥, 𝑦), where 𝑥, 𝑦 ∈ 𝑉 , 𝑖𝑛(𝑥, 𝑚) and 𝑛𝑜𝑡𝑖𝑛(𝑥, 𝑚), where 𝑥 ∈ 𝑉 and 𝑚 ∈ 𝑀 (Conditions); 𝑙𝑜𝑐𝑎𝑙, 𝑛𝑒𝑤(𝑥), where 𝑥 ∈ 𝑉 , 𝑏𝑐𝑎𝑠𝑡(𝑚, 𝑥) and 𝑟𝑒𝑐(𝑚, 𝑥), where 𝑚 ∈ 𝑀, 𝑥 ∈ 𝑉 ; 𝑎𝑑𝑑(𝑥, 𝑠), where 𝑥 ∈ 𝑉, 𝑠 ∈ 𝑆, 𝑟𝑒𝑠𝑒𝑡(𝑠), where 𝑠 ∈ 𝑆, 𝑟𝑒𝑔(𝑚, 𝑠), where 𝑚 ∈ 𝑀, 𝑠 ∈ 𝑆 (Operations).

A protocol is defined as a Data Automaton 𝑃 = ⟨𝑄, 𝑀, 𝑉, 𝑆, 𝑅, 𝑞 0 ⟩, where 𝑞 0 ∈ 𝑄 and 𝑅 ⊆ 𝑄 × Act(𝑀, 𝑆, 𝑉 ) × 𝑄. We assume here that 𝑏𝑐𝑎𝑠𝑡 and 𝑟𝑒𝑔 actions are always defined on distinct labels in 𝑀 . Consider a protocol 𝑃 = ⟨𝑄, 𝑀, 𝑉, 𝑆, 𝑅, 𝑞 0 ⟩. A process configuration of 𝑃 is a triple 𝑝𝑐 = ⟨𝑞, 𝛿, 𝛾⟩ where: 𝑞 ∈ 𝑄 is the current user state; 𝛿 : 𝑉 → ℐ is the current evaluation of first order variables; 𝛾 : 𝑆 → 𝒫(ℐ) is the current evaluation of second order variables. We denote by 𝒫𝒞 the set of process configurations. A global configuration of 𝑃 is then a pair (𝐾, Θ), where 𝐾 ∈ N 𝒫𝒞 is a finite multiset of process configurations and Θ : 𝑀 ↦ → 𝒫(ℐ) corresponds to a centralized memory. 𝒢𝒞 denotes the set of global configurations. For 𝜎 ∈ 𝒢𝒞, we will use 𝑖𝑑𝑠(𝜎) to denote the set of pure names occurring in 𝜎. The operational semantics is then defined as the minimal relation →⊆ 𝒢 × 𝒢 that satisfies the following property definitions in which will use ⊎ to denote multiset union:

-𝜎 = ⟨{⟨𝑞, 𝛿, 𝛾⟩} ⊎ 𝐾, Θ⟩ → ⟨{⟨𝑞 ′ , 𝛿, 𝛾⟩} ⊎ 𝐾, Θ⟩ if one of the following conditions is satisfied: ⟨𝑞, 𝑙𝑜𝑐𝑎𝑙, 𝑞 ′ ⟩ ∈ 𝑅, ⟨𝑞, 𝑒𝑞(𝑥, 𝑦), 𝑞 ′ ⟩ ∈ 𝑅 and 𝛿(𝑥) = 𝛿(𝑦) [for 𝑛𝑜𝑡𝑒𝑞(𝑥, 𝑦),𝛿(𝑥) ̸ = 𝛿(𝑦)], ⟨𝑞, 𝑖𝑛(𝑥, 𝑚), 𝑞 ′ ⟩ ∈ 𝑅 and 𝛿(𝑥 For the resulting model, we are interested in safety properties for parameterized version of a protocol instance. More specifically, given a protocol definition 𝑃 and a given process state 𝑞 𝑒 ∈ 𝑄 that denotes an error state, we would like to verify that global configurations that contain occurrences of 𝑞 𝑒 are unreachable starting from any possibile initial configuration (i.e. independently from the number of process instances). A similar property can be formulated by adding an error flags to the server state instead of selecting a special error state in 𝑄. We are also interested in properties expressed by violations in which global configurations contain a process in state 𝑞 𝑒 while all other processes are in states contained in These properties are referred to as control state reachability and constrained control state reachabiliy, respectively. Violations of this kind of properties can be defined using quantified assertions, such as there exists a process 𝑖 in control state 𝑞 𝑒 and, for constrained properties, universally quantified conditions on the control states of other processes. In the rest of the paper we will illustrate how to encode our formalism in Cubicle and how to verify control state reachability problems using the corresponding symbolic exploration procedure provided by the tool.

) ∈ Θ(𝑚) [for 𝑛𝑜𝑡𝑖𝑛(𝑥, 𝑦) 𝛿(𝑥) ̸ ∈ Θ(𝑚)]. -𝜎 = ⟨{⟨𝑞, 𝛿, 𝛾⟩} ⊎ 𝐾, Θ⟩ → ⟨{⟨𝑞 ′ , 𝛿 ′ , 𝛾⟩} ⊎ 𝐾, Θ⟩ if ⟨𝑞, 𝑛𝑒𝑤(𝑥), 𝑞 ′ ⟩ ∈ 𝑅 and 𝛿 ′ (𝑥) = 𝑖𝑑 ̸ ∈ 𝑖𝑑𝑠(𝜎), 𝑖𝑑 ̸ = ⊥, and 𝛿 ′ (𝑦) = 𝛿(𝑦) for 𝑥 ̸ = 𝑦. -𝜎 = ⟨{⟨𝑞, 𝛿, 𝛾⟩} ⊎ 𝐾, Θ⟩ → ⟨{⟨𝑞 ′ , 𝛿, 𝛾 ′ ⟩} ⊎ 𝐾, Θ⟩ if ⟨𝑞, 𝑎𝑑𝑑(𝑥, 𝑠), 𝑞 ′ ⟩ ∈ 𝑅 and 𝛾 ′ (𝑠) = 𝛾(𝑠) ∪ {𝛿(𝑥)} and 𝛾 ′ (𝑡) = 𝛾(𝑡) for 𝑡 ̸ = 𝑠. -𝜎 = ⟨{⟨𝑞, 𝛿, 𝛾⟩} ⊎ 𝐾, Θ⟩ → ⟨{⟨𝑞 ′ , 𝛿, 𝛾 ′ ⟩} ⊎ 𝐾, Θ⟩ if ⟨𝑞, 𝑟𝑒𝑠𝑒𝑡(𝑠), 𝑞 ′ ⟩ ∈ 𝑅 and 𝛾 ′ (𝑠) = ∅ and 𝛾 ′ (𝑡) = 𝛾(𝑡) for 𝑡 ̸ = 𝑠. -𝜎 = ⟨{⟨𝑞, 𝛿, 𝛾⟩} ⊎ 𝐾, Θ⟩ → ⟨{⟨𝑞 ′ , 𝛿, 𝛾⟩} ⊎ 𝐾, Θ ′ ⟩ if ⟨𝑞, 𝑟𝑒𝑔(𝑚, 𝑠), 𝑞 ′ ⟩ ∈ 𝑅 and Θ ′ (𝑚) = Θ(𝑚) ∪ 𝛾(𝑠) and Θ ′ (𝑛) = Θ(𝑛) for 𝑛 ̸ = 𝑚. -𝜎 = ⟨{⟨𝑞, 𝛿, 𝛾⟩, ⟨𝑞 1 , 𝛿 1 , 𝛾 1 ⟩, . . . , ⟨𝑞 𝑘 , 𝛿 𝑘 , 𝛾⟩ 𝑘 } ⊎ 𝐾, Θ⟩ → ⟨𝐾 ′ , Θ⟩ where 𝐾 ′ = {⟨𝑞 ′ , 𝛿, 𝛾⟩, ⟨𝑞 ′ 1 , 𝛿 ′ 1 , 𝛾

Case Studies: Contact Tracing Protocols

We present below a formal specifications of the protocol scheme of Contact Tracing applications abstracting away identifier creation, i.e., assuming that user app generate fresh identifiers, and reasoning within the validity epoch of identifiers, i.e., those maintained in local memory. The system is composed of a finite but arbitrary number of user apps and of a server modeled via a centralized memory. Each user apps has local variables 𝑉 = {𝑥, 𝑦, 𝑧} and 𝑆 = {𝑖𝑛, 𝑜𝑢𝑡}. Furthermore, 𝑀 = {𝑏, 𝑚} where 𝑏 denotes beacon messages broadcasted by user apps, and 𝑚 denotes report messages sent to the centralized memory. The user app starts their part of protocol in state 𝑞 0 and operate in three different modes.

In emitter mode the app generates and emits fresh beacons: ⟨𝑞 0 , 𝑛𝑒𝑤(𝑥), 𝑞 1 ⟩, the user app generates a fresh identifier and stores it in the local variable 𝑥; ⟨𝑞 1 , 𝑎𝑑𝑑(𝑥, 𝑜𝑢𝑡), 𝑞 2 ⟩, in 𝑞 1 the fresh identifier stored in 𝑥 is added to the local memory 𝑜𝑢𝑡; ⟨𝑞 2 , 𝑏𝑐𝑎𝑠𝑡(𝑏, 𝑥), 𝑞 2 ⟩, ⟨𝑞 2 , 𝑙𝑜𝑐𝑎𝑙, 𝑞 0 ⟩, in 𝑞 2 the user app either emits the message (𝑏, 𝑥) or returns to the initial state in order to apply a rotation scheme for the beacon identifiers or perform other steps. In reception mode the app, while in any state 𝑙 0 ∈ 𝑄 ∖ {𝑟 1 , 𝑠 2 }, receives a beacon, stores it in the local memory 𝑖𝑛, and then returns to the current state: ⟨𝑙 0 , 𝑟𝑒𝑐(𝑏, 𝑦), 𝑙 1 ⟩ in state 𝑙 0 the user is always ready to receive beacons; ⟨𝑙 1 , 𝑎𝑑𝑑(𝑦, 𝑖𝑛), 𝑙 0 ⟩, in state 𝑙 1 the beacon is stored in the local memory 𝑖𝑛. In report mode, enabled only in state 𝑟 0 = 𝑞 0 , the app sends its local memory 𝑜𝑢𝑡 to the server and moves to the halt state 𝑟 1 : ⟨𝑞 0 , 𝑠𝑒𝑛𝑑(𝑚, 𝑜𝑢𝑡), 𝑟 1 ⟩. In query mode, enabled only in state 𝑠 0 = 𝑞 0 , the user app selects a beacon 𝑧 from the local memory 𝑖𝑛, i.e., ⟨𝑠 0 , 𝑠𝑒𝑙(𝑖𝑛, 𝑧), 𝑠 1 ⟩, sends it to the server to check whether it has been reported by another app or not. In the former case it moves to the halting state 𝑠 2 , i.e, ⟨𝑠 1 , 𝑖𝑛(𝑚, 𝑥), 𝑠 2 ⟩. In the latter case it returns to state 𝑠 0 , i.e, ⟨𝑠 1 , 𝑛𝑜𝑡𝑖𝑛(𝑚, 𝑥), 𝑠 0 ⟩.

From Data Automata to Cubicle

Let us now discuss how to model a protocol definition 𝑃 = ⟨𝑄, 𝑀, 𝑉, 𝑆, 𝑅, 𝑞 0 ⟩ in Cubicle. A global configuration is a pair (𝐾, Θ), where 𝐾 is a finite multiset of process configurations and Θ corresponds to a centralized memory. The encoding if Θ is quite immediate since we can represent the global memory as a finite set of unbounded arrays 𝐴 𝑚 1 , . . . , 𝐴 𝑚𝑛 with cells of Boolean type one for each 𝑚 𝑖 ∈ 𝑀 . The array 𝐴 𝑚 is such that 𝐴 𝑚 [𝑥] = 𝑇 𝑟𝑢𝑒 if and only if 𝑥 ∈ Θ(𝑚) for each pair 𝑥, 𝑚. For the encoding of 𝐾 we can proceed in several different ways. Remember that a process configuration is a triple 𝑝𝑐 = ⟨𝑞, 𝛿, 𝛾⟩, in which 𝑞 ∈ 𝑄 but is the current user state, 𝛿 is the current evaluation of first order variables; and 𝛾 is the current evaluation of second order variables. One possible encoding is defined as follows: To represent control states, we introduce an unbounded array 𝑠𝑡𝑎𝑡𝑒 that associates an enumerative type associated to 𝑄 to represent the current state of each process, i.e., 𝑠𝑡𝑎𝑡𝑒[𝑖] = 𝑞 if process 𝑖 is in state 𝑞. To represent the current state of a first order variable 𝑣 we can introduce an unbounded array 𝑣𝑎𝑙 𝑣 such that 𝑣𝑎𝑙 𝑣 [𝑖] = 𝑑 if 𝛿(𝑣) = 𝑑 holds in 𝑝𝑐 𝑖 (in process 𝑖). To represent the current state of a second order variable 𝑠 we can introduce an unbounded bidimensional array 𝑣𝑎𝑙 𝑠 such that 𝑣𝑎𝑙 𝑠 [𝑖, 𝑑] = 𝑇 𝑟𝑢𝑒 if and only if 𝑑 ∈ 𝛾(𝑠) holds in 𝑝𝑐 𝑖 (in process 𝑖). Transition rules can then be expressed via Cubicle transition rules. In particular, to model send operation involving second order variables, we can use global operations on arrays, in which all cells of an arrays are copied into another one (whole-place operations in Petri net languages).

The Cubicle verification engine is based on symbolic backward exploration. Cubicle operates over sets of existentially quantified formulas called cubes. Formulas containing universally quantified formulas (generated during the computation of predecessors) are over-approximated by existentially quantified formulas. In other words Cubicle applies monotone abstraction [8] and over-approximates predecessors via upward-closed sets of configurations. Infinite sets of unsafe states (bad configurations) are symbolically defined by using 𝑢𝑛𝑠𝑎𝑓 𝑒 constraints in which all variables are implicitly existentially quantified. In our case studies we are interested in checking the consistency between local and global information. More specifically, when user 𝑈 queries the server, she/he supposed to receive a notification only in presence of at least one positive user who emitted a beacon that has been received by 𝑈 . The server does not maintain any association between identities and beacons collected in the log. Consistency of global and local states combined with the privacy preservation property of the protocol can be tested by adding an Error state and a special rule in which we only compare local states of different users. Namely, the rule generates an error whenever there exist a user 𝑈 in the Contact state without any positive user in the global system. If this happens the protocol does not trace physical contacts in correct way. To validate the considered properties, we define the following assertion that specifies bad configurations in the sense of control state reachability, unsafe () { Error = True } i.e., configurations of any size in which Error is True. Due to the presence of universally quantified conditions both in the protocol rule and in the precondition of the error rule, there is no termination guarantee on the execution of the verification task in Cubicle. Furthermore, when terminating the tool may return spurious traces as in our case study. Indeed , Cubicle, after visiting 41 cubes, detects a spurious trace of the form: start(#3, #2) -> in(#1, #2) -> end(#1, #2) -> report(#3) -> query(#1, #2) -> bad(#1) -> unsafe.

The imprecision here is due to the over-approximation introduced via monotone abstraction. Preconditions with universally quantified guards are transformed into post-conditions, and thus they are not propagated through different steps of predecessor computations. Since in the correctness property of the protocol local states are put in relation via hidden data (not explicitly mentioned in control states) stored in the server memory, it seems necessary to strengthen the symbolic reasoning procedure with some form of propagation of universally quantified conditions. One solutions comes from the combination of the existentially quantified formulas used to represent sets of states in Cubicle (cubes) with other forms of constraints on the global configuration e.g. constraints inspired to counting abstraction used in Petri nets. More in detail, we enrich our assertions by adding counters that keep track of the number of users in a given state. For our purposes, we will focus only on a counter associated to the Pos flag. We now add a global variable Count whose initial state is defined as Count=0. The counter is updated in the report rule (𝐶𝑜𝑢𝑛𝑡 ≥ 0 is added to the guard and 𝐶𝑜𝑢𝑛𝑡 := 𝐶𝑜𝑢𝑛𝑡 + 1 is added to the body off the transition) and used as precondition in the error rule as specified below.

The enriched assertional language combining array formulas (for expressing precise properties of individual processes and of global variables) and Presburger constraints (for expressing global constraints via the counting abstraction) is the key point in order to enforce termination and prove correctness for the desired property. When executed on the refined model, Cubicle proves the model SAFE after visiting 10 cubes and performing 138 fixpoint tests and 41 SMT solver calls.

Although not yet implemented, the above mentioned strategy could be incorporated into the Cubicle algorithm for instance by associating counters to specific control states and by generating counter manipulation operations in each transition rule via a preliminary static analysis of the Cubicle specification as done in our example via human ingenuity.