Reto Koenig
email: reto.koenig@unifr.ch

Rolf Haenni
email: rolf.haenni@bfh.ch

Stephan Fischli
email: stephan.fischli@bfh.ch

Preventing Board Flooding Attacks in Coercion-Resistant Electronic Voting Schemes

This paper addresses the board flooding problem of Juels et al.'s coercion-resistant electronic voting scheme. A key property of this scheme is the possibility of casting invalid votes to the public board, which are indistinguishable from proper votes. Exactly this possibility is crucial for making the scheme coercion-resistant, but it also opens doors for flooding the board with an enormous amount of invalid votes, therefore spoiling the efficiency of the tallying process. To prevent such attacks, we present an adaption of the scheme in which each voter receivesin addition to the proper credential-some dummy credentials from the election registrars. Dummy credentials may be used to deceive possible coercers. The list of all dummy credentials is published along with the electoral register. Based on the electoral register and the list of dummy credentials, the system is now capable of making a distinction between invalid votes generated from dummy credentials and invalid votes generated from fake credentials. While the former are kept until the tallying phase, the latter are immediately rejected by the public board. If the public board additionally rejects all incoming duplicate votes, then its maximum size is bounded by the total number of issued credentials. This guarantees an efficient linear-time tallying phase even in case of a massive board flooding attack with a very large number of invalid votes. Although the solution presented in this paper does not yet entirely rule out vote selling or coercion, it makes it at least unbearable for the vast majority of voters.

Introduction

One of the most challenging problems in remote electronic voting is the design of a system that prevents voters from selling their votes or from being coerced. The first scheme that is resistant against both the selling of votes and the coercion of voters has been proposed by Juels, Catalano, and Jakobsson in [START_REF] Juels | Coercion-resistant electronic elections[END_REF]. To achieve coercion-resistance (which implies mere receipt-freeness), the so-called "JCJ-scheme" uses an anonymous authentication mechanism to guarantee that the identities of the voters remain hidden during the whole voting and tallying process. The anonymous authentication mechanism requires that during the registration phase each voter receives a secret credential over an untappable channel. The knowledge of the secret credential allows the voter then to post an encrypted vote anonymously to the public board, such that its inclusion in the final tally is guaranteed. It is also possible to post invalid votes based on fake credentials, but those will be filtered out later during the tallying phase. Since board entries created from proper credentials are indistinguishable from those created from fake credentials, it is always possible to lie about the secret credential or to supply a coercer with a fake credential. The vote buyer or coercer will then see the posted invalid vote on the public board, but at this early stage of the protocol, there is no way to tell whether a particular board entry will be included in the final tally or not. This is the principal mechanism that renders the JCJ-scheme coercion-resistant.

The JCJ-scheme is the point of departure of most advanced protocols for remote electronic voting today dealing with coercion-resistance, but the protocol as presented in [START_REF] Juels | Coercion-resistant electronic elections[END_REF] has at least two major open problems. 3 The first problem is the quadratic running time of the tallying process, where duplicate and invalid votes need to be eliminated. Detecting duplicate votes requires so-called plaintext equivalence tests (PET) [START_REF] Jakobsson | Mix and match: Secure function evaluation via ciphertexts[END_REF] for every pair of votes cast, and detecting invalid votes requires each vote cast to be checked against the public electoral register, thus making the scheme quite inefficient for large scale elections. The Civitas system [START_REF] Clarkson | Civitas: Toward a secure voting system[END_REF], an implementation of the JCJ-scheme, weakens this problem by breaking up the electoral register into various independent blocks of a given fixed size. Several other improvements based on hash tables were proposed by Smith, Weber, and others [START_REF] Meister | eVoting with the European citizen card[END_REF][START_REF] Schweisgut | Coercion-resistant electronic elections with observer[END_REF][START_REF] Smith | New cryptographic voting scheme with best-known theoretical properties[END_REF][START_REF] Weber | On coercion-resistant electronic elections with linear work[END_REF][START_REF] Weber | Coercion-Resistant Cryptographic Voting: Implementing Free and Secret Electronic Elections[END_REF], but they have been shown to be vulnerable to Pfitzmann's attack against anonymous channels [START_REF] Pfitzmann | Breaking an efficient anonymous channel[END_REF]. More recent developments in this direction are based on group signatures [START_REF] Araújo | A practical and secure coercion-resistant scheme for remote elections[END_REF][START_REF] Araújo | Towards practical and secure coercion-resistant electronic elections[END_REF] or fake votes generated by the talliers [START_REF] Spycher | A new approach towards coercion-resistant remote e-voting in linear time[END_REF].

The second major problem of the JCJ-scheme results from the aforementioned possibility of posting invalid votes based on fake credentials to the public board. Exactly this possibility is crucial for making the scheme coercionresistant, but it also opens doors for flooding the public board with an enormous amount of invalid votes. Because invalid votes are indistinguishable from proper votes from the perspective of the public board, there are no direct countermeasures against such types of attack, i.e., as long as the incoming votes cast are well-formed and comply with the protocol, the public board needs to treat them all in the exactly same manner. A massive application-level flooding attack of that kind may therefore both jeopardize the availability of the public board and spoil the efficiency of the tallying process. To our best knowledge, no practical solution to this problem has yet been proposed in the literature. The problem itself seems to be intrinsic to the chosen approach.

In this paper, we propose an extension of the JCJ-scheme that addresses both aforementioned problems. The key idea is to equip the public board with a stronger filter on what is an acceptable vote cast. For this, the voters receive during the registration phase some dummy credentials (in addition to the secret credential), which may then be used to mislead potential vote buyers or coercers.

Invalid votes generated from these dummy credentials will be accepted by the public board (and filtered out later), but invalid votes from fake credentials will be rejected immediately. As we will see, enhancing the JCJ-scheme in such a way has a number of potential pitfalls. These pitfalls will be discussed and possible solutions will be presented.

The major benefit of our method results from the public board's ability to separate invalid votes created by fake credentials from those created by dummy credentials. Let n denote the number of voters, m the number of issued dummy credentials, and s the number of votes cast using fake credentials. Note that n and m are fixed during the registration phase, whereas s is unbounded (and possibly orders of magnitude larger than n + m). If we further assume that the public board is also capable of eliminating duplicate votes, we can introduce an upper limit n + m for the size of the public board.

Another important benefit of our approach is the fact that the known attacks against the linear-time improvements proposed by Smith [START_REF] Smith | New cryptographic voting scheme with best-known theoretical properties[END_REF] and Weber [START_REF] Weber | On coercion-resistant electronic elections with linear work[END_REF][START_REF] Weber | Coercion-Resistant Cryptographic Voting: Implementing Free and Secret Electronic Elections[END_REF] are no longer possible. The reintroduction of these improvements allows the elimination of all types of invalid votes (duplicate, fake, and dummy) in linear time, which reduces the total running time of the original JCJ tallying phase from O(n 2 + s 2 ) to O(n + m). If furthermore m = d • n for some constant d > 0 (the average number of dummy credentials issued per voter), then the tallying phase even runs in O(n) time.

Unfortunately, this unprecedented leap in performance and robustness has some negative effect with respect to perfect coercion-resistance. It is possible to minimize this effect to a small subset of unfortunate voters, which receive the minimum amount of dummy credentials, but some residual affliction will remain. The same holds true for vote buying. We will discuss this topic and see how to further minimize this problem.

The paper is organized in the following way. In Section 2, we give a short overview of the original JCJ-scheme and discuss its properties and problems. The proposed solution for the board flooding problem and the corresponding extension of the JCJ-scheme is discussed in Section 3. We first exhibit the general idea, then give a semi-formal sketch of the adapted protocol, and finally discuss some of the above-mentioned pitfalls. Section 4 concludes the paper.

Coercion-Resistant E-Voting

The goal of the scheme proposed by Jules, Catalano, and Jakobsson in [START_REF] Juels | Coercion-resistant electronic elections[END_REF] is to make remote electronic voting resistant against all sorts of coercion. Coercionresistance is defined as a stronger form of privacy. While privacy is defined in terms of an adversary that cannot interact with voters during the election process, it is assumed that a coersive adversary may interact with voters at any time. Thus an election scheme is called private, if the adversary cannot guess the vote of any voter better than an adversarial algorithm whose only input is the final tally, and the scheme is called coercion-resistant, if the adversary can be deceived into thinking that a coerced voter has behaved as instructed. Such a scheme thus prevents voters from selling their votes or from being coerced in various ways, e.g. to vote in a particular way, to vote at random, to abstain from voting, or even to divulge the private keying material [START_REF] Juels | Coercion-resistant electronic elections[END_REF].

The JCJ-scheme is the first electronic voting protocol that offers full coercionresistance under minimal assumptions. While many other protocols assume the existence of an untappable channel during the voting phase to offer mere receiptfreeness, an untappable channel is only required during the registration phase of the JCJ-scheme. Note that this assumption is realistic, because the registration process often requires the voters to visit the registration office in person. We will now briefly describe the JCJ-scheme in a semi-formal way. The main entities in the protocol beside the voters are the following:

Registrars They issue the secret credential to voter V i and pronounce corresponding encryptions publicly to the system. A threshold encryption system guarantees that the secret credential is only known to the voter and that the protocol is safe even if a minority of the registrars is corrupted or under attack. Tallying Authorities They are responsible for processing the votes cast, jointly decrypting and counting the votes, and publishing the final tally. Again, a threshold encryption systems guarantees the safety of the protocol even if a minority of the tallying authorities is corrupted or under attack.

The votes cast are published on an append-only public board. Its task is to accept and publish every well-formed vote cast that complies with the protocol.

To guarantee the integrity and availability of the board, it may be replicated in such a way that a minority of unavailable or corrupted board servers does not prevent its functioning properly as a whole [START_REF] Heather | The append-only web bulletin board[END_REF][START_REF] Peters | A Secure Bulletin Board[END_REF].

The whole voting protocol is divided into three major phases, during which the voters are authenticated anonymously. The protocol uses numerous cryptographic primitives such as encryption, digital signatures, non-interactive zeroknowledge proofs of knowledge, plaintext equivalence tests, re-encryption mixnets, anonymous channels, etc. A first overview of the protocol is given in Fig

