Denis Butin
email: denis.butin@inria.fr

David Gray
email: david.gray@computing.dcu.ie

Giampaolo Bella

Towards Verifying Voter Privacy Through Unlinkability

Keywords: E-voting, Trustworthy Voting System, Privacy, Security Protocols, Formal Methods

The increasing official use of security protocols for electronic voting deepens the need for their trustworthiness, hence for their formal verification. The impossibility of linking a voter to her vote, often called voter privacy or ballot secrecy, is the core property of many such protocols. Most existing work relies on equivalence statements in cryptographic extensions of process calculi. This paper provides the first theorem-proving based verification of voter privacy and overcomes some of the limitations inherent to process calculi-based analysis. Unlinkability between two pieces of information is specified as an extension to the Inductive Method for security protocol verification in Isabelle/HOL. New message operators for association extraction and synthesis are defined. Proving voter privacy demanded substantial effort and provided novel insights into both electronic voting protocols themselves and the analysed security goals. The central proof elements are described and shown to be reusable for different protocols with minimal interaction.

Introduction

The use of electronic voting (e-voting) for official elections is on the rise across the world. Security protocols claiming properties that protect voters and guarantee regular elections require formal scrutiny because of their sensitive nature. Voters are asked to trust, in particular, election officials regarding the handling of their votes. With e-voting, they are asked to trust a security protocol with special goals. One key goal of e-voting protocols is to hide the way a particular voter votes. Most recent efforts [START_REF] Ryan | Keynote: Analysing security properties of electronic voting systems[END_REF] to advance formal verification are based on process equivalence. Despite substantial progress, issues remain regarding simplification of protocol models or termination of supporting tools.

The benefits of specifying privacy in an interactive theorem prover have never been explored until now. Isabelle [START_REF] Paulson | Isabelle: A Generic Theorem Prover[END_REF], a generic theorem prover, is flexible enough when used with higher-order logic to allow new classes of security properties to be analysed in the framework provided by the Inductive Method [START_REF] Bella | Formal Correctness of Security Protocols[END_REF]. Its extensions for dealing with voter privacy are described and demonstrated on a classical protocol in the sequel of this manuscript. They required new proof techniques and lines of reasoning, whose development in turn demanded substantial effort. Nevertheless, their application to other protocols is expected to be straightforward, as has been the case for the confidentiality argument [START_REF] Martina | Verifying Multicast-Based Security Protocols Using the Inductive Method[END_REF] for example, with most of the proof scripts adapted for new protocols without significant effort. Automated tools are ideal for checking conjectures about protocols quickly. However, the interactive nature of the Inductive Method pays back, also with e-voting, with a greater support to the analyst's understanding of the protocol entanglements than what automated tools offer today.

The most notable findings in this area stem from formalising the protocols with a process algebra and encoding the privacy properties by process equivalence [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]. As detailed below, process equivalence supports a notion of indistinguishability between two situations where a voter voted, respectively, for two different candidates. This implies that an observer cannot discern the two situations being formalised. In line with the operational semantics of the protocols specified by the Inductive Method, we develop an operational encoding of privacy based on unlinkability of voter with vote, focusing on the associations that an active attacker can derive from intercepting the protocol traffic. For example, if Alice sent her vote for Bob to the election administrator as a clear-text, then the attacker would build the association Alice-Bob. However, actual protocol messages are complicated nestings of advanced cryptographic operations (which are still assumed to be reliable), so that the attacker's inspection is far from straightforward. This inspection is formalised by the innovative association analyser operator aanalz -naming is coherent with the existing lingo. Also, the attacker can intelligently merge associations when they have at least an element in common, similarly to an investigator relating Alice to a crime scene because she wears the same shoe size as that of a shoeprint in the scene. This merge is formalised by the innovative association synthesiser operator asynth. When it is impossible to build, by means of analysis and then synthesis, an association that features both voter and vote, then there is unlinkability of voter with vote, hence the protocol enforces voter privacy (about their vote). Conversely, the protocol violates voter privacy, irrespectively of how many other voters cast that vote.

An outline of the indistinguishability and unlinkability approaches to modelling privacy ( §2) leads to our extensions to the Inductive Method to account for privacy specification and analysis ( §3). These extensions are then demonstrated on a classical e-voting protocol known as FOO [START_REF] Fujioka | A Practical Secret Voting Scheme for Large Scale Elections[END_REF] through its inductive specification ( §4) and verification of voter privacy ( §5). Conclusions and future work end the manuscript ( §6).

Voter privacy (also known as ballot secrecy) is generally [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF][START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF] defined as follows: how a particular voter voted is not revealed to anyone. Votes may or may not be published at the end of an election, so it is not the confidentiality of the vote in itself that matters but its association with the voter who cast it. In other words, the way a voter votes should not be discoverable by anyone, even after vote count. A caveat on this definition is the exclusion of the corner case where all voters vote identically.

Indistinguishability

A common way of modelling privacy involves showing the indistinguishability between two situations:

1. Voter V a votes x and Voter V b votes y 2. Voter V a votes y and Voter V b votes x Indistinguishability here means that when V a and V b swap their votes, no party (including trusted parties running the election) can tell situations 1 and 2 apart.

Formal analysis is often performed in cryptographic extensions of process calculi, with the applied pi calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF] being most typical. Automated tools such as ProVerif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF] or, more recently, AKiSs [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF] can be used to assist with such analysis.

ProVerif is used to check protocols represented by processes modelled in the applied pi calculus. It does not restrict the number of protocol sessions. A stronger condition than observational equivalence between processes is checked. Since the validity criterion is an under-approximation, spurious attacks may be found in some cases. There is no risk for flawed protocols to be deemed correct, but correct protocols may be invalidated by the tool because of the approximation. Various approaches to checking voter privacy have been presented. Notably, Kremer and Ryan [START_REF] Kremer | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus[END_REF] presented an analysis with some manual parts. In 2008 [START_REF] Delaune | Automatic verification of privacy properties in the applied pi calculus[END_REF], a fully automatic verification was done. However, a translation algorithm was used without formal proof of correctness. The next year, Delaune, Kremer and Ryan published a detailed analysis in which the number of voters is fixed, with a partially automated privacy proof [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]. New cryptographic primitives can be added easily to the tool via equational theories, but the resulting processes may not terminate in some cases.

AKiSs, the most recent automated tool able to check privacy automatically, is also based on equivalence properties. However, a new kind of cryptographic process calculus is used and a different type of process equivalence is checked, called trace equivalence. Under-and over-approximations of trace equivalence are used to detect flawed protocols and validate correct ones, respectively. The set of supported cryptographic primitives is broader than in ProVerif. For a specific class of processes, called determinate, a precise verification can be done. However, not all e-voting protocols fall in this class, in which case one of the approximations must be used. The number of sessions must be bounded as it has critical impact on the computational cost.

Unlinkability

In contrast to the indistinguishability modelling of privacy, an operational view reflects the natural threat model of an attacker monitoring all network traffic and using the data she can extract to associate a voter with a vote. An outline of this approach and comparison with the one based on indistinguishability first appeared in our recent position paper [START_REF] Butin | Verifying Privacy by Little Interaction and No Process Equivalence[END_REF]. Initially, the attacker decomposes each individual message, and records all plaintexts and ciphertexts for which keys are available. She can also associate these with the intended recipient agent of the message. For each protocol event whereby an agent sends a message to another agent, this analysis gives the attacker a set of (components of) messages, namely an association. Moreover, if the communication channel is not anonymous, then the attacker can also extend the association just gathered by storing the identity of the sender.

