Development
This section introduces the source code that makes up the verifier. According to C.A.R Hoare:
There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other way is to make it so complicated that there are no obvious deficiencies.
Our goal is to always write code that is obviously correct.
Introduction
To get the most out of this tour, view the relevant sources as you read each section. The tour begins with the datatypes that reflect the contents of an election record followed by the procedures used to load an election record into those datatypes. Common utilities used to implement ElectionGuard checks is next.
Pay close attention to the section on answers, as it describes how check failures are linked to the section in the specification where the check is specified. The Check section describes the top-level loop used to drive the verification process. Finally, the section on verification routes describes how individual checks are implemented.
Datatypes
The way to understand the software is to start by viewing the Datatypes module.
ElectionGuardVerifier.Datatypes — ModuleDatatypesThis module contains the structures that appear in the JSON data files that make up an ElectionGuard election record. The field names in structs are the field names that appear in the JSON file with the exception of constants. The use of constants is too ubiquitous to use the verbose field names.
To see the structure of the data, it is best that you read the structs in this file in reverse order.
Loader
The loader describes the expected directory structure of an election record.
ElectionGuardVerifier.Loader — ModuleLoaderThe loader assumes the records are delivered using a standard directory structure that is encoded here. The structure is
- manifest.json: Data about the election
- constants.json: Constants used for ElGamal cryptography
- context.json: Election parameters
- coefficients.json: Lagrange coefficients
- guardians/*.json: Per guardian data
- encryption_devices/*.json: Encryption devices
- submitted_ballots/*.json: Submitted ballots
- spoiled_ballots/*.json: Spoiled ballots (may be missing)
- encrypted_tally: Encrypted tally
- tally.json: The tally
ElectionGuardVerifier.Loader.load — Methodload(path::AbstractString)::Election_recordLoad election records in the given directory. On error, print load error message before crashing.
Utililies
ElectionGuardVerifier.Utils — ModuleUtilsFunctions used to implement Election Guard checks.
ElectionGuardVerifier.Utils.mulpowmod — Methodmulpowermod(a, x, b, p) = (a * x ^ b) mod p
ElectionGuardVerifier.Utils.same — Methodsame(c1::Constants, c2::Constants)::BoolAre two sets of constants the same?
ElectionGuardVerifier.Utils.same — Methodsame(c1::Ciphertext, c2::Ciphertext)::BoolAre two ciphertexts the same?
ElectionGuardVerifier.Utils.within — Methodwithin(x::BigInt, p::BigInt)::BoolIs 0 ≤ x < p?
ElectionGuardVerifier.Utils.within_mod — Functionwithin_mod(x::BigInt, q::BigInt, p::BigInt)::BoolIs 0 ≤ x < p and (x ^ q) mod p == 1?
ElectionGuardVerifier.Utils.one_ct — Constantone_ct::Ciphertextone_ct = Ciphertext(1, 1)
ElectionGuardVerifier.Utils.prod_ct — Methodprod_ct(x1::Ciphertext, x2::Ciphertext, p::BigInt)::CiphertextMultiply two ciphertexts mod p
Answers
ElectionGuardVerifier.Answers — ModuleAnswersThis module provides data structures and operations used to report verification answers. At the top-level, there is a verification record. It identifies the specification version, the election, and contains a list of verification answers. A verification answer is the result of checking all or part of a verification step as defined in an ElectionGuard specification.
A verification answer contains a verification step number, a string listing items that failed while verifying the step, the step title, a comment, the number of records checked, and the number of records that failed. A failing step that has no items is marked using item "X".
In the verification routies, each verification item check returns an integer. The integer is zero if the check passes, otherwise it is an integer with one bit set. The bit is used to identify the item being checked. The bit patterns are exported as constants A, B, C, D, E, F, G, H, I, J, and K. The bit patterns for multiple checks are combined using bitwise or.
ElectionGuardVerifier.Answers.answer — MethodConstruct a step answer
ElectionGuardVerifier.Answers.verification_record — MethodConstruct a verification record
ElectionGuardVerifier.Answers.bits2items — MethodConvert a bit pattern to items
Check
The check function implements what is described in the version 1.0 ElectionGuard Specification.
ElectionGuardVerifier.check — Methodcheck(er::Election_record, path::String="")::BoolCheck election record. Write answers to path in JSON if path is not empty.
The check function calls function verify, which returns a verification record that check optionally prints into a JSON file, and then returns the element in the record that says if all of the verification routines succeeded.
The verify function runs each verification routine. Each routine creates an Answer. The verify function sequentially runs each routine, prints the result, and stores the answer for inclusion in the returned verification record.
Verification Routines
All verification routines have a comment structure. The structure is revealed by studying the source code for three representative routines.
A Simple Routine
The simplest routine is the one that checks for standard constants.
ElectionGuardVerifier.Params — ModuleParamsEnsure the constants are the standard ones.
The specification for this routine has no items and there is only one check required. Notice the items field in the answer is always the empty string.
A Routine That Checks a Small Number of Records
The following routine checks each guardian.
ElectionGuardVerifier.Guardian_pubkey — ModuleGuardian_pubkeyVerify the correct computation of the joint election public key and extended base hash.
There are two checks in the specification labeled as Item A, and Item B. The check for each item returns an integer that is zero when the check succeeds. When a check is non-zero, it returns a bit pattern that reveals which item failed. The main loop accumulates the bit patterns in the acc variable, which is used to produce the items field in the answer.
When there are multiple failures, the comment returned as an answer is the one generated by one of the failures. In this case, it will be the last failure.
A Routine That Checks Each Submitted Ballot
The following routine checks each submitted ballot.
ElectionGuardVerifier.Selection_encryptions — ModuleSelection_encryptionsEnsure the selection encryptions in each ballot are valid.
The code uses mapreduce to apply a check to each ballot and then combines all of the results to produce an answer.
This check is one of the most complicated verification routes, however, its computation is quite similar to what occurs in the previous routine with one exception, the routine is structured so its results can be computed with mapreduce. Mapreduce provides a means to encode embarrassingly parallel computations in a way that can be easily exploited by concurrent hardware.
Mapreduce$(f, op, vec)$ applies unary function $f:A\to B$ to each element in vector $vec:A^\ast$, and then binary function $op:B\times B\to B$ is used to reduce every value computed by $f$ into a single value of type $B$ that is returned. During the reduction process, the order in which pairs of values are reduced to one is unspecified, and therefore to produce a deterministic value, $op$ must be associative. A thread parallel implementation of mapreduce follows.
ElectionGuardVerifier.Parallel_mapreduce.pmapreduce — Functionpmapreduce(f, op, vec::AbstractVector)When Julia is started with enough threads, this version of mapreduce divides a vector into into sections, runs mapreduce on each section in parallel, and then collects the results using the op function.
For the verification routine, type $A$ is the type of a submitted ballot, and type $B$ is the structure Accum.
ElectionGuardVerifier.Selection_encryptions.Accum — TypeAccumAccumulated value type for mapreduce
Notice it contains what is needed to produce an answer.
Function $op$ is implemented by function combine.
ElectionGuardVerifier.Selection_encryptions.combine — Functioncombine(accum1::Accum, accum2::Accum)Combine accumulated values.
Notice that combine is not associative, and therefore the output of a call to mapreduce using it is not deterministic. This is because the comment returned by mapreduce is allowed to be the one associated with any failure.
The function $f$ is constructed using the following.
ElectionGuardVerifier.Selection_encryptions.verify_ballot — Methodverify_ballot(er::Election_record, ballot::Submitted_ballot)Verify one ballot.
The actual call is to mapreduce is
accum = pmapreduce(ballot -> verify_ballot(er, ballot),
combine, er.submitted_ballots)where er is a variable captured from the environment of the call.