- ure 1.
Registration Each voter V i , 1 ≤ i ≤ n, receives a secret credential σ i jointly generated by the registrars. This credential constitutes a proof of eligibility, which is used in the voting phase to cast the vote. Additionally, an encryption S i = Enc ε (σ i , γ i ) of σ i with randomness γ i is appended to the (digitally signed) electoral register on the public board. ε denotes the tallying authorities' common public key. The protocol assumes the majority of the registrars to be trustworthy and the channel between the registrars and V i to be untappable. Voting The voters cast their candidate selection c i ∈ C via an anonymous channel to the public board. The message posted to the board consists of Fig. 1. Overview of the original JCJ-scheme: the first filter eliminates votes with invalid proofs and duplicate votes from the public board, while the second filter checks the votes cast against the electoral register (and thus eliminates votes created from fake credentials).

A i = Enc ε (σ i , α i ) and B i = Enc ε (c i , β i ) along
a valid candidate choice is provided. This proof is needed to prevent the construction of receipts based on invalid candidate choices. Tallying The tallying authorities check the proofs included in the votes cast and jointly perform pairwise PETs on the encrypted credentials to eliminate duplicates. The resulting adjusted list of votes cast is shuffled in a verifiable re-encryption mix-net to anonymize the votes and credentials included.

Respective proofs of correct shuffling are published on the public board. Another verifiable re-encryption mix-net is applied to the electoral register, which finally allows the tallying authorities to jointly check the validity of the encrypted credentials involved in the votes cast (without decrypting them). Votes accompanied with fake credentials are discarded. The resulting adjusted list of proper votes is decrypted and tallied.

What makes this particular system coercion-resistant is the fact, that any posted entry to the public board is accepted if it is well-formed and complies with the protocol. It must thus consist of a valid candidate selection and some credential encrypted by the tallying authorities' common public key (together with corresponding proofs of knowledge). But the credential must not necessarily be a proper credential issued by the registrars and thus constituting a proof of eligibility, it simply needs to have the format of a proper secret credential. This enables the voter to deceive potential coercers with a fake credential, simply by choosing one at random. Votes accompanied with such fake credentials are discarded during the tallying phase. The two mix-nets involved in the tallying phase guarantee that no voter can prove to a third party whether a particular vote cast has been discarded before tallying or not. This feature makes the system resistant against selling votes or coercing voters.

Scheme by Smith and Weber [START_REF] Smith | New cryptographic voting scheme with best-known theoretical properties[END_REF][START_REF] Weber | On coercion-resistant electronic elections with linear work[END_REF][START_REF] Weber | Coercion-Resistant Cryptographic Voting: Implementing Free and Secret Electronic Elections[END_REF] Instead of applying PETs on all pairs of distinct votes for removing duplicates, both Smith and Weber in essence suggest computing and decrypting A z i = Enc ε (σ z i , α z i ), where z ∈ Z q is a random value shared among the talliers. The resulting blinded credentials σ z i are stored in a hash table for collision detection in linear time (clearly, σ i = σ j , iff σ z i = σ z j ). Both authors propose using the same procedure for eliminating votes created from fake credentials, but since the same exponent z is used across all ciphertexts A i , the coercer gets an attack strategy to identify whether a vote with known σ i is counted, namely by posting two votes, one that includes an encryption of σ i and one an encryption of σ 2

i [START_REF] Araújo | A practical and secure coercion-resistant scheme for remote elections[END_REF][START_REF] Clarkson | Civitas: Toward a secure voting system[END_REF][START_REF] Pfitzmann | Breaking an efficient anonymous channel[END_REF]. Note that this attack is not applicable to the mere removal of duplicates.

Preventing Board Flooding Attacks

In this section, we describe a way of modifying the JCJ-scheme to become resistant against board flooding attacks and to allow a linear-time tallying phase. As this implies several major and minor changes to the JCJ-scheme throughout various parts of the scheme due to different reasons, we uncover them step by step. A discussion of some important related questions follows in the second part of this section.

The Modified JCJ-Scheme

To protect the public board against application-level flooding attacks, it needs to be equipped with a stronger filter on what to accept. The main idea of our approach is to accept only votes cast from legitimate voters. Since it is crucial for the original JCJ-scheme to accept any vote cast, even those accompanied with a fake credential, it seems to be impossible in the first place to make such a distinction between legitimate and non-legitimate voters. But by introducing a third category of credentials, so-called dummy credentials, which are distributed to the voters during the registration phase (together with the proper secret credential), it is possible to reject all votes accompanied by fake credentials right from the beginning. Thus the idea is that the dummy credentials take over the role of deceiving potential vote buyers or coercers. This means that during the vote casting phase, they need to be treated in the same way as the secret credentials, whereas fake credentials are immediately rejected. In other words, voters are equipped with several access keys for posting votes to the public board, but only one of them is a key to include votes in the final tally. A first overview of the extended protocol is given in Figure 2.

More formally, let {τ ij : 1 ≤ j ≤ d i } be the set of dummy credentials for voter V i (note that that d i might be different for every voter, see Subsection 3.2). They are generated jointly by the registrars during the registration phase, together with V i 's secret credential σ i . Corresponding encryptions T ij = Enc ε (τ ij , γ ij ) with randomness γ ij are published on the public board together with S i = Enc ε (σ i , γ i ). The public board thus contains two separate lists of encrypted Fig. 2. Overview of the extended JCJ-scheme: the first filter discards votes created from fake credentials, the second filter removes duplicates, and the third filter checks the votes against the electoral register (and thus eliminates votes created from dummy credentials). The final list of proper votes is decrypted and counted. credentials: the original electoral register S = {S i : 1 ≤ i ≤ n} and the new set To detect fake credentials for filtering out corresponding invalid votes, the public board needs to check for each incoming vote cast whether the included encrypted credential matches with one of the entries in the list ST . We can safely apply Smith's and Weber's linear-time scheme here, because all votes based on arbitrarily fake credentials are already dropped at this early stage. Note that to install this first filter, we require the help of the talliers already during the voting phase. Compared to the original JCJ-scheme, this is a true disadvantage of our approach, but it is the key for restricting the size of the public board to an upper limit. To do so, the detection and removal of duplicate votes needs to be performed simultaneously, again by applying safely Smith's and Weber's scheme and with the help of the tallying authorities. In Figure 2, these tasks of the public board are called "Filter 1" and "Filter 2", respectively. Note that ST needs to be shuffled in a verifiable re-encryption mix-net, similar to the shuffling of S in the original JCJ-scheme. This is important for disguising the links between the voters and their entries in ST .

T = {T ij : 1 ≤ i ≤ n, 1 ≤ j ≤ d i } of
The rest of the tallying phase is similar to the original JCJ-scheme, except that the elimination of duplicate votes has already been conducted. Therefore both, the list of encrypted votes registered on the public board and the list S of encrypted secret credentials, are shuffled in corresponding re-encryption mix-nets. Respective proofs of correct shuffling are published. The output of the two mix-nets are then used to separate the valid votes from those generated by dummy credentials, again by applying safely Smith's and Weber's linear-time scheme. In Figure 2, this task is called "Filter 3". At the end, the adjusted list of encrypted votes is jointly decrypted and tallied by the tallying authorities.

Discussion

The above description of the adapted JCJ-scheme outlines the general ideas of our approach. The modifications raise several important questions. Some of them will be discussed below.

How many dummy credentials are needed?

To answer this question, suppose first that each voter receives exactly d ≥ 1 dummy credentials from the registrars, i.e., let d i = d for all 1 ≤ i ≤ n. Each voter would then have d extra credentials to deceive potential vote buyers or coercers. The problem of such a scenario is that the secret credential could only be withhold as long as not all d dummy credentials are "expended". A coercer could thus force the voter to release all d + 1 credentials and use them to cast d + 1 identical votes. If all d + 1 votes cast appear on the public board, it follows that one of them (the one that includes the proper credential σ i ) will be included in the final tally. Otherwise, if some of the votes cast do not appear on the public board, then the coercer knows that the voter was lying about some of the credentials. Using a similar line of reasoning, votes could be sold by passing all d + 1 credential to a vote buyer. Therefore, a constant number of dummy credentials clearly ruins the coercion-resistance property of the scheme.

The above argument leads to the conclusion that the registrars have to generate a varying number of dummy credentials for each voter. Suppose that V i receives d i ∈ R {1, . . . , d} dummy credentials, i.e., d i is chosen at random between 1 and a fixed upper limit d. If the scheme guarantees that d i is unknown to potential coercers (which includes the registrars and the tallying authorities), then V i may lie about d i , for example by passing all d i (or less) dummy credentials to the coercer and by claiming that the secret credential is included in that list. This argument works for every V i with d i > 1, but unfortunately not for those with d i = 1. Under coercion, such (unfortunate) voters could only give away a single dummy credential, but they could not claim it to be the secret credential. Note that this problem does not disappear by increasing the lower limit of the interval {1, . . . , d} to some value c < d or by decreasing it to 0. Even worse, a similar problem exists for the upper bound d, because voters with d i = d dummy credentials could sell their votes by simply handing over all d + 1 credentials to the vote buyer (as in the case of a constant number of dummy credentials). This problem could be solved by not imposing an upper limit to the interval, but this brings up new problems of practicability in cases where d i becomes very large.

As an answer to the above question, we suggest here that d i , the number of dummy credentials for voter V i , is determined according to some non-uniform probability distribution over sets N d = {1, . . . , d} or N = {1, . . . , ∞} of natural numbers. 4 The most natural candidate distribution with an upper limit d is a binomial distribution B(d, p) with shape parameters d and p. The idea is to choose d and p such that only a very small fraction of voters get the minimum number (d i = 1) or the maximum number (d i = d) of dummy credentials. This is the case if the variance of the distribution is relatively small compared to d. In this way, we cannot entirely rule out vote selling or coercion, but we can at least make it unbearable for the vast majority of voters.

The most natural candidate distribution with no upper limit is a normal distribution N (µ, σ 2 ) with some reasonable values for the mean and the variance. Since normal distributions are density functions defined over R, they need to be applied in some discretized manner over N. Many other distributions are possible, but a more exhaustive discussion of this questions is beyond the scope of this paper.

How do the registrars generate a random number of dummy credentials? The naïve approach for the registrars to generate a random number of dummy credentials for voter V i is to jointly apply the chosen probability distribution to determine d i and to generate each of the d i dummy credentials using the same distributed procedure as for the secret credential σ i . The problem of this simple approach is that d i is not a secret of V i alone, i.e., V i cannot lie about it towards potential voter buyers or coercers if they collude with one of the registrars.