However, it is not sufficient to inspect in isolation each of the messages sent in the traffic. A voter's identity V may appear near an element m that is later to be extracted again, this time in conjunction with the vote N v . In this case, such a common element m provides the link between voter V and vote N v . An attacker monitoring the network sees messages as discrete entities and can exploit the shared context of elements extracted from one given message. This process of combining sets of associations builds up an association synthesis. When all possible protocol scenarios are taken into account, establishing voter privacy boils down to inspecting the synthesised set for the presence of a voter's vote.

The only pieces of information that should not be treated as a possible link to synthesise new associations are those that can be linked to all voters, such as the name of the precise election officials that a protocol prescribes. Because their identities appear in each and every protocol session, using one of them as a link would lead to the synthesis of insignificant, that is, privacy-irrelevant, associations. For example, an investigator will not call up every human being as suspect of murder simply upon the basis that everyone could pull a trigger. We shall see that with the FOO protocol, the administrator and the collector are omnipresent, hence must be ruled out to synthesise significant associations.

Without setting bounds on the number of agents, sessions, or message nesting depth, the number of different associations that the attacker can synthesise is very large. Precisely, an unbounded number of associations can be derived by observing a full trace, due to the fact that its length is unbounded. This size limits the tool support that traditional finite-state search can offer. As experienced before with other goals [START_REF] Bella | Formal Correctness of Security Protocols[END_REF], inductive reasoning bypasses the size constraints also with the analysis of associations.

3 Specifying unlinkability in Isabelle/HOL

Isabelle/HOL and the Inductive Method

Isabelle is a generic interactive theorem prover supporting many logics. The most commonly used one, HOL, allows formalisation and proof of predicates in higher-order logic. Automated reasoning tools are available, but the user must still define the line of reasoning and guide the proving process. A file-based hierarchy of theories is available. All theorems from parent theories are available when those theories are imported in the current one.

The Inductive Method for security protocol verification was introduced in Paulson's paper [START_REF] Paulson | The Inductive Approach to Verifying Cryptographic Protocols[END_REF] and later applied widely, notably to electronic payment [START_REF] Bella | Formal Verification of Cardholder Registration in SET[END_REF], non-repudiation [START_REF] Bella | Mechanical Proofs about a Non-Repudiation Protocol[END_REF], certified e-mail [START_REF] Bella | Formal Correctness of Security Protocols[END_REF] and multicast protocols [START_REF] Martina | Verifying Multicast-Based Security Protocols Using the Inductive Method[END_REF]. Its central idea is the use of mathematical induction to model security protocols and their properties. The proofs are also done by induction. A specification of the standard Dolev-Yao threat model, common cryptographic primitives and their properties are provided. All seminal elements of the Inductive Method reside in three theory files. Message describes messages and agents, Event specifies network event datatypes and Public contains the lemmas relevant to cryptographic keys and initial states.

Because of the nature of induction, both the number of protocol sessions and participating agents are unbounded. This allows detection of interleaving or replay attacks. The threat model is incarnated by a special agent called Spy, who sees all protocol messages, decrypts whatever she can, and participates actively by sending anything she can build from parts previously obtained. The Spy's capabilities are subsumed by an inductive rule called Fake:

| Fake: [[evsf ∈ ns public; X ∈ synth (analz (knows Spy evsf ))]] =⇒ Says Spy B X # evsf ∈ ns public
Protocol steps are also modelled as inductive rules with pre-and postconditions. Security properties are proven by checking that inductive theorem statements hold over all possible network histories (traces).

Available network events are Says, Gets and Notes. The latter represents internal storage of a message by an agent. Says A B X represents the sending of message X by agent A to agent B. Delivery does not have to happen, but when it does, this is denoted using Gets.

The message operators are as follows:

analz formalises the breaking-up of messages without cryptanalysis. Plaintext is only extracted when the relevant decryption key is part of the knowledge of the agent applying the operator.

parts returns all message building blocks ; it can be seen as analz expanded with cryptanalysis. synth applied to a set of message returns the set of compound messages.

Asymmetric cryptography is available through functions priEK and pubEK for private and public encryption keys, and then priSK and pubSK for private and public signing keys. Each of them takes the proprietor agent as a parameter. A private key of a given operation mode is required to decrypt a message encrypted with the corresponding public key, and conversely.

Agent knowledge, formalised by the function knows, maps an agent and a list of network events to a set of messages: the knowledge that the agent can extract from this trace. Agents already know some elements (those in initState) such as keys before a protocol even begins.

A hands-on, step by step guide to using the Inductive Method can be found in a recent paper [START_REF] Bella | Inductive study of confidentiality: for everyone[END_REF].

Extensions for unlinkability

The analysis of associations requires a new message operator, analzplus. It is built on the traditional analz message operator, endowed with an external message set providing extra decryption keys: inductive set analzplus :: msg set ⇒ msg set ⇒ msg set for H :: msg set and ks ::

msg set where Inj [intro,simp]: X ∈ H =⇒ X ∈ analzplus H ks | Fst: {|X ,Y | } ∈ analzplus H ks =⇒ X ∈ analzplus H ks | Snd : {|X ,Y | } ∈ analzplus H ks =⇒ Y ∈ analzplus H ks | Decrypt [dest]: [[Crypt K X ∈ analzplus H ks; Key (invKey K ) ∈ analzplus H ks]] =⇒ X ∈ analzplus H ks | Decrypt2 [dest]: [[Crypt K X ∈ analzplus H ks; Key (invKey K ) ∈ ks]] =⇒ X ∈ analzplus H ks
In particular, the new operator is useful to formalise everything, namely the set of all message components, that the attacker can extract from a single message sent in the traffic by hammering it with the entire knowledge she has acquired on an entire trace. For a message X and a trace evs, this set can be defined as analzplus {X } (analz (knows Spy evs)).

Using analzplus, the message association analyser aanalz can be defined inductively. Only Says events influence it. Indeed, each Gets message reception event follow a message sending event Says, and Notes events correspond to private recording of data by agents: The definition indicates, among other aspects, that only the attacker can analyse associations. Also, she will neglect the associations created by compromised agents, thus including those that she may have created, by sending out specific messages. It can also be seen that the sender identity is extracted only for messages that are not sent anonymously. The isAnms predicate holds of messages with a specific form that we conventionally interpret to signify anonymity.

The association synthesiser asynth can be introduced now. Its definition is not tied to aanalz, but it will always be used in conjunction with it for our purposes. Specifically, we will examine the contents of the set asynth (aanalz Spy evs), where evs is a generic protocol history. The asynth operator introduces a new association as the union of association sets that share a common element: As noted above, the definition insists that the common element is not a piece of information that can be linked to all voters -for instance, the name of election officials since they appear in every step. The version below can be used for protocols that define two election officials, here called Adm and Col, in line with the subsequent case study.

Modelling the FOO protocol in the Inductive Method

The well-known Fujioka, Okamoto and Ohta (FOO) [START_REF] Fujioka | A Practical Secret Voting Scheme for Large Scale Elections[END_REF] protocol features two election officials called administrator and collector and involves bit commitments as well as blind signatures. The specification of its protocol steps follows after a description of some extensions. Blind signatures are a cryptographic primitive often found in e-voting protocols, and in particular in the FOO protocol. We specify them for the first time in the Inductive Method, as an inductive rule in the protocol model. The Spy gains knowledge of a plain signature if she knows the corresponding blinded signature and blinding factor, modelled as a symmetric key:

