We present an automata-based model speci cally devised to formalise abstractions of distributed protocols used by contact-tracing applications that combine Bluetooth and TCP/IP communication with a centralised server. The model provides pure names, store and read operations on both value and set variables, synchronous and asynchronous communication primitives for both kind of variables. A protocol con guration consists of the current state of a nite set of local states containing the states of individual devices. The transition system models the interaction between devices in the same physical location and between a single device and possible distributed servers. We will use the resulting model to specify the logic underlying contact tracing protocols. To automatically validate our formal models, we employ an extension of the Cubicle in nite-state model checker based on the Alt-Ergo SMT solver. To overcome spurious results due to the application of monotone abstraction, we propose to re ne the predecessor computation adopted in Cubicle by combining predicates on the Theory of Arrays (as provided by Cubicle) with Presburger predicates inferred via a counting abstraction applied on a subset of control states of individual processes.
The goal of contact tracing is to make people aware of possible contacts with
positively diagnosed people so that they should possibly have an infection test
[
Tracing (PEPP-PT) proposed both centralized and decentralized solutions. As a
decentralized solution, they propose the Decentralized Privacy-Preserving
Proximity Tracing (DP3T), and the speci cations of ROBERT4 and NTK5. Both
centralized and non-centralized systems require a central server for alerts and
typically di er in the way ephemeral identi ers are generated. In general the
system architecture is based on a smart app, a noti cation server as in
Publish/Subscribe architectures, and a possibly trusted server. An important notion
here is that of ephemeral identi ers, i.e., identi ers that are frequently changed
either by a trusted authority/server or by the app itself in order to reduce the
risk of a malicious use of private user data from third parties such as the attacks
presented in [
Building up on the formalization of decentralized protocols in [
To automatically validate protocols in our formalism, we resort to an
extension of the Cubicle SMT-based in nite-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 [
Properties of contact tracing protocols are strongly related to the consistency of global and local state information, e.g., ensure that the local user state re ects data stored in the server. Violation of this kind of property are speci ed via universally quanti ed assertions, the more di cult type of assertions for in nitestate model checking. This kind of assertions or transitions is a potential cause of undecidability already in simpler in nite-state models such as Petri Nets.
To deal with universally quanti ed conditions, Cubicle applies monotone abstraction in order to over-approximate the symbolic computation of predecessors states turning universally quanti ed preconditions into postconditions. Unfortunately, this approximation does not work well for the class of properties of interest for contact tracing protocols. Our proposed solution is based on the strengthening of the symbolic computation performed in Cubicle by combining array-based assertions with Presburger formulas generated via a Counting Abstraction.
Plan of the paper In Section 2 we introduce Data Automata as a formal model for protocols such as those used in contact tracing In Section 3 we discuss an example of contact tracing protocol speci cation via Data Automata. In Section 4 we present an encoding of Data Automata in the Cubicle input language with the help of our case study. In Section 5 we discuss the problems encountered with the current search strategy implemented in Cubicle and propose our solution based on a combination of array and counting assertions. In Section 6 we address conclusions and related works. 2
In this section we introduce a possible formalization of a decentralized contact tracing protocol. To specify the protocol rules and behaviour (computation), we will use a transition system de ned on con gurations consisting of a set of states of individual users. User con gurations contain a local memory needed to store the list of broadcasted and collected identi ers. System con gurations contain a global memory that gathers user logs and a set of user states that corresponds to the current number of registered individuals. To simplify the model, we x the number of agents and simulate dynamic injection by randomly selecting the initial value of local clocks used to de ne validity of ephemeral identi ers (i.e. local clocks may have di erent values).
Syntax We will use the following general de nitions: { I is a denumerable set of pure names (identi ers) containing the unde ned label ?; { M is a nite set of message labels (a; b; c; : : : ); { V is a nite set of rst order variables (identi ers) that are part of the local state of users (x; y; : : : ); { S is a nite set of second order variables (a set of identi ers) that are part of the local state of users (s; t; : : : ).
We then de ne Act(M; V; S) the set containing the following elements: 1. Conditions: { eq(x; y) and noteq(x; y), where x; y 2 V ; { in(x; m) and notin(x; m), where x 2 V and m 2 M ; 2. Operations: { local; { new(x), where x 2 V ; { bcast(m; x) and rec(m; x), where m 2 M; x 2 V ; { add(x; s), where x 2 V; s 2 S; { reset(s), where s 2 S; { reg(m; s), where m 2 M; s 2 S.
A protocol is de ned as an automaton P = hQ; M; V; S; R; q0i, where q0 2 Q and R Q Act(M; S; V ) Q. We assume here that bcast and reg actions are always de ned on distinct labels in M .
Semantics Consider a protocol P = hQ; M; V; S; R; q0i. A process con guration of P is a triple pc = hq; ; i where: { q 2 Q is the current user state; { : V ! I is the current evaluation of rst order variables; { : S ! P(I) is the current evaluation of second order variables.
We denote by PC the set of process con gurations. A global con guration of P is then a pair (K; ), where K 2 NPC is a nite multiset of process con gurations and : M 7! P(I) corresponds to a centralized memory. GC denotes the set of global con gurations.
For 2 GC, we will use ids( ) to denote the set of pure names occurring in . The operational semantics is then de ned as the minimal relation ! G G that satis es the following property de nitions in which will use ] to denote multiset union: { hfhq; ; ig ] K; i ! hfhq0; ; ig ] K; i if one of the following conditions is satis ed hq; local; q0i 2 R, hq; eq(x; y); q0i 2 R and (x) = (y) [for noteq(x; y) (x) 6= (y)], hq; in(x; m); q0i 2 R and (x) 2 (m) [for notin(x; y) (x) 62 (m)]. { = hfhq; ; ig ] K; i ! hfhq0; 0; ig ] K; i if hq; new(x); q0i 2 R and 0(x) = id 62 ids( ); id 6= ?, and 0(y) = (y) for x 6= y. { hfhq; ; ig ] K; i ! hfhq0; ; 0ig ] K; i if hq; add(x; s); q0i 2 R and 0(s) = (s) [ f (x)g and 0(t) = (t) for t 6= s. { hfhq; ; ig]K; i ! hfhq0; ; 0ig]K; i if hq; reset(s); q0i 2 R and 0(s) = ; and 0(t) = (t) for t 6= s. { hfhq; ; ig ] K; i ! hfhq0; ; ig ] K; 0i if hq; reg(m; s); q0i 2 R and 0(m) = (m) [ (s) and 0(n) = (n) for n 6= m. { hfhq; ; i; hq1; 1; 1i; : : : ; hqk; k; ikg ] K; i ! hfhq0; ; i; hq10; 10; 1i; : : : ; hqk0; k0; kig ] K; i if k 0 holds, the transition hq; bcast(m; x); q0i 2 R, and, for all i 2 [1; k], we have that hqi; rec(m; xi); qi0i 2 R and i0(xi) = (x) and i0(y) = i(y) for y 6= xi. 2.1
Given a protocol P and an initial global con guration 0, a computation is a possibly in nite sequence of con gurations 0 1 : : : s.t. i ! i+1 for i 0. In this paper we are particularly interested in veri cation problems for protocol instances with a nite but arbitrary number of processes. In other words we will consider the in nite set of initial con gurations I consisting of initial congurations containing any ( nite) number of processes and study reachability problems that might expose anomalies during protocol execution. 2.2
For the resulting model, we are interested in safety properties for parameterized version of a protocol instance. More speci cally, given a protocol de nition P and a given process state qe 2 Q that denotes an error state, we would like to verify that global con gurations that contain occurrences of qe are unreachable starting from any possibile initial con guration (i.e. independently from the number of process instances). A similar property can be formulated by adding an error ags to the server state instead of selecting a special error state in Q. We are also interested in properties expressed by violations in which global con gurations contain a process in state qe while all other processes are in states contained in a given set of control locations. We will refer to these properties as control state reachability and constrained control state reachabiliy, respectively. Violations of control state reachability can be de ned using quanti ed assertions, such as there exists a process i in control state qe, without further constraints on global memory of local states. Similarly, violations of constrained properties can be expressed by adding universally quanti ed conditions on the control states of other processes.
In the rest of the paper we will illustrate, with the help of a case study, how to encode our formalism in the Cubicle input language and how to verify control state reachability problems by a re nement of the symbolic exploration procedure provided by the tool. 3
We present below a formal speci cations of the protocol scheme of Contact Tracing applications abstracting away identi er creation, i.e., assuming that user app generate fresh identi ers, and reasoning within the validity epoch of identi ers, i.e., those maintained in local memory. The system is composed of a nite but arbitrary number of user apps and of a server modeled via a centralized memory. Each user apps has local variables V = fx; y; zg and S = fin; outg. Furthermore, M = fb; mg where b denotes beacon messages broadcasted by user apps, and m denotes report messages sent to the centralized memory. The user app starts their part of protocol in state q0 and operate in three di erent modes. In emitter mode the app generates and emits fresh beacons: { hq0; new(x); q1i, the user app generates a fresh identi er and stores it in the local variable x. { hq1; add(x; out); q2i, in q1 the fresh identi er stored in x is added to the local memory out. { hq2; bcast(b; x); q2i; hq2; local; q0i, in q2 the user app either emits the message (b; x) or returns to the initial state in order to apply a rotation scheme for the beacon identi ers or perform other steps.
In reception mode the app, while in any state l0 2 Q n fr1; s2g, receives a beacon and stores in the local memory in and returns the current state: { hl0; rec(b; y); l1i in state l0 the user is always ready to receive beacons. { hl1; add(y; in); l0i, in state l1 the beacon is stored in the local memory in. In report mode, enabled only in state r0 = q0, the app sends its local memory out to the server and moves to the halt state r1: hq0; send(m; out); r1i.
In query mode, enabled only in state s0 = q0, the user app selects a beacon z from the local memory in, i.e., hs0; sel(in; z); s1i, sends it to the server to check if it has been reported by another app or not. In the former case it moves to the halting state s2, i.e, hs1; in(m; x); s2i. In the latter case it returns to the initial state s0. 4
Let us now discuss how to model a protocol de nition P = hQ; M; V; S; R; q0i in Cubicle. A global con guration is a pair (K; ), where K is a nite multiset of process con gurations and corresponds to a centralized memory. The encoding if is quite immediate since we can represent the global memory as a nite set of unbounded arrays Am1 ; : : : ; Amn with cells of Boolean type one for each mi 2 M . The array Am is such that Am[x] = T rue if and only if x 2 (m) for each pair x; m.
For the encoding of K we can proceed in several di erent ways. Remember that a process con guration is a triple pc = hq; ; i, in which q 2 Q but is the current user state, is the current evaluation of rst order variables; and is the current evaluation of second order variables. One possible encoding is de ned as follows: { To represent control states, we introduce an unbounded array state that associates an enumerative type associated to Q to represent the current state of each process, i.e., state[i] = q if process i is in state q. { To represent the current state of a rst order variable v we can introduce an unbounded array valv such that valv[i] = d if (v) = d holds in pci (in process i). { To represent the current state of a second order variable s we can introduce an unbounded array vals such that vals[i; d] = T rue if and only if d 2 (s) holds in pci (in process i).
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). For the sake of brevity, we illustrate the idea with the help of an example inspired to the contact tracing protocols described in the previous sections. 4.1
To encode our protocol speci cation, we introduce the following array declarations for modelling individual users: array Pos[proc] : bool array Contact[proc] : bool array In[proc,proc] : bool array Out[proc,proc] : bool Pos[i] de nes the current value of positive status of user i. Contact[i] de nes the current value of the variable that de nes whether or not user i has detected a contact with a positive user. In[i] de nes the current value of the In set variable. Namely, In[i,b] is true if and only if b is in the In local memory of process i. Out[i] de nes the current value of the Out set variable. Namely, Out[i,b] is true if and only if b is in the Out local memory of process i.
The server can be modelled using a single array array Server[proc] : bool in such a way that Server[b] is True only when b is in the global memory . Finally, we can model freshness of pure names (identi ers) but using an additional array in which we mark used names: array Used[proc] : bool
We remark here that all above introduce declarations de ne potentially unbounded mono- or bi-dimensional data structures. In other words the array-based formalism allows us to symbolically represent and reason on an in nite family of transition systems, each one with nitely many process instances.
The emission of a beacon requires a broadcast operation that involves a set of non-deterministically selected nodes. To model this step, we introduce a special global variable Lockstep that is initially set to False and used to split transitions in locksteps (e.g. to perform broadcast operations within a single lockstep). array Lockstep[proc] : bool Let us now illustrate the way we can encode the Protocol transitions using Cubicle parametric rules. The set of initial global con gurations is de ned as follows: init (x y) {
Pos[x] = False && Contact[x] = False && In[x,y] = False && Out[x,y] = False && Used[x] = False && Server[x] = False &&
Lockstep[x] = False Here x; y are universally quanti ed variables that de ne constraints on the array cells in every possible instance of an initial con guration, i.e., with one formula we state a constraint over in nitely many initial con gurations. Initially, all cells are set to F alse (no used names, empty memory, no reported positive user, no reported contact).
Emission To model the emission of a beacon via a broadcast message sent to a set of nodes, non deterministically selected from those in the current global states, we introduce a special Lockstep array indexed on beacon identi ers that will be used to split a single broadcast operations in a sequence of steps that do not interfere with other operations. In other words the cell Lockstep[b] is set to True only during the emission of beacon b. Reception rules will use this cell as a guard for ring the rule. All other operations will use the Lockstep ags to avoid to interfere with the broadcast operation.
More speci cally, we introduce the following ignition rule: transition out(u b) requires {
Pos[u] = False && Used[b] = False && Lockstep[b] = False && forall_other x. (Lockstep[x] = False) } {
Used[b] := True; Out[u,b] := True;
Lockstep[b] :=True Here u; b are existentially quanti ed variables ranging on pairs of distinct values. Notice that the guard requires the process u to be non positive, freshness of beacon b, and b to be not present in the local Out memory. We avoid interferences with other (broadcast or non broadcast) operations via a guard that ensures that no lockstep have been activated in the current state. This guard is expressed using the universally quanti ed formula of the Cubicle language: Lockstep[u] = False && forall_other x. (Lockstep[x] = False) The e ect of the rule is to emit the beacon, i.e., set it to U sed, and store it in the Out memory. We also set Lockstep to True to start a lockstep in which to include all subsequent reception steps with other nodes in the current global state.
We can also add the following rule in order to cover the range of all identi ers as a potentially emitted beacon. transition out(u) requires {
Pos[u] = False && Used[u] = False && Out[u,u] = False && Lockstep[u] = False && forall_other x. (Lockstep[x] = False) Out[u,u] := True; Lockstep[u] :=True;
Used[u] := True The reception of a beacon, within a given lockstep, is modeled via the following rules: Each lockstep is non deterministically terminated via the following rule: This rule terminates the selection of the nite set of receivers of a certain beacon emitted at the beginning of the lockstep.
Report The report rule involves a global operation in which the local memory of a process is copied to the global memory of the server. The copy operation can be expressed using the following operation This action set to True every cell of the array Server associated to a beacon b that is included in the Out local memory of the sender that sends the report. } { This action set to True every cell of the array Server associated to a beacon b that is included in the Out local memory of the sender that sends the report. Query In the query rule a process and the server are supposed to synchronize on a given beacon request. We can simplify the encoding of the selection and rendezvous step by simply checking if there exists a beacon b in the local memory that also occurs in the global memory. transition query(u b) requires {
Pos[u] = False && Contact[u] = False && In[u,b] = True && Server[b] = True && Lockstep[b] = False && forall_other x. (Lockstep[x] = False) } {
Contact[u] := True; } This action set to True every cell of the array Server associated to a beacon b that is included in the Out local memory of the sender that sends the report. Although this rule does not mimic all steps speci ed in the protocol (selection of a beacon from In, request to the server, ack or nack to the user) it captures the essence of these operations in a more concise form.
The Cubicle veri cation engine is based on symbolic backward exploration.
Cubicle operates over sets of existentially quanti ed formulas called cubes. Formulas
containing universally quanti ed formulas (generated during the computation
of predecessors) are over-approximated by existentially quanti ed formulas. In
other words Cubicle applies monotone abstraction [
Contact[v] = True && forall_other u. (Pos[u] = False) } { }
Error := True; To validate the considered properties, we de ne the following assertion that speci es bad con gurations in the sense of control state reachability, unsafe () { Error = True } i.e., con gurations of any size in which Error is True.Due to the presence of universally quanti ed conditions both in the protocol rule and in the precondition of the error rule, there is no termination guarantee on the execution of the veri cation task in Cubicle. In our case-study Cubicle, after visiting 41 nodes and computing 364 xpoint tests with 864 solvers calls, returns a spurious trace. The problem is due to the over-approximation introduced via monotone abstraction. Preconditions with universally quanti ed guards are transformed in postconditions and thus they are not propagated through di erent 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 quanti ed conditions.
One solutions comes from the combination of the existentially quanti ed formulas used to represent sets of states in Cubicle (cubes) with other forms of constraints on the global con guration 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 ag. We now add a global variable Count whose initial state is de ned as Count=0. The counter is updated in the report rule and used as precondition in the error rule as speci ed 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. Cubicle indeed proves the protocol correct for any number of users and beacons after visiting 10 nodes, computing 138 xpoint tests and 41 solver calls. 6
In this paper we have presented a formal model of distributed systems that can
be used to specify protocols that combine bluetooth and network communication
and make use of noti cation systems based on a central server. Our formalism
is an extension of automata-based formalisms in which individual process have
a local memory with rst-order and second-order variables. Broadcast
communication is inspired to Broadcast Protocols [
Di erently from more foundational works, see again [