As a solution to this problem, we suggest to split up the group of registrars into r sub-groups. Each of these sub-groups is then responsible for generating roughly d i /r dummy credentials, but without informing the other groups about the exact number. To do so, we need to decompose the chosen probability function into a sum of r probability functions with parameters adapted accordingly. In the case of a binomial distribution B(d, p), for example, each sub-group may simply use the distribution B(d/r, p) to determine their numbers independently, because B(d, p) = r•B(d/r, p). Similarly, a normal distribution N (µ, σ 2 ) can be split up into a sum of r normal distributions N (µ/r, σ 2 /r 2 ), because normal distributions are closed under linear combination. Note that we need to assume a majority of each sub-group to be trustworthy.

How should the public board store the encrypted dummy credentials? In the original JCJ-scheme, the encrypted credentials S i are published on the public board together with the plaintext identities of the voters. The list S plays thus the role of a electoral register, which can be inspected and verified by everybody. By doing the same with the encrypted dummy credentials, i.e., by linking each T ij ∈ T publicly with V i 's identity, we would allow potential coercers or vote buyers to derive the secret number d i = |{T ij ∈ T }| from T . But as already discussed above, coercion-resistance can only be guaranteed as long as d i is V i 's secret, since otherwise V i looses the ability to lie about it.

As a simple solution to this problem, we suggest that the set T of encrypted dummy credentials is published anonymously without any links to the voters. Since T does not serve as an electoral register, it does not necessarily need to be treated in exactly the same way as S. However, this solution is only applicable if deleting entries from the electoral register is prohibited over multiple voting events. Otherwise, additional mechanisms need to be introduced to delete the entries in T that belong to the deleted entry in S.

What is the benefit of the modified scheme? The original JCJ-scheme has three critical time-consuming components: the elimination of duplicates, the mixing of the votes in the re-encryption mix-net (as well as the verification of the proofs produced by the mix-net), and the elimination of invalid votes (see Figure 1). The input size of each of these components depends directly on the number of votes, not the number of voters. Since costly cryptographic computations such as zero-knowledge proofs and multi-party computations are needed to perform these tasks, processing a single additional vote is expensive. Techniques that avoid the processing of votes that will not appear in the final tally are therefore inherently appealing.

Let n = |S| denote the number of voters (or the number of proper votes if all voters participate in the election) and s the number of duplicate or invalid votes. In the original JCJ-scheme, eliminating duplicates by performing pairwise PETs over all n+s votes requires O(n 2 +s 2 ) relatively expensive steps. If no duplicates are removed (worst case), n+s is the input size for both the re-encryption mix-net and the final procedure for eliminating fake votes. In the literature of verifiable mix-nets, we find techniques with proofs of linear size [START_REF] Groth | A verifiable secret shuffle of homomorphic encryptions[END_REF][START_REF] Neff | A verifiable secret shuffle and its application to e-voting[END_REF][START_REF] Wikström | A commitment-consistent proof of a shuffle[END_REF], but all of them involve relatively high constant factors. The final elimination of fake votes again requires O(n 2 +n•s) expensive PETs. In total, the JCJ-scheme runs in O(n 2 +s 2 ) time and O(n + s) space.

Our modified approach improves the overall performance of the scheme in respect of both, computation time and memory space. Note that we have the same three critical components, only arranged in a different order. If m = n i=1 d i = |T | denotes the total amount of dummy credentials issued during the registration phase, we get an O(n + m) upper limit for both the size of the public board and the input of the mix-net. As s may become orders of magnitudes larger than m in case of a large scale board flooding attack, this states a major improvement over the original scheme. It prevents situations where the system becomes unavailable due to a memory overflow of the public board.

The modified scheme also eliminates the need for the quadratic number of PETs for eliminating invalid votes. Here we benefit from the methods proposed by Smith [START_REF] Smith | New cryptographic voting scheme with best-known theoretical properties[END_REF] and Weber [START_REF] Weber | On coercion-resistant electronic elections with linear work[END_REF][START_REF] Weber | Coercion-Resistant Cryptographic Voting: Implementing Free and Secret Electronic Elections[END_REF], which allow duplicate and fake votes to be detected in linear time. Therefore, all components involved in the tallying phase run in O(n + m) time and space, which implies an overall O(n + m) running time for the whole modified scheme. This is a considerable improvement over the original scheme under all possible circumstances.

What is the downside of the modified scheme? In the presented form, our scheme allows statistical attacks which may possibly influence the outcome of a voting event. For example, a vote buyer may offer a certain amount of money for each additional credential (dummy or proper) handed over by the voter. In this way, a potential vote seller gets a personal interest in handing over as many credentials as possible-including the proper one. An analogous strategy may be applied by the coercer. However, depending on the total number of dummy credentials and the parameters of the chosen distribution function, these attacks may become very cost-intensive for both, the vote buyer and the coercer. This raises the question of finding the optimal distribution function to maximize the cost of such statistical attacks. Answering this question is beyond the scope of this paper and is left for future work.

Conclusion

In this paper, we have discussed the board flooding problem in the JCJ-scheme for remote electronic elections. As a solution, we propose that each voter receives a set of dummy credentials along with the proper secret credential during the registration phase. For this enhancement to work, it is important that the number of dummy credentials varies from one voter to an other, and that only few voters will get the minimum or maximum number of dummy credentials. The votes posted to the public board can then be filtered such that only votes created from proper or dummy credentials are retained. Duplicate votes are also immediately eliminated in linear time. In this way, there will never be more entries on the public board than the total number of issued (proper and dummy) credentials. The lack of such a filter leads to the board flooding problem in the JCJ-scheme.

This paper is a first step in transforming the impractical JCJ-schemeapplicable under the assumption of unrealistic computing power only-into a practical scheme. Our proposal allows the voting authorities to trade-off the efficiency of the tallying procedure against the obtained level of coercion-resistance. Future work will focus on the residual statistical vulnerability for coercion and vote buying. Currently, we are studying the possibility of obtaining additional dummy credentials on demand during the voting phase, for example by exchanging dummy credentials between voters.

  dummy credentials. With ST = S ∪ T we denote the complete set of encrypted credentials. Furthermore, we denote the number of all issued dummy credentials by m = |T | = n i=1 d i , which implies that a total of |ST | = n + m credentials have been issued in all. Those are the ones that will be accepted by the public board during the vote casting phase.

  with corresponding zeroknowledge proofs of knowledge of σ i and c i . It is important that the candidate set C is finite and that an additional disjunctive proof that c i represents

	Registrars
	Electoral Register			Re-Encryption Mixnet
	Encrypted Votes	Filter 1	Re-Encryption Mix-Net	Filter 2	Encrypted Votes	Decrypt	Decrypted Votes
	Voters
			Tallying
			Authorities

Further major and minor problems of the JCJ-scheme are discussed in[START_REF] Meng | A critical review of receipt-freeness and coercion-resistance[END_REF][START_REF] Smith | New cryptographic voting scheme with best-known theoretical properties[END_REF].

We explicitly exclude the borderline case di = 0, because it would completely disallow Vi to deceive a passive coercer who does nothing but directly observing Vi's vote casting process (shoulder surfing attack).

Acknowledgments. Research supported by the Hasler Foundation (project No. 09037).


Benjamin Kellermann
email: benjamin.kellermann@tu-dresden.de

Privacy-Enhanced Web-Based Event Scheduling with Majority Agreement

Keywords: event scheduling, electronic voting, superposed sending, anonymity, privacy-enhanced application design