| Unblinding: [[evsb ∈ foo; Crypt (priSK V ) BSBody ∈ analz (spies evsb); BSBody = Crypt b (Crypt c (Nonce N )); b ∈ symKeys; Key b ∈ analz (spies evsb)]] =⇒ Notes Spy (Crypt (priSK V ) (Crypt c (Nonce N ))) # evsb ∈ foo
Anonymous channels are specified by defining a function to replace Says when needed. We are conventionally defining an anonymous message by means of a precise message format -the actual message is prepended with a constant number: Administrator and collector are introduced as translations Adm and Col of specific agents. We now turn to the actual protocol steps and their model.

FOO protocol steps and inductive protocol model

The FOO protocol features six phases that give rise to as many protocol steps and corresponding inductive rules.

Preparation:

The voter V picks a vote N v , builds N v c using the commitment key c, and blinds this vote commitment using the blinding factor b. V then signs the blinded commitment and sends it to the administrator along with V 's identity.

| EV1 : [[evs1 ∈ foo; V = Adm; V = Col ; c ∈ symKeys; Key c / ∈ used evs1 ; b ∈ symKeys; Key b / ∈ used evs1 ; b =c; Nonce Nv / ∈ used evs1 ]] =⇒ Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv )))| } # Notes V (Key c) # Notes V (Key b) # evs1 ∈ foo
2. Administration: Upon reception of a signed, blinded commitment, the administrator opens it and checks that the quoted agent name is equal to the signer of the blind signature. If such is the case and the agent has not voted before, the administrator returns the message to V , now signed by the former. The administrator also records V 's name.

| EV2 : [[evs2 ∈ foo; V = Adm; V = Col ; Notes Adm (Agent V ) / ∈ set evs2 ; Gets Adm {|Agent V , Crypt (priSK V ) BSBody| } ∈ set evs2 ; BSBody = Crypt P R; ∀ X Y . MPair X Y / ∈ parts{BSBody}]] =⇒ Says Adm V (Crypt (priSK Adm) BSBody) # Notes Adm (Agent V ) # evs2 ∈ foo 3.
Voting: If V obtained the administrator's reply, V unblinds it and sends the resulting plain signature to the collector over an anonymous channel.

| EV3 : [[evs3 ∈ foo; Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv )))| } ∈ set evs3 ; Gets V (Crypt (priSK Adm) (Crypt b (Crypt c (Nonce Nv )))) ∈ set evs3 ]] =⇒ Anms V Col (Crypt (priSK Adm) (Crypt c (Nonce Nv ))) # evs3 ∈ foo

Collecting:

The collector checks the signature and publishes the enclosed vote commitment N v c on a bulletin board, provided that it was not published before and that all votes have been received.

| EV4 : [[evs4 ∈ foo; V = Adm; V = Col ; Says Col Col CX / ∈ set evs4 ; Gets Col {|Number anms, Crypt (priSK Adm) CX | } ∈ set evs4 ; CX = Crypt P R; ∀ X Y . MPair X Y / ∈ parts{CX }]] =⇒ Says Col Col CX # evs4 ∈ foo

5.

Opening: Once N v c has appeared on the bulletin board, V sends c over an anonymous channel so that N v can be revealed.

| EV5 : [[evs5 ∈ foo; Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv )))| } ∈ set evs5 ; Gets Col (Crypt c (Nonce Nv )) ∈ set evs5 ; Key c ∈ analz (knows V evs5 ); c / ∈ range shrK ; c ∈ symKeys]] =⇒ Anms V Col (Key c) # evs5 ∈ foo 6.
Counting: Upon reception of V 's key, the collector publishes N v on the condition that the key be identical to c.

Main results

The following theorem, foo V privacy asynth, is the culmination of the entire proof process and states that the FOO protocol guarantees voter privacy to all honest voters that started the protocol. More precisely, assume that the regular, honest voter V sent the administrator a message in line with the first step of the protocol, containing a blinded commitment on the vote Nv. Also assume that this very vote is in the message set of association syntheses. Then the name of V is not in that set:

theorem foo V privacy asynth: [[Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv )))| } ∈ set evs; a ∈ (asynth (aanalz Spy evs)); Nonce Nv ∈ a; V / ∈ bad ; V = Adm; V = Col ; evs ∈ foo]] =⇒ Agent V / ∈ a
Before turning to the proof itself, we focus on the most important proof elements, which are mainly results about associations.

A fundamental result is foo V privacy aanalz, which looks similar to the foo V privacy asynth theorem. However, whereas the latter is a statement about asynth, hence about association synthesis, the former only considers aanalz, that is associations arising from individual messages. Whenever an honest voter performed the first step of the protocol, the voter's identity and vote cannot be found in the same association:

theorem foo V privacy aanalz : [[Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv )))| } ∈ set evs; a ∈ (aanalz Spy evs); Nonce Nv ∈ a; V / ∈ bad ; evs ∈ foo]] =⇒ Agent V / ∈ a
The lemma called asynth insert is a direct consequence of the definition of asynth quoted in 3.2. By introducing the various cases that an application of asynth may imply, it provides a useful rewrite rule for expressions involving the operator name:

lemma asynth insert: a ∈ asynth(insert a1 as) =⇒ (a=a1 ∨ a ∈ asynth as ∨ (∃ a2 m. a2 ∈ as ∧ a = a1 ∪ a2 ∧ m ∈ a1 ∧ m ∈ a2 ∧ m = Agent Adm ∧ m = Agent Col ))
The next three theorems allow more precise reasoning about messages that contain encryption. They are all concerned with the situation where a message yields an association set containing at least one ciphertext. They are necessary for dealing with situations where protocol messages are not completely specified. For instance, an agent may have to transmit an encrypted commitment without even being able to check that the commitment is actually about a vote. In those situations, protocol step specification must model agents' limited knowledge when dealing with sealed messages. However, even when the complete contents of a ciphertext is not known, a number of scenarios can be distinguished. Various encryption key values and partial knowledge of the ciphertext contents lead to contradictions. Possible configurations are therefore made explicit in the following results.

Lemma aanalz PR states constraints about the possible forms of a generic ciphertext appearing in any association. Its conclusion is expressed as a conjunction between two predicates that are themselves disjunctions. The first conjunct relates to the presence of an agent name in the association. If the name of the collector appears in the association and any nonce (a vote) is an atomic component of R, then no agents that are both honest and different from the collector can also be in a. The second conjunct states that if any nonce is part of the association, then the Spy must be able to decrypt the ciphertext and no agent name can be an atomic component of R:

lemma aanalz PR: [[a ∈ aanalz Spy evs; Crypt P R ∈ a; evs ∈ foo]] =⇒ (Agent Col / ∈ a ∨ (Agent V ∈ a -→ V ∈ bad ∨ V = Col ) ∨ (Nonce Nv / ∈ parts {R})) ∧ ((Nonce Nv / ∈ a) ∨ (Key (invKey P ) ∈ analz (spies evs) ∧ Agent V / ∈ parts {R}))
Then, lemma aanalz AdmPR V Nparts relates to the specific case when a ciphertext signed by the administrator is in an association. It establishes a disjunction: either no nonce is an atomic component of the ciphertext's body, or

the Spy cannot open the ciphertext inside the signature, or there is no regular, honest agent name in the association:

