ions 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. To automatically validate protocols in our formalism, we resort to an extension of the Cubicle SMT-based infinite-state model checker, in which the monotonic abstraction applied during the predecessor computation is strengthen by introducing abstract predicates obtained via Counting Abstraction.
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. [
Based on a preliminary study present at Overlay 2020 [
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
[
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.
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 satisifed: ⟨, , ′⟩ ∈ , ⟨, (, ), ′⟩ ∈ and () = () [for (, ), () ̸= ()], ⟨, (, ), ′⟩ ∈ and () ∈ Θ( ) [for (, ) () ̸∈ Θ( )]. - = ⟨{⟨, , ⟩} ⊎ , Θ ⟩ → ⟨{⟨′, ′, ⟩} ⊎ , Θ ⟩ if ⟨, (), ′⟩ ∈ and ′() = ̸∈ ( ), ̸= ⊥, and ′() = () for ̸= . - = ⟨{⟨, , ⟩} ⊎ , Θ ⟩ → ⟨{⟨′, , ′⟩} ⊎ , Θ ⟩ if ⟨, (, ), ′⟩ ∈ and ′() = () ∪ { ()} and ′() = () for ̸= . - = ⟨{⟨, , ⟩} ⊎ , Θ ⟩ → ⟨{⟨′, , ′⟩} ⊎ , Θ ⟩ if ⟨, (), ′⟩ ∈ and ′() = ∅ and ′() = () for ̸= . - = ⟨{⟨, , ⟩} ⊎ , Θ ⟩ → ⟨{⟨′, , ⟩} ⊎ , Θ ′⟩ if ⟨, (, ), ′⟩ ∈ and Θ ′() = Θ( ) ∪ () and Θ ′() = Θ( ) for ̸= . - = ⟨{⟨, , ⟩, ⟨1, 1, 1⟩, . . . , ⟨, , ⟩} ⊎ , Θ ⟩ → ⟨′, Θ ⟩ where ′ = {⟨′, , ⟩, ⟨1′, 1′, 1⟩, . . . , ⟨′, ′, ⟩} ⊎ if ≥ 0 and ⟨, (, ), ′⟩ ∈ and for all ∈ [1, ], we have ⟨, (, ), ′⟩ ∈ and ′() = () and ′() = () for ̸= .
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.
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 diferent 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⟩.
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 diferent 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 [
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 diferent 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 of the transition) and used as precondition in the error rule as specified below. transition bad(v) requires { Pos[v] = False { Error := True; }
&& Contact[v] = True && Count = 0 } 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.