Applications which help users to schedule events are becoming more and more important. A drawback of most existing applications is, that the preferences of all participants are revealed to the others. Previously proposed privacy-friendly solutions could only schedule meetings if all participants were available at the same time slot. We propose a new scheme, which overcomes this limitation, i.e., the meeting can be scheduled at the time slot, where just the majority of participants is available. Dudle (http://dudle.inf.tu-dresden.de), a web-application which implements the protocol is presented. We measured its performance in order to show that the protocol is practical and feasible.

Introduction

There are numerous Web 2.0 applications (e.g., doodle.com, moreganize.ch, . . .), which allow users to create polls. The most important use case of these applications is to schedule events. They all have in common, that they disclose detailed availability patterns of their users. These patterns contain sensible information in at least two respects. First, one is able to read information directly out of such a pattern ("Does my boss work after 3pm?"). Secondly, due to the fact, that these patterns contain much entropy, one is able to connect them with other information sources easily to read indirect information and re-identify participants who would otherwise remain pseudonymous ("This availability pattern looks like Peters who goes to lunch everyday at 11:30."). All existing applications for event scheduling allow some privacy settings, but none of them tries to overcome the need of complete trust in the application server and the poll initiator.

A privacy-friendly and verifiable solution for scheduling a single event, which reveals only the sum of available participants at every time slot was proposed [START_REF] Kellermann | Privacy-enhanced event scheduling[END_REF]. Despite being efficient enough for a Web 2.0-implementation, it has the drawback that unanimous agreement is required for resisting internal attacks.

In this paper we present, a better solution for the problem of internal attackers. Therefore we discuss two extensions to the original protocol described in [START_REF] Kellermann | Privacy-enhanced event scheduling[END_REF]. These extensions prevent internal attacks and allow majority agreement simultaneously.

There are several approaches dealing with event scheduling. It can be seen as distributed constraint satisfaction / optimization problem (DCSP/DCOP) or as an instance of electronic voting.

Many algorithms for DCSP [START_REF] Silaghi | Asynchronous search with aggregations[END_REF][START_REF] Yokoo | Algorithms for distributed constraint satisfaction: A review[END_REF][START_REF] Léauté | Privacy-preserving multi-agent constraint satisfaction[END_REF] and DCOP [START_REF] Modi | Adopt: Asynchronous distributed constraint optimization with quality guarantees[END_REF][START_REF] Maheswaran | Taking DCOP to the real world: Efficient complete solutions for distributed multi-event scheduling[END_REF][START_REF] Mailler | Solving distributed constraint optimization problems using cooperative mediation[END_REF] exist and measurements of the information leakage were done [START_REF] Franzin | Multi-agent meeting scheduling with preferences: Efficiency, privacy loss, and solution quality[END_REF][START_REF] Greenstadt | Experimental analysis of privacy loss in DCOP algorithms[END_REF]. With the help of these algorithms, complex scheduling problems may be solved (e. g., scheduling of many events, where different subsets of the participants participate in each event with constraints about place, travel time etc.). However, all DCOP algorithms share the problem that they are complex in terms of message exchanges even for basic scenarios. To solve the problem of message exchanges, agents are used, which send and receive the messages. As users do not want to setup such an agent at some server, they have to run it locally and have to be online at the same time. Therefore, the DCOP approach is too complex in terms of message exchanges to be implemented in a web application and a simpler solution for the simpler problem of scheduling a single meeting would be appropriate.

There is a lot of literature about electronic voting [START_REF] Chaum | Untraceable electronic mail, return addresses, and digital pseudonyms[END_REF][START_REF] Fujioka | A practical secret voting scheme for large scale elections[END_REF][START_REF] Benaloh | Receipt-free secret-ballot elections[END_REF][START_REF] Sako | Receipt-free mix-type voting scheme: a practical solution to the implementation of a voting booth[END_REF][START_REF] Cramer | A secure and optimally efficient multi-authority election scheme[END_REF][START_REF] Hirt | Efficient receipt-free voting based on homomorphic encryption[END_REF][START_REF] Juels | Coercion-resistant electronic elections[END_REF], some of them lead to implementations [START_REF] Herschberg | Secure electronic voting over the world wide web[END_REF][START_REF] Adida | Helios: Web-based open-audit voting[END_REF][START_REF] Clarkson | Civitas: Toward a secure voting system[END_REF]. 4 observations occur, when event scheduling is done with e-voting: (1) Only the sum of available participants, not the single availabilities, can be used to schedule the time slot. (2) The short ballot assumption [START_REF] Rivest | Three voting protocols: Threeballot, vav, and twin[END_REF] does not hold as the availability pattern contains much entropy and there are few voters (participants). ( 3) All participants have to be voting officials to minimize trust in other entities. (4) Coercion resistance is not necessarily required.

To overcome the short ballot assumption, one has to apply an e-voting scheme for every time slot, which is scheduled. However, if the computational complexity of the scheme depends on the number of time slots and the number of participants (voting officials, assumption 3), an application will exceed the possibilities of current browsers. To illustrate this, we implemented a performance measurement for a discrete exponentiation modulo a 786 bit long integer using different libraries and browsers. We measured 3 of the 5 investigated libraries. The remaining two were too slow to be mentioned here. If, e.g., a scheme would need only one asymmetric operation per time slot and participant and a concrete poll would ask for 20 time slots for a meeting with 5 participants, the scheme would need only for the asymmetric operations about 5 • 20 • 0.78 s = 78 s, using the BigInteger Library of Wu on a Firefox 3.6, IE 8 would be blocked for at least 4 minutes. Having a low computation complexity is even more important considering small mobile devices like smartphones (cp. the last column of Table 1).

Besides e-voting, there are two specific schemes, which try to solve event scheduling in a privacy-friendly way [START_REF] Kellermann | Privacy-enhanced event scheduling[END_REF][START_REF] Herlea | On securely scheduling a meeting[END_REF], both offering unanimous agreement only. The main idea of [START_REF] Kellermann | Privacy-enhanced event scheduling[END_REF] is to use DC-Net [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF] to calculate the sum of available participants to the time slots. Therefore, a dedicated DC-Net round is executed for every nominated time slot. Each participant sends an encrypted 1 in the specific round if he is available at the time slot, and 0 otherwise. Through the homomorphism in the DC-Net, the sum of the votes is calculated. The result of one DC-Net round is the number of available participants at this time slot. The main problem of using the DC-Net is that a participant may send values different from 0 or 1. I.e., a participant may send values below 0 to lower the chance for a specific time slot of being chosen, and values above 1 to increase it. An example of this is illustrated in Fig. 1. The tables show two polls with 3 participants and 4 time slots (𝑡 0 , . . . , 𝑡 3 ). The unencrypted votes are shown inside each table (𝑣 𝑢,𝑡 ∈ {0, 1}). Mallory manipulates the poll in a way that time slot 𝑡 3 results in the largest sum. Because of the anonymization of all messages through the DC-Net, Mallory's attack is hidden to Alice and Bob.

𝑡0 𝑡1 𝑡2 𝑡3 Alice 0 1 0 0 Bob 1 1 0 1 Mallory -1 -1 -1 1 ∑ 0 1 -1 2 (
In the following, we will discuss how to extend the original protocol [START_REF] Kellermann | Privacy-enhanced event scheduling[END_REF] in a way that sending values different from 0 or 1 can be prevented without the need of unanimous agreement (which was used there to overcome the problem).

Preventing (-1)-Attacks

The main idea for preventing (-1)-attacks is the fact that the results of a DC-Net at some time slot must not be lower than 0. I.e., in Fig. 1a the attack cannot be detected at time slot 𝑡 0 and 𝑡 1 , but it is visible at time slot 𝑡 2 , where the result is -1. If all participants are honest, the result of every time slot should be a value between 0 and the number of all participants.

Instead of using one dedicated DC-Net round for every time slot, we use several simultaneously running DC-Net rounds. Let 𝐼 be the number of simultaneously running DC-Net rounds (we will see later in this section, that 𝐼 should be chosen in some dependence of the number of participants). Every participant 𝑢 splits each vote 𝑣 𝑢,𝑡 ∈ {0, 1} into 𝐼 partial votes v𝑢,𝑡,0 , . . . , v𝑢,𝑡,𝐼-1 such that:

1. An index 𝑗 ∈ Z 𝐼 for one partial vote is chosen randomly and kept secret. 2. The partial vote with index 𝑗 (v 𝑢,𝑡,𝑗 ) is equal to the actual vote 𝑣 𝑢,𝑡 . 3. The remaining 𝐼 -1 partial votes are equal to 0.

Let 𝑇 be the set of time slots, 𝑈 the set of participants of the poll, 𝜎 𝑡 the number of available participants at time slot 𝑡, k𝑢,𝑢 ′ ,𝑡,𝑖 the DC-Key between two voters, and d𝑢,𝑡,𝑖 the encrypted vote within a DC-Net round ( d𝑢,𝑡,𝑖 = v𝑢,𝑡,𝑖 + ∑ 𝑢 ′ ∈𝑈,𝑢 ′ ̸ =𝑢 k𝑢,𝑢 ′ ,𝑡,𝑖 ). If all participants are honest, the following properties result from the construction:

1. For all time slots 𝑡 ∈ 𝑇 and partial vote indices 𝑖 ∈ Z 𝐼 , the sum of all partial votes of all participants is an element between 0 and the number of participants (∀𝑡, 𝑖 : ∑ 𝑢∈𝑈 v𝑢,𝑡,𝑖 = ∑ 𝑢∈𝑈 d𝑢,𝑡,𝑖 ∈ {0, . . . , |𝑈 |}). 2. At one time slot, the sum of all partial votes of all participants is the sum of all available participants at this time slot (𝜎 𝑡 = ∑ 𝑢∈𝑈,𝑖∈Z 𝐼 v𝑢,𝑡,𝑖 ).

In Fig. 1, we have seen that an attacker has to guess at which time slot a honest participant will send a 1. With the proposed extension it is not sufficient for the attacker Mallory to guess the availability of another participant, she further has to guess at which partial vote the actual vote was sent. This is difficult as long as the chosen partial vote index is random, kept secret, and the number of partial votes per time slot Z 𝐼 is sufficiently high.

Fig. 2 shows an example of the vote vector splitting with 𝐼 = 3, where Mallory tries to send a -1 at 𝑡 1 (𝑣 𝑢𝑚,𝑡1 = -1). The left table shows the original protocol. There the attack would remain undetected as all elements of the result vector are in the allowed range. The right table shows the same vote vectors split into several vectors. There, for time slot 𝑡 1 Alice has chosen the first table (𝑖 = 0) for her vote (v 𝑢𝑎,𝑡1,0 = 𝑣 𝑢𝑎,𝑡1 = 1) and Bob has chosen the second one. As Mallory has chosen the third table (𝑖 = 2) her attack can be detected.

Note, that the enrypted vote vectors must not be published until the last participant has sent his vector. Otherwise, if the server would cooperate with Mallory, she may wait until all other participants sent their vote and then calculate the preliminary result before casting her own vote. This allows her to state -1s where other participants sent a 1. As already stated in the original protocol, this restriction can be relaxed with one additional communication phase in which all voters have to commit to their votes [START_REF] Kellermann | Privacy-enhanced event scheduling[END_REF].

Verifiability

When verifying that no attack occurred, we can distinguish two cases: (1) In the simpler case, one DC-Net round results -1 ( ∑ 𝑢∈𝑈 d𝑢,𝑡,𝑖 = -1). This case occurred in the example in Fig. 2. (2) In a more complex scenario, some participant sent a 1 in some DC-Net round, but the result equals 0 due to a (-1)-attack. This may also occur in the original protocol. Bob for example can detect that Mallory has cheated at 𝑡 0 in Fig. 1a. However, to prove that Mallory has cheated at 𝑡 0 , Bob has to give up his privacy. In such a case, Bob can decide for himself what is worth more, his privacy or to unmask Mallory. We first discuss the case where privacy is the most valuable good, and we discuss situations later where participants are willing to give up their privacy for unmasking attackers. For reasons of simplicity, we write all calculations which are done in the DC-Net without the modulo operations. We consider only 1 attacker.

𝑡0 𝑡1 𝑡2 𝑡3 Alice 0 1 0 0 Bob 1 1 0 1 Mallory 0 -1 0 1 ∑ 1 1 0 2 𝑡0 𝑡1 𝑡2 𝑡3 Alice 0 1 0 0 𝑖 = 0 Bob 0 0 0 0 Mallory 0 0 0 0 ∑ 0 1 0 0 Alice 0 0 0 0 𝑖 = 1 Bob 0 1 0 1 Mallory 0 0 0 1 ∑ 0 1 0 2 Alice 0 0 0 0 𝑖 = 2 Bob 1 0 0 0 Mallory 0 -1 0 0 ∑ 1 -1 0 0 ∑ 1 1 0 2 Fig. 2.
Without Privacy-Loss Checking the correctness of a poll can be expressed by a function. It takes all messages sent within the poll and returns true if the poll was correct, and false otherwise 𝒱 : Z |𝑈 |×|𝑇 |×𝐼 → {true, false}. Let d ∈ Z |𝑈 |×|𝑇 |×𝐼 be the 3-dimensional array of all DC-Net messages containing elements of d𝑢,𝑡,𝑖 for a DC-Net message from participant 𝑢 at time slot 𝑡 and partial vote index 𝑖. The function which checks the correctness of the poll is defined as:

𝒱( d) = { true if ∀𝑡 ∈ 𝑇, 𝑖 ∈ Z 𝐼 : ∑ 𝑢∈𝑈 d𝑢,𝑡,𝑖 ∈ {0, . . . , |𝑈 |} false otherwise. ( 1
)
We assume one attacker Mallory (𝑢 𝑚 ) who tries to send a -1 at time slot 𝑡. With an increasing amount of participants, voting for 𝑡, the probability of detection would decrease. In a worst case scenario w.r.t. detecting attackers all honest participants (|𝑈 | -1) send a 1 for all time slots and therefore the lower bound of the probability to detect the attack is

𝑃 (𝒱( d) = false | 𝑣 𝑢𝑚,𝑡 = -1) ≥ ( 𝐼 -1 𝐼 ) |𝑈 |-1 . (2)
The probability of successfully performing an attack would increase with an increasing number of participants. Therefore, one should choose the number of DC-Net rounds 𝐼 dependent on the number of participants. If Mallory tries to send a -2 the chance of detection increases, but this is out of scope of this paper.

With Privacy-Loss We already discussed that a person who sent a 1 in a DC-Net which results in 0 is in the position to unmask the attacker with the drawback of giving up his privacy. 1 For such a case, we can define another function checking the correctness of the poll. This function will return false if there exists a participant 𝑢 𝑝 , who can prove that he sent a 1 at a time slot 𝑡 and DC-Net round with partial vote index 𝑖 which resulted in 0 ( ∑ 𝑢∈𝑈 d𝑢,𝑡,𝑖 = 0).2 Let k ∈ Z |𝑈 |×(|𝑈 |-1)×|𝑇 |×𝐼 be the 4-dimensional array of all keys used in all DC-Nets of the poll. The function which checks the correctness of the poll under the assumption that all participants are willing to disclose their availability at one time slot to unmask an attacker is defined as

ℬ ( d, k) = ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ true if ¬∃𝑢 𝑝 ∈ 𝑈, 𝑡 ∈ 𝑇, 𝑖 ∈ Z 𝐼 : (∑ 𝑢∈𝑈 d𝑢,𝑡,𝑖 = 0 ) ∧ ( d𝑢𝑝,𝑡,𝑖 + ∑ 𝑢∈𝑈,𝑢̸ =𝑢𝑝 k𝑢𝑝,𝑢,𝑡,𝑖 = 1
) false otherwise.

(3) Now, Mallory needs two honest participants sending a 1 in the same DC-Net round to hide her (-1)-attack under these assumptions. 3 The probability that this attack is detected is calculated by adding the probabilities of the two cases (1) nobody choses Mallory's DC-Net, and (2) one participant choses Mallory's DC-Net. For case 1, the sum of the attacked DC-Net will be -1 and therefore 𝒱( d) will fail (see Equation 2). The lower bound 4 for the probability of case 2 is the probability where the output of ℬ ( d, k) is false and can be calculated with

𝑃 (ℬ ( d, k) = false | 𝑣 𝑢,𝑡 = -1) ≥ (|𝑈 | -1) • 1 𝐼 • ( 𝐼 -1 𝐼 ) |𝑈 |-2 . (4)
Note that it is not possible, that 𝒱( d) = false and ℬ ( d, k) = false (cp. Footnote 2) if we stick to only one attack at one time and therefore we can add the probabilities of Equations 2 and 4 to get the overall probability of detecting a (-1)-attack if users are willing to disclose their availability to unmask attackers.

Summary Table 2 illustrates these formulas with some example values. One can see that splitting the vote vector into 20 partial vote vectors makes it rather unlikely to perform an undetected attack against small polls with 5 participants.

The chance to detect a (-1)-vote at each time slot is at least 5 81.5 %. Additionally to these 81.5 %, the attack can be discovered with a probability of 17.1 % by one of the participants. If all participants are willing to disclose their availability at the attacked time slot, the detection probability is at least 98.6 %.

In case of 𝒱( d) = false, the decryption of the DC-Net round can be requested where the invalid value occured. Therefore every participant has to reveal his key for the DC-Net round. The single votes can be decrypted with the keys which identifies the attacker. The attacker may modify her key to hide her attack in this phase. However, this can be prevented in the same way as it was proposed for the verification phase of the original protocol.

However, if availabilities should not be disclosed under any circumstances, the attacker identification phase may be skipped. One has to accept in this case that attackers are able to perform denial of service attacks anonymously. Then one may decide with function 𝒱( d) (Equation 1) that some attack occurred, but skip revealing keys to avoid possible decryption of votes. Note that the decision to perform a poll with identification phase or without has to be accepted by all participants. If every participant may decide on his own, an attacker will always refuse to reveal her keys, stating she has to cover some vote.

If a participant discovers an attack with the function ℬ ( d, k) , he may decide on his own if he gives up his privacy to unmask the attacker. Therefore, the lower bound for the probability of detecting an attack is between both lower bounds.

Privacy

The possible decryption in the identification phase to detect the attacker may be a privacy problem. The original protocol had the same decryption in the verification phase. However, unlike in the original protocol, the probability that this really is a privacy problem is very low, as the attacker has to guess the index for the DC-Net round where the victim sent his vote. The probability of guessing the index of a specific victim is 1 𝐼 . Attacking more than one DC-Net round with negative values to increase the probability of hitting the victim's DC-Net does not help the attacker, because the goal of the honest participants is to find only one DC-Net which was attacked. Therefore, it is enough to disclose the keys for one attacked round. The algorithm to choose the DC-Net round to be disclosed should choose one of the rounds with the lowest sum. The function 𝒟 : Z

|𝑈 |×|𝑇 |×𝐼 𝑛

→ 𝒫(𝑇 × Z 𝐼 ) which takes all DC-Net messages as input, and results a set of time slot-partial vote index-pairs (𝑡, 𝑖) which should be disclosed, can be defined as

𝒟(𝑑) = { (𝑡, 𝑖) : ∑ 𝑢∈𝑈 d𝑢,𝑡,𝑖 = min 𝑡 ′ ∈𝑇,𝑖 ′ ∈Z 𝐼 { ∑ 𝑢∈𝑈 d𝑢,𝑡 ′ ,𝑖 ′ }} . (5)
However, as already discussed in Section 3.1, one may decide to skip attacker identification, with the drawback, that denial of service attacks are possible then.

The privacy of a message in the DC-Net depends only on the secrecy of the keys. This is the same for the original as well as the new protocol but splitting the vote vector into several parts introduces a new point of attack. Now, the anonymity of the message also depends on the randomness and secrecy of the partial vote index. If an attacker can predict at which DC-Net rounds messages from some participants occur, she can separate the other messages into smaller anonymity sets. If all participants distribute their votes randomly over all rounds, Mallory needs the cooperation of the other participants to deanonymize her victim. However, deanonymization can be done without the help of the different partial DC-Nets, if participants disclose their shared DC-Net keys.

In a successful schedule with no attacker, one sum for every time slot with the number of all available participants is disclosed.

Preventing (+2)-Attacks

In the example of Fig. 1b, Alice can detect a (+2)-attack of Mallory as she knows that the sum is an element of {0, . . . , |𝑈 | -1}. However, it may be the case that nobody voted for a time slot (cp. e.g., time slot 𝑡 2 of Fig. 1b) where a 2 is sent. In such a case neither Alice nor Bob can detect the attack on their own.

A simple solution to this attack would be to request the verification phase in any case for the agreed time slot. This would neither be privacy-friendly nor efficient in terms of message exchanges.

In the following, another solution is proposed. The main idea is to reduce the problem of preventing (+2)-attacks to the already solved problem of preventing -1-attacks. Therefore, in addition to the normal poll, every participant sends his votes for the same time slots in a check poll. Every participant 𝑢 calculates for every time slot 𝑡 a check vote 𝑣 ′ 𝑢,𝑡 which depends on his vote 𝑣 𝑢,𝑡 such that

𝑣 𝑢,𝑡 + 𝑣 ′ 𝑢,𝑡 = 1. (6)
With the check votes 𝑣 ′ 𝑢,𝑡 , a check poll is done like for the normal poll. The sum of both result vectors, the one from the normal poll and the one from the check poll, should be a vector where all elements are equal to the Fig. 3. By the use of a check poll, the (+2)-attack can be reduced to the (-1)-attack.

Mallory has to send a -1 at 𝑡3 in the right table, because the sum regarding 𝑡3 of both tables would not be equal to the number of participants otherwise.

number of participants |𝑈 |. By checking this property, it is ensured that every participant calculated the check vote vector according to Equation 6. If Mallory wants to send a 2 for some time slot, she then has to send a -1 in the check poll. However, splitting the check vote vector into several ones, this attack can be prevented in the same way (-1)-attacks were prevented within the vote vector.

Verifiability

When evaluating the result, two kinds of inconsistencies may occur: the sum of both polls may be lower or higher than the number of participants. As we split the votes into several ones (cp. Section 3), we do not consider (-1)-attacks at this point. Therefore, a value lower than the number of participants may occur only if one or more participants sent 𝑣 𝑢,𝑡 = 𝑣 ′ 𝑢,𝑡 = 0. Having such a case would mean that the number of available participants 𝜎 𝑡 would be the result of the normal poll at least. The difference of the sum of both polls and the total number of participants are wrongly cast votes.

The second kind of inconsistency is if the sum of both polls is higher than the number of participants. As we prevented (-1)-votes, the result of the normal poll at a time slot 𝑡 should be greater or equal than the number of available participants at this time slot. In addition, the number of available participants is greater or equal than the total number of participants minus the result of the check poll at a certain time slot. Putting both inequations together, one obtains a range which expresses the possible number of available participants:

∑ 𝑖∈𝐼,𝑢∈𝑈 d𝑢,𝑡,𝑖 ≥ 𝜎 𝑡 ≥ |𝑈 | - ∑ 𝑖∈𝐼,𝑢∈𝑈 d′ 𝑢,𝑡,𝑖 . (8)
Table 3. Comparison of the computational complexity of the original protocol with unanimous agreement and the scheme with our extension (assuming no attack). discrete exp. symmetric decr. hash values

original protocol |𝑈 | -1 |𝑇 | • (|𝑈 | -1) |𝑇 | • (|𝑈 | -1) new scheme |𝑈 | -1 2 • 𝐼 • |𝑇 | • (|𝑈 | -1) 2 • 𝐼 • |𝑇 | • (|𝑈 | -1)
However, as an attacker may manipulate his vote in a way that this range results in {0, . . . , |𝑈 |}, he may attack the availability of the poll in such a way. To unmask the attacker, all DC-Net rounds for the inconsistent time slot can be decrypted as shown before. If the attack discovery goes along with some cost (penalty, reputation loss, etc.), it makes such attacks unattractive.

Privacy

During the verification phase of an inconsistent check poll, the availability of all participants at the inconsistent time slot are disclosed. To avoid disclosure of all availabilities, one may disclose the DC-Net rounds step by step and stop when the attacker is found. The sequence of disclosure should therefore be a fixed order, which is not known before every participant stated his vote. 6In a successful run, no more information is disclosed than in the original protocol, the check poll contains only redundant information.

Computational Complexity

The extension presented in this paper affects the computational complexity of the original protocol only in terms of symmetric cryptographic operations, i.e., the amount of asymmetric cryptographic operations is not affected. The number symmetric operations of the original scheme increases with the number of DC-Net rounds 𝐼 and is doubled due to the check poll. Table 3 compares the complexity of our extension with the complexity of the original protocol.

Implementation

An implementation of the protocol is available at dudle.inf.tu-dresden.de. The cryptographic operations are implemented in JavaScript; no installation on the client side is needed.

The implementation has been done using the JavaScript BigInteger library from Tom Wu [START_REF] Wu | BigIntegers and RSA in JavaScript[END_REF]. Like in the original protocol, a symmetric cipher and a hash function is used for key generation. AES-128 and SHA-256 from the JavaScript libraries of B. Poettering are used here [START_REF] Poettering | The AES block cipher and the SHA256 message digest in JavaScript[END_REF]. Table 4 shows a performance measurement of the key calculation for an example poll. One can see, that the calculation needs about 23 s, using Firefox 3.6.12. If browsers run a script which needs longer calculation time, it is usual that the browser asks the user if he wants to stop the script. To avoid these pop-ups, the BigInteger library was modified in a way that it calculates exponentiations asynchronously with a callback function. This enables the calculation to be forked in the background and the browser remains responsive. The user can enter his availabilities, while the browser calculates the keys. The submit button is enabled after the calculation has been done. Assuming, that a user needs some time to enter his preferences (look up the time slots in his personal calendar, click the buttons etc.), there is no extra waiting time.

Conclusion

We proposed a scheme, which is able to schedule events in a privacy-enhanced way. Our scheme prevents attacks to neglect or promote certain time slots, has no negative influence on the privacy and affect the computational complexity only in terms of symmetric cryptographic operations. To demonstrate that the scheme performs in practice, we presented Dudle, an implementation of the scheme in JavaScript. Due to the use of JavaScript for all client side operations, no installation is needed for the user. We therefore showed, that complex cryptography is possible in zero footprint applications.

a) attacking with - 1 𝑡0Fig. 1 .

 11 Fig. 1. Different ways to attack a poll if Mallory wants 𝑡3 to win. The plain text votes (𝑣𝑢,𝑡 ) are displayed.

  (a) without giving up privacy 𝑃 (𝒱( d) = false | 𝑣𝑢,𝑡 = -1) (b) with privacy-loss 𝑃 (𝒱( d) = false ∨ ℬ ( d, k) = false | 𝑣𝑢,𝑡 = -1) (c) probability of privacy-loss 𝑃 (ℬ ( d, k) = false | 𝑣𝑢,𝑡 = -1)

Fig. 3

 3 illustrates the whole process. Let d be the 3-dimensional array of all DC-Net messages sent to the normal poll and d′ be the 3-dimensional array of all DC-Net messages sent to the check DC-Nets. The verification function of correctness is defined as 𝒞( d, d′ ) = { true if ∀𝑡 ∈ 𝑇 : |𝑈 | = ∑ 𝑢∈𝑈,𝑖∈Z 𝐼 ( d𝑢,𝑡,𝑖 + d′

Table 1 .

 1 Execution time for an exponentiation modulo a 786 bit long integer in JavaScript with different libraries. The first 5 columns were measured on an Intel

	Pentium 4 Duo with 2.8 GHz, 2 GB RAM running Windows XP SP3. The last one was
	measured on a Motorola Milestone running Android.
		IE	Firefox Safari Opera Chrome	Android
		8.0.6001 3.6.12	5.0.3	10.63	8.0.552 Firefox 4.0b2
	Wu [21]	2.80 s	0.78 s	0.91 s 0.31 s	0.10 s	7.87 s
	Baird [22]	5.05 s	0.43 s	0.15 s 0.18 s	0.16 s	5.10 s
	Shapiro [23] 21.47 s	2.12 s	1.18 s 0.99 s	0.61 s	(crashes)

  Split the votes into several partial votes. While Mallory's attack remains undetected in the left table, Alice and Bob are able to detect it in the right one.

Table 2 .

 2 Lower bounds for the probability of successfully detecting an attack

	𝐼 |𝑈 |	(a)	(b)	(c)
	20 15 48.8 % 84.7 % (35.9 %)
	20	5 81.5 % 98.6 % (17.1 %)
	50 15 75.4 % 96.9 % (21.5 %)
	50	5 92.2 % 99.8 % ( 7.5 %)
	100 15 86.9 % 99.2 % (12.3 %)
	100	5 96.1 % 99.9 % ( 3.9 %)

Table 4 .

 4 Performance measurement of the key calculation in a poll with |𝑈 | = 5, |𝑇 | = 20 and 𝐼 = 20. The first 5 columns were measured on an Intel Pentium 4 Duo with 2.8 GHz, 2 GB RAM running Windows XP SP3. The last one was measured on a Motorola Milestone running Android.

		IE	Firefox Safari Opera Chrome	Android
		8.0.6001 3.6.12	5.0.3	10.63	8.0.552 Firefox 4.0b2
	AES-128+SHA-256 18.4 s	7.7 s	2.9 s	1.4 s	2.8 s	31.7 s
	DH	15.0 s	11.7 s	8.2 s	2.0 s	2.5 s	40.5 s
	total	37.6 s	22.5 s	13.5 s	4.3 s	6.3 s	84.2 s

E. g., Bob could detect that Mallory cheated at 𝑡0 in Fig.1a.

If this sum is lower than 0, an attack occurred as well. However, as this attack would be discovered by function 𝒱( d) (Equation1), we want to neglect this case here.

This is like trying to perform a (-2)-attack without privacy-loss, but choosing one partial DC-Net to send the -2.

E.g., every participant may commit himself to a random number together with his vote vector. In case of verification all commitments are revealed and the random numbers are added to one single seed which is used to bootstrap a sequence.

Acknowledgments The author wants to thank the whole DuD-Group in Dresden for the fruitful coffee breaks. Special thanks goes to Rainer Böhme, Sebastian Clauss, Stefan Köpsell and Sandra Steinbrecher. The research leading to these results has received funding from the European Community's Seventh Framework Programme (FP7/2007-2013) under grant agreement № 216483.


Sebastien Mondet

Ion Alberdi

Thomas Plagemann
email: plageman@ifi.uio.no2ion.alberdi.research@gmail.com

Generating Optimised and Formally Checked Packet Parsing Code

While implementing distributed applications, the parsing of binary packets is a very difficult and error-prone task the developer has to face. Moreover, these programming mistakes are often the source of distant vulnerabilities. In this paper we present a code-generation library, called Promiwag, for creating optimised and safe packet parsing code. Its input is concise human-readable descriptions of the protocols and the interests of the application in specific pieces of information. Promiwag follows a dependency-based algorithm, and uses high-level optimisation techniques to generate minimal parsing automatons. These automatons can be compiled into C or OCaml code for efficient execution, and to annotated Why code. This latter output is then used to automatically prove that for any possible input packet, the generated code cannot perform any illegal memory access, and that no infinite loop can be triggered. We have used our code generator to implement a pretty-printer for Internet protocols, and we provide experimental results on the performance of the generated code.

Introduction

One of the currently observable trends for future distributed applications is the convergence of Internet and Mobile networks. More and more small, mobile, and cheap electronic devices must be able to communicate with personal laptops, servers, and/or clouds. Therefore, one needs to implement specialised and complex software for many different platforms. Some of these platforms require special attention to be given to performance. Indeed, computing resources may be very limited, e.g., on mobile devices. In parallel, the error-proneness and the lack of static guaranties of the common tools and languages used by developers (unsafe memory accesses, dynamic typing, etc.) lead to a very large amount of bugs and security vulnerabilities present in distributed applications 3 .

One common task that many distributed application developers have to handle is the parsing of binary protocols. For example, this is the case in almost every piece of protection software (firewalls, intrusion detection systems, etc.). The code handling these aspects, especially when hand-written in C or C++, is very often swarming with implementation mistakes. The latter often lead to exploitable buffer over-flow vulnerabilities or easy-to-trigger denial-of-service attacks [START_REF]Top 20 internet security problems, threats and risks. section 5 anti-virus software[END_REF].

Code generation techniques (a.k.a. Meta-Programming) have already been often used to automate programming tasks. Examples range from the lex and yacc tools developed in the 70s, to the compiler of the "Fastest Fourier Transform in the West" [START_REF] Frigo | A fast Fourier transform compiler[END_REF]. Generating code from a higher level representation allows adapting the output specifically to the target platform. It also allows providing aggressively optimised code while keeping the required level of safety. From the initial input representation, one can also generate additional output which may assist the developer in other ways; e.g. for testing or documentation extraction.

The safety provided by code generation will often be much better than with hand-written code. However, the code generator itself is generally a piece of software developed by one or more human beings. As such, it can (and will) be the victim of many programming mistakes. How can one trust the code generated by an external tool? Expert and careful proof-reading of thousands of lines of generated code is by far too expensive for most software projects; and testing requires identifying in advance all the possible ways to make a program go wrong. When dealing with input as binary packets which can be erroneous, or maliciously crafted, both approaches are not realistic. We address this issue by mathematically ensuring the safety of the generated code against any possible input. Formal properties are automatically proved on the output of the Promiwag library.

In this paper, we focus on the generation of code for parsing network packets. From a high-level representation of network protocols and their handling by the user, our code generator creates optimised code on which safety and security properties are formally proved. The user describes i) the binary formats of the packets, ii) the transitions between (micro-)protocols (e.g. how to pass from IP to TCP), iii) a few logical properties to insure, iv) which pieces of information he is interested in, and v) what user-function to call with the parsing results as arguments. Out of these concise declarations, the Promiwag library builds a parsing automaton which parses only the necessary fields (i.e. the fields required by the user and their dependencies). This intermediate representation also contains logical properties about the algorithms involved. It is then compiled into i) C code for high performance parsing, ii) OCaml code, and iii) annotated Why code [START_REF] Filliâtre | Why: A Multi-Language Multi-Prover Verification Tool[END_REF]. This latter output allows, thanks to the Alt-Ergo theorem prover [START_REF] Conchon | Lightweight integration of the ergo theorem prover inside a proof assistant[END_REF], automatically proving that, for any possible input packet, no wrong memory accesses can be provoked, and no infinite loops can be triggered.