lemma aanalz AdmPR V Nparts: [[a ∈ aanalz Spy evs; Crypt (priSK Adm) (Crypt P R) ∈ a; evs ∈ foo]] =⇒ Nonce Nv / ∈ parts {R} ∨ Key (invKey P ) / ∈ analz (knows Spy evs) ∨ (Agent V ∈ a -→ V ∈ bad ∨ V = Adm ∨ V = Col )
Finally, lemma aanalz Adm is still about associations containing a ciphertext. Like foo V privacy aanalz, it binds the variables involved in a version of the first step of the protocol. Assume an association contains the name of an honest agent who already sent a message corresponding to step one. Also assume it contains a ciphertext Crypt P R, and that the nonce from step one is in parts of R. If the name of the collector is absent from the association, then the following conclusions hold:

-If P is neither the signing key of the voter mentioned in the precondition nor the signing key of the administrator, then it must be the blinding factor; -If P is the administrator's signing key, then the body of the ciphertext is exactly the body of the message signed by the voter in the bound first message:

lemma aanalz Adm: [[Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv )))| } ∈ set evs; a ∈ aanalz Spy evs; Agent Col / ∈ a; Agent V ∈ a; V / ∈ bad ; Crypt P R ∈ a; Nonce Nv ∈ parts {R}; evs ∈ foo]] =⇒ (P = priSK V ∨ P = priSK Adm ∨ P = b) ∧ (P = priSK Adm ∨ R = Crypt b (Crypt c (Nonce Nv )))

Proof of the main theorem

Proving privacy by foo V privacy asynth is done, as usual in the Inductive Method, by induction on the protocol model. Every protocol step generates a subgoal. When all subgoals are closed, the theorem is proven. Developing the proof required considerable effort. After eliminating redundancies and streamlining, it was reduced to about 170 steps. It will be shown that despite its length, the proving strategy is general, hence reusable for different protocols. Induction and simplification leaves us with seven subgoals: the six protocols steps, plus Fake. The Fake is closed thanks to the classical reasoner blast. Its proof is simple because messages sent by dishonest agents do not yield associations. Intuitively, the goal of the Spy is to extract plausible associations, not make up new ones. However, it keeps its traditional Dolev-Yao attacker role and influences all usual theorems proven for the protocol ; those are used in the privacy proof.

The subgoal arising from EV1 is first simplified by remarking that fresh keys (the blinding factor and commitment key) can never be known to the Spy -they cannot yet be in the set analz (knows Spy evs1). We then perform a case split about the agent Va involved in the version of the first protocol step generated by this subgoal. If Va is dishonest (a member of the bad set), then the message it sent yields no new association and the subgoal concludes thanks to the inductive hypothesis. If Va is an honest agent, we must apply, for the first time, asynth insert. This lemma is of constant use throughout the proof because it allows us to split the asynth set. For instance, this stage of the proof features the following precondition:

a ∈ asynth (insert {{|Agent Va, Crypt (priSK Va) (Crypt ba (Crypt ca (Nonce Nva)))| }, Agent Va, Crypt (priSK Va) (Crypt ba (Crypt ca (Nonce Nva))), Agent Va, Agent Adm, Crypt ba (Crypt ca (Nonce Nva))} (aanalz Spy evs1))
Let us call X the set such that a ∈ asynth (insert X (aanalz Spy evs1)). Applying asynth insert leaves us with three possibilities:

1. a = X.

a ∈ asynth (aanalz Spy evs1).

3. There exists a2 in aanalz Spy evs1 and an element m such that a is the union of a2 and X and m is both in X and in a2.

The inductive hypothesis tells us that Nv is in a and X contains no nonces, so the first disjunct is excluded. The second disjunct is eliminated thanks to the lemma nv fresh a2, not quoted here, which states that fresh nonces do not appear in association syntheses.

If a is a union, more precision is required. First, if the agent V from the inductive hypothesis and the agent Va introduced by the induction are different, then V / ∈ X and therefore V must be in a2. Since Nv is also in a2, foo V privacy aanalz leads us to a contradiction.

Otherwise, V = Va. If Nv and Nva are equal, Nv must be fresh like Nva. The auxiliary lemma aanalz traffic, according to which elements in associations which are not agent names must have appeared in the traffic, solves this case (fresh elements never appeared in network traffic). On the other hand, if Nv = Nva, the element in common m can be any of the elements in X. We appeal to another lemma, association Nv. It is specifically tailored for this subgoal, used only here, and shows that an association containing a nonce can not contain also any of the possibilities for m listed here except for V. Together with foo V privacy aanalz, that takes care precisely of the case m = V, this solves the subgoal.

The use of asynth insert to split the association synthesis is a technique used for all subgoals of the theorem. It turns out that the third disjunct generates the bulk of the proving work for the remaining subgoals. We will therefore focus on it. It requires taking a close look at the structure of sets in aanalz.

Subgoals arising from protocol steps two and four are much larger than the other ones because of the generic specification of the steps. For instance, in the second protocol step, the administrator has received a signed ciphertext from the voter. The administrator can extract the ciphertext from the signature, but has no means in general to look inside. We only assume that it is possible to know that the ciphertext contains no more than one atomic component, by inspecting its length. However, the precise nature of the plaintext is unknown in general and this generality in the specification of the inductive step explains the additional complexity of the proof. It is necessary if the precondition is to be realistic. Likewise, in step four, the collector receives a signed ciphertext that he cannot open in general. The concrete consequence in terms of association syntheses is that potential common elements m are not listed explicitly in the goal preconditions. Instead of belonging to a finite set of bound variables, only partial information is known about them. For instance, we may only know that an element m can be deduced from some ciphertext via analzplus. By contrast, for non-generic protocol steps, we obtain an explicit set and the proof is much easier.

A number of results about elements in aanalz are available, such as aanalz PR and aanalz Adm. These theorems are stated with weak premises and offer a number of conclusions as disjunctions. The most systematic proof strategy is therefore to perform case splits about the ciphertext contained in aanalz. As this is done, one can reason more precisely about encryption keys and plaintexts until a contradiction is reached thanks to the aforementioned results. One crucial distinction is whether the name of the collector appears in the association. If such is the case, the elements in aanalz arose from the collection step EV4. Conversely, if Agent Col / ∈ a2, the association set in the precondition was generated by another protocol step. The encryption key P from the ciphertext Crypt P R, assumed to be in an association, is then compared in turn to the voter's signing key, the administrator's signing key, and to the blinding factor. Contradictions are reached in every case. The value of the payload R is also compared with the voter's blinded vote commitment Crypt b (Crypt c (Nonce Nv)). Those different situations obviously refer to various ciphertext values naturally generated by the protocol steps. In essence, the proving strategy amounts to zooming in sufficiently into the various possible association configurations to uncover contradictions that are not apparent at a more general level.

The outline of this proving strategy is not dependent of a given protocol. Let us recall the important steps:

1. For every subgoal, split the association syntheses set asynth using asynth insert. 2. The subgoals arising from explicit protocol steps are straightforward to close because the set of potential common elements m becomes explicit as well. 3. For more general subgoals, case splits about the possible values of initially generic ciphertexts are combined with lemmas describing their structure in associations in a systematic way.

Proof of the supporting theorems

Rather than describing the full proof of every theorem required for the privacy one, we focus on aanalz PR due to space constraints. It is of constant use in the privacy proof, appearing in it eleven times, and its proof exemplifies the kind of reasoning required for the other supporting theorems. Recall its statement from earlier (5.1) ; it constrains the form of elements of aanalz that contain a ciphertext.

