Skip to content

Latest commit

 

History

History
228 lines (169 loc) · 5.96 KB

development.md

File metadata and controls

228 lines (169 loc) · 5.96 KB
Raw

Development

CurrentModule = ElectionGuardVerifier1X

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.

Datatypes

Loader

The loader describes the expected directory structure of an election record.

Loader
load(path::AbstractString)

Utililies

CurrentModule = ElectionGuardVerifier1X.Utils

Utils
mulpowmod(a::BigInt, x::BigInt, b::BigInt, p::BigInt)
same(c1::Constants, c2::Constants)
same(c1::Ciphertext, c2::Ciphertext)
within(x::BigInt, p::BigInt)
within_mod
one_ct
prod_ct(x1::Ciphertext, x2::Ciphertext, p::BigInt)

Answers

CurrentModule = ElectionGuardVerifier1X.Answers

Answers
answer(step::Int64, items::String, section::String,
       comment::String, count::Int64, failed::Int64)
verification_record(er::Election_record,
                    anss::Vector{Answer})
bits2items(bits::Int64)

Check

CurrentModule = ElectionGuardVerifier1X

The check function implements what is described in the version 1.0 ElectionGuard Specification.

check(er::Election_record)

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.

validate(path::AbstractString, log::String="")

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.

CurrentModule = ElectionGuardVerifier1X.Params

Params

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.

CurrentModule = ElectionGuardVerifier1X.Guardian_pubkey

Guardian_pubkey

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.

CurrentModule = ElectionGuardVerifier1X.Selection_encryptions

Selection_encryptions

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.

CurrentModule = ElectionGuardVerifier1X.Parallel_mapreduce

pmapreduce

For the verification routine, type A is the type of a submitted ballot, and type B is the structure Accum.

CurrentModule = ElectionGuardVerifier1X.Selection_encryptions

Accum

Notice it contains what is needed to produce an answer.

Function op is implemented by function combine.

combine

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.

verify_ballot(er::Election_record, ballot::Submitted_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.