In Section 2, we detail and discuss the design of our code generation approach. Then, in Section 3, we assess the performance of the code through experiments. We discuss related projects in Section 4, before concluding and suggesting future work (Section 5).

Figure 1 illustrates the high-level idea of the structure of the code generation process in the Promiwag library. We have developed our code generation tool as an Objective Caml4 library. The user can link their programs with the library to generate the code. A dedicated and independent input language could be easily implemented, but the slight benefit of readability would not overcome the loss in flexibility. Indeed, as Promiwag can generate code for different target platforms, and can adapt the code to the needs of the user, having a powerful programming language can be very practical for code reuse and maintainability. We present the code generation process from an input/output point of view in Sections 2.1 and 2.2. Afterwards, we discuss the limitations and some issues related to the current state of our implementation in Sections 2.3 and 2.4.

Input

For each protocol or micro-protocol (e.g. for a given type of packet header, and its links to the "upper" layers), the input required from the user is composed of two declarative pieces of code; the (micro-)protocol description and the user handler.

The first, is the description of the (micro-)protocol itself. The user gives a precise definition of the binary format, i.e., they name the fields and their size(s). A field can be an integer of any size between 0 and 32 bits, or a string of any byte size. They also provide the "parsing transitions", which are a sequence of switchlike statements to tell the generator how to continue the parsing. For example, given the value of a protocol field, the parser has to continue with another (micro-)protocol included in a given payload. Finally, the user can provide "runtime checks" that tell the generator to include assertion checking code, about the fields of the parsed packet. The goal of the run-time checks is not to write a full stateless firewall, but to insure a few consistency properties needed for the formal proofs on the code. For example, the soundness of the binary format may depend on assumptions about certain fields in a given (micro-)protocol.