As expected, complications arise again from the generic steps, namely EV2 and EV4. As the other subgoals are easier to prove, let us concentrate on EV2, as the proof for EV4 is similar.

We require the following subsidiary results in addition to standard lemmas from the existing Inductive Method framework:

analzplus into parts: Elements in the set analzplus X ks (recall ks is the external key set) are in parts X. no pairs: If a message contains only atomic components and already contains an agent name in its parts set, a number of other elements cannot be in the parts set. analzplus Nv : Assume an analzplus Q (analz H) set contains a ciphertext and a nonce. If parts Q contains only atomic components, then the decryption key of the ciphertext must be in analz (insert Q H).

The case where the administrator (Adm) is dishonest is closed easily. Else, we must distinguish cases on the basis of the origin of the association in the inductive hypothesis. The first possibility is that it was generated by the EV2 message introduced by the induction. In that case, the key P in the aanalz PR theorem statement could either be the administrator's signing key, or the encryption key of the ciphertext that he signed. A third possibility is that the entire Crypt P R is embedded deeper in the signed ciphertext. Let us examine each possibility in turn.

In the first case, we must show that an agent name (either the collector or a regular voter) and a nonce cannot be present in analzplus R at the same time. This is shown by combining analzplus into parts and no pairs. In the second case, the ciphertext Crypt P R from the theorem precondition is exactly the ciphertext Crypt Pa Ra signed by the administrator in this version of the second protocol step. Disentangling the precondition conjunction leads to the same scenario and an additional one that entails proving that if the inverse of key P is known to the attacker in the first place, it is all the more known to her after getting hold of R.

If Crypt P R is embedded in the ciphertext generated by the administrator, we must perform a few additional case splits but the line of reasoning is the same, with the additional use of analzplus Nv.

Even though specifying the possible forms of elements in aanalz requires inspecting a number of scenarios, the proving process is straightforward once some crucial building blocks are established. Notably, the three subsidiary results we listed earlier (analzplus into parts and so on) are stated without any reference to the FOO protocol -they are protocol-independent and can be reused directly. A submission of our Isabelle theories to the online Archive of Formal Proofs [START_REF] Klein | The Archive of Formal Proofs[END_REF] is being prepared.

We have presented the first interactive theorem proving-based analysis of voter privacy. It offers an independent and complementary means of investigation to consolidated work based on process equivalence, ultimately contributing to the trustworthiness of voting systems. Privacy is modelled as an unlinkability property between a voter and her ballot. Extensions to the Inductive Method are implemented in Isabelle/HOL to specify associations between elements and combinations of associations that share a common element.

The initial proof development effort was significant, but a coherent line of reasoning emerges from the proof. This general strategy and a number of protocolindependent results about the new operators support the case of re-usability for other e-voting protocols. Interactive proofs entail a level of clarity about protocol scenarios that is unavailable from automatic tools. The inductive nature of our specification eliminates termination issues or inherent size limitations. While the benefits of automated tools are clear, our approach sheds a complementary light on voter privacy by its operational view.

A more general version of the asynth operator, allowing unbounded association synthesis, is needed. Other privacy-type properties such as receipt-freeness and coercion-resistance ought to be specified in the Inductive Method. Additionally, e-voting protocols that are not amenable to analysis in the process equivalence model must be studied in our framework to investigate its domain of applicability. We would also like to program some of the recurring proof steps as ML tactics.

  inductive set asynth :: msg set set ⇒ msg set set for as :: msg set set where asynth Build [intro]: [[a1 ∈ as; a2 ∈ as; m ∈ a1 ; m ∈ a2 ; m = Agent Adm; m = Agent Col ]] =⇒ a1 ∪ a2 ∈ asynth as

  consts anms :: nat definition Anms :: [agent, agent, msg] ⇒ event whereAnms A B X ≡ Says A B {|Number anms, X | }

Acknowledgement This research was supported in part by the Science Fundation Ireland (SFI) grant 08/RFP/CMS1347.


Nadjib Lazaar
email: nad-jib.lazaar@inria.fr

Youssef Hamadi
email: youssefh@microsoft.com

Said Jabbour
email: jab-bour@cril.fr

Michle Sebag
email: sebag@lri.fr

Cooperation control in Parallel SAT Solving: a Multi-armed Bandit Approach

Keywords: Algorithmique, programmation, logiciels et architectures Parallel SAT solvers, portfolio approach, Multi-Armed Bandit problem Solveurs SAT parallles, approche portfolio, problme du Bandit Manchot

, specifically the allowed length of the shared clauses. In the present paper, a new approach is used to control the cooperation topology (pairs of units able to exchange clauses). This approach, referred to as Bandit Ensemble for parallel SAT Solving (BESS), relies on a multi-armed bandit formalization of the cooperation choices. BESS is empirically validated on the recent 2012 SAT challenge benchmark.

Introduction

The widespread adoption of modern SAT solvers based on the Conflict-Directed Clause Learning (CDCL) is the result of the efficiency gains made during the last decade. Nowadays, industrial problems with hundreds of thousands of variables and millions of clauses are routinely solved. However, many new application domains with instances of increasing size and complexity are coming to challenge modern solvers. For instance, in the last SAT competitions, many instances coming from Computational Biology remained unsolved. Fortunately for the domain, multi-core based parallel processing capabilities are now on every desktop. It then becomes legitimate to consider parallelization as a way to leverage existing CDCLs in order to efficiently meet the requirements of new application domains.

This technological shift has restarted research into parallel SAT solving, and many solvers have been presented since the early 2000. For historical reasons, many of them are based on the divide-and-conquer methodology [START_REF] Chrabakh | Gridsat: A chaff-based distributed sat solver for the grid[END_REF][START_REF] Chu | PMiniSat: a parallelization of MiniSat 2.0[END_REF]. However, the most successful ones (regularly winning parallel tracks in SAT competitions) exploit the Parallel Portfolio architecture where a set of independent CDCLs solver compete and cooperate through Clause Sharing [START_REF] Hamadi | Manysat: a parallel sat solver[END_REF][START_REF] Biere | Lingeling, plingeling, picosat and precosat. solver description[END_REF]. Systematic clause sharing among the CDCLs however hardly scales up with the number n of cores, as n to n -1 communications slow down the search performance of the whole system. Previous work has shown how the efficiency of the approach can be improved through controlling dynamically the amount of information shared by the cores, specifically the allowed length of the shared clauses [START_REF] Hamadi | Control-based clause sharing in parallel sat solving[END_REF].

The present paper is concerned with controlling the cooperation network, that is, selecting the cores referred to as emitter cores that are allowed to send clauses to any given core called receiver core. The presented approach is based on a Multi-Armed Bandit (MAB) formalization of the emitter selection. The challenge is twofold. On the one hand, the relevance of an emitter core w.r.t. the receiver core, referred to as emitter reward, must be defined in order to select the best emitter cores relatively to a receiver core. The selection relies on the famed MAB Upper Confidence Bound algorithm (UCB) [START_REF] Auer | The nonstochastic multiarmed bandit problem[END_REF]. On the other hand, such rewards do not follow a static distribution; every core explores the search landscape and its production of clauses is bound to vary along its search. The UCB criterion is accordingly extended to accommodate non-stationary distributions. The proposed approach, a Bandit Ensemble for parallel SAT Solving (BESS), is empirically validated on the 2012 SAT challenge benchmark.

The paper is organized as follows. Section 2 briefly reviews related work and introduces formal background on modern parallel SAT solvers and Multi-Arm Bandits. Section 3 describes the BESS algorithm. Section 4 reports on the experimental setting and discusses the validation results. The paper concludes with some perspectives for further research.

Related work and formal background

This section briefly discusses the state of the art in parallel SAT solving, focussing on portfolio-based parallel approaches. For the sake of containedness, the multi-armed bandit framework is also presented together with the UCB algorithm [START_REF] Auer | The nonstochastic multiarmed bandit problem[END_REF].

Modern Parallel SAT Solvers

Modern SAT solvers extend the original Davis, Putnam, Logemann and Loveland procedure (DPLL) [START_REF] Davis | A machine program for theorem-proving[END_REF] with important components such as CDCL for conflict directed clause learning, restart policy, activity based heuristics, and pruning of the database of learnt clauses [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF]. In these settings, when a conflict arises during the inference step, the implication graph converges on a conflict vertex capturing a variable assignment. This implication sequence is analyzed to determine the unsatisfying variable assignments that explain the conflict. This explanation is used in turn for intelligent backtracking, clause learning and the adjustment of the variable selection heuristics (i.e., variables activity).

Gradsat [START_REF] Chrabakh | Gridsat: A chaff-based distributed sat solver for the grid[END_REF], the first parallel SAT solver based on a a CDCL, extends the zChaff solver using a master-slave model. It implements guiding-paths to divide the search space of a problem using a set of unit clauses. Moreover, learned conflict clauses can be exchanged between all slaves if they are smaller than a predefined size limit. Using a similar technology we can point to MiraXT [START_REF] Matthew | Multithreaded sat solving[END_REF], and pMiniSat [START_REF] Chu | PMiniSat: a parallelization of MiniSat 2.0[END_REF].

ManySAT [START_REF] Hamadi | Manysat: a parallel sat solver[END_REF] and Plingeling [START_REF] Biere | Lingeling, plingeling, picosat and precosat. solver description[END_REF] exploit a different solving strategy. Unlike the divide and conquer approach, these solvers use a portfolio approach which lets several sequential CDCLs complete and cooperate to solve the original instance. These CD-CLs can differ from each other through complementary and/or different restart strategies, activity and polarity variables heuristics, clause-learning schemes, etc. The Plingeling solver presents a master-slave communication with only unit clauses exchange, whereas in ManySAT, all processing units share and exchange learned clauses up to some size limit. These limits can be static [START_REF] Hamadi | Manysat: a parallel sat solver[END_REF] or dynamic [START_REF] Hamadi | Control-based clause sharing in parallel sat solving[END_REF].

Portfolio-based approaches

In [START_REF] Guo | Diversification and intensification in parallel sat solving[END_REF], the authors explore the diversification and intensification principles in a portfoliobased parallel SAT solver. The challenging question here is to find a good diversification/intensification tradeoff, enforcing an efficient division of labor between the different units and the search space they explore. A study of this tradeoff is proposed by defining two roles for the computational units. Some units are classified as masters and perform an original search strategy, ensuring diversification. The remaining units are classified as slaves that intensify their master's strategy.

The control-based clause sharing policy aimdTQ was first presented by [START_REF] Hamadi | Control-based clause sharing in parallel sat solving[END_REF]. This dynamic clause sharing policy uses an AIMD (i.e., Additive Increase/Multiplicative Decrease) feedback control-based algorithm used in TCP congestion avoidance. The aimdTQ policy adjusts dynamically the size of shared clauses between any pair of processing units. It maintains an overall number of exchanged clauses (i.e., throughput) and exploits the activity-based quality of shared clauses.

This algorithm has demonstrated that the efficiency of the parallel portfolio approach can be improved through dynamically controlling the amount of information shared by the units, specifically the allowed length of the shared clauses.

This approach however hardly scales up when the number of cores increases, due to the communication costs. In such cases, it becomes necessary to control which cores are allowed to send information to any other core.

Multi-armed bandit framework

How to control the communication and clause sharing among cores is formalized as an exploration vs exploitation (EvE) dilemma. A formal setting for EvE is the Multi-Armed Bandit problem (MAB), pertaining to the field of Game Theory [START_REF] Lai | Asymptotically efficient adaptive allocation rules[END_REF].

The MAB problem involves K independent arms a.k.a. options. The i-th arm is characterized by its fixed reward probability p i in [0, 1]. In each time step t, the arm selection strategy selects some arm j; with probability p j it gets reward r t = 1, otherwise r t = 0.

The quality of an arm selection strategy is measured after its regret, defined as its loss compared to the optimal strategy, playing the arm with maximal reward p * in each time step. Formally, the regret after N time steps is defined as:

L(N ) = N p * - N t=1 r t
The Upper Confidence Bound algorithm devised by Auer et al. [START_REF] Auer | The nonstochastic multiarmed bandit problem[END_REF] maintains two indicators for each i-th arm: the number of times it has been played up to time t, noted n i,t and the average corresponding reward noted pi,t . Subscript t is omitted when clear from the context. The UCB1 strategy selects in each time step the arm maximizing the quantity below:

pj,t + 2 log k n k,t n j,t
where the left term pj,t enforces the exploitation (favoring the arm with best empirical reward) and the right term changed between the cores when considering large-scale parallel architectures: beyond the upper-bound on the length of the shared clauses [START_REF] Hamadi | Control-based clause sharing in parallel sat solving[END_REF], the communication architecture needs be dynamically controlled as well. The BESS algorithm achieves decentralized adaptive decision making: for each core, the selection of its emitter cores is dynamically achieved by a multi-armed bandit, referred to as individual MAB. The question thus is to determine in each time period whether a given emitter core (naturally, distinct from the receiver core) is allowed to send clauses to the receiver; if this is the case, the emitter core is referred to as alive; otherwise it is sleeping.

Every K conflicts (K = 25, 50, 100 and 200 in the experiments), the decision of which emitters should be alive or sleeping is reconsidered. The lapse of time between two consecutive decision makings is referred to as generation.

Each individual bandit is a four-step process, which exploits the only information available to the receiver, that is, the one coming from the alive emitters. The individual bandit thus:

1. Updates the average cumulative reward associated to each alive emitter (since it has last been awakened) in the last generations;

2. Updates the reward threshold;

3. Determines the alive emitters with worse average cumulative reward, and compares these individual rewards with the threshold reward;

4. If the worst individual reward is confidently higher than the threshold, then basically all alive emitters are relevant in the sense that they are better than average; 5. Otherwise, each worse alive emitter is sent to sleep, and the emitter that was sleeping for the longest period of time is awakened (set alive).

Let us describe the MAB approach and each step of the individual bandit on alg.1 and alg.2.

Algorithm 1: BESS Input : A CNF formula F, N cores, n alive emitters, L clause limit size Output: A solution s of F or unsat if F is not satisfiable