The second declaration, the user-handler, is optional. It describes the user's interest in specific parsable values and their handling by an external function.

Each user-handler refers to a described (micro-)protocol. The user specifies their request for values, offsets, pointers, and/or sizes in the binary format, and provides a function in the target programming language (C or OCaml) which expects these values as arguments. The function returns a boolean/integer deciding whether to continue parsing or not. ). The first is a (micro-)protocol description; the binary format, the parsing transitions, and a single run-time check. The second listing is the corresponding user-handler specification. In the binary format description, one can see how variable-length fields like the "options" are created with arithmetic expressions. This particular case requires a run-time check. Indeed, the positiveness of the size of the field depends on the fact that the field "header_length" is between 5 and 15 as required by the RFC 791. If the corresponding run-time check is not provided by the user, the formal proving of the parsing code will fail. This non-provability matches a hypothetical malicious attack of crafted IP packets containing wrong "header_length" fields. Note that this run-time check is the only one needed to implement and prove the Tcpdump-lite experiment in Section 3.

Output

From the previously described declarations, Promiwag builds the parsing automaton code. It starts from the fields required by the user request, the parsing transitions, and the run-time checks, and then follows their dependencies to minimise the amount of code. This parsing automaton is expressed in an internal representation. This representation contains the parsing algorithm in a strictlytyped imperative language. The language is low-level as it can handle pointer arithmetic, bit-wise operations, etc., but platform independent (for example, endianness is explicit). It is also annotated with logical properties gathered during its construction. Many human-readable comments are also kept for debugging or proof-reading purposes. During the code-generation, the library performs relatively high-level code optimisations, including constant propagation, partial evaluation, common sub-expression elimination, and "factorisation" of buffer access verifications. The lowest-level optimisations are left to the back-end compilers of the output languages; implementing them would be redundant.