1 s ← ∅ 2 shared f inish ← f alse foreach i ∈ 0..N -1 do in parallel 4 s ← M AB i (F, N, n, L) return s Algorithm 2: M AB i (F, N, n, L) 1 N set ← {0, . . . , i -1, i + 1, . . . , N -1}, A b ← rand(N set , n), S b ← N set \A b 2 k, τ i ← 0 ∆ i , R i ← ∅ while true do 4 (∆ k+1 i , s) ← search(F, ∆ i , R i ) 5 if s = ∅ then f inish ← true return s 6 if f inish then break 7 foreach j ∈ N set do send(∆ k+1 i , L) 8 foreach j ∈ A b do R k+1 i ← R k+1 i ∪ receive j () 9 (∆ i , R i ) ← (∆ i ∪ ∆ k+1 i , R i ∪ R k+1 i ) 10 r i (A b ) ← reward(R k+1 i ) 11 τ i ← threshod update(τ i , r i (A b )) 12 (A b , S b ) ← swap(r i (A b ), τ i )
14 return ∅ BESS algorithm (Algo.1) takes a CNF formula F for a parallel solving on N cores (from 0 to N -1) which generates N individual MAB. The cooperation-control approach is presented in Algo.2. This algorithm returns (sat/unsat) if it finishes, in which case all other units end by checking the finish shared variable (algo.2 line 6). For a given core i, first we select randomly n alive emitters (i.e., A b for alive bandits). The remaining and/or sleeping ones are in S b . The search starts with an initial state where the proper learnt clauses ∆ i and the foreign ones R i are empty (i.e., (∆ i , R i ) = (∅, ∅)). For each iteration, a CDCL procedure is called (line 4) throughout a generation defined in term of number of conflicts (K conflicts). After each generation, the pair (∆ i , R i ) evolves (line 9). We note ∆ k+1 i (resp. R k+1 i ) the learnt clauses (resp. received clauses) in the k + 1 iteration. On line 7 of alg.2, the unit i sends its proper learnt clauses ∆ k+1 i to each other unit j according to the clause size limit L. After that, the individual MAB receives all foreign clauses from the alive emitters (line 8). Based on the received clauses, the reward and threshold update functions update, respectively, the cumulative reward r i←j and the reward threshold τ i associated to the receiver core i (more details are in presented next sections 3.2, 3.3 and 3.4). Based on reward and threshold values, the swap function on line 12 swaps each worse alive emitter to sleep state and select the emitter with the longest sleeping time to be swapped to alive state.

Instant Rewards

In a given generation g, each core receives clauses of length up to the limit L from the alive emitters. In this section, we define the instant reward of each alive emitter according to different clause quality measurements. In the following, we note R g i←j (resp. r g i←j ) the received clauses (resp. the instant reward) from the alive emitter j to the receiver core i in generation g :

Size-based instant reward

Each clause c of size s removes 2 V -s possible instantiations from the search space, if V denotes the total number of variables of the current SAT formula F. A first clause quality measurement is:

Q size (c) = -log(1 -2 -s )
Where the instant reward is set to

r g i←j = c∈R g i←j Q size (c)

LBD-based instant reward

As introduced in [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF], the Literals Blocks Distance (LBD) is a way to measure the quality of learnt clauses. During search, each decision level produces a number of unit propagations. For a given clause, a "literal block" represents all literals of the same level. These literals have a chance that they are linked with direct dependencies from a semantic point of view. In practice, this measurement was introduced as a way to manage the learnt clause database of GLUCOSE solver [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF].

Here, each receiver core computes the LBD of each received clause (noted lbd(c) as LBD value of c clause). We propose an LBD-based clause quality as:

Q LBD (c) = Q size(c) lbd(c)
The instant reward is set to

r g i←j = c∈R g i←j Q LBD (c) RR n°8070
(Size/LBD)-based clause reward

It is established that clauses with the smallest size and/or LBD are more interesting.

Here, we combine the two precedent quality measurements to produce a (Size/LBD)based clause quality

Q Size/LBD (c) = -log(1 -2 -lbd(c) )
with an instant reward as

r g i←j = c∈R g i←j Q SIZE/LBD (c)

AH-based clause reward

In [START_REF] Hamadi | Control-based clause sharing in parallel sat solving[END_REF], a clause quality is defined using the activity of literals at the basis of VSIDS heuristic [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF] (AH for Activity Heuristic). This heuristic allows the literals with greatest activity to be used in most of the recent conflicts. Indeed, when a conflict occurs, the activity of the literal that appears in the learnt clause is incremented. The most active literals are those related to the current part of the search space. Consequently, the clause quality measurement proposed in [START_REF] Hamadi | Control-based clause sharing in parallel sat solving[END_REF] exploits these VSIDS activities to quantify the relevance of a clause. Let us take A max i the current maximal activity of the receiver core i, and A i (x) the current activity of a given literal x. We note L(c) the set of active literals of a a given clause c:

L i (c) = {x : x ∈ c s.t. A i (x) ≤ A max i 2 }
We note also P i←j the set of clauses received by i from j with at least |c| 3 active literals:

P i←j = {c : c ∈ R g i←j s.t. |L i (c)| ≥ |c| 3 }
The AH-based quality of clauses sent by j to i is given as:

Q AH = |P i←j | |R g i←j | + 1
Using this new quality measurement, the instant reward is set to:

r g i←j = Q AH × c∈R g i←j -log(1 -2 |c| )

CAH-based clause reward

In this section, we propose a (Continuous Activity Heuristic)-based quality. Let us recall that A i (x) (resp. A max i ) the activity of the literal x (resp. activity max) according to the receiver core i:

Q CAH (c) = 1 |c| x∈c f ( A i (x) A max i )
With f a particular sigmoid function (f : [0 1] → [0 1]) which starts with small beginnings and accelerates to reach a climax point (fig. 2):

f (x) = (1/(1 + e α(2x-1) ) -β) × γ RR n°8070
with α a constant, β = 1 (1+e α ) and γ = (2+e -α +e α ) (e α -e -α ) Now, using this new quality measurement, we set the instant reward as:

r g i←j = c∈R g i←j f (Q CAH (c))

The cumulative reward

The instant reward r g i←j , defined in precedent section, is used to update by relaxation the cumulative reward estimate of the j-th alive emitter, where parameter λ is the relaxation rate:

r i←j = (1 -λ)r i←j + λr g i←j

Threshold update

In this section, we present different methods (M1 to M4) to update the reward threshold τ i (associated to the receiver core i).

M1: first generation reward average. Here, the threshold is determined as a static value calculated at the beginning as the average reward of the first generation over all emitters,

τ g i = 1 n j∈A b r 1 i←j M2:
Previous generation reward average. At generation g, the threshold τ g i is determined as the average reward of the previous generation (g -1) over all emitters,

τ g i = 1 n j∈A b r g-1 i←j RR n°8070
M3: Cumulative reward average of new alive emitters. Since obviously only the rewards of alive emitters are known, the threshold is updated from the reward of the alive emitters in the first generation after they have been awakened. Let n τ , initialized to 1, be the number of times a new emitter has been set alive since the beginning of the search. Let δ τ be 1 if there is a new alive emitter j in generation g, with r g i←j its instant reward; then

τ g i = n τ * τ g i + r g i←j n τ + δ τ
M4: Weighted threshold. The reward threshold τ i is determined by relaxation on the cumulative average reward over all emitters,

τ g i = (1 -λ)τ g i + (λ × 1 n j∈A b r g i←j )
The comparison between the reward threshold and the worst average reward relies on the Hoeffding bound. Let us remind that the probability for an empirical average pn built from n trials (all ranging in interval [a, b]) to be less than the true average p by a margin is bounded as:

P r(p n < p -) < exp -2 n/(b -a) 2
One accordingly computes whether the probability for the minimum r i over all alive emitters, to be less than τ g i by is less than η, where η is a parameter of the algorithm:

τ g -min i {r i } = > (b -a) log(η) n τ
and if this is the case, the worst alive emitter is sent to sleep and a sleeping emitter is awakened.

While the emitter to be awakened could be uniformly selected, one selects the emitter that was sleeping for the longest period of time, emulating a no-replacement selection and thus avoiding the chance of forgetting any emitter for long.

The behavior of the individual MAB using the precedent update-threshold methods is illustrated on a simple artificial problem.

Let the instant reward associated to the j-th emitter w.r.t. the receiver i in generation g be defined as r g i←j = sin(a j × g + b j ) where parameters a i and b i , uniformly drawn in respectively [-1, 1] and [0, 2π], are attached to the i-th emitter.

In the first generation, n emitters are uniformly selected among the N ones, and set to alive. The figure m-threshold compares the cumulative reward regret using the four methods (i.e., M1 to M4) w.r.t. the oracle. Here, the oracle selects, at each generation, the best n emitters to set as alive. Over 50 generation, the weighted threshold method (i.e., M4) is better than the cumulative and static ones (i.e., M1, M2 and M3).

Evaluation

This section reports on the empirical evaluation of the BESS algorithm, which is implemented on the top of the ManySAT parallel SAT solver. ManySAT, chosen as it won the parallel track on 2008 SAT race, is a portfolio approach involving several sequential CDCLs (which include all the classical features like two-watched-literal, unit propagation, activity-based decision heuristics, lemma deletion strategies, and clause learning). In addition to the classical first-UIP scheme, these CDCLs incorporate a new technique which extends the classical implication graph used during conflict-analysis to exploit the satisfied clauses of a formula They are differentiated in many ways (e.g., the use of different and complementary restarts, learning schemes...).

Experimental setting

Our tests were conducted on two platforms, 8-core Intel Xeon machines with 16GB of RAM running at 2.33GHz, and 32-core AMD Opteron Proc. 6136 machines with 64GB of RAM running at 2.4GHz. We used the 588 "Application" SAT+UNSAT instances of the latest SAT-Challenge 2012. The CPU time limit was set to 30mn CPU per core, hence a total of 4 hours on the first (resp. 16 hours on the second) platform. The number n of alive emitters is set to 4 (resp. 16) for the 8-cores (resp. 32-cores) architecture with a shared clause limit size L = 8.

Figure 4 shows the results on 8-cores, the time period K was set to 25 after a few preliminary tests. ManySAT uses a complete communication topology, every core sharing its clauses with every other core. The number n of alive emitter cores is set to 4, selected by BESS. As a sanity check, the performance obtained when the alive emitters are uniformly selected in each time period (legend Random) is also reported.

RR n°8070

Experimental validation

Here, both ManySAT and BESS, with a CAH-based reward (R=5), significantly outperform Random. Let us take part(a) of Fig. 4, ManySAT and BESS coincide at the beginning of the curve, that is for the "easy" problems; for more difficult problems (resolution time > 4,000 sec.), BESS with CAH-based reward moderately but significantly outperforms ManySAT (solving 7 more problem instances).

A much clearer picture is obtained on the 32-core architecture. Fig. 5 displays a comparative performance of BESS with the best setting get from 8-cores results (i.e., CAH-based reward, |g| = 25) w.r.t., ManySAT and the random mode. The number n of alive emitter cores is set to 16, selected by BESS. Here, Random moderately but significantly outperforms ManySAT, which confirms that the communication overload is detrimental to the resolution efficiency. The accuracy of the BESS process is demonstrated as BESS significantly outperforms ManySAT and Random, solving 30 more instances than ManySAT in the imparted time. In the meanwhile, BESS is also faster than ManySAT 2.0 (requiring less than 20,000 s. versus more than 50,000 s to solve 300 problems).

Conclusion

This paper, aimed at the scalability of parallel portfolio-based SAT, presents an ensemble Bandit-based approach which outperforms the state of the art ManySAT 2.0 parallel algorithm, by replacing a complete communication topology with an adaptively adjusted one.

More generally, this paper shows how a Multi-Armed Bandit approach can be used to adaptively control a communication topology in a decentralized way, yielding an efficient trade-off between i) the cooperation of a massive number of cores; ii) an affordable overall communication load among the cores; iii) an efficient communication topology adjustment. The main lesson learned concerns the interaction between the reward definition and the periodicity of the selection decisions.

As mentioned, a much simplified MAB framework has been considered in BESS insofar. The MAB framework however offers room to extend the BESS scope to adaptively determining i) the appropriate number of emitters for a given receiver; ii) the maximum length of the shared clauses, again for a given receiver.

3. 1

 1 Individual MAB An individual MAB is thus attached to a fixed receiver core. Let N denote the overall number of cores, and let n denote the fixed number of emitter cores allowed to share clauses (with a size up to L) with the receiver core 1 . The density ρ = n N.(N -1) of the communication topology is thus fixed (i.e., figure1).

Figure 1 :

 1 Figure 1: A directed graph density with (N, n, ρ) = (8, 4, 0.14).

Figure 2 :

 2 Figure 2: Sigmoid function f (x) with α = 5

Figure 3 :

 3 Figure 3: Threshold update methods comparison

Fig. 4

 4 Fig. 4 displays the comparative performance of the different BESS settings and ManySAT, that is the time in seconds needed to solve a given number of instances on the 8-core architecture. Using a different time period g (i.e., 25, 50, 100 and 200), we compare the different reward functions: R=1: Size-based reward R=2: LBD-based reward R=3: (Size/LBD)-based reward R=4: AH-based reward R=5: CAH-based reward

Figure 4 :

 4 Figure 4: Results on 8 cores

Figure 5 :

 5 Figure 5: Results on 32 cores

RR n°8070

log k n k,t nj,t takes care of the exploration: each arm is selected infinitely many times as t goes to infinity; however the lapse of time between two selections of some under-optimal arm increases exponentially. The UCB algorithm provides optimal regret guarantees, logarithmically increasing with the number N of time steps (to be contrasted with the linear regret achieved by -greedy approaches).Interestingly, the exploration vs exploitation dilemma is at the core of many portfoliobased approaches. For instance,[START_REF] Gagliolo | Algorithm portfolio selection as a bandit problem with unbounded losses[END_REF] handle the algorithm selection problem as a MAB problem, where the goal is to select the algorithm most able to solve a given sequence of problem instances. Likewise,[START_REF] Da | Adaptive operator selection with dynamic multi-armed bandits[END_REF] address the Adaptive Operator Selection (AOS) issue in Evolutionary Algorithms as a MAB problem, where the goal is to select the operator which maximizes the expectation of the fitness improvement.Note that in the latter context, the challenge is also to deal with a non-stationary setting: what is the best-suited evolutionary operator depends on the current phase of search. In the considered cooperation control problem, we likewise face a nonstationary setting: the reward associated to a core varies along search. whereas the standard MAB setting only considers stationary reward distributions.[START_REF] Da | Adaptive operator selection with dynamic multi-armed bandits[END_REF] thus extended the standard MAB criterion (which only considers stationary reward distributions) through estimating indicators pj,t (respectively n i,t ) from respectively the rewards (resp. the number of selections) observed in the last W time steps, where the window length W is a user-supplied

parameter.3 Bandit Ensemble for Parallel SAT Solving: OverviewThis section presents the Bandit Ensemble for Parallel SAT Solving (BESS) algorithm. As mentioned, parallel SAT solving needs to control more finely the information ex-RR n°8070

The upper-bound L on the size of the shared clauses is fixed in the remainder of the paper, as well as the number n of emitters. Further work is concerned with adaptively adjusting parameters L and n along the SAT search.RR n°8070