In the example presented in Listings 1.1 and 1.2, the initial "required fields" correspond to the ones requested by the user (the values of "src" and "dest", and the size of the "ip_payload"), the field "header_length" for the run-time check, the value of "protocol" and the offset of the "ip_payload". The generator needs the last two to be able to continue the parsing with the next protocol. Then, the computation of, for instance, the length of the "options" field will be required as a dependency in order to compute the offset of the payload.

The internal representation of the parsing code can then be "compiled" into the three targets shown in Figure 1. On the one hand, the two "programming language" targets are C and OCaml. The former may be seen as the main target, as the code generator was originally designed for C. The transformation to this language is parametrised by a representation of the target platform (endianness, sizes of the types, etc.). The OCaml output was implemented in order to show that adding other target languages is a relatively easy task. Implementing this transformation from scratch took only 4 hours for one developer. After this time, the OCaml version of the Tcpdump-lite application presented in Section 3 was successfully tested. Generating OCaml is useful by itself: it is used for some experiments for instance to count the buffer accesses in Table 1.

On the other hand, Promiwag's code generator uses the intermediate representation to generate input for the Why tool. Why5 is a "verification condition generator" created by Jean-Christophe Filliâtre. For a given annotated algorithm, it propagates "weakest preconditions" [START_REF] Filliâtre | Verification of non-functional programs using interpretations in type theory[END_REF] and generates "proof goals" when an assertion needs to be proved. The annotations are, generally, intermediary proof goals or "hints" to guide the proving steps. The generated proof goals must then be proved by another tool, an automatic prover and/or a proof assistant.

In our case, we use the "fast" weakest precondition algorithm presented by Barnett and Leino [START_REF] Barnett | Weakest-precondition of unstructured programs[END_REF]. Thanks to the annotations, the proof goals can be automatically proved by the Alt-Ergo 6 theorem prover [START_REF] Conchon | Lightweight integration of the ergo theorem prover inside a proof assistant[END_REF]. The Why code generated by the Promiwag library represents the algorithm of the parsing automaton. The user-handlers for the protocols are ignored; we prove only the code we generate.

The accesses to the packet buffer are abstracted as logical functional parameters. They are modelled in order to require a proof that they are not out of bounds each time they are "called/used", and at the same time, to express that accessing a packet can lead to any arbitrary value, i.e., there is absolutely no assumption on the content of the packet. The automaton is able to parse "protocol loops", like IP/GRE/IP, but we provide enough annotations to guide the proof that the parser always strictly "advances" in the packet. Hence, given that a packet has constant arbitrary size, the tools can prove that the parsing always finishes eventually.

At the end of a successful proving process, we can assert that the generated parsing automaton verifies the following theorem:

For any possible input packet, -no unsafe memory accesses can happen, and -no infinite loops can be triggered.

Current Limitations

As work-in-progress, the Promiwag library currently does not implement any adhoc "parsing state" management. This means that the generated code cannot yet use information from previous packets, and/or from other (micro-)protocols in the same packet. The implementation of features like the handling of IP fragmentation or the transitions present inside protocols like DNS or DHCP are subject to future work. They have to be implemented for now within the user's handlers; note that the user can still use generated code for the low-level parsing related to this. The theorem which can be proved on the code, is certainly a huge benefit over most other implementations of packet parsing; especially from a security standpoint. The proof asserts that the code cannot be used to provoke a fatal error. However, we do not have yet any formal proof that the code does what it is actually supposed to do. This means that checking the correctness of the computation of a given field of a (micro-)protocol requires testing. Of course, testing for example that the "header length" field parsed for an IP packet has the expected value is much easier than trying to imagine all the possible ways to alter it in order to make the program crash. Moreover, in C or C++ programs, the error reporting of unsafe memory accesses depends on the exact memory layout at the time of testing. They may be completely silent in some cases and appear later in production; this problem is completely addressed by the current proof.

Finally, from an ergonomics point of view, the error reporting related to formal proving is still quite difficult to understand. In the example of Listings 1.1 and 1.2, if one forgets the run-time check on the "header length", the theorem prover just fails saying "I don't know" about a possibly very long proof goal. Then, tracking down the error to find the original mistake is not an easy task. For now, we have implemented a very explicit naming of generated variables together with high-level comments which are propagated to the different outputs. While these are helpful, more sophisticated techniques will be needed in the future.

Trust Issues

When hearing about mechanised and/or automated proofs, one has to ask the question: 'Who and what do we really have to trust?' Regarding the theorem proved on the generated code, apart from the soundness of the underlying mathematical framework, one has to trust our work in some respects, and the external tools in others.

On the one hand, the trust bottleneck in the Promiwag library is the final compilation stage. Currently, there is no proof that the different outputs are semantically equivalent. This means that when the theorem prover succeeds, one has to trust us that the C and OCaml outputs are equivalent, and actually proved by the proof on the Why code. To address this, we have restricted the size of the critical code to the minimum. We also note that implementing the OCaml output in half a day (c.f. Section 2.2) partially shows that this part of the code is quite straight-forward.

On the other hand, the whole tool-chain depends on many external tools. First, one has to trust the theorem proving tools; Why and Alt-Ergo themselves. Both rely on formally proved algorithms, but their implementations are not. Note that other theorem provers can be used with Why if needed. Second, every software project has to trust its compilers; in our case, the C and OCaml compilers. For C, we use the GNU Compiler Collection (GCC). Even though it is widely tested, at least for the C language within the mainstream architectures, many bugs are often found in official releases. As a side note, we have successfully tested the compilation of the C code generated for our Tcpdump-lite example with Compcert7 . Compcert is a formally proved compiler for a subset of the C language [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. For OCaml, we use the standard compilers. They may also be a trust issue but a substantial part of the system (compiler and run-time) has already been qualified under the DO-178B standard to be used as tool for critical aircraft software development [START_REF] Pagano | Experience report: using Objective Caml to develop safety-critical embedded tools in a certification framework[END_REF].

Experimental Results

In this section, we provide the results of our experimental study into the performance of the generated code. We aim to show that the use of a code generator does not degrade the performance compared to hand-written code, and that the size of the generated code is still quite controllable by the user.

We have used the Promiwag library to implement a pretty printer for Internet protocols (Ethernet, IPv4, ARP, GRE, TCP, UDP, etc.). As previously mentioned, we have named it "Tcpdump-lite". It is based on libpcap 8 , and uses our code generator to call user-handlers which are only pretty-printing the requested values (printf). We have generated three different "flavours" of Tcmpdump-lite:

-Full: requests various meaningful fields for every (micro-)protocol, and displays them.

-Muted: requests the same fields as Full but does not print them; (micro-)protocol user-handlers are just empty, it just prints "error" messages (i.e. alerts when packets are malformed). -Light: requests and prints fields only for UDP and TCP.

To estimate the running times of the tool-chain, we just measure the times taken by the different programs on an old Pentium 4 desktop computer for the Full version: i) compiling a code generation program and linking against our library: 0.12 s; ii) running the code generation: 0.04 s; iii) compiling the C code output with GCC: 0.13 s; iv) running the Why tool: 13.8 s; and v) proving all the goals with Alt-Ergo: 21 s.

We have done experiments listening to "live" network interfaces and with many "PCAP capture files" (generated by us or found on the Web). To simplify their presentations, we present here the results obtained with two characteristic files. We call the first one Fuzz-10K, it is a capture of 10 000 packets, where many are malformed, and contain potential "attacks". The second one is 24GRE-132 which is composed of 132 packets among which many are using 24 encapsulated GRE tunnels. This means that for those packets the "protocol stack" is: Ethernet/IPv4/GRE/IPv4/GRE/IPv4/.../GRE/IPv4/UDP where there are 24 GRE encapsulations. Note that handling multiple encapsulations is an important feature [START_REF] Alberdi | Luth: composing and parallelizing midpoint inspection devices[END_REF] which many networking tools cannot handle; explicitly or not. For example the Section 1.8.1 of the Snort manual [START_REF]Snort Users Manual. The official documentation produced by the Snort team at Sourcefire[END_REF] states that for more than one GRE tunnel, packets will not be inspected, and the Linux kernel simply crashes for more than 36 encapsulations (c.f. Debian bug number 599816). The first experiment is an analysis of the control the user has on the generated code. Table 1 shows a comparison between the Full and Light versions of our Tcpdump-lite. We provide the raw size of the whole program, and the number of buffer accesses actually executed during the parsing of both capture files. This shows that, from the same set of (micro-)protocol descriptions, just by removing requests and user-handlers, the user can lighten the application significantly. It matches the goal of writing software adapted to the resources of the target device. For example, one can make a special version of a firewall application for mobile phones with a more affordable development effort.

We also provide results for brute performance evaluation. We compare the running times of the different versions of Tcpdump-lite, against an "empty" PCAP application (i.e., the same code as Tcpdump-lite but without any parsing of the packets) and different options of the original Tcpdump application. To be less unfair with the latter, we use the options -n so that IP addresses are not converted to host names and -K so that checksums are not computed. We also redirected all outputs to /dev/null. We measure Tcpdump's (noted "T") running times for the different verbosity levels: the default, -v, -vv, and -vvv. In order to try to reduce the entropy of the measurements, we run them 2000 times on an old machine (Pentium 4) and on a more recent one (Core 2 Duo P8700). The results are presented in Table 2. Note that the Fuzz-10K capture involves some malformed packets which trigger error-message printing even for the Muted version, and that the 24GRE-132 one induces a lot of parsing logic compared to the display of information. If we assume the two following approximations: i) the Empty program represents the operating system plus the "PCAP machinery", and ii) the difference between Full and Muted measures the time spent in printing, then we can compute the following statistics (for the Pentium 4 9 ):

-For the capture Fuzz-10K, the distribution of the time spent is: OS+Pcap: 9.7 %, Generated code: 2.2 %, Printing: 88.1 %; and the average time per packet for the Full version is: 5.67 µs. -For the capture 24GRE-132 the distribution of the time spent is: OS+Pcap: 62.4 %, Generated code: 4.4 %, Printing: 33.2 %; and the average time per packet for the Full version is: 41.7 µs.

The running times for the original Tcpdump are given as a comparative indication. Indeed, the application is more feature-full, and dynamically configurable (i.e. on command line).

Related Work

The use of code-generation techniques in order to improve the performance and/ or the safety of distributed systems has been gaining a lot of interest in literature.

For instance, with the Statecall Policy Language presented by Madhavapeddy et al. [START_REF] Madhavapeddy | Combining Static Model Checking with Dynamic Enforcement using the Statecall Policy Language[END_REF], one can describe statefull automatons which are compiled into three different targets: OCaml code to embed in an application, Promela code to check temporal properties with the SPIN10 model checker, and HTML/Ajax code for real-time monitoring of the application. Another example is the declarative sensor networks (DSN) platform (Chu et al. [START_REF] Chu | The design and implementation of a declarative sensor network system[END_REF]). There, the user describes application overlays using a declarative language (paradigm similar to Prolog) and the compiler generates code for sensors in NesC (the C dialect for the TinyOS operating system).

Regarding the management of packet streams, two projects use metaprogramming for high-level packet filtering purposes. First, the BPF+ packet filter [START_REF] Begel | Bpf+: exploiting global data-flow optimization in a generalized packet filter architecture[END_REF] uses a high-level language to describe boolean predicates on packet flows. This language is compiled to bytecode which can be verified or interpreted (or JIT-assembled). Among the verifications, the halting of the application is insured by forbidding any kind of cycles or loops in the filtering program. Second, the FFPF project (Fairly Fast Packet Filter [START_REF] Bos | FFPF: Fairly Fast Packet Filters[END_REF]) implements a filtering language which allows one to "chain" (mostly independent) packet analysis applications while sharing kernel-space buffers to avoid copying.

Examples of projects using code-generation especially for packet parsing are Binpac, GAPAL, and Melange's MPL. Binpac [START_REF] Pang | binpac: a yacc for writing application protocol parsers[END_REF] is a C++ code generator for the Bro intrusion detection system 11 . It uses a yacc-like language to mix the specification of binary formats and user's C++ code in order to help them in their task. State and parsing transitions are written directly by the user as well as bit-level accesses, e.g. by including inline C++ code. GAPAL [START_REF] Borisov | Generic application-level protocol analyzer and its language[END_REF] is a high-level language for analysing application protocols which is evaluated by a C++ interpreter. The Meta-Packet Language of the Melange framework [START_REF] Madhavapeddy | Melange: Towards a functional Internet[END_REF], is a domain specific language to describe Internet protocols. Its compiler generates optimised OCaml pieces of code for each protocol; the use of a memory-safe language naturally avoids wrong buffer accesses. It also features ad-hoc parsing state management for situations commonly found in Internet protocols. Parsing transitions between protocols are left to the developer (but they fit well with ML-style programming).

Even though these projects may handle more complex protocols and/or fragmentation thanks to ad-hoc parsing-state management, they all have a unique output language and they do not give any formal proof on the generated code. Moreover, they all generate code for the whole defined set of protocols, i.e. even for non-used portions. As they rely on a lot of hand-written code, brute performance comparisons would be quite meaningless. For example, to compare the performance of the Tcpdump-lite, implemented with Promiwag, against another one implemented with Binpac, the developer would have to implement the parsing transitions or the "bit-level" accesses directly in C++. This would mean comparing a lot of generated code against hand-written code.

Conclusion

Our goal is to provide reduced development costs while keeping performance and enforcing safety. We have presented a code-generator which, from concise and high-level descriptions, can generate optimised code for parsing binary packets. The code is safe-by-construction thanks to automated formal proofs done on the output. The user control the amount and the performance of the generated code. Indeed, the generation is dependency-based; we build only the code that is actually needed by the user. The experiments we provide assess that the run-time performance will not be degraded by the use of our library. Future work will be divided in three directions. First, state, persistence, and memory management are needed to add features to the parsing generation. This problem is much more generic than just packet parsing and will have to be treated as such to be used in other aspects of distributed applications. Second, more aggressive optimisations on the code could be implemented. As the performance of a given program transformation depends on the actual code, potential optimisations could be evaluated on the generated code in order to choose the right option at the last time. Finally, the formal proving framework gives us a lot of room for interesting improvements. More properties could be proved on the code, e.g. the accuracy of the computations regarding the user's requests, or the absence of dead code. The "trust bottleneck" of the Promiwag library, i.e. the code which transforms the (last) internal representation to the different targets, could be re-implemented in a directly certified way with a proof assistant like Coq 12 . This family of formal tools have "executable code extraction" capabilities, and these kinds of program transformations, even if they require a lot of specification and proving work, are well suited for programming with proof assistants [START_REF] Leroy | Mechanized semantics. In: Logics and languages for reliability and security[END_REF][START_REF] Chlipala | Certified Programming with Dependent Types[END_REF].

Figure 1 .

 1 Figure 1. The Structure of the Code Generation Process in the Promiwag Library

Table 1 .

 1 Code Comparison of The Full and Light Versions

	Size (bytes) Buffer Accesses
	Binary C File Fuzz-10K 24GRE-132
	Full 19 157 35 027 242 050	8 457
	Light 14 378 22 272	65 482	2 921

Table 2 .

 2 Results for 2000 runs (times in seconds)

	Machine:	Pentium 4	Core 2 Duo P8700
	File:	Fuzz-10K 24GRE-132 Fuzz-10K 24GRE-132
	Empty	10.97	6.88	5.16	2.40
	Full	113.35	11.02	84.32	5.64
	Muted	13.49	7.36	6.94	2.52
	Light	19.71	7.44	11.97	2.61
	T	122.38	10.79	86.57	5.86
	T -v	168.76	14.67	123.49	8.69
	T -vv	169.14	15.16	127.49	9.18
	T -vvv	168.46	15.17	127.67	9.20

c.f. CVE (Common Vulnerabilities and Exposures); cve.mitre.org

ocaml.org

why.lri.fr

compcert.inria.fr

The results for the Core 2 Duo P8700 are slightly better for the generated code but the true parallelism of the architecture may make these computations less meaningful.

spinroot.com