Page
321
/
324

Page 1 of 324

Building Reliable Voting Machine Software

Ka-Ping Yee

B. A. Sc. (University of Waterloo) 1998

A dissertation submitted to the Graduate Division

of the University of California, Berkeley

in partial fulfillment of the requirements for the degree of

Doctor of Philosophy

in

Computer Science

Committee in charge:

Professor David Wagner, Co-chair

Professor Marti Hearst, Co-chair

Professor Henry Brady

Professor Joseph Hellerstein

Fall 2007

Page 1 of 324
Page 2 of 324

The dissertation of Ka-Ping Yee is approved.

Professor David Wagner (Co-chair) Date

Professor Marti Hearst (Co-chair) Date

Professor Henry Brady Date

Professor Joseph Hellerstein Date

University of California, Berkeley

Fall 2007

Page 2 of 324
Page 3 of 324

Building Reliable Voting Machine Software

Copyright © 2007

Ka-Ping Yee

Permission is granted to copy, distribute, and/or modify this document under the terms

of the GNU Free Documentation License, version 1.2 or any later version published by the

Free Software Foundation, with no Invariant Sections, no Front-Cover Texts, and no

Back-Cover Texts. A copy of the license is included in the appendix entitled GNU Free

Documentation License.

Page 3 of 324
Page 4 of 324

Abstract

Building Reliable Voting Machine Software

Ka-Ping Yee

Doctor of Philosophy in Computer Science

University of California, Berkeley

Professor David Wagner, Co-chair

Professor Marti Hearst, Co-chair

I examine the question of how to design election-related software, with particular

attention to the threat of insider attacks, and propose the goal of simplifying the software

in electronic voting machines. I apply a technique called prerendering to reduce the

security-critical, voting-specific software by a factor of 10 to 100 while supporting similar

or better usability and accessibility, compared to today’s voting machines. Smaller and

simpler software generally contributes to easier verification and higher confidence.

I demonstrate and validate the prerendering approach by presenting Pvote, a

vote-entry program that allows a high degree of freedom in the design of the user

interface and supports synchronized audio and video, touchscreen input, and input

devices for people with disabilities. Despite all its capabilities, Pvote is just 460 lines of

Python code; thus, it directly addresses the conflict between flexibility and reliability that

underlies much of the current controversy over electronic voting. A security review of

Pvote found no bugs in the Pvote code and yielded lessons on the practice of adversarial

code review. The analysis and design methods I used, including the prerendering

technique, are also applicable to other high-assurance software.

Professor David Wagner

Professor Marti Hearst

1

Page 4 of 324
Page 5 of 324

This dissertation is dedicated to those who work to run

elections everywhere in the world: registrars, officers,

pollworkers, clerks, judges, scrutineers, observers, and

everyone else involved in the process. You carry out the

mechanisms that make democracy work; this research is

devoted to helping you make democracy work better.

i

Page 5 of 324
Page 6 of 324

Preface

The democracy upon which our modern society is built

ultimately depends on a system that collects and counts votes.

For many voters in the United States and other countries, nearly

every part of that system relies on computer software in some

way. If you had to design that software, how would you do it?

This dissertation offers an exploration of that question and

a proposed answer: create the simplest possible voting machine

software. I use a technique called prerendering to reduce the

critical voting-specific software by a factor of 10 to 100 while

supporting similar or better accessibility and usability,

compared to today’s machines. Central to this dissertation is

the story of Pvote, the program I developed to realize this goal.

The first reason to simplify software is the threat of an

insider attack. The challenge is to prevent not just inadvertent

flaws, but flaws intentionally crafted by programmers who

stand to gain from subverting their own software. The only way

to meet this challenge is to require simpler software.

The second reason is that much of the controversy over

electronic voting stems from a conflict between flexibility and

reliability. Computers offer the promise of broader and more

effective access to voting, but computer programs are more

complicated and fragile than hand-counted paper ballots.

Simplifying the voting machine software mitigates this dilemma.

The problem of electronic voting is illustrative of the

challenges of building reliable software in general. In particular,

I report on insights from the Pvote work about managing the

complexity of high-assurance software and about reviewing

software for correctness without assuming trust in its author.

Both are relevant to the prevention of insider attacks, which are

a thorny and long-standing problem in software security.

ii

Page 6 of 324
Page 7 of 324

This dissertation is intended for several audiences:

• Election staff, policymakers, and activists: If you run

elections or influence how elections are conducted, I hope

to make you aware of the perils of complexity in software

(Chapters 1 and 9), and to calibrate your tolerance for

complexity in election software by demonstrating how much

it can be simplified. I also hope to contribute to your

understanding of the tradeoffs among various choices of

voting equipment and verification methods (Chapter 3).

• Engineers: If you build software, you may be able to achieve

greater confidence in it using the analysis, design, and

review strategies presented here (Chapters 2, 3, and . If

you develop voting machines, you can apply the

prerendering strategy to create more reliable software

(Chapter 4), use ideas from Pvote’s design and

implementation (Chapters 5, 6, and 7), or use the Pvote code

as a basis for your own software (Appendices A and B).

• Researchers: If you investigate software reliability or

security, you may be interested in assurance trees (Chapter

2), a way of structuring assurance claims during software

design, prerendering (Chapter 4) as a strategy for reducing

the trusted code base of a system, or derivation maps

(Chapter 9) for understanding sources of vulnerability to

insiders and the effects of shifting complexity among

components. The Pvote review experience (Chapter 8 and

Appendix E) motivates research challenges in the design of

programming languages, development environments, and

reviewing tools to support adversarial code review.

• Designers: If you practice visual design or interaction

design, you may be interested to learn how prerendering

(Chapter 4), the main software approach presented here, can

offer you unprecedented freedom in designing electronic

ballots and new opportunities for advancing democracy

through the power of design.

Preface iii

Page 7 of 324
Page 8 of 324

Contributions

This is a quick guide to the main contributions of this work and

where to find them.

1. A set of correctness properties for voting software derived as

an assurance tree (page 24).

2. An assurance chart comparing types of voting systems

according to the verification mechanisms available to voters

at each step of the voting process (page 56).

3. User interface prerendering, a technique for reducing the

complexity of critical software components (page 57).

4. Pvote’s ballot definition file format, a platform-independent

format for describing the ballot and the voting user interface

in a prerendered user interface voting system (page 121).

5. The software design of Pvote, a vote-entry program with

support for a wide range of ballot designs and voters with

disabilities (page 127).

6. A set of desirable properties of programming languages to

support adversarial code review (page 149).

7. Lessons learned from the Pvote security review, the first

open adversarial code review of voting software designed

for minimal complexity and high assurance (page 153).

8. Derivation mapping, a method of diagramming the

provenance of a security-critical artifact to identify sources

of vulnerability to insider attacks (page 161).

9. A security argument for the use of high-level programming

languages in high-assurance software (page 173).

10. Proof by construction (the implementation of Pvote) that a

fully featured user interface for voting can be implemented

in 460 lines of Python (page 217).

11. A security analysis and a set of assurance arguments for

Pvote, which are given in a separate document [92].

iv

Page 8 of 324
Page 9 of 324

Acknowledgements

I have been extremely lucky to have David Wagner and Marti

Hearst as my advisors. They supervised and supported this

work, and provided me with guidance and insight during my

career as a graduate student. They removed obstacles and

sought out opportunities for me. Their responsiveness and

detailed feedback have been fantastic. I also thank Henry Brady

and Joe Hellerstein, who served on my committee and went out

of their way to review this dissertation on a short time frame.

Steve Bellovin suggested the idea of prerendering, which

sparked this work. Candy Lopez of the Contra Costa County

Elections Department patiently showed me how real elections

are run. Scott Luebking and Noel Runyan helped me understand

the accessibility issues surrounding voting. Matt Bishop, Ian

Goldberg, Tadayoshi Kohno, Mark Miller, Dan Sandler, and Dan

Wallach generously volunteered many, many hours of their time

to serve as expert reviewers in the Pvote security review. Joseph

Hall has been a wonderful resource on election policy.

Debra Bowen and David Wagner created and gave me the

rare opportunity to review the source code of a widely used

commercial voting system in the California Top-to-Bottom

Review. It was a privilege to work with my collaborators on that

project: Matt Blaze, Arel Cordero, Sophie Engle, Chris Karlof,

Naveen Sastry, Micah Sherr, and Till Stegers.

Public attention to electronic voting did not appear

overnight; it is the result of a long history of hard work by

civic-minded heroes such as David Dill (founder of the Verified

Voting Foundation), Avi Rubin (director of ACCURATE), and

many others. Their efforts are a big part of what has made

research like mine possible. This work was funded by the

National Science Foundation, through ACCURATE.

v

Page 9 of 324
Page 10 of 324

Mark Miller, Jonathan Shapiro, and Marc Stiegler sparked my

interest in computer security and have deeply shaped my

understanding of it through many years of fruitful collaboration

and shared wisdom. I am exceptionally fortunate to have met

and worked with them.

Scott Kim’s dissertation inspired the page design of this

dissertation. La Shana Porlaris of the EECS Department saved

me from crisis time and again; her help and calm advice were

invaluable.

I am especially grateful to Lisa Friedman for her support

during the writing of this dissertation, and to my parents, for a

lifetime of devotion to me and my education.

vi

Page 10 of 324
Page 11 of 324

Contents

Preface ii

Contributions iv

Acknowledgements v

Contents x

1 Voting 1

What makes the voting problem so hard? 2

How does an election work? 6

Why use computers for elections? 9

How did electronic voting become controversial? 11

Why does software correctness matter? 14

2 Correctness 16

What constitutes a democratic election? 17

What does it mean for a voting system to be correct? 19

How does correctness relate to safety? 20

What is the tree of assurance goals for an election? 24

What does it mean for a voting system to be secure? 30

3 Verification 33

How do we gain confidence in election results? 34

How can we verify the computerized parts of an election? 36

What kind of election data can be published? 39

What makes software hard to verify? 41

In what ways are today’s voting systems verifiable? 44

What is the minimum software that needs to be verified? 48

What other alternatives for verification are possible? 52

vii

Page 11 of 324
Page 12 of 324

4 Prerendering 57

How can we make vote-entry software easier to verify? 58

What is prerendering? 59

Why put the entire user interface in the ballot definition? 60

How would a voting computer use a prerendered ballot? 62

What is gained by publishing the ballot definition? 63

What are the advantages of prerendering? 65

How can prerendering be applied to other software? 66

How are votes recorded anonymously? 67

5 Ptouch: the touchscreen prototype 69

Overview 70

Ballot definition format 71

Software design 80

Implementation 83

Evaluation 88

Shortcomings 93

6 Accessibility 96

Why was a second prototype needed? 97

What is Pvote’s approach to accessibility? 98

How are alternative input devices handled? 99

How does blindness affect interface navigation? 100

How do blind users stay oriented within an interface? 101

How do blind users keep track of what is selected? 102

How do blind users get feedback on their actions? 103

How are vision-impaired users accommodated? 104

7 Pvote: the multimodal prototype 105

Overview 106

Goals 107

Design principles 110

Differences between Pvote and Ptouch 114

Ballot definition format 121

Software design 127

Implementation 132

Evaluation 133

viii

Page 12 of 324
Page 13 of 324

8 Security review 136

How was Pvote’s security evaluated? 137

What were Pvote’s security claims? 139

How was Pthin defined? 143

What flaws did the reviewers find? 145

What improvements did the reviewers suggest? 146

Did the reviewers find the inserted bugs? 148

What ideas did reviewers have on programming languages? 149

What ideas did reviewers have on conducting reviews? 151

What lessons were learned from the review? 153

9 Complexity 156

Does prerendering actually eliminate complexity? 157

What is achieved by shifting complexity? 158

Why do software reviews assume trust in compilers? 160

How far back can the derivation of a program be traced? 161

What affects the tolerance of complexity in a component? 164

How does Pvote reallocate complexity? 167

What is gained by using interpreted languages? 173

10 Related work 174

Do any other voting systems use prerendering? 175

What other voting proposals reduce reliance on software? 176

What are “frog” voting systems? 177

Do frogs solve the electronic voting problem? 178

What is “software independence” (SI)? 179

Does SI make software reliability irrelevant? 181

What is end-to-end (E2E) verification? 186

Does E2E verification make software reliability irrelevant? 187

What are other approaches to high-assurance software? 188

Conclusion 191

Bibliography 193

A Ptouch source code 204

main.py 205

ix

Page 13 of 324
Page 14 of 324

Ballot.py 206

Navigator.py 210

Video.py 214

Recorder.py 215

B Pvote source code 217

main.py 218

Ballot.py 220

verifier.py 224

Navigator.py 228

Audio.py 233

Video.py 235

Printer.py 236

C Sample Pvote ballot definition 237

D Sample Pvote ballot designs 267

E Pvote security review findings 272

Correctness 273

Consensus recommendations 278

Inconclusive recommendations 282

Observations 284

Open issues 288

Bug insertion 296

Review process 300

Post-review survey 304

GNU Free Documentation License 306

x

Page 14 of 324
Page 15 of 324

1 Voting

What makes the voting problem so hard? 2

How does an election work? 6

Why use computers for elections? 9

How did electronic voting become controversial? 11

Why does software correctness matter? 14

1

Page 15 of 324
Page 16 of 324

What makes the voting problem so hard?

When I say the “voting problem,” I’m referring specifically to the

system that collects and counts votes. There are many other

parts of the election process that I’m not going to address in

this dissertation, such as voter registration, electoral systems,

and election campaigning. The collection and counting of votes

has been particularly controversial in the United States due to

problems with electronic voting in recent elections.

One of the great things about doing election-related

research is that just about everyone immediately understands

why it’s important. In my experience, whenever elections are

the topic of conversation, people have a lot to say about their

opinions on the matter. It’s encouraging to see that so many

people care deeply about democracy.

In conversations about the voting problem, there seem to be

four ideas in particular that come up all the time. It’s not

unusual to think that running a fair election ought to be a

straightforward task—after all, in some sense, it’s just counting.

To give you a taste of why the voting problem is not as easy as it

might seem, let’s begin by examining these four suggestions.

Banking machines work fine, so voting machines should be

no problem. On the surface, banking machines and voting

machines seem similar: users walk up and make selections on a

touchscreen to carry out a transaction. One of the largest

vendors, Diebold Inc., even produces both kinds of machines.

But the incentives and risks are very different.

Banking machines have money inside—the bank’s money. If

money goes missing, you can bet the bank will find out right

away and be strongly motivated to fix the problem. If the bank

machine incorrectly gives out too much cash, the bank loses

money; if it gives out too little, the bank will be dealing with

irate customers. Everything about the bank transaction is

recorded, from the entries in your bank statement to the video

recorded by the camera in most bank machines. That’s because

Voting 2

Page 16 of 324
Page 17 of 324

the bank has a strong incentive to audit that money and track

where it goes. If the machine makes mistakes, the bank loses—

either they expend time and money correcting your problem, or

you will probably leave and take your business to another bank.

With voting machines, it’s another story altogether. Voting

machines aren’t supposed to record video or keep any record

that associates you with your votes, because your ballot is

supposed to be secret. You don’t receive any tangible

confirmation that your vote was counted, so you can’t find out

if there’s a problem. Anybody can stand to gain by causing

votes to be miscounted—a voter, pollworker, election

administrator, or voting machine programmer—and the

consequences are much harder to reverse. Correcting an error

in your bank balance is straightforward, but the only way to fix

an improperly counted election is to do an expensive manual

recount or run the whole election again. And if you’re unhappy

with the way your vote was handled, you can’t easily choose to

vote on a competitor’s machine.

Give each voter a printed receipt, just like we do for any

other transaction. The surface comparison between voting and

a financial transaction also leads many people to suggest that

receipts are the answer. But the purpose of a receipt is quite

different from what is needed to ensure an accurate election.

When you buy something, the receipt confirms that you

paid for it. If there turns out to be a problem with the product,

you can use the receipt to get your money back or to get the

defective product exchanged.

When talking about a receipt from a voting machine, what

most people have in mind is a printed record of the choices you

made, just like a receipt from a cash register. If you took home

such a receipt, what would you do with it? There’s nothing to

refund, and you can’t use a receipt to get an exchange on a

defective politician. The receipt could record the choices you

made, but the receipt alone doesn’t assure that those choices

were counted in the final result. In fact, if the receipt

constitutes proof of which choices you made, it can be sold—

Voting 3

Page 17 of 324
Page 18 of 324

defeating the whole point of the secret ballot, which is to avoid

the corruption that vote-buying campaigns can cause.

A truly useful voting “receipt” would do exactly the

opposite: it would not reveal which choices you made but would

let you confirm that your choices were counted. Although these

two requirements sound paradoxical, researchers have invented

a variety of schemes that achieve them through the clever use

of cryptography. However, a key weakness of the schemes

proposed so far is that they rely on advanced mathematics, with

a counting process that would be a mystery to all but a tiny

minority of voters. This would run counter to the democratic

principle of transparent elections. Researchers are continuing

to search for simpler verification schemes that can be

understood by an acceptably large fraction of the public.

If we can trust computers to fly airplanes, we can trust

computers to run elections. The comparison between airplanes

and elections misses at least three key differences.

First, the visibility of failure is different. An airplane cannot

secretly fail to fly. When an airplane crashes, it makes

headlines; everybody knows. A forensic investigation takes

place, and if the crash is due to a manufacturing defect, the

airplane manufacturer may be sued for millions of dollars. But

an election system can produce incorrect results without any

obvious signs of failure. Therefore, we require something more

from election system software than what we require from

airplane software. A successful election system must not only

work correctly; it must also allow the public to verify that it

worked correctly.

Second, the target audience is different. Commercial

airplanes are designed to be flown by pilots with expert

training, but voting machines have to be set up by pollworkers

and operated by the general public. Our trust in airplanes is a

combination of trust in the equipment and trust in the pilots

who operate it. Whereas pilots have to log hundreds of hours of

flight time to get a license, pollworkers are often hired on a

temporary basis with only an afternoon or a day of training.

Voting 4

Page 18 of 324
Page 19 of 324

Third, security violations affect the perpetrators differently.

Pilots and flight attendants are strongly motivated to uphold

security procedures because their own lives could be at risk. A

rogue voter or pollworker, on the other hand, would have more

to gain and less to lose by surreptitiously changing the outcome

of an election.

Count the ballots by hand—it works for the Canadians.

Ballots are considerably longer and more complicated in the

United States than in many other countries. Whereas there is

just one contest in a Canadian federal election (each voter

selects a Member of Parliament), ballots in the United States can

contain dozens of contests. For example, a typical ballot1

for the

November 2004 general election in Orange County, California

contained 7 offices and 16 referenda, for a total of 23 contests

that would have to be tallied by hand. Ballots in Chicago, Illinois

that year2 were even longer: ten pages of selections, consisting

of 15 elected offices, confirmations of 74 sitting judges, and

one referendum—a total of 90 contests. When you appreciate

the scale of the task, it becomes easier to understand why many

people are motivated to automate the process with computers.

Hand-counting paper ballots is by no means impossible, but it

would be considerably more expensive and time-consuming in

the United States than in other countries with simpler ballots.

∗ ∗ ∗

In summary, voting is especially challenging because:

• All involved parties can gain by corrupting an election.

• Results can be incorrect without an obvious failure.

• Democracy demands verifiability, not just correctness.

• Voter privacy and election transparency are in conflict.

• Elections must be accessible and usable by the public.

• Ballots in the United States are long and complex.

1The example here is Orange County’s ballot type SB019 from November 2004, available in NIST’s collection

of sample ballots at http://vote.nist.gov/ballots.htm.

2 This refers to the “Code 9” ballot style in Cook County, Illinois (also available in NIST’s collection), used in

Ward 19, Precincts 28, 43(R), 48, 50(R), and 66, as well as precincts in Wards 21 and 34.

Voting 5

Page 19 of 324
Page 20 of 324

How does an election work?

Running an election is a tremendous organizational task. In the

end, it does come down to counting, but it’s what’s being

counted that makes it such a challenge. Election administrators

are, in effect, trying to take a fair and accurate measurement of

the preferences of the entire population—a controlled

experiment on a grand scale. As any psychologist will tell you,

performing experimental measurements on human subjects is

fraught with logistic pitfalls and sources of error. But elections

are worse: virtually everybody has an incentive to actively bias

the measurement toward their own preferred outcome. Thus,

elections involve a security element as well, unlike most

scientific measurements.

As if that weren’t enough, a typical election in the United

States is not just one opinion poll but many different polls

conducted on the same day—for federal, state, and local elected

offices, as well as state and local referenda—and each poll has

to be localized to a specific region. Each contest appears on

some ballots but not others, resulting in different combinations

of contests on different ballots. Each combination is called a

ballot style. Because there are so many kinds of districts (such

as congressional districts, state assembly districts,

municipalities, hospital districts, and school districts), and

district boundaries of each kind often run through districts of

other kinds, there can be over a hundred different ballot styles

in a single county. There can also be multiple ballot styles at

one polling place, if it serves voters on both sides of a district

boundary, or if there are different ballots for voters of different

political parties.

Process. Here is a simplified breakdown of the election process,

setting aside voter registration and considering only the

collection and counting of votes. The events before, during, and

after actual voting make up the three stages of the process:

preparation, polling, and counting.

Voting 6

Page 20 of 324
Page 21 of 324

• Preparation. Before any votes can be cast, election officials

must prepare the ballots. Election officials map out all the

different kinds of political districts, assemble the contests

that are relevant to each political district, compose the

contests into ballot styles, and determine which ballot styles

go to which polling places.

• Polling. At polling places, pollworkers sign in each voter and

make sure that each voter gets the correct style of ballot.

Each voter makes their selections privately and casts a

ballot. Voters may also have the option of voting by mail or

participating in “early voting” by showing up in person at a

special polling place before election day.

• Counting. The records of cast votes are counted, either at

the polling places or at a central election office. If counting

initially occurs at polling places, the counts are then

transmitted to the central office for tallying. The votes for

each contest are extracted from all the ballots on which that

contest appears, and tallied to produce a result.

Equipment. The preceding description is intentionally

ambiguous about whether paper or electronic voting is used,

because the same three stages take place regardless of the type

of equipment.

If paper ballots are used, a layout is prepared for each ballot

style, usually designed on a computer. Election administrators

estimate how many ballots of each style will be needed so that

an adequate number can be printed for distribution to polling

places. After being marked, paper ballots can be counted by

hand or scanned on machines (called optical scanning

machines). The scanning can take place at the polls (precinct

count optical scanning), where each voter feeds their ballot

through a scanning machine into a ballot box, or it can take

place at a central office, where all the paper ballots are gathered

and scanned in high-speed machines after polls close (central

count optical scanning).

An alternative to paper ballots is to make selections on an

electronic voting machine that directly records the selections in

Voting 7

Page 21 of 324
Page 22 of 324

computer memory. These machines are called direct recording

electronic (DRE) machines. In this case, preparing ballots

consists of producing ballot definition files on electronic media

(such as memory cards or cartridges) to be placed in voting

machines. The ballot definition determines what will be

displayed to the voter. (Machines for scanning paper ballots

also require ballot definitions that specify how the marks on the

paper should be counted.) Some DRE machines also print a

voter-verified paper audit trail (VVPAT)—a paper record of the

voter’s selections that is shown to the voter for confirmation,

but kept sealed inside the machine to enable later recounts.

∗ ∗ ∗

To sum up, there are three broad categories of elections in

terms of how machines are used:

1. Vote on paper; count by hand.

2. Vote on paper; count by machine.

3. Vote on machine; count by machine.

(3a. The voting machine may also produce a paper record.)

Voting 8

Page 22 of 324
Page 23 of 324

Why use computers for elections?

As the preceding description makes clear, all three stages of the

election process involve complex and detail-oriented work.

Preparation involves managing information about all the

different contests, candidates, and ballot styles. Polling involves

distributing this information and collecting results from all the

polling places. Counting involves consolidating all the votes for

each candidate in each contest across all the ballots and ballot

styles. With so many contests on the ballot, computers can

make this process much easier.

It’s not surprising that election administrators have looked

to computers for help with elections. Computers are used to

great benefit in automating a broad range of complex and

repetitive tasks and for recordkeeping functions throughout all

kinds of government agencies. Running an election involves

organizing and processing a lot of information, such as ballot

descriptions and vote tallies, and databases are effective tools

for managing this information.

The appeal of computers goes beyond their potential to

increase the speed and accuracy of the count. Computerized

vote-entry machines have much greater flexibility than paper

ballots in the method of presenting contests and choices to

voters. They can walk voters through the voting process,

provide more detailed instructions, and prevent overvotes. They

eliminate the possibility of ambiguous or improperly scanned

marks on paper. They can offer a larger selection of languages.

They can point out contests that a voter may have missed

before finalizing the marked ballot. They can even read the

names of candidates aloud, in headphones, for voters who have

trouble reading or voters who are blind. Some voters have

physical disabilities that prevent them from using pencil and

paper. Computerized vote-entry machines allow people to vote

using a variety of input devices, such as large buttons, foot

pedals, head-controlled switches, or switches controlled by air

pressure (“sip-and-puff” devices).

Voting 9

Page 23 of 324
Page 24 of 324

All of these things become possible when the voting process

is conducted by an interactive computer program instead of an

inert piece of paper. There appears to be a substantial rate of

voter errors when voting on paper ballots— in a Rice University

study of paper ballots [24], over 11% of the 126 ballots collected

contained at least one error. A friendlier and richer voting

interface offered by a computer might help voters avoid making

mistakes. Furthermore, the principle of equal rights demands

that we provide a way for disabled citizens to cast their votes

privately and independently.

∗ ∗ ∗

In short, computers can offer several advantages:

• Computers can help manage election-related data.

• Computers can count and tally votes faster.

• Counting by computer avoids human counting errors.

• Computers can offer a richer user interface to voters,

potentially improving accessibility and voter accuracy.

Depending on how computers are used in an election, some or

all of these advantages may apply.

1. Vote on paper; count by hand.

2. Vote on paper; count by machine.

3. Vote on machine; count by machine.

enrich voting

user interface

reduce

counting error

speed up

counting

manage

election data

For this type of election: Computers could be used to:

Figure 1.1. Advantages that computers could potentially offer for elections.

Voting 10

Page 24 of 324
Page 25 of 324

How did electronic voting become

controversial?

In November 2000, Florida’s confusing “butterfly ballot” and

heavily disputed punch-card recounts [2, 85] brought highly

public embarrassment to the United States election system. The

election system suffered widespread criticism on many fronts,

particularly for using an outdated counting mechanism.

Determined to avoid repeating this fiasco, policymakers and

election administrators looked to new technology for a solution.

The result was a growing wave of interest in electronic voting,

which many hoped would eliminate the ambiguity of punch

cards and provide fast, accurate counts.

Two years later, the U. S. Congress passed the Help America

Vote Act (HAVA) [78], authorizing hundreds of millions of

dollars to be spent on new voting machines. Disability

organizations were optimistic about the new requirement for

“at least one direct recording electronic voting system or other

voting system equipped for individuals with disabilities at each

polling place.” But computer scientists warned against a hasty

switch to electronic voting, citing damage to the transparency

and reliability of elections. Though electronic voting machines

were already in use in some localities (more than 10% of

registered voters used them in 2000 [22]), their adoption surged

after HAVA passed in 2002.

In early 2003, election activist Bev Harris made a startling

discovery [32]. She used Google to search for “Global Election

Systems”—the old name of the company that was acquired by

Diebold and renamed “Diebold Election Systems.” Diebold

Election Systems is one of the heavyweights of the United States

election systems industry; its touchscreen voting machine, the

AccuVote-TS, was the leading DRE machine used in the 2004

United States election [22]. By following the links from her

search results, Harris found a completely unprotected Internet

site containing a large collection of company files, including the

source code for the AccuVote-TS.

Voting 11

Page 25 of 324
Page 26 of 324

Researchers at Johns Hopkins University and Rice University

examined this source code and published a landmark

report [43] in May 2004, detailing their discovery of “significant

and wide-reaching security vulnerabilities.” They discovered

that voters could vote multiple times and perform

administrative functions; they found that cryptography was

both misused and missing where it should have been used; and

they expressed a lack of confidence in the quality of the

software in general, concluding that it was “far below even the

most minimal security standards applicable in other contexts.”

Their findings starkly contradicted Diebold’s public claims that

its system was “state-of-the-art,” “reliable,” “accurate,” and

“secure” [20].

The state of Maryland then commissioned reviews of the

same system from two other agencies: Science Applications

International Corporation (SAIC) and RABA Technologies. The

SAIC report [72], released in September 2003, confirmed that

the system was “at high risk of compromise,” and the RABA

report [64], released in January 2004, agreed that the “general

lack of security awareness, as reflected in the Diebold code, is a

valid and troubling revelation.”

In the 2004 U. S. general election, over 30% of voters cast

their votes on electronic voting machines [22]. Voters called in

thousands of reports of machine problems, including total

breakdowns, incorrectly displayed ballots, premarked choices

on the ballot, incorrectly recorded votes, undesired cancellation

of ballots or selections, and nonfunctioning or incorrect

audio [82].

Since 2004, further investigations have continued to tear

down the façade of confidence in the security of voting

machines, the claims of vendors, and the testing regime under

which the machines were certified. Media story after media

story reported on conflicts of interest, regulatory failures, and

newly exposed technical vulnerabilities in all the major voting

systems, not just Diebold’s.

In the summer of 2007, the California Secretary of State

conducted a “top-to-bottom review” of the voting systems used

Voting 12

Page 26 of 324
Page 27 of 324

in California, in which I had the opportunity to participate as a

reviewer. This was the broadest review of voting system source

code to date; the review included source code for DRE machines

and optical scan machines from each of three major vendors

(Diebold Election Systems, Sequoia Voting Systems, and Hart

InterCivic), as well as the election management software

responsible for ballot preparation and tallying. However, the

review teams only had five weeks to examine the source code.

Despite the short time frame, they found serious and pervasive

security problems in every system reviewed [7, 12, 35]. The

software was not written defensively; security measures were

inadequate, misapplied, or poorly implemented; the presence of

numerous elementary mistakes suggested that thorough testing

had not been done. In particular, every system was found

vulnerable to catastrophic viral attacks: the compromise of a

single machine during one election could affect results

throughout the jurisdiction and potentially affect the results of

future elections.

As of this writing, it has become clear that we cannot trust

our elections to the electronic voting machines of today’s

leading vendors. Whether we will ever be able to trust them

remains an open question. There is not yet a clear consensus on

what standards a voting machine should reasonably be

expected to meet. It is also by no means obvious that any set of

feasible technical requirements would yield a voting machine

worthy of our trust— it might simply be beyond the state of the

art to create a sufficiently reliable and economical electronic

voting machine. The point of this work is to make progress

toward a better design, so as to bring us closer to

understanding what is possible and to inform our standards

and expectations for these machines.

Voting 13

Page 27 of 324
Page 28 of 324

Why does software correctness matter?

Switching from mechanical to electronic voting machines is a

bigger step than it might seem at first. Today’s electronic voting

machines are not just electrically-powered devices performing

the same function as their mechanical predecessors, the way

electric light bulbs replaced oil-burning lanterns. Electronic

voting machines contain general-purpose digital computers,

which makes them fundamentally different and capable of

much more than the special-purpose machines they replace. It

would really be more accurate to call them “voting computers,”

as they are called in the Netherlands.

Just like any other general-purpose computer, a voting

computer can be programmed to do anything—count votes,

miscount votes, lie to voters, play games, or even attack other

computers. To prove the point, a Dutch group called “Wij

vertrouwen stemcomputers niet” (“We do not trust voting

computers”) reprogrammed the Nedap ES3B, their nation’s

leading voting computer, to play a passable game of chess [31].

Consequently, the types of attacks that are possible against

voting computers are also fundamentally different than those

possible against mechanical voting machines. Tampering with a

lever machine can cause it to lose some votes or stop working

entirely. Tampering with a computer can cause it to actively

engage in sophisticated schemes to deceive voters and

pollworkers, behave in different ways at different times or

under different circumstances, and even subvert or conspire

with other computers.

The behaviour of a general-purpose computer is determined

entirely by its software. Assuring the correctness of software

has been a major unsolved problem in computer science

research for decades. Computer scientists have been able to

prove some aspects of correctness for small programs, but all

will readily acknowledge that nobody knows a general method

for proving software programs to be correct. The software

developed in industry tends to be larger and more complex

Voting 14

Page 28 of 324
Page 29 of 324

than can be analyzed by the best known techniques, while the

programming languages and tools used in industry generally

lag behind the state of the art in research.

Mistakes in software can remain latent for years, even when

the code is publicly disclosed and inspected by motivated

programmers. For example, OpenSSH is a popular program for

secure login. Its developers have declared security to be their

number one goal [17], and they have gained a reputation for

security practices more rigorous than most. Nonetheless,

security flaws were discovered in OpenSSH in 2003 that had

been present since its first release in 1999, and had survived

intensive software audits by the OpenSSH team.

The problem is exacerbated by the possibility of insider

attacks: what if someone involved in writing the voting software

wants to bias the election? As far as anyone knows, the flaws in

OpenSSH were inadvertent mistakes, so intentional flaws can

probably be made even harder to find. (Chapter 8 offers some

anecdotal evidence that detecting purposely hidden software

flaws can be extremely difficult.) Reviewing the voting software

is not just a matter of looking for code that seems intended to

change votes or tallies. Any flaw that lets an attacker infiltrate

the machine is a serious problem, since that flaw can then be

exploited to reprogram the machine to do anything. So, a

malicious programmer of voting machine software doesn’t have

to write suspicious-looking vote-altering code; he or she only

needs to leave an innocent-looking security weakness. When a

security weakness is found, there’s no way to tell whether it is

an intentional backdoor or an inadvertent mistake—as long as

someone knows the flaw, it can be exploited. If any flaw can be

an attack, we need voting software to be essentially flawless.

All of this explains why this dissertation focuses on

software correctness. There are people who have many years of

experience managing election personnel and running

paper-based elections. There are people who know how to build

reliable machines and reliable computer hardware. But the part

that no one fully understands yet is how to get the software

right.

Voting 15

Page 29 of 324
Page 30 of 324

2 Correctness

What constitutes a democratic election? 17

What does it mean for a voting system to be correct? 19

How does correctness relate to safety? 20

What is the tree of assurance goals for an election? 24

What does it mean for a voting system to be secure? 30

16

Page 30 of 324
Page 31 of 324

What constitutes a democratic election?

The democratic ideal of a legitimate election requires that the

results reflect an unbiased poll of the voters—accurate

according to what each voter intended, and fair in that each

eligible voter has equal and unhindered opportunity to

influence the outcome. These two basic goals can be broken

down according to the mechanics of how elections are run.

Accuracy. By “accurate,” I mean that the data about voter

preferences is accurately gathered and combined to produce the

final result. To make this happen, each ballot has to be

processed correctly at the three stages of voting:

• Correct ballot: Each voter should be presented a ballot with

complete and accurate information on the contests for

which they are eligible to vote.

• Cast as intended: Each voter’s recorded vote should match

what the voter intended to cast.

• Counted as cast: The calculation that decides the outcome

should accurately incorporate every recorded vote and no

extraneous votes.

Fairness. By “fair,” I mean that eligible voters (and only eligible

voters) are free to vote as they please, without bias. We can look

at this from two angles: how the sample of voters is drawn from

the population, and how the opinions of the voters are

measured.

• Unbiased sampling: Votes should come from a fair sample

of the population of eligible voters.

• Unbiased measurement: Each vote should be a fair

measurement of a voter’s preference.

Each of these two aspects of fairness can be elaborated in

further detail. In modern democracies, fair sampling is upheld

through measures aimed at offering equal access to the polls,

and also through the principle of “one person, one vote.”

Correctness 17

Page 31 of 324
Page 32 of 324

• Unbiased sampling is achieved by ensuring:

Authorized voters: Only voters that are eligible for a

contest should be permitted to vote on it.

One ballot per voter: No voter may cast more than one

ballot.

Equal suffrage: Every voter eligible for a contest should

have an equitable opportunity to vote on it.

An unbiased measurement depends on eliminating influence

from external pressures as well as influence from the

presentation of the ballot itself.

• Unbiased measurement is achieved by ensuring:

Secret ballot: No voter’s choices should be exposed by

the voting system or demonstrable by the voter to

others, lest votes be influenced by social pressure,

bribery, threats, or other means.

Equal choice: Every option in a contest should have an

equitable opportunity to receive votes.

Democracy also demands a further virtue: since power is

derived from the consent of the governed, the election process

itself must be accountable to the people. The manner in which

all of the above goals are achieved should be verifiable, so that

members of the public can assure for themselves that the

election is accurate and fair. The verifiability of the election is

not listed among the above goals because it is a “meta-goal,”

like a layer on top of all the other goals.

A widely preferred avenue for achieving verifiability is

through transparency—exposing the election process to public

scrutiny. However, verification can also take place through the

investment of trust in independent experts or inspectors (or

suitably balanced committees thereof), or through

cryptographic means, in which a calculation provides

mathematical evidence of the property to be verified.

Correctness 18

Page 32 of 324
Page 33 of 324

What does it mean for a voting system to be

correct?

In order to be confident that an election is democratic, we

would want to have assurance of all of the goals just

mentioned. But these goals are for the election as a whole,

including all the people, processes, and technology involved.

When we talk about a particular piece of equipment, such as a

voting machine, we have to choose a specific set of subgoals

that it is responsible for. For example, a voting machine cannot,

by itself, guarantee that each voter only votes once. However, if

the machine requires something like an access card in order to

cast each ballot, this feature in combination with a suitably

controlled process for handing out access cards, carried out by

competent, trustworthy pollworkers, can effectively limit each

voter to casting just one ballot.

Every goal is achieved through some combination of human

processes and technology. This dissertation is primarily

concerned with the technological part of an election—the

equipment and software involved in collecting and counting

votes, which I am calling the “voting system” for short. To say

that the voting system works correctly means that it fulfills the

responsibilities that have been assigned to it. Only after we’ve

decided on this assignment of responsibilities is it meaningful

to say whether it is correct. As the access card example

illustrates, it is usually necessary to subdivide goals in some

detail in order to separate out subgoals that technology can

address.

Correctness 19

Page 33 of 324
Page 34 of 324

How does correctness relate to safety?

Engineers have been designing safety-critical systems for many

years, so it’s instructive to examine the research and practice in

methodologies for developing these systems.

Analysis. One of the most common analysis techniques for

safety-critical systems is fault tree analysis [83]. Fault tree

analysis is a way of identifying all the ways that a particular

failure can occur. To perform fault tree analysis, one begins

with a root node that represents the undesired event (the fault);

then one identifies all the events or situations that could cause

that undesired event, and each one becomes a child of the root

node. Each node can be further refined by adding children that

identify possible causes. For example, a few nodes in a fault tree

for a fire extinguisher might look like this:

fire extinguisher

fails to deploy

pin is stuck in

handle

insufficient pressure

in tank

gas has leaked out

of the tank

fire extinguisher has

been previously used

Figure 2.1. A small portion of a fault tree for a fire extinguisher.

Fault trees are known in the computer security world as

threat trees [3] or attack trees [70]. An attack tree lays out all

the possible ways that an attacker might come to violate a

specific security restriction. In an attack tree, the top node is

the attacker’s ultimate goal. The children of a node specify

various ways that an attacker can achieve the goal. For example,

if the ultimate goal is to break open a safe, an attacker could do

Correctness 20

Page 34 of 324
Page 35 of 324

so by obtaining the combination or by drilling open the safe.

Part of the attack tree might look like this:

open the safe

drill the safe obtain the

combination

manipulate the safe bribe someone who

knows the combination

Figure 2.2. A small portion of an attack tree for an attacker who wants to break into a safe.

In the above examples, any one of the children of a node is

sufficient to lead to the parent; the relationship among siblings

is a disjunction (OR). Fault trees and attack trees can also

specify conjunctions (AND) and other logical relationships. The

nodes can be labelled with numbers to indicate the probability

of an event or the cost of a step in an attack.

Design. Fault trees and attack trees are used to analyze existing

systems to identify their weaknesses. But when one is designing

a system, the goal is to establish the system’s worthiness.

In the safety-critical literature, a written justification of a

system’s safety is called a safety case [87]. Safety cases are

required by many safety standards. A safety case is often a very

large document, as it incorporates all the arguments and

supporting evidence for the safety of each element of the

system. The development of the safety case can take up a large

fraction of the effort in designing a safety-critical system.

Hence, significant research efforts have been directed toward

ways of organizing and maintaining safety cases.

Like fault trees, safety cases are also typically structured in

a top-down approach based on successive refinement. The

technique that is probably the most prominent in the research

Correctness 21

Page 35 of 324
Page 36 of 324

literature is the Goal Structuring Notation [41], which elaborates

on a basic tree-like organization of goals by allowing nodes of

several different types: goals, strategies, justifications,

assumptions, and so on. Here is an example of a section of a

safety case for a microwave oven diagrammed in Goal

Structuring Notation:

microwave is

acceptably safe

argument that

radiation

emission levels

are safe

emission levels are

safe when door is

closed

emission levels are

safe when door is

open

results of

radiation

testing

argument that

door interlock

deactivates

emitter

. . .

. . .

Figure 2.3. Part of a safety case for a microwave oven in Goal Structuring Notation.

Voting systems. A safety case would be appropriate for

justifying why we should place our confidence in a voting

system. Ideally, certification of any voting system for

deployment would require the manufacturer to provide a

convincing and clearly structured safety case.

The hierarchy of goals for a democratic election form the

Correctness 22

Page 36 of 324
Page 37 of 324

starting point for such a safety case. The process of dividing

goals into subgoals produces a tree of assurance goals for a

system, which I’ll call an assurance tree. (An assurance tree

could be considered a simplified instance of Goal Structuring

Notation in which all the nodes are correctness goals.) When an

assurance tree is fully elaborated, the leaves of the tree are

individual responsibilities that can be assigned to specific

people and specific devices.

The process of refining the general goals into specific

subgoals is a type of design activity. Different solutions will

subdivide the main goals differently and assign responsibilities

for the subgoals differently. For example, access cards are one

possible way to keep voters from voting multiple times, but of

course they are not the only way. It is a design choice to

implement “one ballot per voter” in terms of the two parts:

“pollworkers give one access card to each eligible voter” and

“the voting machine allows each access card to be used just

once to cast a ballot.” Making these design choices and refining

the goals at every level eventually leads to a set of specific

technical requirements for the voting system.

In an assurance tree, the children of each node indicate

what requirements have to be upheld in order for the parent

goal to be upheld. The final result of refining the tree is an

assignment of specific responsibilities to various parts of the

system—for example, a set of tasks to be carried out by

humans and a set of tasks to be carried out by computers—

such that all the assurance goals are upheld. The tree captures

the design of the system as well as the security assumptions

that the designer made.

Correctness 23

Page 37 of 324
Page 38 of 324

What is the tree of assurance goals for an

election?

The requirements that were presented earlier can be refined one

step further without specifying a particular voting system

design. First I’ll explain each subgoal, then present the whole

tree, which can form a basis for the safety case of any election.

Accuracy: correct ballot. In order for a voter to receive a

correct ballot, the correct ballot has to exist for that voter and it

must contain the correct instructions and choices for the

election. The voter then has to be given the right kind of ballot,

and the voter has to receive it without alteration.

Accuracy: cast as intended. The voter’s vote is properly

recorded if the ballot indicates what the voter wanted and is

cast when the voter is ready. Choices should be selected if and

only if the voter makes them, and the voter should be free to

mark the ballot in any manner that is valid. (When paper is

used, the voter can also cast an invalid ballot; then the ballot is

not counted. When electronic machines are used, the machine

usually prohibits the voter from marking the ballot in an invalid

manner.) To further ensure that the cast ballot matched the

voter intent, the voter should get accurate feedback about what

is currently selected, and should be able to make changes or

corrections before casting the ballot.

Accuracy: counted as cast. For the count to be correct, there

must be no extra or missing votes, and the votes that are

counted must be exactly as voters indicated them on their cast

ballots.

Fairness: authorized voters. I use the term voting session for

the interval that begins with a voter entering a protected area of

the polling place such as a voting booth, and ends when the

voter walks away, either having cast or failed to cast a ballot. In

Correctness 24

Page 38 of 324
Page 39 of 324

a typical election, voter authorization consists of controlling

access to voting sessions and ensuring that there is no other

way to cast a ballot except in a voting session.

Fairness: one ballot per voter. Limiting each voter to one cast

ballot is also achieved by controlling access to voting sessions.

In practice, each voter is authorized for one voting session at a

time. If a voter wants to try again, a pollworker either destroys

the ballot or determines that the voter did not already cast a

ballot, and then authorizes another voting session.

Fairness: equal suffrage. There are three steps to casting a

ballot. First the voter has to get to a polling station. Then, at the

polling station, the voter has to be allowed to begin a voting

session. Then, in the voting session, the voter has to

successfully cast the ballot. Equal suffrage demands that voters

have reasonable access and be free of discrimination at all of

these stages.

Another way that a voter can be disenfranchised is to make

an error. It is infeasible to demand that there be no errors at all,

but fairness requires that errors not be biased against any

particular group of voters. The controversy over the 2006 race

for Florida’s Congressional District 13 highlighted the

significance of biased error. Different voters saw different ballot

layouts, and post-election analysis [29] has suggested that the

particular layout used in Sarasota County caused a large

fraction of voters to skip the congressional race by mistake.

Fairness: secret ballot. The election system should not itself

violate the voter’s privacy. But it’s a tougher task to prevent

coercion. Voters’ susceptibility to influence may not be based in

reality: as long as voters believe they will profit or suffer by

voting a certain way, the belief is sufficient to influence their

votes. For example, an attacker could claim to have insider

access that allows him to identify which voters voted for a

particular candidate and punish them. Whether or not the

attacker has such insider access, or whether discovering voters’

Correctness 25

Page 39 of 324
Page 40 of 324

identities is even possible, the fear of punishment could be

enough to sway votes. Different kinds of voting systems will

lend differing degrees of plausibility to such claims—for

example, some voters might be easily persuaded that someone

could violate their privacy via computerized vote records, but

they might find it harder to see how such a violation would be

possible with hand-counted paper ballots.

The formal definitions of coercion-resistance in the research

literature [18, 38, 60] require that voters be unable to prove to a

vote-buyer that they voted a certain way. But the issue is more

nuanced than that. A vote-buyer doesn’t need solid proof, just

evidence sufficiently plausible that offering a reward for it will

influence the vote.

For example, consider an election system in which voters

receive receipts indicating how they voted, but could also forge

such receipts. One might think that such an election system is

coercion-resistant, since it isn’t worthwhile for a vote-buyer to

buy something that can be forged. But resistance to coercion

also depends on the cost of producing a forgery: if forgeries

require enough effort that a significant number of voters will

vote as directed by the vote-buyer instead of carrying out the

forgery, the vote-buyer will succeed at influencing the election.

Therefore, the secret ballot goal includes the requirement that

voters not be given any plausible evidence (not just hard proof)

of their votes that could be sold to an external party.

Fairness: equal choice. Since the goal is to avoid bias among

the options within a contest, it would not do for some of the

options to be shown one way to some voters and a different way

(say, in red, or in larger print) to others.

It would be ideal to avoid all bias among options presented

on the same ballot, but this is not possible: some option has to

be presented first, and there is a well-documented bias toward

the first item [46]. The next best thing is to change the order of

presentation from ballot to ballot such that there is a uniform

distribution of bias towards all the options, when the ballots are

considered in aggregate.

Correctness 26

Page 40 of 324
Page 41 of 324

There is a more subtle kind of bias that also should be

avoided: a bias relative to the voter’s preferred choice. Imagine,

for example, a contest with three options A, B, and C. Suppose

the ballot design causes half the voters who intend to mark A to

mistakenly mark B, half of those who want B to mark C, and

half of those who want C to mark A. Such a ballot is not biased

toward any particular option, but it is still clearly unfair: B

could win an election in which most voters intended to vote for

A. So there is also a requirement for a uniform distribution of

errors with respect to the voter’s intended choice.

∗ ∗ ∗

Gathering all the requirements just mentioned gives us the

following high-level assurance tree for elections.

Accuracy

• Correct ballot

G1. For every voter, there exists a ballot style containing

the complete set of contests in which that voter is

eligible to vote.

G2. On every ballot, all the information is complete and

accurate, including instructions, contests, and

options.

G3. In every voting session, the correct choice of ballot

style is presented to the voter.

G4. Every ballot is presented to the voter as the ballot

designer intended.

• Cast as intended

G5. At the start of every voting session, no choices are

selected.

G6. The voter’s selections change only in accordance

with the voter’s intentions.

G7. The voter receives accurate feedback about which

choices are selected.

G8. The voter can achieve any combination of selections

that is allowable to cast, and no others.

Correctness 27

Page 41 of 324
Page 42 of 324

G9. The voter has adequate opportunity to review the

ballot and make changes before casting it.

G10. The ballot is cast when and only when the voter

intends to cast it.

• Counted as cast

G11. Every selection recorded on a ballot cast by a voter is

counted.

G12. No extra ballots or selections are added to the count.

G13. The selections on the ballots are not altered between

the time they are cast and the time they are counted.

G14. The tally is a correct count of the voters’ selections.

Fairness

• Unbiased sampling

Authorized voters

G15. Only authorized voters can begin voting

sessions.

G16. Only in voting sessions can ballots be cast.

One ballot per voter

G17. No voting session allows more than one ballot to

be cast.

G18. Each voter is allowed at most one voting session

in which a ballot was cast.

Equal suffrage

G19. Every voter has reasonable, non-discriminatory

access to a polling station they can use.

G20. Every voter can begin a voting session within a

reasonable, non-discriminatory waiting time.

G21. Every voting session provides a reasonable,

non-discriminatory opportunity to cast a ballot.

G22. For every voter that is eligible to vote in a

particular contest, there is a uniform likelihood

of voter error on that contest.

• Unbiased measurement

Secret ballot

G23. The processing of voter choices does not expose

how any particular voter voted.

Correctness 28

Page 42 of 324
Page 43 of 324

G24. Voters are not provided any way to give plausible

evidence of how they voted to an external party.

Equal choice

G25. Within each contest, all the options are

presented in the same manner on each ballot

and across all ballots.

G26. For each contest, the voters are presented with

ballots that, in aggregate, yield a uniform

distribution of bias in favour of each option.

G27. For each contest, the voters are presented with

ballots that, in aggregate, yield a uniform

frequency of voting errors across the voters that

intend to vote for each option.

G28. In each contest, for each option, voters intending

to vote for that option are presented with ballots

that, in aggregate, yield a uniform distribution of

voting errors in favour of every other option.

Correctness 29

Page 43 of 324
Page 44 of 324

What does it mean for a voting system to be

secure?

A voting system is secure if it can be relied upon to produce the

correct results in the face of determined attempts to corrupt

the outcome. Thus, security and correctness are closely related:

security is just correctness in an adversarial context. The

intentional violation of any subgoal in the assurance tree would

constitute a security breach.

Since this dissertation is focused on the software security

questions surrounding electronic voting machines, let’s separate

out the goals that rely on software from those that don’t.

Of the goals in the assurance tree, these are normally addressed

by humans in the preparation and conduct of the election:

G1. For every voter, there exists a ballot style containing the

complete set of contests in which that voter is eligible to

vote.

G2. On every ballot, all the information is complete and

accurate, including instructions, contests, and options.

G18. Each voter is allowed at most one voting session in

which a ballot was cast.

G19. Every voter has reasonable, non-discriminatory access to

a polling station they can use.

The following goals are addressed through good ballot design.

They could be violated by voting machine software that displays

the ballot incorrectly or lacks the ability to display ballots in a

fair manner. However, as long as the voting machine presents

the ballot as the ballot designers intended (which is goal G4), we

can consider these goals the responsibility of ballot designers:

G22. For every voter that is eligible to vote in a particular

contest, there is a uniform likelihood of voter error on

that contest.

G25. Within each contest, all the options are presented in the

same manner on each ballot and across all ballots.

Correctness 30

Page 44 of 324
Page 45 of 324

G26. For each contest, the voters are presented with ballots

that, in aggregate, yield a uniform distribution of bias in

favour of each option.

G27. For each contest, the voters are presented with ballots

that, in aggregate, yield a uniform frequency of voting

errors across the voters that intend to vote for each

option.

G28. In each contest, for each option, voters intending to vote

for that option are presented with ballots that, in

aggregate, yield a uniform distribution of voting errors

in favour of every other option.

The following goals could be addressed almost entirely by

election-day procedures, or through a combination of such

procedures and proper software behaviour, depending on how

the voting system is designed:

G15. Only authorized voters can begin voting sessions.

G16. Only in voting sessions can ballots be cast.

The proposed designs in this dissertation assume that the

above two goals are upheld by human procedures. For G15,

election workers ensure that only authorized voters are

permitted physical access to voting machines. And for G16,

election workers should provide no other way to cast ballots

outside of the officially approved procedures.

The remaining goals are those that necessarily depend on the

correctness of the voting machine software implementation:

G3. In every voting session, the correct choice of ballot style

is presented to the voter.

G4. Every ballot is presented to the voter as the ballot

designer intended.

G5. At the start of every voting session, no choices are

selected.

G6. The voter’s selections change only in accordance with

the voter’s intentions.

G7. The voter receives accurate feedback about which

choices are selected.

Correctness 31

Page 45 of 324
Page 46 of 324

G8. The voter can achieve any combination of selections that

is allowable to cast, and no others.

G9. The voter has adequate opportunity to review the ballot

and make changes before casting it.

G10. The ballot is cast when and only when the voter intends

to cast it.

G11. Every selection recorded on a ballot cast by a voter is

counted.

G12. No extra ballots or selections are added to the count.

G13. The selections on the ballots are not altered between the

time they are cast and the time they are counted.

G14. The tally is a correct count of the voters’ selections.

G17. No voting session allows more than one ballot to be cast.

G20. Every voter can begin a voting session within a

reasonable, non-discriminatory waiting time.

G21. Every voting session provides a reasonable,

non-discriminatory opportunity to cast a ballot.

G23. The processing of voter choices does not expose how

any particular voter voted.

G24. Voters are not provided any way to give plausible

evidence of how they voted to an external party.

G3 and G20 depend on election-day procedures as well as the

voting machine software. For G3, typically a pollworker is

responsible for selecting the correct ballot style for each voter,

and the voting machine must correctly use the ballot style

indicated by the pollworker. For G20, the polling station needs

to serve voters efficiently and fairly, but also the voting

machines should be available and ready to serve voters and

should not freeze up or crash. G23 and G24 depend on the

overall design of the voting system, including the human

procedures, as well as the correct functioning of the voting

machine software.

Security issues with voting machine software usually have to do

with upholding and enforcing the 17 goals in this last list.

These 17 goals are the focus of my efforts to achieve and verify

software correctness.

Correctness 32

Page 46 of 324
Page 47 of 324

3 Verification

How do we gain confidence in election results? 34

How can we verify the computerized parts of an election? 36

What kind of election data can be published? 39

What makes software hard to verify? 41

In what ways are today’s voting systems verifiable? 44

What is the minimum software that needs to be verified? 48

What other alternatives for verification are possible? 52

33

Page 47 of 324
Page 48 of 324

How do we gain confidence in election results?

An election consists of many steps, each of which processes

information such as ballot and candidate data, voter

information, and records of cast votes. At the most basic level,

each step takes some input and produces some output.

Confidence in the ultimate result—the output of the last step in

the chain—depends on confidence that each step was correctly

performed. The choice of the type of voting system determines

which steps are carried out by people and which by computers.

Earlier we described the election process in terms of three

stages: preparation, polling, and counting. With respect to

establishing confidence in a voting system, these stages can be

broken down further into the nine steps shown at the left, which

include transmission as well as processing of information.

design

ballots

present

ballots

count

votes

tally

subtotals

distribute

ballots

mark or

enter votes

collect

votes

transmit

subtotals

Preparation

Polling

Counting

cast

votes

The preparation stage consists of events prior to the

opening of polls, which includes not only designing the ballots

but also distributing them to polling places. This production

and distribution takes place for both paper ballots and

electronic ballot definition files.

The polling stage involves presenting the ballots to voters,

who make selections and cast the ballots. For sighted voters

reading paper ballots, presentation of the ballot is a trivial step,

but for electronic voting computers the fidelity of the

presentation is a real issue.

In many elections, counting occurs in two parts: votes are

first counted at polling places, then the counts are centrally

tallied to yield the final results. This stage includes the

transmission of votes to the person or machine that counts

them. The distinction between local and central counting is

important because the local counting process often takes place

in public, whereas the aggregation of results and central tallying

does not.

For a step that transforms information from one form to

another, confidence comes from ensuring that it produced the

correct output for the input it was given. For a step that

Verification 34

Page 48 of 324
Page 49 of 324

transports information from one place to another, confidence

comes from ensuring that the integrity of the information was

preserved.

Because of the way I’ve defined the three accuracy goals

(correct ballot, cast as intended, and counted as cast), they differ

slightly from the three chronological stages: getting the correct

ballot to the voter includes the presentation step at the polls.

The following figure shows which steps correspond to the three

accuracy goals. Under each step is the name of a subgoal for

that step.

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots count

votes

collect

votes tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

Preparation Polling Counting

Figure 3.1. The nine steps in the election process and their corresponding integrity and

correctness goals.

Verification 35

Page 49 of 324
Page 50 of 324

How can we verify the computerized parts of

an election?

Suppose that a particular information processing step in an

election is carried out by a computer. As I mentioned in

Chapter 1, the computer’s behaviour is completely controlled by

its software. Let’s say the software program responsible for this

step takes some input x and produces some output y. For

example, if this is the vote-tallying step, x could be a collection

of electronic vote records and y could be the election totals.

input

x

output

y program

Figure 3.2. For some particular processing step in an election, a software program takes

the input x and produces the output y.

If you want to check that the program produced the correct

result, you have two main choices:

1. Software verification. You can examine the program itself

and confirm that it works the way you expected. Depending

on the assumptions you make, this may include manual

inspection of the source code, automated analysis, or formal

mathematical proofs. Once you have confirmed that the

program does exactly what it’s supposed to do in every

possible circumstance, you can be confident that this

particular output, y, is correct.

2. Result verification. You can take the input x and figure out

what the corresponding output should be. If the actual

output y matches the expected output, then you know it’s

correct. To do this, you need records of both x and y, as well

as some way to independently repeat the operation—

perhaps you have another program that you trust, or

perhaps you can work out the expected output by hand.

Verification 36

Page 50 of 324
Page 51 of 324

There is also a variant of result verification:

2a. Indirect result verification. Some schemes allow you to

establish confidence without repeating the entire operation.

For example, given information derived from x and y, you

might have a way to mathematically check their consistency.

Or, you might be allowed to choose parts of x and y to

check, enabling you to establish a high probability of a

correct result.

Software verification has the advantage that it only needs to be

done once on a given program to establish confidence in all the

output it will ever produce. Result verification has to be

repeated each time the program produces new output.

However, there are three major factors weighing in favour of

result verification.

Programs change. The apparent advantage of doing software

verification only once becomes less compelling when you

consider that software changes all the time. Features are added;

bugs are discovered and fixed; demands change. In particular,

election software is subject to election law, which differs from

state to state in the United States. Whenever legislation gets

passed, election software may have to be updated to satisfy new

requirements. Any change would invalidate previous reviews or

proofs of correctness and require the software to be verified

over again.

Software verification requires disclosure. Disclosure of

software code often faces legal, financial, or political barriers.

Voting machine companies have resisted public disclosure of

their source code on the grounds that it could help a motivated

attacker, and they claim that copyright and trade secret

protection are necessary to support a sustainable, profitable

business. [34] Disclosing code would certainly increase the

transparency of an election and improve the accountability of

the testing process. But having ways to check the correctness of

an election without depending on disclosure of all the code

would allow the election to sidestep this disclosure dispute. The

Verification 37

Page 51 of 324
Page 52 of 324

democratic process is healthier if private interests have fewer

opportunities and fewer plausible incentives to prevent the

public from verifying an election.

Software verification is much harder. As a later section of this

chapter will explain (page 41), the behaviour of software can be

extremely difficult to analyze. Software review by human

experts is expensive, time-consuming, and prone to error. The

only way to be truly sure is to construct a mathematical proof,

but it is well beyond the state of the art to do this for programs

the size of typical computer applications. When such proofs are

constructed, they often aim to prove things about a simplified

model of the program rather than the program itself.

Unfortunately, a mathematical proof can only prove that a

program satisfies a formal specification of what it’s supposed

to do. The proof only establishes that the program is correct if

the specification accurately expresses what it means to be

correct—and such specifications are themselves complex and

tricky to write.

Verification 38

Page 52 of 324
Page 53 of 324

What kind of election data can be published?

There is an inherent tension between voter privacy and the

desire for verifiable elections. As argued earlier in this chapter,

verifying results is preferable to verifying software. But public

verification of results depends on publishing election data.

Suppose there is some data made available to the public to

enable verification. This might include partial or complete

information about ballots, votes, and results, or something

derived from such data. Each published piece of data (let’s call

it a record) might be identifiable as corresponding to a

particular voter, or it might not. And each record might contain

sufficient information to reveal votes, or it might not. These two

features are independent: for example, a published record could

indicate a vote for a particular candidate, yet not be associated

with any particular voter.

For voters to be able to check that their own ballot was

correctly received (i.e., cast as intended), they need to be able to

look up their own ballots. To do this, they need some kind of

public record of their ballot that is identifiable.

For voters to be able to confirm the tally by directly

performing their own recount, they have to be able to see the

votes. To do this, they need public records that reveal votes.

Published records that are identifiable and reveal votes

would enable the public to verify everything, at the expense of

voter privacy. Imagine an election in which every ballot is

published online and uniquely associated with the voter who

cast it. Any voter could look up their ballot online to confirm

that it is correct as published, and anyone could count the

published ballots to confirm the tally. In such a system,

software correctness would be irrelevant—software could be

used at any stage of the process and there would be no need to

verify it, because the entire election can be checked by result

verification. But in such an election, voters could also easily sell

their votes—for example, they could tell a vote-buyer where to

find their ballots online.

Verification 39

Page 53 of 324
Page 54 of 324

∗ ∗ ∗

In summary:

• Public confirmation that ballots are cast as intended

requires public records that are identifiable.

• Public confirmation of the tally by direct recount requires

public records that are vote-revealing.

• If any public records are identifiable and vote-revealing,

they enable bribery and coercion.

This suggests two possible kinds of public records:

1. Anonymous records that do reveal votes.

2. Identifiable records that don’t reveal votes.

Several proposals for voting systems, including those proposed

in this dissertation, publish records of the first kind. These

records enable direct result verification of the tally. Later in this

chapter, I’ll discuss end-to-end cryptographic voting systems, in

which both kinds of records are published, and an additional

verification step confirms the correspondence between the two.

Verification 40

Page 54 of 324
Page 55 of 324

What makes software hard to verify?

Most software is hard to verify because it is complex.

Here are some of the main reasons why complexity in

software is more difficult to manage than complexity in a

physical machine.

Number of components. The number of parts in a physical

machine is limited by the costs of manufacturing, but there is

no such limit on software. A software program costs the same

to distribute—virtually nothing—whether it contains ten

components or a million components. It is easier to add

complexity to a software program than to a physical device, and

removing code often has a higher risk of breaking the program

than adding new code. Requirements change and customers ask

for more features; in response, software tends to grow

boundlessly during the course of development, unless there are

determined and persistent efforts to keep it small.

Software programs also often incorporate large ready-made

packages of components written by others, to save the effort of

writing code from scratch. Even if only a small part of a

package’s functionality is used, it is easier to include the entire

package than to separate the parts that are used from those

that are not. These pressures lead to software applications with

millions of lines of code and thousands of interacting

components.

Complex interconnections. There are likely to be more

connections between the parts of a software program than

those of a physical machine. Whereas a machine part can only

interact with other parts near it, there is no limit on the number

of other parts that a software component can depend on. For

example, it is common for a single component to be relied upon

by thousands of other components.

These connections are also harder to see in software. The

way that a machine part affects other parts is usually clear from

Verification 41

Page 55 of 324
Page 56 of 324

direct physical inspection. But finding all the other software

components that depend upon a given software component can

be a difficult task.

Far-reaching effects. Because software components can be so

deeply interconnected, a small change in one part can affect

another part that is far away, affect parts written by different

people, or have wide-ranging effects on the behaviour of the

whole program. The software engineering practices of

modularity (dividing up a program into distinct modules) and

encapsulation (protecting each module from outside

interference) aim to limit these kinds of effects, but software

programs nonetheless tend to be more sensitive to change than

physical machines.

Nonlinearity. The power of general-purpose computers derives

from their ability to make decisions. With software, a tiny

change in input can yield a completely different outcome; for

example, a program can decide to behave one way when the

result of a calculation turns out to be zero and another way

when it is nonzero. This means that similar situations cannot be

assumed to yield similar behaviour. This nonlinear nature

makes it hard to predict how software will behave and hard to

test software thoroughly. Mechanical devices can be nonlinear

too, but software tends to be pervasively nonlinear.

∗ ∗ ∗

One of the most serious threats that is currently poorly

addressed in voting systems is the insider threat from software

developers. Intentionally placed bugs or backdoors are hard to

detect even when software is carefully audited [5]. The

persistent failure of the federal testing process to detect major

security flaws [21, 37] and the continuing revelations of security

vulnerabilities in certified voting systems [33, 43, 64, 84, 88]

suggest that voting software has not been audited anywhere

near enough to defend against this threat.

Verification 42

Page 56 of 324
Page 57 of 324

The complexity of software is what makes it difficult to be

sure: sure that the software will behave as expected, that it will

produce the correct results, and that it will resist determined

attempts to subvert the outcome of an election. Software

complexity is the ultimate enemy of reliable computer-based

elections.

There are two ways to fight this enemy: design the system

so less of the software needs to be verified, and simplify the

software that needs to be verified. Both can be applied together.

Verification 43

Page 57 of 324
Page 58 of 324

In what ways are today’s voting systems

verifiable?

Different voting systems offer different ways for voters to gain

confidence that the election results are correct. We can compare

systems by looking at what mechanism for assurance is

provided, if any, at each step of the process.

The two kinds of voting technology most commonly used in

the United States are optical scan systems and direct recording

electronic (DRE) systems.

Optical scan voting. When an election is conducted by optical

scan, paper ballots are prepared and printed before polls open.

Voters mark the ballots by hand and deposit them into a ballot

box. There are two variants of optical scan voting: the scanning

can take place at individual precincts or at a central election

office.

Although software is usually involved in preparing the

ballots, voters and candidates can verify for themselves the

sample ballots published before polling. Voters can also bring

sample ballots to the polling place and compare them with the

blank ballots they receive. This is an example of avoiding

software verification, which is possible because the results of

the preparation stage are public.

We know the ballot is presented exactly as prepared,

because the voter directly reads the printed paper. There is no

recording device to misrecord the voter’s marks; the voter is

responsible for clearly marking the paper to be counted. The

election relies on the physical durability of paper for the

integrity of printed ballots and recorded votes.

A precinct-based

optical scanner.

When scanning takes place at individual precincts, the

ballots pass through a scanning machine on their way into the

ballot box. After polls close, each machine prints out its counts

on a paper tape. If the paper tapes are posted immediately for

public viewing, then no one has to trust the software that does

the tallying. The final election report will contain both the

Verification 44

Page 58 of 324
Page 59 of 324

counts in each precinct and the overall totals. Anyone can

confirm that the locally posted results are correctly included in

the election report, and anyone can confirm that the overall

totals were calculated properly.

When scanning is performed centrally, voters can’t perform

the same check on the tally step. They have to trust election

personnel to safely transport the ballots from the polls to the

central office and to enter the results from the central scanner

into the software that tallies them (known as the election

management system, or EMS).

Figure 3.3 summarizes the mechanisms by which any

individual voter can ensure the validity of each step in this

process. (I’ll call this an assurance chart.)

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

published sample ballots paper

ballot box

in public view

results posted

at each

precinct

subtotals and

totals posted

online

precinct

optical scan

central

optical scan

election administrators recount ballots

scanner

personnel personnel

ballot box

in public view EMS

EMS

scanner

Figure 3.3. Assurance chart for elections with hand-marked, optically scanned ballots.

The starbursts mark mechanisms that voters have to accept

on faith—they have to trust software they can’t see or people

they don’t know. For precinct-based scanning, voters have to

trust the software that controls the optical scanner. For central

scanning, the voters also have to trust the personnel who collect

the ballots and convey counts from the scanner to the EMS.

They also have to trust the EMS itself, since they have no way to

independently check that the totals were added up correctly.

Paper ballots provide a useful backup record, as they can be

recounted by hand or by machine. The same stack of ballots can

even be counted multiple times, and the counts from different

people or different machines can be compared to improve

Verification 45

Page 59 of 324
Page 60 of 324

confidence. In Figure 3.3, recounts are shown as a secondary

assurance mechanism, below the three boxes on the right. They

are shown as secondary because ordinary voters cannot conduct

or order recounts; only election administrators can do so.

DRE voting. Figure 3.4 shows what voters have to trust for each

step of an election process with a DRE voting system. There are

two possibilities here as well: the results from DRE machines

might be reported at each precinct, or they might be reported

only by the central election office.

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

DRE with

precinct-level

reporting

DRE with

central

reporting

individual voters check VVPATs; effective only if recounted election administrators recount VVPATs

personnel

personnel

personnel personnel

counts posted

at each

precinct

subtotals and

totals posted

online

DRE

DRE

DRE

DRE

EMS

EMS

EMS

EMS

Figure 3.4. Assurance chart for elections with direct recording electronic (DRE) voting.

When DRE machines are used, voters don’t get to see a

sample of the ballot definition in the machine, in the same way

that a sample ballot is a direct preview of what will be used on

election day. At best, voters might get images of the screens

displayed by the DRE, printed on paper. But, in general, they

don’t get to test-drive a DRE with the ballot definition they will

be using, and they can’t check whether their machines have

received the correct ballot definitions. Voters have to trust the

EMS, which produces the ballot definition files, the personnel

that operated the EMS, and the personnel that loaded the ballot

definitions into the DRE machines.

A DRE voting machine.

The DRE machines are responsible for presenting the

choices to the voter and recording the voter’s selections. For

these steps the voter is forced to trust that the DRE software is

correct. For the counting stage, voters have to trust either the

Verification 46

Page 60 of 324
Page 61 of 324

software in the DRE that counts and reports results locally, or

the software in the EMS that counts and tallies the results

centrally, along with the personnel that convey the information

to the EMS.

As a backup verification mechanism, some DRE machines

print voter-verified paper audit trails (VVPATs). This is a paper

tape that shows the voter’s selections for viewing and

confirmation by the voter. Printed VVPATs are retained by the

machine so that they can later be recounted if a recount is

deemed necessary. However, voter inspection of VVPATs is not

as strong a backup as voter inspection of paper ballots; in the

case of VVPATs, the thing being inspected is not what is

normally counted. With DRE machines, the results are derived

from the electronic records, not the VVPATs that voters see; the

VVPATs are only relevant if election officials decide to conduct a

recount.

A DRE with a VVPAT

printer (at lower right).

There are also good reasons to believe that voters are

unlikely to catch discrepancies on VVPATs. In a study by

Everett [25], voters using a mock DRE were shown a review

screen with selections different from what they had chosen, and

68% of voters failed to notice the changes. It seems likely that

even more voters would miss discrepancies on the VVPAT,

which is generally smaller than the screen and shown off to the

side of the machine.

As Figure 3.4 makes obvious, DRE voting systems depend

heavily on software. Because so little information is typically

published about these programs and their inputs and outputs,

trusting the outcome of such an election often requires trusting

virtually every piece of software in the system—software for

designing ballots, software that produces ballot definitions,

voting machine software, software that tallies votes, and all the

operating systems, compilers, editors, and other tools that were

used to produce these programs.

It doesn’t have to be this way. By publishing information

about the software and the data processed by that software, it’s

possible to reduce what voters have to accept on faith in order

to trust the validity of the election result.

Verification 47

Page 61 of 324
Page 62 of 324

What is the minimum software that needs to

be verified?

The degree to which software verification is avoidable depends

on a critical decision: how do voters indicate their votes—on

paper or on a computer? Of all the steps in the process, this one

is special because it must take place in private.

A big part of the present controversy over electronic voting

machines is a conflict about the user interface presented to

voters. Proponents of the machines point to the real benefits

that computers could offer in improved usability and

accessibility. For people with certain disabilities, voting

computers may be the only way to vote privately and

independently. Whether these advantages are enough to

outweigh the loss of a tangible, directly marked ballot is a

complicated question, and I argue for neither side of that issue

here. But an important factor in deciding whether vote entry

should occur on paper or on a computer is the feasibility of

ensuring the integrity of votes in either case.

Each of the two cases has its own answer to “what is the

minimum software that needs to be verified?”

Case 1: The paper option. If voters directly mark paper ballots,

the answer is “nothing.” To avoid all software verification, just

publicly count the ballots by hand right after the polls close.

Sample ballots, mailed out before polls open, let voters check

that the real ballots are printed correctly. There is no software

involved in marking and casting votes, only paper. And if the

results of the hand count are posted immediately at the polling

place, then no one has to trust the software that does the

tallying.

So, in a voting system where paper ballots are hand-marked

and hand-counted at the polls, any step that uses software can

be publicly checked by direct result verification. As with any

paper ballot system, the ballots are available to be recounted

later if necessary.

Verification 48

Page 62 of 324
Page 63 of 324

Figure 3.5 summarizes the preceding analysis in an

assurance chart.

published sample ballots

hand-marked,

hand-counted

paper ballots

paper ballot box

in public view

multiple

counters in

public view

counts posted

at each

precinct

subtotals and

totals posted

online

election administrators recount ballots

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

Figure 3.5. Assurance chart for an election with hand-marked, hand-counted ballots.

Case 2. Entering votes by computer. In this case, the answer is

“just the vote-entry software.” Here’s why.

The “mark or enter votes” step, central to the voter

experience, also turns out to be critical in terms of verification.

This step cannot be publicly verified by result verification.

Result verification requires a complete record of inputs and

outputs. But one of the inputs to this step is the input from

individual voters, which must be kept private due to the

principle of the secret ballot. Moreover, if the ballot is

presented to the voter by a computer, the voter’s input is

subject to influence by the computer.

Therefore, if choices are presented or selected on a

computer, software verification is unavoidable. However, the

secret ballot is the only privacy requirement that elections have

to uphold. Recorded votes can be published as long as they

cannot be associated with any particular voter. The only part of

the process that needs to be secret—and thus the only part

for which software verification is really necessary—is from

the private interaction with an individual voter up until the

moment the voter’s votes are recorded in anonymous form.

That interval is the critical interval during which private

information gets turned into publishable information. All the

inputs and outputs for other steps can be published, so

everything else can be checked by result verification.

Verification 49

Page 63 of 324
Page 64 of 324

It follows that the way to minimize software verification is

to make that critical interval as short and simple as possible:

use software to present the ballot, accept selections from

voters, and record the votes in anonymous form, then publish

the anonymous votes immediately when polls close. The

preparation that takes place before the election produces a

ballot definition file for the voting machine. If this file is also

published, no one needs to verify the ballot preparation

software either. Figure 3.6 gives the assurance chart for this

case.

anonymous vote

records posted

at each precinct

published

ballot

definition

DRE with

published

vote records

personnel DRE anonymous vote records posted online

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

Figure 3.6. Assurance chart for a DRE-based election with published ballot definition and

published, anonymous vote records.

In the ballot distribution step, voters have to assume that

election personnel have properly distributed the ballot

definitions and loaded them into the machines; they have no

way to check this for themselves. And in the ballot presentation

and vote recording steps, voters still have to trust the software

in the DRE machine.

Practical example. Here’s one way that an election with

computerized voting but minimal software verification could be

carried out in practice.

The software for the voting computer would be written to

run on a free computing platform, and finalized and published

far in advance of the election so that everyone has time to

inspect it and test it. The ballot definition files for the election

would be published on government websites, also far enough in

advance that members of the public have time to examine them

Verification 50

Page 64 of 324
Page 65 of 324

before the polls open. Anyone would be able to download a

ballot definition and run the voting computer software on their

own computer to see exactly what will be shown to voters on

election day. This provides a chance to detect omitted races,

misspelled candidate names, layout errors, and other ballot

errors. Thus, the published ballot definition file serves a similar

purpose to the paper sample ballot typically mailed to voters

before an election.

When a polling place stops accepting new votes at the end

of the day, each machine should contain a vote file containing

all of its anonymously recorded votes. At this point, every

machine would print out a cryptographic hash of its vote file;

observers can copy down (or photograph) the hashes. A

cryptographic hash is a number derived from the contents of a

file in such a way that it is easy to calculate the hash for a given

file, but difficult to produce a different file that yields the same

hash. Publishing the hash makes a public commitment to the

contents of the file. (The reason for using a hash is that it is less

cumbersome than printing out the entire vote file, but it serves

the same purpose.)

The anonymous vote files from every machine would then

be published online for all to see after the election. Anyone can

calculate the hashes of these files and compare them to the

hashes that were printed on election night, to verify that the

files are authentic and unaltered. And anyone can count the

votes in these files to confirm that the tallying is performed

correctly.

The consequence is that neither the ballot layout software

nor the vote tallying software would need to be verified. The

published ballot definitions, voting computer software, and

anonymous vote records would be sufficient to allow members

of the public to independently check the accuracy of the

election outcome.

Verification 51

Page 65 of 324
Page 66 of 324

What other alternatives for verification are

possible?

Electronic ballot markers and printers. An electronic ballot

marker (EBM) is a computer that marks a paper ballot [80, 81].

The voter inserts a paper ballot and makes selections on the

computer, and the EBM prints marks onto the ballot in the

appropriate positions. An electronic ballot printer (EBP) is a

computer that prints out a marked paper ballot. No ballot is

inserted; the voter makes selections on the computer, and the

EBP prints out a fresh paper ballot that indicates the voter’s

choices. In both cases, the voter then deposits the paper ballot

into a ballot box as usual.

EBMs and EBPs occupy a middle ground between optical

scan systems and DRE systems. They provide the flexibility of a

computerized user interface for voting, together with a durable

paper record that can be recounted later. Like a DRE machine,

an EBM or EBP relies on a ballot definition file to describe the

choices to present to the voter, and the proper recording of the

voter’s choices depends on the software running in the EBM or

EBP. But the voter now has the option of checking the printed

ballot before casting it, instead of having to trust this software.

And unlike the printed VVPAT produced by a DRE, this printed

ballot is always counted, so the voter’s check is more effective.

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

EBM/EBP with

precinct

optical scan

EBM/EBP with

central

optical scan

individual voters check paper ballots election administrators recount ballots

personnel

personnel EBM/EBP

EMS

ballot box

in public view

results posted

at each

precinct

subtotals and

totals posted

online

scanner

personnel personnel

ballot box

in public view EMS

EMS

scanner

Figure 3.7. Assurance chart for an election with electronically marked or printed, optically

scanned ballots.

Verification 52

Page 66 of 324
Page 67 of 324

The corresponding assurance chart, in Figure 3.7, has a left half

similar to that of a DRE system, and a right half similar to that

of an optical scan system.

End-to-end cryptographic voting. There are several proposed

voting systems that provide end-to-end cryptographic methods

for letting voters verify the election. “End-to-end” refers to the

ability of any individual voter to check that his or her ballot

survived from one end of the process straight through to the

other—from casting to the final result—without special access

from election officials.

Recall that earlier in this chapter, I described two possible

kinds of publishable records—anonymous vote-revealing

records, and identifiable but non-vote-revealing records.

End-to-end cryptographic schemes publish records of the

second kind as well as the first kind. Examples of these

schemes are Punchscan [26], Scratch & Vote [1], Prêt-à-Voter [13],

and VoteHere [54]. What they all have in common is that they

publish some information about each voter’s ballot: enough to

let the voter partially check the recorded ballot, but not enough

to reveal an actual vote so a voter can sell it. That is, indirect

result verification is used to ensure the integrity of individual

ballots. The partial records are set up in such a way that, with

enough voters checking this partial information, the likelihood

of an incorrectly posted ballot is nearly zero.

In addition to the partial ballots, actual vote records are

separately posted—but these votes have been shuffled so they

cannot be associated with particular voters. Anyone can count

the posted votes to check the tally. The shuffling is performed

using a system called a “mix net,” in which multiple parties

participate in the shuffling; no single party learns the total

shuffling order, and thus voter privacy is protected.

In these end-to-end cryptographic schemes, the election

authorities keep some secret information that enables them to

process the ballots into verifiable totals, and the ballots contain

serial numbers or cryptographic information as well. In all of

these schemes, there is a pre-election audit procedure that lets

Verification 53

Page 67 of 324
Page 68 of 324

voters ensure that this information is consistent and properly

formed. After the election, voters can also audit the shuffling

procedure to confirm that the posted partial ballots correspond

to the posted anonymous vote records, and thus to the tally.

The same mathematical techniques can be applied to votes

cast in any fashion (by hand-marked paper, by machine-marked

paper, or directly by machine). When hand-marked paper is

used, the election can completely escape dependence on

software. Figure 3.8 summarizes how assurance is provided in

this category of systems.

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

hand-marked

ballot with

end-to-end

verification

EBM/EBP with

end-to-end

verification

DRE with

end-to-end

verification

individual voters check paper ballots

individual voters check receipts

pre-election

public audit

pre-election

public audit

paper

voters’ receipts;

(partial or encrypted)

ballots posted online

post-election

public audit

anonymous vote records

posted online

pre-election

public audit

EMS

EMS

DRE

EBM/EBP

personnel

personnel

personnel

Figure 3.8. Assurance chart for elections with end-to-end cryptographic verification.

Non-cryptographic end-to-end schemes. Of special note are

ThreeBallot, VAV, and Twin [67], which provide end-to-end

verification without cryptography. These schemes publish all

the cast ballots, which anyone can recount to verify the tally. In

ThreeBallot and VAV, only some of the posted items are

identifiable. Each voter’s ballot is split into three parts; although

all the parts are posted, the voter gets a receipt for only one

part—and a single part isn’t enough to reveal how they voted.

In Twin, each voter gets a receipt for someone else’s ballot.

Thus, while the posted records can be matched with receipts,

they can’t be identified as belonging to any particular voter. The

Verification 54

Page 68 of 324
Page 69 of 324

assurance chart for all these schemes is similar to Figure 3.8,

except there is no need for a post-election cryptographic audit

because no encryption or shuffling has taken place.

Comparing voting systems. Figure 3.9 summarizes several

types of voting systems on a single chart for comparison.

For conventional paper-based systems, shown at the top,

any method of marking ballots (by hand, by EBM, or by EBP) can

be combined with any method of counting ballots (by hand

count, by precinct optical scan, or by central optical scan). Next

come the conventional electronic systems, based on DREs; then

the end-to-end cryptographic systems. Finally, at the bottom is

the DRE with its ballot definition and results published, as well

as a variant of the same scheme using an EBM or EBP instead.

The systems least dependent on software (all other concerns

aside) are the hand-marked, hand-counted paper ballots and the

hand-marked ballots with cryptographic verification.

If one chooses to exclude the systems with hand-marked

ballots (shaded in grey) from consideration, due to the potential

usability,
accessibility, and accuracy advantages of computer- based vote entry,
then the bottom two options in the “public- ballot electronic” category
are the least dependent on software.

A system based on a DRE with a published ballot definition and

published vote records will use the least amount of critical

software, but also requires voters to place great trust in that

software. A system based on an EBP with a published ballot

definition will be dependent on the optical scanner’s software

as well as the EBP software, but both software-dependent steps

are subject to paper-based checks. The choice between these

two options would depend on one’s confidence in the ability to

verify DRE software and one’s estimate of the likelihood that

significant errors will be caught by observant voters and

recounts.

All of the systems that involve entry of votes using any kind

of voting computer—DRE, EBM, or EBP—could stand to benefit

from easier verification of the software in that computer. This

is where we will turn our attention in the next chapter.

Verification 55

Page 69 of 324
Page 70 of 324

counting

correctness

count-to-tally

integrity

tallying

correctness

ballot-to-voter

integrity

vote recording

correctness

ballot

correctness

ballot-to-poll

integrity

design

ballots

mark or

enter votes

present

ballots

distribute

ballots

count

votes

collect

votes

tally

subtotals

transmit

subtotals

C O R R E C T B A L L O T C A S T A S I N T E N D E D C O U N T E D A S C A S T

vote-to-count

integrity

cast

votes

PUBLIC-BALLOT

ELECTRONIC

electronic

ballot printer

published

ballot

definition

anonymous vote

records posted

at each precinct

published

ballot

definition

direct

recording

electronic

anonymous vote records posted online

ballot box in

public view

counts posted

at each

precinct

subtotals and

totals posted

online

individual voters check paper ballots election administrators recount ballots

DRE

personnel

personnel

EBP scanner

hand-marked

paper ballot

END-TO-END

CRYPTOGRAPHIC

electronic

ballot marker

or printer

direct

recording

electronic

pre-election

public audit

pre-election

public audit

paper

voters’ receipts;

(partial or encrypted)

ballots posted online

post-election

public audit

anonymous vote records

posted online

pre-election

public audit

individual voters check paper ballots

individual voters check receipts

EMS

EMS

DRE

EBM/EBP

personnel

personnel

personnel

personnel

personnel

personnel personnel

direct

recording

electronic

precinct

reporting

central

reporting

counts posted

at each

precinct

subtotals and

totals posted

online

CONVENTIONAL

ELECTRONIC

individual voters check VVPATs; effective only if recounted election administrators recount VVPATs

DRE

DRE

DRE

DRE

EMS

EMS

EMS

EMS

hand-marked

paper ballot

scanner

personnel personnel

personnel

EBM/EBP

published sample ballots paper

electronic

ballot marker

or printer

ballot box in

public view

ballot box in

public view

multiple

counters in

public view counts posted

at each

precinct

subtotals and

totals posted

online

precinct

hand

counting

precinct

optical

scanning

central

optical

scanning

individual voters check paper ballots

CONVENTIONAL

PAPER-BASED

election administrators recount ballots

personnel

EMS

EMS

EMS

scanner

Figure 3.9. Summary of assurance mechanisms for various types of voting systems.

Verification 56

Page 70 of 324
Page 71 of 324

4 Prerendering

How can we make vote-entry software easier to verify? 58

What is prerendering? 59

Why put the entire user interface in the ballot definition? 60

How would a voting computer use a prerendered ballot? 62

What is gained by publishing the ballot definition? 63

What are the advantages of prerendering? 65

How can prerendering be applied to other software? 66

How are votes recorded anonymously? 67

57

Page 71 of 324
Page 72 of 324

How can we make vote-entry software easier

to verify?

For vote-entry software to be easier to verify, we have to make it

simpler. The vote-entry software can be simpler if we give it

less work to do and shift its responsibilities elsewhere: either

earlier, to the preparation stage, or later, to the counting stage.

Shifting responsibilities to the preparation stage is a

significant design challenge, but it leads to a dramatic

simplification of the vote-entry software. Most of this chapter is

devoted to prerendering, the technique that makes this

possible. Shifting responsibilities to the counting stage means

that the vote-entry software should recording votes

anonymously with as little processing as possible; this is

comparatively straightforward to do and will be discussed in

the last section of this chapter.

I developed two prototypes of voting machine software to

find out just how small a practical vote-entry program could be.

They are called Ptouch and Pvote, described in Chapters 5 and 7

respectively.

Prerendering 58

Page 72 of 324
Page 73 of 324

What is prerendering?

In a typical voting computer, much of the software code is

responsible for generating the user interface for the voter. This

includes the code for arranging the layout of elements on the

screen, drawing text in a variety of typefaces and languages,

drawing buttons, boxes, icons, and so on. In a voting computer

with audio features, this also includes code for manipulating or

synthesizing sound. (Some voting computers, such as the

Avante Vote-Trakker [11], contain speech synthesis software.)

The user interface is generated in real time—the visual display

and audio are produced (“rendered”) as the voter interacts with

the machine.

Prerendering the ballot. The software in the voting computer

could be considerably simplified by moving all this rendering

work into the preparation stage—prerendering the interface

before election day.1 Both Ptouch and Pvote realize this idea.

Today’s DRE machines use a ballot definition that contains

only essential data about the ballot: the names of the offices,

the names of the candidates running for each office, and so on.

But the ballot definition could be expanded to describe the user

interface as well. For a visual interface, this would include

images of the screen with the layout already performed, buttons

already placed, and text already drawn. For an audio interface,

this would include prerecorded sound clips. Everything

presented to the user would be prepared ahead of time, so that

all the software complexity associated with rendering can be

taken out of the voting computer.

The ballot definition could specify not just appearance but

also behaviour—the locations where images will appear, the

transitions from screen to screen, the user actions that will

trigger these transitions, and so on. This is exactly the case for

both Ptouch and Pvote: the ballot definition is a high-level

description of the entire user interface for voting.

1

It was Steve Bellovin who prompted my line of research by suggesting prerendering for voting machines.

Prerendering 59

Page 73 of 324
Page 74 of 324

Why put the entire user interface in the ballot

definition?

Including a complete description of the user interface in the

ballot definition, rather than just a set of images, yields several

benefits.

Less code in the voting computer. Some of the software in a

typical voting computer handles user interface logic. User

interface logic tells the computer how to respond to any given

user action—for example, to select a candidate when you touch

the candidate’s name, or to go to the next page when you press

a “Next Page” button. Putting a description of this logic in the

ballot definition means the voting computer needs less code for

interface logic, just as putting images in the ballot definition

means less code for rendering the display.

More thorough public review. If the ballot definition

completely describes the user interface, one can review the

behaviour of the user interface by examining it. The user

interface becomes a separately verifiable artifact.

Compared to the vote-entry software, the ballot definition is

more likely to be accessible for inspection by the public, for two

reasons. First, there may be fewer legal and political barriers to

publishing the ballot definition than the software source code.

Second, the ballot definition is a high-level description, which

makes it easier to examine than a computer program written in

a general-purpose programming language. The result is that

more of the voting process is reviewable by non-programmers:

both the appearance and the behaviour of the ballot can be

inspected without looking at source code for the voting

computer.

A more complete public record. The ballot definition file, like

any other election information, should be archived and should

become part of the public record of the election. It contributes

Prerendering 60

Page 74 of 324
Page 75 of 324

to making the election a reproducible experiment. In the event

of a later investigation, a ballot definition with a complete

description of the interface makes it easier to reconstruct the

voter experience. Such reconstruction could help investigators

evaluate hypotheses about sources of bias or voter error, for

example.

Better division of expertise. Separating the user interface

definition from the voting machine software mitigates the

conflict between accessibility (which requires design flexibility)

and security (which requires software simplicity). Instead of

playing tug-of-war over the vote-entry software, experts can

work independently on what they do best—design can be left to

designers, and software security to security experts. Experts in

human factors, accessibility, and graphic design can create

better ballots themselves, without relying on programmers to

implement their designs in code, and without requiring

co-operation from voting machine companies. Programmers of

the vote-entry software can focus on making the software

secure and reliable without affecting the user interface.

Software stability. Regulations that govern ballots can change

from election to election and differ from jurisdiction to

jurisdiction. Different jurisdictions may prefer to present their

ballots differently. Designs will change as we discover better

ways to create fair and understandable ballots.

Putting the user interface description in the ballot definition

provides the flexibility to handle future changes without having

to change the vote-entry software. This means more resources

can be devoted toward ensuring that the vote-entry software is

correct and secure. It’s difficult to complete a rigourous

certification process when voting software changes as

frequently as it does today, with new versions released every

year or two.

Prerendering 61

Page 75 of 324
Page 76 of 324

How would a voting computer use a

prerendered ballot?

In a prerendered-ballot system, the ballot definition is like a

small program—a program in an extremely simple language,

with limited capabilities. All it can do is present a sequence of

images and/or audio clips and accept the user’s selections.

The voting computer simply carries out the program. Thus,

the vote-entry software is a virtual machine (VM): it abstracts

away the details of the computer hardware and its input and

output devices. The job of the VM is to respond to user input by

displaying images or playing sound clips as prescribed by the

ballot definition, keep track of the user’s selections, and record

the user’s selections anonymously.

Implementing the VM for a variety of different hardware

platforms would enable all of them to use the same formats for

ballot definitions and recorded votes—just as other VMs like

the Python VM and the Java VM allow a single program to run

on different kinds of computers. There can even be multiple

implementations of the VM written separately by different

people, and as long as they follow a standard ballot definition

format, the same ballot definition will work on all of them. For

example, there are multiple independently-written Python VMs

out there, but most Python programs will run unchanged on all

of them.

My hypothesis was that the implementation of the voting

VM can be made considerably smaller, simpler, and easier to

verify than the software in today’s DRE machines. This

dissertation presents Ptouch and Pvote as confirmation of this

hypothesis.

Prerendering 62

Page 76 of 324
Page 77 of 324

What is gained by publishing the ballot

definition?

The published ballot definition serves the role of an electronic

sample ballot, analogous to a sample ballot in a paper election.

Standardizing the file format of the ballot definition and

implementing the VM for personal computers enables voters to

try out the ballot in advance with exactly the same user

interface that they will see at the polls. This could be used for

training voters as well as testing the ballot.

Verifying the accuracy and fairness of the user interface is

critical, because the user interface of any voting machine is in a

position to mislead or otherwise influence voters and hence

bias the collected votes. The published electronic sample ballot

gives the election a verifiable user interface, which can be

examined by all voters, members of the disabled community,

usability experts, and accessibility experts. Anyone could

conduct their own user tests of ballots, independent of the

voting machine company or the election authority.

Today, less commonly used ballot designs, such as ballots

for voters with disabilities or ballots in alternate languages,

receive significantly less attention, as only the election office

can compose and check electronic ballots. A rather alarming

example of this lack of attention occurred at the June 2006

primary election in Santa Clara County, where pollworkers

discovered that there was no “continue” button on one of the

Chinese screens [40], which made it impossible to cast the

Chinese version of the ballot. A published ballot definition

would have increased the chances of catching such an error

before the election. Publishing an electronic sample ballot helps

to level the playing field for members of minority communities

and empowers them to play a role in ensuring that the

electronic ballot serves them fairly.

Visualizing the ballot definition. Running the ballot definition

in a live test might show that the ballot appears to behave

Prerendering 63

Page 77 of 324
Page 78 of 324

correctly, but it wouldn’t be a sure way to test the complete

behaviour of the ballot. It would be infeasible to test every

possible sequence of inputs. To be certain that the ballot

contains no hidden behaviour or incorrect behaviour triggered

by rare combinations of inputs, one would have to examine the

ballot definition file itself.

In the future, a software tool could be developed to facilitate

such examination. The tool would transform an electronic

sample ballot into a human-readable format that completely

describes the user interface. One possible visualization would

be a flowchart-like diagram that illustrates the steps of the user

interface with the prerendered screen images. Anyone would be

able to download the electronic sample ballot, use the program

to produce a diagram, print it out, and examine it. This would

make possible a new level of assurance: the electronic voting UI

could be verified even by non-programmers. The hardcopy of

the UI visualization could also be archived in the records of the

election. The visualization alone should be sufficient to

reconstruct the interface that voters used at the polls.

Prerendering 64

Page 78 of 324
Page 79 of 324

What are the advantages of prerendering?

In summary, prerendering the user interface (UI) yields these

benefits:

• The critical software is smaller and simpler, facilitating its

verification.

• The critical software changes less frequently, so each release

can be tested and audited more thoroughly.

• The user interface can be designed by designers, not

programmers.

• The conflict between human factors and security is

mitigated; usability and accessibility can be improved

without affecting software security.

• The conflict between transparency and proprietary interests

is mitigated because less code has to be disclosed in order

to evaluate the security of the voting machine.

• The user interface is subject to broader public review, since

it can be separately published and tested by anyone (not

just those who have election equipment).

Standardizing the ballot definition format also yields benefits in

interoperability, in addition to the benefits mentioned so far in

this chapter.2 A standardized format for describing the user

interface allows election officials to mix and match components

from different vendors, leading to increased purchasing power

and better product quality, and enabling independently

manufactured components to be tested against each other.

2Thanks to David Jefferson for bringing the importance of interoperability to my attention.

Prerendering 65

Page 79 of 324
Page 80 of 324

How can prerendering be applied to other

software?

The prerendering technique can be applied to any kind of

software to make verification easier. Applying this technique

consists of the following steps:

1. Define a user interface specification language with a set of

features that are limited and chosen to suit the intended

purpose.

2. Implement a virtual machine that interprets the

specification language and presents the user interface it

describes.

3. Create user interface designs using the specification

language, and publish them for inspection.

Particularly suitable application areas for this technique are

those in which a general-purpose computer is used for a

specialized purpose, the user interface (UI) is likely to change

periodically, and high reliability must be maintained despite

changes in the UI. Aside from voting machines, other examples

include bank machines, vending machines, and airport check-in

kiosks. The user interaction required to operate these kinds of

machines is usually limited to a small set of actions, such as

selecting from menus and typing in numbers or short pieces of

text. This makes it possible to design a simple language for

specifying the UI.

In each case, the transaction-handling software can be

written once and reviewed thoroughly to ensure its correctness

and security. In a voting machine, the transaction-handling

software is the part that records the votes; in a bank machine,

for instance, this would be the software that communicates

transactions to the bank and dispenses cash. The UI can then be

easily changed without affecting that critical software—for

example, when a bank wants to offer new functionality, a

vending machine updates its list of available products, or an

airline wants to change the look of its brand.

Prerendering 66

Page 80 of 324
Page 81 of 324

How are votes recorded anonymously?

In the correctness goals listed in Chapter 2, I identified two

components of upholding the secret ballot:

• Voter privacy: The processing of voter choices does not

expose how any particular voter voted.

• Coercion prevention: Voters are not provided any way to

present plausible evidence of how they voted to an external

party.

Voter privacy. To protect voter privacy, ballots should be

stored without any identifying information. The ballots should

also be stored in an order independent of the order in which

they were cast, so that someone who observes the sequence of

voters entering the polling place cannot correlate the sequence

of voters with the sequence of stored ballots.

One common method of doing this is to store the vote

records in random order, effectively shuffling them as ballots

would be shuffled in a real ballot box. Voter privacy depends on

the quality of the randomization performed; if the shuffling is

predictable, then voter privacy can be compromised.

Unfortunately, it’s hard to make a computer behave in a truly

random way. In fact, independent source code analysis of two

leading voting machines (Diebold [12] and Sequoia [7])

discovered flaws in the randomization schemes used for just

this purpose. Even worse, randomness is not a quality that can

be practically tested, because it is impossible to prove that any

behaviour really is random. For example, given a list of

numbers, there is simply no way to tell whether the numbers

were chosen at random.

A simpler way to avoid revealing the casting order is to sort

the vote records according to their contents. (Naor and

Teague [49] observed that sorting a list of elements gives them a

history-independent representation.) It doesn’t matter how the

records are placed in order, as long as it’s consistent. For

example, if there is just one contest with candidates Andrew,

Prerendering 67

Page 81 of 324
Page 82 of 324

Barbara, and Chris, you could sort the ballots alphabetically by

which candidate was selected. Regardless of the casting order,

the sorted order will always be the same. Because this method

is simple to program and completely obscures the casting order

in a verifiable way, this is the method that Ptouch uses.

Coercion prevention. To prevent coercion, voters must not be

allowed to put identifying marks on their ballots. In one

possible coercion scenario, the coercing party gives each voter a

unique secret phrase to enter as a write-in candidate. For

example, suppose Ted tells Alice to vote for Carol for President

with “moldy explosion” as write-in for Dogcatcher, and also tells

Bob to vote for Carol for President with “wrinkled tourbus” as

write-in for Dogcatcher. Then the recorded ballots are no longer

publishable because they would enable Ted to confirm, and thus

buy, Alice’s and Bob’s votes.

One way to resolve this problem is to store each of the

voter’s selections as a separate item instead of the entire ballot

as a unit. There has been precedent for such a scheme in some

paper elections in Switzerland [15], where the ballots are

perforated so that they can be separated into strips, one for

each contest, before being counted. If an individual voter’s

selections cannot be associated with each other, then the voter

cannot use a specially marked selection to identify the rest of

their ballot.

Storing the ballot in parts might not satisfy election

standards that are based around the handling of complete

ballot images. For example, the 2005 Voluntary Voting System

Guidelines in the United States [80] require DRE machines to

“record and retain redundant copies of the original ballot

image,” where a ballot image is “an electronic record of all votes

cast by the voter, including undervotes” (Section 2.1.2). One way

to satisfy this requirement would be to store ballots in both

ways: as complete images for non-public auditing, and in

separated form for publishing.

Prerendering 68

Page 82 of 324
Page 83 of 324

5 Ptouch

the touchscreen prototype

Overview 70

Ballot definition format 71

Software design 80

Implementation 83

Evaluation 88

Shortcomings 93

69

Page 83 of 324
Page 84 of 324

Overview

This chapter describes Ptouch [90], the first prototype

vote-entry program I developed, which is designed for a

touchscreen voting machine. It provides only a visual interface;

the goal was to handle the most common types of elections for

fully sighted voters. (Pvote, the second prototype, adds support

for most voters with disabilities and for less common types of

contests and ballots, at the cost of increased software

complexity.)

Ptouch handles contests in which voters can choose one or

multiple options (up to a fixed limit) from a list of options, and

also allows voters to vote for write-in candidates. This is

sufficient to indicate anything that could be expressed by

selecting bubbles or arrows on an optically scanned ballot.

The format of the ballot definition forms the core of the

design, since it dictates how ballots are designed, displayed,

and voted upon. Thus, I’ll start by describing the ballot

definition format in detail, then proceed to the software itself,

which is a VM for displaying ballots in this format.

Ptouch 70

Page 84 of 324
Page 85 of 324

Ballot definition format

The ballot definition is divided into two parts—the ballot model

and the image library—corresponding to the medium- independent and medium-specific information about the voting

user interface (see below). The ballot model specifies the

interaction sequence, while the image library specifies the

appearance.

Separating the ballot model from the image library reduces

the cost and effort of validating changes to the ballot. Replacing

the image library is sufficient to adjust the layout or visual style

of the ballot, change the display resolution, or translate the

interface into another language, all without altering the ballot

model. For these kinds of changes, only the new image library

needs to be validated, not the entire ballot definition.

Comparing two image libraries (for example, to check a

language translation) is easier than checking the correctness of

a ballot model.

ballot model

contest page

int max_sels

int max_chars

subpage

target

int action

int page_i

int contest_i

subtarget

int action option

int contest_i

write-in

int contest_i

review

int contest_i

image library

int width

int height

layout

background

sprite

int width

int height

byte[] pixels

subtarget

int left

int top

int width

int height

int width

int height

byte[] pixels

Figure 5.1. The Ptouch ballot definition data structure. Stacked boxes represent arrays.

Ptouch 71

Page 85 of 324
Page 86 of 324

ballot model

page

contest

int max_sels

int max_chars

subpage

target

int action

int page_i

int contest_i

subtarget

int action

option

int contest_i

write-in

int contest_i

review

int contest_i

Ballot model. The ballot model consists of an array of contests,

an array of pages, and an array of subpages.

A contest is a question being put to the voters, such as a

referendum on an issue or the election of a candidate (or

several candidates) to a position. Each contest has an integer

parameter max sels specifying the maximum number of

selections that a voter may choose (usually 1, but possibly more

in contests that allow choosing multiple candidates) and an

integer parameter max chars specifying the maximum number

of characters that can be entered for a write-in option.

The page is the basic unit of presentation. For example, a single

page might display some instructions, a description of a

contest, or a list of available options. At any given moment, one

of the pages is the current page. The user interface begins on

the first page in the array of pages. When it transitions to the

last page, the ballot is cast with the user’s current selections.

Associated with each page are arrays of targets, options,

reviews, and write-ins, and any of these can be activated by the

user. In a touchscreen interface, these elements correspond to

rectangular areas of the screen that are activated by touches.

• A target is a user-triggered transition to another page. In a

touchscreen interface, a target appears as a button that the

user can press. Optionally, a target can also trigger one of

the following actions:

• Clear all the selections in a particular contest.

• Clear all the selections in the entire ballot.

• An option is an option that the user can choose in a

particular contest. For example, a contest for President

would have one option for each of the eligible candidates; a

referendum contest would typically have one option for

“Yes” and one option for “No.” Each option belongs to

exactly one page, though there may be options on different

pages that belong to the same contest—for example, if the

contest has too many options to fit on one page. Activating

an option toggles it between a selected state and an

Ptouch 72

Page 86 of 324
Page 87 of 324

option (slot 4)

background image

write-in (slot 5)

write-in (slot 27)

write-in characters (slots 6–26)

write-in characters (slots 28–48)

target
(slot 0) target (slot 1) target (slot 2) target (slot 3) Figure 5.2. A
selection page with two options currently selected, and its layout.

Ptouch 73

Page 87 of 324
Page 88 of 324

unselected state. In a touchscreen interface, an option

appears as a labelled box that changes appearance to show

whether it is selected.

• A write-in is a write-in option. It can be in a selected or

unselected state, just like a regular option; when selected, it

also has an associated list of entered characters. When a

write-in is activated, it triggers a jump to a subpage where

the voter can type in the text of the write-in selection.

• A review displays the current selections in a particular

contest. Activating a review has no effect, though targets

can overlap reviews. In a touchscreen interface, a review

appears as a screen area (or multiple screen areas) filled in

with the option (or options) currently selected in its

associated contest. For example, a confirmation page could

summarize the voter’s selections by presenting reviews for

several contests.

A subpage is a temporary page for entering a write-in. A

subpage is like a subroutine call, but only one level deep—the

only possible transition is back to the current page. In a

touchscreen interface, a subpage provides a text field and an

on-screen keyboard for the voter to type in the name of a

write-in candidate. The number of subpages is determined by

the contests: there is one subpage for each contest that

contains a write-in. A subpage contains an array of subtargets.

• A subtarget triggers one of these actions:

• APPEND a particular character to the text field.

• APPEND2: if the text field is not empty, then append a

particular character to the text field.

• DELETE the last character.

• CLEAR all the characters.

• ACCEPT the write-in text and return.

• CANCEL the write-in text and return.

If the write-in text already contains max chars characters,

activating an APPEND or APPEND2 subtarget has no effect. If the

write-in text is empty, activating an APPEND2 or ACCEPT

subtarget has no effect. If the subpage is exited by an ACCEPT

Ptouch 74

Page 88 of 324
Page 89 of 324

background image

CANCEL subtarget (slot 2) ACCEPT subtarget (slot 3)

CLEAR

subtarget (slot 0) write-in characters (slots 33–53)

APPEND subtargets (slots 4–31)

DELETE

subtarget (slot 1)

APPEND2

subtarget (slot 32)

character sprites cursor sprite

Figure 5.3. A write-in subpage with a few characters entered, and its layout.

Ptouch 75

Page 89 of 324
Page 90 of 324

subtarget, the write-in option becomes selected and acquires

the contents of the text field. If the subpage is exited by a

CANCEL subtarget, the write-in option becomes unselected and

empty. Thus, it is not possible for a write-in to contain text yet

remain unselected.

Because an ACCEPT subtarget only works when there is

write-in text present, a write-in cannot be simultaneously empty

and selected. The purpose of APPEND2 is to prevent a write-in

from appearing empty and yet being selected. For example, if

the keyboard’s “space” button is an APPEND2 subtarget, then the

write-in text cannot consist of only spaces.

image library

int width

int height

layout

background

sprite

int width

int height

byte[] pixels

subtarget

int left

int top

int width

int height

int width

int height

byte[] pixels

Image library. The image library consists of an array of layouts

and an array of sprites, and also specifies the screen dimensions

in pixels.

A layout consists of a background image and an array of

slots. Each page or subpage corresponds to exactly one layout,

and vice versa. A slot is a rectangular region of the screen where

a sprite can be pasted or where a touch will have an effect.

A sprite is an image smaller than the screen size that is

meant to be pasted into a slot on a background image. The

array of sprites contains images of options and write-ins in

their selected states, images of characters that for use in a

write-in, and the image of the text entry cursor shown while

entering a write-in. To keep the DRE software simple, all images

are stored uncompressed with 3 bytes per pixel.

In a layout corresponding to a page, the slots correspond to

the targets, options, write-ins, and reviews for that page. Each

target has one slot, specifying the touch region that activates

the target; the image of the target button (or other widget) is

part of the background image. Each option has one slot, which

specifies both its touch region and also the position for pasting

the sprite showing the option in its selected state. The image of

the unselected option is part of the background image, and

when the option is selected, the sprite is pasted over it. Each

write-in also has a sprite for its selected state, which would

typically look like a selected option but with space provided for

Ptouch 76

Page 90 of 324
Page 91 of 324

the write-in text. A write-in has one slot for its touch region and

for pasting the selected write-in sprite, and max chars more

slots specifying the positions where the entered characters are

to be pasted. Each review has max sels groups of slots (for

displaying up to max sels options selected by the voter). In

each group of slots, there is one slot for pasting the selected

option sprite and max chars slots for displaying the write-in

text if a write-in is selected.

In the layout corresponding to a subpage, the slots

correspond to the subtargets and character slots for the page.

Each subtarget has one slot, the touch region that activates it.

Additionally there are max chars slots specifying the positions

where the entered characters are to be pasted.

page

target

int action

int page_i

int contest_i

option

int contest_i

write-in

int contest_i

review

int contest_i

Referential integrity. To simplify verification, the ballot format

minimizes its use of pointers and other kinds of references.

There are only two kinds of references in these data structures:

• Targets refer to the page they transition to. This is

necessary to allow for multiple outgoing and incoming

transitions to and from each page.

• Targets, options, write-ins, and reviews refer to contests.

This is necessary to allow options, write-ins, and reviews to

be freely arranged among the pages, so there can be

multiple contests on a single page or multiple pages for a

single contest.

These references are stored as integer array indices in the ballot

definition because it is simpler to verify that an index is in range

than to verify that a pointer is valid. All other associations

between elements of the ballot definition are implied through

structural correspondence. For instance, if there are p pages

and q subpages, then there are exactly p + q layouts in the

layout array, where the first p are for pages and the last q are

for subpages. This use of corresponding array indices avoids

the need for pages or layouts to contain pointers to each other.

Similarly, the meanings of the slots are determined by their

order in the slot array. The slot array for a page contains, in

Ptouch 77

Page 91 of 324
Page 92 of 324

order, one slot for each target, then one slot for each option,

then 1 + max chars slots for each write-in, then

max sels × (1 + max chars) slots for each review. The slot

array for a subpage contains one slot for each subtarget

followed by max chars slots for the entered text.

The sprite array contains one sprite for each option and

write-in, in the order they appear among the pages, followed by,

for each subpage, a character sprite for each APPEND or APPEND2

subtarget and one cursor image sprite.

Well-formedness and validity. There are many possible ways in

which one might consider a particular ballot definition to be

acceptable; I’ll point out two important ones here. I’ll use the

term well-formed to mean that a ballot definition satisfies the

assumptions made by the virtual machine implementation. I’ll

use the term valid to mean that a ballot definition represents an

acceptable user interface for voting according to the standards

of a given jursidiction.

Because the ballot definition must be well-formed in order for

the VM to read it and operate safely and correctly, a verifier in

the voting machine checks for well-formedness before accepting

a ballot definition. To be well-formed, a ballot definition must

meet the following conditions:

• There is at least one page and one contest.

• There is one subpage for each contest that has a write-in.

• There is one layout for each page or subpage.

• Every index referring to a page or contest is in bounds for

its respective array.

• Every target or subtarget has a valid action.

• Every layout contains the correct number of slots to match

its page or subpage, as described in the preceding section.

• All background images match the screen size.

• All slots fit entirely within the screen bounds.

• All option slots, write-in slots, review slots, option sprites,

and write-in sprites associated with the same contest have

the same size.

Ptouch 78

Page 92 of 324
Page 93 of 324

• All character slots, character sprites, and cursor sprites

associated with the same contest have the same size.

• The image library contains the correct number of sprites to

match the ballot model, as described in the preceding

section.

Validity, on the other hand, does not have a single definition

because it depends on election regulations that can vary by

locality. The following are some examples of conditions for

validity that are likely to be common, as they prevent some

obvious pitfalls and potential sources of confusion in the user

interface:

• Target, option, write-in, and review slots do not overlap each

other, except that target slots may overlap review slots.

• Character slots do not overlap each other and fit inside their

corresponding write-in or review slot.

• Character slots in write-ins and reviews are arranged in the

same relative positions as the character slots on the

corresponding subpages.

• The user is never trapped in a subgraph of pages, except

after arriving on the last page.

• The last page has no target, option, write-in, or review slots.

• There exists some transition path from the first page to

every other page.

• Every subpage contains an ACCEPT subtarget, a CANCEL

subtarget, and at least one APPEND subtarget.

• Every path that leads to the last page passes through pages

that contain reviews for all the contests (thus ensuring that

the voter has the opportunity to review all selections before

casting the ballot).

Ballot definition files would be produced by ballot design

software, such as an interactive tool for laying out and

specifying the appearance of a ballot. Such a tool could offer

guidance on the usability or accessibility of the design, enforce

validity conditions appropriate for a particular jurisdiction, or

give notification when validity conditions are not met.

Ptouch 79

Page 93 of 324
Page 94 of 324

Software design

The Ptouch virtual machine (VM) is composed of four software

modules: the navigator, the video driver, the event loop, and the

vote recorder (see the figure below). This separation does not in

itself prevent attacks, as the corruption of any module still has

the potential to corrupt the outcome of the election. However,

separating the software into modules is a design choice

intended to facilitate verification. It is easier to audit and test

each module separately when there are limited responsibilities

for each module and limited communication between modules.

The navigator walks through the pages in the ballot model,

always starting on the first page. It keeps track of the current

page, the user’s current selections, the current subpage (if any),

and the entered characters on the current subpage (if any). The

navigator responds to just one message:

• When told to activate a slot, the navigator takes the action

for the corresponding target or subtarget, toggles the

corresponding option, or transitions to the subpage for the

corresponding write-in.

The navigator issues three kinds of messages to other modules:

• It tells the video driver to goto a layout upon transition to a

page or subpage. The message specifies the layout index.

LEGEND

one-way data flow

image library

navigator vote

recorder

video

driver frame buffer

paste(sprite_i, slot_i)

goto(layout_i) write(selections)

touch sensor event loop x, y

locate(x, y) slot_i

activate(slot_i) storage device

ballot

definition

hardware

device

software

module

ballot model

Figure 5.4. Block diagram of the Ptouch VM. The arguments layout i, sprite i, slot i,

x, and y are integers; selections is an array of arrays of lists of integers.

Ptouch 80

Page 94 of 324
Page 95 of 324

• It tells the video driver to paste sprites into slots as

necessary to display options, write-ins, reviews, and write-in

text. The message specifies the sprite index and slot index.

• It tells the vote recorder to write the selections when the

ballot is cast (when transitioning to the last page). The

message contains an array of max sels selections for each

contest. Each selection is a list of integers: for a selected

option this is a single integer, the index of the selected

sprite; for a write-in, this is the index of the selected sprite

followed by the indices of the entered character sprites.

The video driver has only one piece of state: it keeps track of

which layout is the current layout. It interprets the slot index in

a paste command in the context of the current layout. The

video driver handles three kinds of messages:

• When told to goto a layout, the video driver copies the

background image into the frame buffer and remembers the

given layout index.

• When told to paste a sprite into a slot, the video driver

copies the sprite into the frame buffer at the position

specified by the slot.

• When told to locate a given point by its co-ordinates, the

video driver looks through the slots in the current layout

and returns the index of the first slot that contains the

point, or a failure code. (When slots overlap, targets take

precedence because they come first in the slot array.)

LEGEND

one-way data flow

image library

navigator vote

recorder

video

driver frame buffer

paste(sprite_i, slot_i)

goto(layout_i) write(selections)

touch sensor event loop x, y

locate(x, y) slot_i

activate(slot_i) storage device

ballot

definition

hardware

device

software

module

ballot model

Figure 5.4. Block diagram of the Ptouch VM. The arguments layout i, sprite i, slot i,

x, and y are integers; selections is an array of arrays of lists of integers.

Ptouch 81

Page 95 of 324
Page 96 of 324

The event loop receives touch events from the screen’s touch

sensor. The software assumes that when the user touches the

screen, the sensor reports (x, y) coordinates in the same

coordinate space used for displaying images. Upon receiving a

touch event, the event loop asks the video driver to locate the

corresponding slot, then passes the slot number on to the

navigator in an activate message.

The vote recorder records the voter’s selections in non-volatile

storage upon receiving a write message from the navigator.

The votes are recorded using a tamper-evident,

history-independent, subliminal-free storage method. Molnar,

Kohno, Sastry, and Wagner have proposed several schemes with

these properties [48] for storing ballots on a programmable

read-only memory (PROM). Each stored selection includes or

indicates its associated ballot definition so that the meaning of

the selections is apparent from the storage contents.

LEGEND

one-way data flow

image library

navigator vote

recorder

video

driver frame buffer

paste(sprite_i, slot_i)

goto(layout_i) write(selections)

touch sensor event loop x, y

locate(x, y) slot_i

activate(slot_i) storage device

ballot

definition

hardware

device

software

module

ballot model

Figure 5.4. Block diagram of the Ptouch VM. The arguments layout i, sprite i, slot i,

x, and y are integers; selections is an array of arrays of lists of integers.

Ptouch 82

Page 96 of 324
Page 97 of 324

Implementation

Ptouch is implemented in Python [63], and it runs on Linux,

MacOS, or Windows. Ptouch uses Pygame [62], an open-source

multimedia library for Python, to handle graphics and mouse

input. It runs on a commodity PC using the video display and

the mouse to simulate a touchscreen device (a mouse click at a

particular location is interpreted as a screen touch).

Ptouch reads the ballot definition from a file named ballot

and writes vote records to a file named votes. The ballot file

represents read-only media and is opened read-only; the votes

file represents a PROM. Each time the program runs, it casts at

most one ballot, then enters a terminal state.

Ptouch models the procedures that would take place in a

real election as follows. Creating an empty votes file

corresponds to opening the polls at the beginning of election

day with a blank PROM. Restarting the program corresponds to

activating the voting machine for a single voter. I have assumed

that only the pollworker has the ability to restart the machine,

so pollworkers can ensure that each voter only votes once.

Setting the votes file read-only corresponds to closing the polls

and removing the PROM.

The source code for Ptouch is available in Appendix A. The

source code is also available online, together with an example of

a ballot definition file in the Ptouch ballot format, at

http://pvote.org/.

Ballot definition. A separate Python module, not shown in

Figure 5.4, reads the ballot file, verifies all the conditions

necessary to determine that it is well-formed, and deserializes it

to objects in memory. All integers in the file are stored as

4-byte unsigned integers; images are uncompressed with 3

bytes for each pixel (corresponding to the red, green, and blue

components of its colour).

Ptouch does not include any user interface for selecting

which ballot definition to use; instead, it assumes that the

Ptouch 83

Page 97 of 324
Page 98 of 324

appropriate ballot file will be present when the program

starts. Different ballot files can be used for different runs.

Note that the selection of a ballot definition can be divided

into two parts: choices that have to be authorized by the

pollworker (such as choosing which precinct’s ballot to use) and

choices that the voter is allowed to make (such as choosing a

preferred language). The former type of choice can be

implemented by having the pollworker select the ballot file.

The latter type of choice can be implemented either by having

the pollworker select a ballot definition file at the voter’s

request, or by combining multiple ballots into a single ballot

definition. For example, a ballot could support both English and

French by including all the pages for an English ballot and all

the pages for a French ballot, with a starting page to let the user

choose between them.

How the pollworker’s selection would be implemented in

hardware remains an open question. One possibility would be

for the ballot definitions to be stored on individual

write-protected memory cards; to support voting for multiple

precincts, a pollworker would insert the appropriate precinct’s

ballot definition card to activate the voting machine for a single

voting session. Alternatively, all the ballot definitions could be

stored on the machine in advance, and the pollworker would

use some other means to choose one when starting each new

voting session. In either case, Ptouch models this step simply as

having the authorized choice of ballot file be present when

the program starts.

Vote storage. The votes file is used to simulate a PROM, a

solid-state storage device initially filled with 1 bits; writing to a

PROM can change 1 bits to 0 bits, but never the reverse. The

vote recorder writes to the file in a manner consistent with this

property.

Ptouch stores the ballots using a copyover list [48], because

it is history-independent, simple to implement, and does not

depend on a random number generator. A copyover list is a list

of items stored in sorted order; each time items are added to

Ptouch 84

Page 98 of 324
Page 99 of 324

new sorted list

maximum space that could have been used to store all

preceding lists, regardless of order in which votes were cast

4. recording complete:

old sorted list new sorted list

3. erasing old list in progress:

old sorted list new sorted list

2. writing new list in progress:

erased (all zeroes) old sorted list unused (all ones)

1. before recording:

first flag indicates start of valid list of vote records

Figure 5.5. Storing votes in a copyover list. The list is always written in sorted order and

the amount of erased space preceding the list is independent of the size of previous lists,

so that no information is revealed about the order in which votes were cast. On a PROM,

changing a bit from 1 to 0 is an irreversible operation.

the list, a new copy of the entire list is written in sorted order

and the old copy is erased by overwriting it with zeroes.

Because the items are sorted according to their content, the list

does not reveal the order in which the items were added. A

copyover list uses O(n2

) space in the number of items, but

previous analysis [48] shows that only a modest and

inexpensive amount of storage would be required to handle all

the votes that could be expected to be cast on one machine in

one day.

The items in the copyover list are the individual selections

within each contest from all the voters. Each item consists of

the SHA-1 hash [52] of the ballot definition, the integer index of

the contest, and the integer index of the selected option sprite.

For a write-in selection, this is followed by the indices of the

selected character sprites. All integers are stored as 4-byte

unsigned integers. The individual selections are stored as

separate items so that the votes file can be published without

letting voters mark their ballots to prove how they voted, as

explained in Section 4.

Because the items in the list can vary in length, the size of

the list depends on the contents of the selections. If the new list

Ptouch 85

Page 99 of 324
Page 100 of 324

were stored immediately after the old list, the size of the erased

space would reveal something about the size of the old list and

hence about the sequence of votes. (For example, if two

selections are stored, one with a short write-in and one with a

long write-in, then the size of the erased space reveals which

one was cast first. Casting the long one first would yield a

larger erased space than if they were cast in the opposite order.)

Therefore, one should always erase the maximum amount of

space that would have been required, regardless of the order in

which the selections were added to the list.

A flag value is stored at the beginning of each list, and the

list is encoded so that it cannot contain the flag value. The first

occurrence of the flag in the file is considered to signal the start

of the current list of votes. After the new list is written, erasing

the flag in front of the old list commits to the new list, as

shown in Figure 5.5. This commitment is atomic, because

changing even one bit invalidates the flag.

Interpreting recorded votes. For a stored selection to have a

well-defined meaning, it must be somehow associated with a

ballot definition. Here are four possible ways to do this:

1. Store an entire copy of the ballot definition with each

selection.

2. Assume a pre-established global mapping of identifiers to

ballot definitions; store an identifier with each selection.

3. Store a cryptographic hash of the ballot definition with each

selection.

4. Store an array of ballot definitions, then store an array

index with each selection.

The first scheme is simple, but uses a lot of storage space.

At a resolution of 1024 by 768 pixels, a full-screen image

occupies about 2.4 megabytes; a typical ballot definition is on

the order of 10 to 100 megabytes. Storing a few hundred votes

would require gigabytes of space.

The second scheme uses very little space, but depends on

management of a global namespace of ballot definition

identifiers, which might be brittle and error-prone. If a vote

Ptouch 86

Page 100 of 324
Page 101 of 324

record says that it belongs to ballot definition #34 and there is a

disagreement about which ballot definition was #34, the vote

record becomes meaningless.

Ptouch uses the third scheme because it uses only a small

amount of space, and as long as the hash function is collision- resistant, there can be no ambiguity about which ballot

definition is associated with each vote record. As long as you

can obtain a copy of the ballot definition, you can ascertain the

true meaning of a vote. Since we’ve already assumed that the

ballot definitions are published, this is not a serious problem.

The fourth scheme yields a vote record that is fully

self-contained. But in order to store all the definitions on

write-once storage, without revealing anything about the order

in which they were used, and without using very large amounts

of space, all the acceptable ballot definitions must be known in

advance. This scheme would make sense for a machine that

provides some way for the pollworker to select which ballot

definition to use.

If the list of acceptable ballot definitions is fixed in advance,

it would be possible to use just one storage device instead of

two. The storage medium would initially contain all the ballot

definitions; the machine would both read the ballot definitions

from it and append the vote records to it. In such an alternative

scheme, vote records could not become inadvertently separated

from their ballot definitions, but it might be more difficult to

provide a hardware-based guarantee that the ballot definitions

are never alterable.

Ptouch 87

Page 101 of 324
Page 102 of 324

Evaluation

Size. The entire implementation of Ptouch is 291 lines long, not

including comments and blank lines. The breakdown of module

sizes is as follows:

ballot definition loader and verifier 126 lines

event loop 13 lines

navigator 92 lines

video driver 22 lines

subtotal (user interface) 255 lines

vote recorder 38 lines

total 291 lines

Dependencies. Ptouch runs on Python version 2.3. It was

implemented with minimal dependencies so that the size of the

Python code would give a reasonable indication of the true

complexity of the program. It uses only one collection type, the

Python list. Although some lists change length while the

program is running, every list has an upper bound on its length

determined by the ballot definition, so an implementation

based on arrays could preallocate the necessary space.

The user interface modules import nothing from Python’s

standard library, and use only these built-in functions:

• open and read on the ballot definition file.

• ord to convert characters to integers.

• enumerate and range for iterating over lists.

• len and the remove method on lists.

The only Pygame drawing function that Ptouch uses is blit,

which copies a bitmap onto the screen. A few other Pygame

functions are used just to initialize the graphics display.

The vote recording module uses Python’s built-in sha module

for computing the SHA-1 hash of the ballot definition, and also

the following built-in functions:

Ptouch 88

Page 102 of 324
Page 103 of 324

• open, read, write, seek, and tell on the vote storage file

to simulate access to a PROM.

• ord and chr to convert characters to integers.

• enumerate for iterating over lists.

• The sort method to sort the copyover list.

• len and max to find the longest item in the copyover list.

Functionality. The ballot definition format is capable of

supporting:

• both general and primary elections

• ballots in any language and any typeface

• voter instructions at any point in the process

• multiple contests on a single screen

• splitting a contest over multiple screens

• contests allowing more than one selection

• photographs or logos shown with candidates

• write-in text in any alphabetic language

• review of selections before casting the ballot

• jumping directly to specific contests or review screens

• regulations requiring voters to review their selections before

casting the ballot

• regulations restricting the number of times that voters may

review their selections

Because the implementation of write-ins assumes that each

character is selected with a single keypress on the touchscreen,

it can only support alphabetic languages; write-ins in

ideographic writing systems such as Chinese are not supported.

Ptouch does not provide administrative functions such as

viewing vote counts or changing configuration settings. It also

does not perform encryption; by design, there is no need to

encrypt the stored votes.

Separation of concerns. The Ptouch software is divided into

five modules that can be implemented and inspected

separately. Each module has a limited responsibility, which

makes it easier to audit and test.

Ptouch 89

Page 103 of 324
Page 104 of 324

The ballot definition loader is responsible for establishing

that the ballot definition is well-formed. If the loader is

implemented correctly, and if the other modules rely only on

the conditions of well-formedness, then the only possible kind

of software failure is a failure to load the ballot definition.

Successful completion of the loading and verification step

assures that software errors cannot occur during the voting

session.

It is easy to see by direct inspection of the source code that

all modules other than the event loop only react to messages

they receive. The event loop is the only module capable of

initiating messages, but it is also the smallest and easiest to

audit.

The video driver is a passive component, never sending any

messages at all. In particular, the video driver does not have the

authority to activate slots (that is, it cannot “press buttons” in

the interface), which reduces vulnerability to errors in its

implementation.

The navigator has access to only the ballot model and

cannot draw arbitrarily on the display. Because it cannot see the

image data, it cannot determine the semantics of the user’s

selections. Freezing the implementation of the VM before

choosing the order of candidates on the ballot would make it

difficult for even the author of the navigator to bias the vote for

or against a specific candidate. Also, the only input to the

navigator is a slot number, which is a small integer, so the

navigator can be subjected to exhaustive testing.

The voting machine has no non-volatile storage other than

the ballot definition and the cast vote storage. Because the

machine is restarted for each new voting session, and because

the ballot definition is read-only, the only state retained

between voting sessions is the vote storage. Furthermore, the

vote recorder module only receives messages and never sends

any messages to any other software module, so no information

in the vote storage can reach any of the other modules.

Consequently, the user interface seen by each voter is

determined only by the ballot definition and cannot reveal any

Ptouch 90

Page 104 of 324
Page 105 of 324

information about previous voting sessions. Also, this ensures

that all voters using the same ballot definition receive the same

voting experience.

Election rules. Election regulations concerning the ballot are

upheld either by the implementation of the navigator module or

by validating the ballot definition.

By design, Ptouch can only cast one ballot each time it runs.

It is easy to confirm by inspection of the navigator that the only

way to cast a ballot is to arrive at the last page and to see that

the last page is a terminal node in the ballot definition.

It is also straightforward to verify that overvoting is

impossible, because only the navigator can manipulate the

user’s selections, and there are only two places in the code

where an item is added to the selection list.

Other election process rules can be verified by examining

the ballot definition. For example, to ensure that the voter will

be notified of undervotes before casting the ballot, we would

check the graph of transitions among pages to see that the

voter must proceed through review pages before arriving at any

page that can cast the ballot.

Comparison. At only 291 lines of Python, the Ptouch code is

much smaller than the 31 000 lines of code in Diebold’s

AccuVote TS software.1

It may be slightly more appropriate to

compare the 255 lines of UI code with the AccuVote’s 14 000

lines of UI code—but neither comparison is entirely fair,

because Ptouch lacks some of the AccuVote’s functionality and

the two systems have different sets of dependencies.

Nonetheless, the correctness of Ptouch is certainly easier to

assure than the correctness of the AccuVote TS code. In general,

programs with less code tend to be easier to review, easier to

test, less likely to contain bugs, and less likely to crash.

One reason that there is less code is the choice of

programming language: Ptouch requires a Python interpreter,

whereas the AccuVote TS does not. On the other hand, the

1This is less than Kohno’s figure of 49 609 lines [43] because it excludes blank lines and comments.

Ptouch 91

Page 105 of 324
Page 106 of 324

AccuVote TS software depends on Microsoft Windows CE and

builds its user interface using the Microsoft Foundation Classes,

which are much larger and more complex that the blit

functionality that Ptouch uses from Pygame.

It is not unreasonable to consider running Python on voting

machines. Python is widely deployed and vetted and is

supported by an active developer community. Unlike Windows

CE and MFC, Python is a mature open source project,

distributed with an extensive suite of regression tests. As a data

point concerning Python’s size, note that Nokia has released a

small Python interpreter that runs on Nokia mobile phones [57].

The interpreter fits in a 504-kilobyte installation package, which

also includes over 40 Python library modules that Ptouch

doesn’t use.

Alternatively, the Python code could be translated into a

compiled language. Although Ptouch is written in a higher-level

language, it uses very few of Python’s library modules and

built-in functions, as described earlier in this section. It is

reasonable to expect that translating this code into a compiled

language would multiply its size by a factor of 3 or 4, but not by

100.

Despite its small size, the Ptouch code maintains clear

boundaries and minimal data flow among its five modules. As

described earlier in this section, many of the desired security

properties of the voting machine are straightforward to verify in

Ptouch, due to its design. The AccuVote TS code does not lend

itself to similarly easy analysis.

Ptouch 92

Page 106 of 324
Page 107 of 324

Shortcomings

Ptouch lacks several kinds of important functionality.

Accessibility. Ptouch only supports a touchscreen for both

input (receiving choices made by the voter) and output

(displaying information to the voter). Thus, it is not usable by

voters who are blind or voters who lack the motor control to

accurately touch buttons on the touchscreen.

Printing. Ptouch does not accommodate a printer, so it does not

produce any permanent paper records. In particular, there is no

voter-verifiable printed record of votes (VVPAT), a feature that is

currently required by law (either for elections or for purchase of

new equipment) in 16 U. S. states [23]. As of this writing, the

United States Congress is considering a bill [79] that would

make VVPATs a nationally required feature on all DRE machines.

Audit logging. Ptouch does not record any logs of its operation.

Audit logs can be of invaluable assistance to investigations in

the event of a dispute, evidence of tampering, or a software

error.

Straight-party voting. Some paper ballots offer a way to make a

single party selection that has the effect of voting for the

candidate of that party in every contest. As of this writing,

straight-party voting is used in 17 U. S. states [50], but Ptouch

does not support such a feature.

Complex voting rules. Some ballots have voting rules that

cross between selections or contests. For example, sometimes

primary elections for multiple parties are combined on a single

paper ballot, where the voter first indicates their choice of party

and then votes in the contests for that party’s primary. Ptouch

would not be able to present different contests depending on

the party selection that the voter made. As another example, a

Ptouch 93

Page 107 of 324
Page 108 of 324

ballot for a recall election would first let voters vote for or

against the recall itself, then offer a selection of replacement

candidates. Typically, it is only valid to vote for a replacement if

one has voted in favour of the recall. Ptouch cannot enforce this

kind of restriction.

Ranked and other election methods. Most single-winner

elections decide the victor by the plurality rule (also known as

“first past the post”), in which each voter votes for a single

candidate and the candidate with the most votes wins. Despite

its popularity, it is a poor method for electing a single winner

because it penalizes moderate candidates and often motivates

voters to misrepresent their preferences [44], locking in

polarized two-party control of the government. Of the many

election methods that have analyzed by social choice theorists,

it is one of the worst methods for electing a single winner.

One simple way to obtain a truer representation of voter

preferences is approval voting [9], in which each voter can vote

for as many candidates as they want. An approval election is

easily conducted with Ptouch by setting max sels equal to the

number of candidates.

Another election method that has been proposed is range

voting [74], in which voters assign scores to the candidates and

the candidate with the highest average or total score wins.

Range voting can be conducted with Ptouch by setting up a

ballot with a separate contest for each candidate. For example,

to allow scores from 0 to 10, the ballot can simply present

eleven choices, numbered 0 to 10, next to each candidate.

Several election methods involve ballots on which voters can

rank the candidates. The Schulze method [71] and the Tideman

method [77] belong to a family of methods called Condorcet

methods, which use ranked ballots to simulate all the possible

one-on-one match-ups among the candidates. With these

methods, voters are allowed to specify rankings that include

ties (i.e., they can assign the same rank to more than one

candidate). Another notable method, in which voters must

specify rankings without ties, simulates a series of runoff

Ptouch 94

Page 108 of 324
Page 109 of 324

elections in which the least popular candidates are successively

eliminated. This method is known as “preferential voting” or

the “alternative vote” in many countries around the world and

called “instant runoff” in the United States.

Ptouch does not provide a way for voters to rank their

choices. Also, because Pvote records each selection separately,

multiple selections cannot be combined to produce the effect of

a ranked ballot.

For example, some paper ballots implement ranking by

repeating the same list of options multiple times. San Francisco

uses a simplified variant of “instant runoff” in which voters

rank only their top three choices. On the ballot, the same list of

candidates appears in each of three columns; voters are

instructed to indicate their first choice in the first column,

second choice in the second column, and third choice in the

third column. This tactic would not work for Pvote because

Pvote would store the voter’s first, second, and third choices as

three separate selections, dissociated and scattered among all

the selections made by other voters.

Ptouch 95

Page 109 of 324
Page 110 of 324

6 Accessibility

Why was a second prototype needed? 97

What is Pvote’s approach to accessibility? 98

How are alternative input devices handled? 99

How does blindness affect interface navigation? 100

How do blind users stay oriented within an interface? 101

How do blind users keep track of what is selected? 102

How do blind users get feedback on their actions? 103

How are vision-impaired users accommodated? 104

96

Page 110 of 324
Page 111 of 324

Why was a second prototype needed?

Ptouch, the first prototype, demonstrates significant progress in

simplifying voting machine software, but it lacks several key

abilities, as explained at the end of the last chapter. It cannot

handle certain ballot features, it does not print a paper record,

and—most significantly— it supports only a touchscreen for

input and output. Such an interface can only be used

conveniently by voters who can see, who can read, and who

have sufficient fine motor ability to accurately select items on

the screen.

A major motivator for using electronic voting machines in

the first place is to meet the accessibility requirements dictated

by HAVA [78]. By failing to support more accessible voting

interfaces, Ptouch left open the question of just how much

software complexity is necessary to fulfill these machines’

ostensible reason for existing. The purpose of Pvote, the second

prototype, is to answer that question, and to show that better

verifiability can be achieved without sacrificing accessibility and

useful functionality.

Accessibility 97

Page 111 of 324
Page 112 of 324

What is Pvote’s approach to accessibility?

When I began working on accessibility support, I started to

create a special “accessible version” of the system just for blind

users, with a keypad for input, an audio-only interface, and no

visual display. Before long, however, it became apparent that a

universal design approach would be more fruitful.

Universal design [75] is the practice of designing artifacts

that are flexible enough to support a wide range of users with

and without disabilities, instead of separate artifacts or

assistive devices for specific disabilities. A unified solution

avoids stigmatizing people with disabilities, and the increased

flexibility often yields benefits for all users. Volume controls on

public telephones are an example of universal design: they help

everyone use the telephone more easily in a noisy environment,

not just those who are hard of hearing.

Pvote’s unified solution is a single user interface with

synchronized audio and video, rather than a visual interface for

sighted voters and a separate audio-only interface for blind

voters. The same information is presented concurrently in

audio and video; user input always yields both audio and visual

feedback. Voters without disabilities can also benefit from

audio confirmation of their choices [73].

Noel Runyan, an expert on accessible technologies,

recommended synchronized audio and video to me during the

early stages of this work. His recent report on voting

interfaces [69] also makes this recommendation. Although not

all of the electronic voting machines currently in use support

synchronized audio and video, such a requirement is present

both in the 2005 Voluntary Voting System Guidelines

(VVSG) [80] (item 3.2.2.1f) and in a draft of the next generation

of these guidelines [81] (item 3.3.2-D).

Accessibility 98

Page 112 of 324
Page 113 of 324

How are alternative input devices handled?

Pvote takes a universal design approach to input devices as well

as output devices. Its design is intended to support voting

hardware with both a touchscreen for input and an alternate

input device. The design assumes that the alternate input

device consists of a fixed number of momentary buttons and

sends a signal identifying a button whenever a button is

pressed. This is a useful input model because it allows a wide

range of devices to serve as the alternate device, including a

regular keyboard, a numeric keypad, a set of hardware buttons

designed for voting, or a sip-and-puff device. The voter can

decide whether to use the touchscreen or the alternate input

device, and can mix them freely.

This simple input model does not account for the timing of

button presses. For a person with severe physical disabilities

who can only operate one or two buttons, the length and timing

of button presses is an important way to convey information.

Although Pvote cannot distinguish between a short press and a

long press, these inputs could be translated in hardware to

separate signals. That is, from Pvote’s perspective there would

be two different buttons: the hardware would send one keycode

for a short press and a different keycode for a long press.

However, Pvote’s input model does not support autoscan, a

typical feature of “single-switch access” software. In an

autoscan interface, a cursor cycles through a list of choices at a

steady rate and the user activates the switch when the cursor

arrives at the desired choice.

A system with both multimodal input and multimodal

output is helpful not only for blind voters but also voters with

low vision, voters who are illiterate, voters with cognitive

disabilities, and voters with physical impairments that make it

hard to use a touchscreen, as well as voters with multiple

disabilities.

Accessibility 99

Page 113 of 324
Page 114 of 324

How does blindness affect interface

navigation?

With respect to voting user interfaces, the visual channel has

two advantages over audio. First, it can convey textual

information at a higher bandwidth: for most people, reading a

printed list of candidates’ names is faster than listening to them

spoken aloud. Second, a visual image can convey more

information at once without an explicit navigation mechanism:

although a screen full of text probably exceeds what a person

can hold in working memory, a sighted person can easily select

and gather information of interest just by looking around at

different parts of the screen.

A consequence of both of these properties is that audio-only

voting interfaces require smaller units of navigation than

video-only voting interfaces. Whereas an entire page can be

visually “current” to the voter, only a few words can be aurally

“current” at any given moment. For example, a visual interface

can present an entire list of candidates at once but an audio

interface must present the candidates one at a time. Therefore,

a multimodal interface should support the notion of the user’s

focus at two different levels of hierarchy, with audio

information at the finer-grained level. Pvote introduces states

within pages to serve this purpose.

Accessibility 100

Page 114 of 324
Page 115 of 324

How do blind users stay oriented within an

interface?

Visual information can be presented passively, whereas

presenting audio information requires continuous activity. Even

an inert display can convey visual information, whereas silence

conveys no audio information at all.

If a user is distracted while viewing static visual

information, then getting reoriented is just a matter of looking

over the information again. But if a user is distracted while

listening to audio, then getting reoriented requires that the

computer actively replay the audio. Therefore, an audio

interface needs fallback mechanisms to trigger reorientation.

The ballot definition needs to be able to specify a “Where am I?”

button that the user can press to recover context.

There also needs to be a way to provide reorienting

information after a period of inactivity, if the user is lost and

doesn’t know what button to press for help. The Pvote ballot

format has a timeout parameter for this purpose (see

Figure 7.2); the ballot definition can specify a transition to

another page or audio message to be played when the timeout

period expires with no user activity. The most recent draft of

the next version of the VVSG [81] includes requirements for a

“defined and documented inactivity time” (item 3.2.6.1-E) after

which the system alerts the user (item 3.2.6.1-F); Pvote’s timeout

functionality addresses these requirements.

Accessibility 101

Page 115 of 324
Page 116 of 324

How do blind users keep track of what is

selected?

At any given moment, the voting machine keeps track of the set

of current selections in each contest, which I’ll call the selection

state. Recall that in Ptouch, the selection state is displayed

visually by option areas, which display a particular option, with

one appearance if it is selected and another if it is not, and by

review areas, which list all the selected options in a specified

contest.

To communicate the selection state to a blind user, the

audio interface needs to be able to play audio messages that

vary depending on what is currently selected. Thus, a Pvote

ballot defines audio in terms of a sequence of audio segments,

where each segment can be constant or variable. A constant

segment always plays the same audio clip independent of the

selection state; a variable segment selects an audio clip to play

as a function of the current selection state. Constant and

variable segments are concatenated together to give the effect

of filling in blanks in spoken prose, yielding a verbal description

of the selection state.

Accessibility 102

Page 116 of 324
Page 117 of 324

How do blind users get feedback on their

actions?

Not every user action succeeds. For example, the user should

not be allowed to overvote. Ptouch enforced this rule, but

provided no particular feedback; an attempt to select an

additional candidate would simply have no effect when the

contest is already full. (I use “full” to mean that the maximum

allowed number of selections in the contest is selected, and

“empty” to mean that none of the options in the contest are

selected.)

In a visual interface this might be considered acceptable

behaviour, as the user can immediately see whether or not the

attempt to select had an effect: either the candidate’s name

takes on a selected appearance, or it doesn’t. But in an audio

interface, there is no such direct feedback without an audio

message describing what just happened. Therefore, to support

audio-only voters, the ballot definition needs to be able to

specify different audio messages depending on whether an

action succeeded or failed, and possibly also depending on the

reason for success or failure. The new condition structure in

Pvote’s ballot format makes this possible (see Figure 7.2).

Accessibility 103

Page 117 of 324
Page 118 of 324

How are vision-impaired users

accommodated?

A large-type mode and a high-contrast mode can be helpful for

users with a vision impairment. Both the 2005 VVSG [80] (items

3.3.2.1b and 3.3.2.1c) and the draft new guidelines [81] (items

3.2.5-E and 3.2.5-I) require electronic voting displays to be

capable of showing all information in at least two type sizes,

3.0–4.0 mm and 6.3–9.0 mm, and to have a high-contrast mode

with a contrast ratio of at least 6:1 (on current voting machines

this usually means a black-and-white mode).

Ptouch can already accommodate these requirements by

providing multiple prerendered versions of the ballot in a single

ballot definition file, together with buttons for selecting or

switching the desired presentation mode. For example, each

normal-type page could include a button for switching to the

large-type version of the same page. However, such a ballot

would contain duplicates of the contests and their options. In

terms of the ballot definition data structures, the large-type

contest and the normal-type contest for each office would be

distinct contests with distinct options. Ptouch’s electronic

records of votes would therefore reveal whether the voter

selected a large-type candidate or a normal-type candidate,

which could be considered a voter privacy violation.

Because Pvote has more flexible handling of user input, it is

possible to design ballots for Pvote that avoid this problem. A

single user action can trigger multiple effects in Pvote, so user

selection of any one option can be made to automatically select

all the corresponding variants in the other display modes (e.g.,

touching the button for Jane Smith in normal print also selects

Jane Smith in large print, Jane Smith in high contrast, etc.). The

results of making the same selections in different presentation

modes would then be indistiguishable.

Accessibility 104

Page 118 of 324
Page 119 of 324

7 Pvote

the multimodal prototype

Overview 106

Goals 107

Design principles 110

Differences between Pvote and Ptouch 114

Ballot definition format 121

Software design 127

Implementation 132

Evaluation 133

105

Page 119 of 324
Page 120 of 324

Overview

This chapter describes Pvote [91], the second prototype

vote-entry program I developed. Unlike Ptouch, Pvote offers

support for most voters with disabilities by providing

synchronized audio and video output, and also by accepting

input from buttons and other accessible input devices as well as

touchscreen input. In addition, Pvote handles several less

common ballot features that Ptouch does not support.

Pvote is intended for voting machines that are electronic

ballot printers; thus, both the ballot definition and the VM

software contain a component specifically to support ballot

printing. An implementation targeted for other types of voting

machines could substitute a different component for recording

the cast votes, such as the tamper-evident direct recording

mechanism in Ptouch.

Pvote 106

Page 120 of 324
Page 121 of 324

Goals

Pvote aims to achieve both functionality goals and security

goals. The set of supported ballot features and user interface

features is determined by the ballot definition format. Security

depends on the correct and verifiable implementation of the

Pvote program.

Functionality. Voting systems should be highly usable by voters

of all kinds, and their usability should be evaluated and

improved through user testing. However, user testing of

specific ballot designs is outside the scope of the present work.

The aim here is to design not a particular ballot, or even a

particular style of ballot, but a ballot definition format—one

flexible enough that usability and accessibility experts can use

it to create better and better ballots as our understanding of

voting human factors improves. As explained in Chapter 4, the

prerendering approach opens up the process so ballot design

can be done by expert ballot designers, not just voting machine

programmers.

If the ballot definition format is rich enough to replicate

what existing voting machines do, then the resulting voting

system will be capable of being at least as usable as today’s

voting systems. We can be assured of not having lost ground in

usability, while throwing open the door to future ballot designs

with better usability. Thus, the goals for the new ballot

definition format are described in terms of sufficient

functionality to match existing systems:

• It should be possible, with an appropriate ballot definition

and corresponding hardware, to produce a similar or better

user experience compared to existing electronic voting

systems, including those that support audio or

synchronized audio and video.

• It should be possible to define a reasonably usable

synchronized audio and video interface corresponding to a

real ballot.

Building Reliable Voting Machine Software

 https://drive.google.com/file/d/0B3FeaMu_1EQyUVE0VzhxWU5kVlU/view

Pvote 107

Page 121 of 324
Page 122 of 324

• It should be possible to create a single ballot definition that

makes sense for a voter who can only hear the audio and

also makes sense for a voter who can only see the visual

display.

• It should be possible to implement most of the voting

features needed for real elections, such as multiple-selection

contests, write-ins, straight-party voting, eligibility for

contests dependent on selections in other contests,

restrictions on cross-endorsed candidates, and ranked

voting.

Security. As elaborated in Chapter 2, the essential task of a

voting system is to obtain an accurate and fair measurement of

the preferences of the electorate. Pvote aims to uphold the

security goals given on page 31 of that chapter:

G3. In every voting session, the correct choice of ballot style

is presented to the voter.

G4. Every ballot is presented to the voter as the ballot

designer intended.

G5. At the start of every voting session, no choices are

selected.

G6. The voter’s selections change only in accordance with

the voter’s intentions.

G7. The voter receives accurate feedback about which

choices are selected.

G8. The voter can achieve any combination of selections that

is allowable to cast, and no others.

G9. The voter has adequate opportunity to review the ballot

and make changes before casting it.

G10. The ballot is cast when and only when the voter intends

to cast it.

G11. Every selection recorded on a ballot cast by a voter is

counted.

G12. No extra ballots or selections are added to the count.

G13. The selections on the ballots are not altered between the

time they are cast and the time they are counted.

G14. The tally is a correct count of the voters’ selections.

Pvote 108

Page 122 of 324
Page 123 of 324

G17. No voting session allows more than one ballot to be cast.

G20. Every voter can begin a voting session within a

reasonable, non-discriminatory waiting time.

G21. Every voting session provides a reasonable,

non-discriminatory opportunity to cast a ballot.

G23. The processing of voter choices does not expose how

any particular voter voted.

G24. Voters are not provided any way to give plausible

evidence of how they voted to an external party.

With Pvote:

• G3 has to be upheld by the pollworker who selects the ballot

style for the voter.

• G4, G5, G6, G7, G8, G9, and G10 are upheld by verifying that

the ballot definition is properly designed and by verifying

that Pvote interprets the ballot definition correctly.

• G11, G12, and G13 are upheld by the physical procedures

for casting and handling the paper ballots printed by Pvote.

• G14 is upheld by the counting procedures for paper ballots.

• G17 is upheld by verifying that Pvote becomes inert

immediately after casting a ballot.

• G20 and G21 are upheld by verifying that Pvote does not

crash or become unresponsive during a voting session.

• G23 is upheld by ensuring that Pvote’s behaviour in each

voting session is independent of all previous sessions.

The security goal is that it must be possible (and preferably

easy) for reviewers to verify to their satisfaction that the system

guarantees the necessary correctness properties, without

relying on faith in the honesty or competence of the system’s

developers.

Pvote 109

Page 123 of 324
Page 124 of 324

Design principles

In the design for Pvote’s ballot definition format, I tried to

anticipate and support many kinds of functionality. Because the

design involved many trade-offs among interdependent factors,

I found that I had to choose some guiding principles to help

keep design decisions well grounded. These principles would

probably also be useful when taking the prerendering approach

to high assurance in other domains as well as voting. The next

few sections outline these principles, in order of decreasing

priority.

Work from a concrete use case. I found it helpful to examine a

specific paper ballot (in this case, a sample ballot from the

November 2006 election—Contra Costa County’s ballot style

167) and consider what would constitute an acceptable

corresponding electronic ballot. Any faithful translation of this

ballot into electronic form must present all of the information

on the paper ballot, enable a voter to navigate through the

ballot, keep the voter oriented as to their position in the ballot,

allow access to all available options, and keep the voter aware

of the current state of their selections. The electronic ballot

must achieve all of these things for voters using only the visual

display as well as voters using only the audio.

The paper ballot turned out to be invaluable for driving the

design process. It was often a good idea to refer back to the

paper ballot to work out exactly what should appear on the

screen, what audio should be played, and the appropriate

responses to all possible user inputs. The exercise of creating a

specific ballot definition file revealed which features had to be

supported by the ballot definition language and when it was

necessary to add more capabilities to the VM.

Minimize VM complexity. The ultimate goal of this work is to

facilitate the review of the software that has to be verified— in

this case, the VM. In general, the smaller and simpler the VM,

Pvote 110

Page 124 of 324
Page 125 of 324

the easier it is to verify. When faced with a design decision, I

would keep returning to this goal and choose whichever option

yielded a smaller or simpler VM. This principle was secondary

only to including the necessary functionality to implement a

real ballot, as described in the preceding section.

One consequence of this principle is that it is more

important to avoid redundancy in the VM code than to avoid

redundancy in the ballot data. For example, although the ballot

definition file is likely to contain images that are highly

compressible, they are not compressed, because that would

require additional decompression code in the VM. Security

reviews are expensive, but storage is cheap.

Maximize UI design flexibility. Other things being equal, it is

better for the ballot definition language to allow a wider range

of user interfaces to be specified. Giving more expressive power

to the ballot definition makes the VM less likely to have to

change to support new user interface designs. Since each

change invalidates previous software reviews, future-proofing

the VM yields real security benefits. Thus, when considering

design options that do not significantly differ in the complexity

of the VM or in the ability of the VM to enforce correctness

constraints, the preferred option is the one that leads to a larger

space of possible user interfaces.

One effective way to make the ballot definition language

more expressive is to embrace orthogonality in language

primitives. Replacing specialized high-level constructs with a

combination of more general-purpose primitives can be doubly

beneficial: the increased generality enables more possibilities to

be expressed, while the increased uniformity makes the

implementation in the VM more concise. For example, the new

ballot definition language has no special cases to distinguish,

say, review screens or write-in screens from other kinds of

screens; all of these are just pages, and information can be

freely arranged on each page.

The trade-off is that using lower-level constructs sometimes

makes the ballot definition more tedious to review. Switching to

Pvote 111

Page 125 of 324
Page 126 of 324

more general, lower-level constructs tends to be advantageous

if it gives the UI designer more flexibility without creating new

ways of violating correctness, and if the additional tediousness

of reviewing ballot definitions can be mitigated by automated

tools for reviewers.

Maximize UI review efficiency. In the prerendering paradigm,

assurance is derived from human review of the user interface

specification (which, in this application, is the ballot definition).

It’s impossible to eliminate the necessity of human involvement

in evaluating the correctness of the user interface—whether a

visual display or a spoken message is misleading is a judgement

that can only be made by a human reviewer.

However, design choices in the UI specification language can

affect the level of confidence with which a human reviewer’s

observations can be generalized across all of the situations a

user might encounter in using the voting interface. A

well-designed ballot definition language can give human

reviewers the leverage to draw broad conclusions from

manageable amounts of review and testing.

In any system with even a modest number of variables, the

number of states that the system can be in is likely to be so

large that a human reviewer cannot observe the user interface

in every possible state. But the ballot definition language can

defend the human reviewer from this combinatorial explosion

of states. The language can facilitate the creation of ballot

definitions for which observing a limited number of states (for

example, walking through the ballot making selections as in

typical pre-election testing) is sufficient for a reviewer to

accurately extrapolate the UI presentation of all the states the

system could come to be in.

For example, candidate’s names are spoken in the audio

interface in several contexts. When the voter selects Candidate

X, there should be an audio confirmation message such as

“Candidate X has been selected.” When the voter is reviewing

selections, the voter should hear a message such as “For

President, your current selection is Candidate X.”

Pvote 112

Page 126 of 324
Page 127 of 324

Suppose that these two messages were each independently

recorded as a single sound clip. In order to verify the

correctness of the audio, a human reviewer would have to listen

to each pair of messages to ensure that the candidate sounds

the same in each pair— it would not do for the selection

message to say “Candidate X” but for the review message to say

“Candidate Y.” In such a scheme, the number of messages to

review would be roughly the number of candidates times the

number of contexts in which they appear.

The reviewer’s work can be made substantially easier by

breaking up the messages into parts. The candidate’s name can

be recorded and stored once, then used for all the messages

that have to do with that candidate. The remaining part (in our

example, “has been selected”) can be recorded once and used

for all the selection messages across all candidates. The

consistent reuse of audio clips can be checked mechanically,

leaving the human reviewer with fewer audio clips to review

(roughly the number of candidates plus the number of contexts).

Pvote 113

Page 127 of 324
Page 128 of 324

Differences between Pvote and Ptouch

In order to support synchronized audio and video, Pvote’s

ballot definition format is substantially more complex than that

of Ptouch. Figure 7.1 presents a side-by-side comparison of the

ballot definition formats for Ptouch and Pvote. Only the main

part of the ballot definition, the ballot model, is shown.

The rest of this section describes some of the main

differences. In the terminology used here, a contest is a race or

a referendum put to the voters and an option is one of the

choices available in a contest. The options in a race are

candidates, whereas the options in a referendum are typically

“yes” and “no.” During voting, the selection state is the voter’s

current set of selections in all the contests. A contest is said to

be empty if none of its options are selected, and full if the

maximum allowed number of selections is selected. The

capacity of a contest is its maximum allowed number of

selections. To undervote in a contest is to leave the contest less

than full; to overvote in a contest is to exceed its capacity.

state

timeout action

int sprite_i

audio segment

binding

audio segment

intn timeout_page_i

int timeout_state_i

Pages contain states. Pvote adds states within pages to

represent a second level of focus, which is necessary to support

navigation for blind users. Because audio navigation units are

finer-grained, audio information is primarily specified at the

state level, whereas visual information is primarily specified at

the page level. All the states belonging to a page share the same

overall appearance and layout, though a part of the screen can

vary in appearance. Behaviours in response to user input can be

specified at either level; at the state level they apply to a single

state; at the page level they apply to all the states in the page.

For example, in a typical ballot layout, a single page

presents a list of candidates, and each state within that page

highlights one of the candidates. The user presses a button to

step through the candidates one at a time. In the state when a

particular candidate becomes the focus, the audio for the

candidate’s name is played and the candidate’s name is

Pvote 114

Page 128 of 324
Page 129 of 324

Pvote ballot definition format

ballot model

page

contest

int max_sels

int max_chars

ballot model

page

int timeout_ms

counter area

int group_i

int sprite_i

state

timeout action

int sprite_i

audio segment

binding

audio segment

group

int max_sels

int max_chars

int option_clips

option

int sprite_i

int clip_i

intn writein_group_i

subpage (write-in page)

subtarget

int action

binding

intn key

intn target_i

condition

audio segment

step

enum op

intn group_i

int option_i

intn next_page_i

int next_state_i

audio segment

condition

enum type

int clip_i

intn group_i

int option_i

condition

enum predicate

intn group_i

int option_i

bool invert

Ptouch ballot definition format

definitions of

substructures (small

dotted rectangles) used

in the Pvote format

intn timeout_page_i

int timeout_state_i

option area

int contest_i

write-in option area

int contest_i

option area

int group_i

int option_i

review area

int contest_i

review area

int group_i

intn cursor_sprite_i

target

int action

int page_i

int contest_i

binding

Figure 7.1. Comparison of Ptouch and Pvote ballot formats (only the ballot model is shown).

Pvote 115

Page 129 of 324
Page 130 of 324

highlighted in the list on the screen. Selecting the currently

highlighted candidate is a state-level behaviour, since the

selection operation is different in each state, whereas moving

on to the next contest is a page-level behaviour.

To help keep the user oriented, each state has a timeout

audio sequence and an optional timeout transition. The ballot

definition as a whole has a timeout parameter in milliseconds.

When there has been no audio playing and no user input for the

timeout period, the timeout audio sequence is automatically

played and the timeout transition takes place, if any.

binding

intn key

intn target_i

audio segment

intn next_page_i

int next_state_i

step

condition

User inputs can be mapped to arbitrary actions. In the Ptouch

format, the behaviours triggered by screen touches were

specialized according to the type of the touched screen region.

For example, option areas were hardcoded in the VM to react to

a touch by toggling whether the associated option was selected,

and write-in option areas were hardcoded to react to a touch by

jumping to an associated write-in page.

This direct binding between screen regions and actions is

inadequate for a multimodal design in several ways. First, direct

binding doesn’t make sense for input from hardware buttons:

there aren’t enough buttons to dedicate a button to each option.

Second, the multimodal design has to allow for a “Where am I?”

button, which could play many different audio messages

depending on the current system state.

Third, text entry in an audio-only interface is a nontrivial

design problem. Ptouch could afford to hardcode text entry

behaviour in the obvious way—a keyboard made of onscreen

buttons, where touching each button types a letter. But there is

no single obvious way to enter text in an audio-only interface.

For example, if the voting machine has space for a physical

keyboard, then each key should type a letter. If the machine

provides a button pad with “next”, “previous”, and “select”

buttons, then the buttons could be used to navigate forward and

backward through the alphabet to enter letters. The text entry

method is likely to vary widely depending on the hardware, so it

should be left up to the ballot definition to specify.

Pvote 116

Page 130 of 324
Page 131 of 324

For all these reasons, Pvote allows more flexible input

handling by adding a layer of indirection: a list of bindings

between input events and the actions they trigger.

step

enum op

intn group_i

int option_i

Actions are generalized to sequences of steps. With the

introduction of bindings, there had to be a new data structure

to represent the action triggered by an input event. An action is

represented as a list of steps, where each step performs a

selection operation (select an option, deselect an option,

deselect the last selected option in a contest, or clear a contest).

Actions with multiple steps are useful for straight-party voting

and for ballots containing multiple versions of the same

contests (e.g., large type and normal type). The list of steps is

embedded in the data structure for a binding.

audio segment

enum type

int clip_i

intn group_i

int option_i

condition

Audio sequences are attached to states and actions. Pvote can

play audio when switching into a new state or when an action is

triggered by user input. Also, when an action is triggered by

user input, any currently playing audio is interrupted.

In the ballot definition, an audio sequence contains a list of

audio segments, where each segment can be constant or

variable. There are four kinds of variable audio segments:

1. A segment that plays the name of a specific option.

2. A segment that plays the names of all the selected options

in a contest.

3. A segment that plays an audio clip chosen according to the

current number of selected options in a contest.

4. A segment that plays an audio clip chosen according to the

maximum number of selections a contest allows.

For example, to tell the voter which candidates are selected for

city council, an audio sequence might consist of two segments:

first a constant segment that says “Your selections for city

council are”, then a variable segment that lists the voter’s

selections in the city council contest. However, a constant

segment is often insufficient to produce a natural-sounding

description. If there is only one selection, the sentence should

Pvote 117

Page 131 of 324
Page 132 of 324

begin “Your selection for city council is”. The third type of

variable segment can be used to select the grammatically

correct sentence.

The first and fourth types don’t vary depending on the

selection state—any ballot that uses them can be defined just

as well in a ballot definition language without them. But their

presence allows more of the ballot definition to be kept the

same from election to election, reducing the work of verifying

the ballot definition.

condition

enum predicate

intn group_i

int option_i

bool invert

Actions and audio segments can be conditional. Because

Pvote’s behaviour in response to user input is no longer

hardcoded, the ballot definition needs a way to specify different

effects that will occur depending on the selection state. For

example, consider what should happen when the user touches

an option. If the option is already selected, then one possible

effect would be to deselect the option. If the option is not

selected, and its contest is not full, then the option should

become selected. And if the option is not selected but its

contest is full, then the selection should not change. Each of

these three cases also needs its own corresponding audio

message describing what happened.

To make this possible, each binding has an attached list of

conditions concerning the selection state. Each condition can

check whether a particular option is selected, a particular

contest is full, or a particular contest is empty. The binding is

triggerable only if all of its conditions are satisfied.

Conditions are also useful for constructing variable audio

sequences. A list of conditions is attached to each segment;

each segment is played or skipped depending on whether all of

its conditions were satisfied. Reusing conditions in this way

increases the flexibility of audio feedback while keeping the

implementation simple.

Groups replace contests and write-ins. A group is a container

of selectable options; it can represent a contest (with options

such as candidates) or a write-in entry field (where the options

Pvote 118

Page 132 of 324
Page 133 of 324

group

int max_sels

int max_chars

int option_clips

option

are the individual characters that can appear in the entry field).

The group data structure is used for both purposes because of

the functionality that is common between them:

• In both cases, the current selection for a group is a list of

options (even though a contest selection has set-like

semantics and a write-in selection has ordered sequence

semantics).

• In both cases, user actions add and remove options to and

from the selection (e.g., selecting candidates in a contest or

typing letters into a write-in field).

• Visual display of the selections in a group consists of

pasting the candidate images or the letter images into a

sequence of equal-sized spaces on the screen.

• Audio playback of the selections in a group consists of

playing each selection in order—reading off the list of

selected candidates or speaking the letters in a write-in field

one by one.

option

int sprite_i

int clip_i

intn writein_group_i

Options have their own data structure. In the Ptouch format,

every option area was assumed to represent a distinct option.

Thus, each option area only had to indicate which contest it

belonged to. The Ptouch structure did not list the options in

each contest; determining the number of options in a contest

required scanning the pages of the ballot definition and

counting the option areas associated with that contest.

In the Pvote format, information about each option—such

as its associated image and audio clip— is kept in an option

structure under the option’s group. The option areas refer to

these option structures. Bindings that select options, audio

segments that play option names, and conditions that examine

options can either refer to options directly or refer to option

areas, which themselves refer to options. This extra layer of

indirection yields two kinds of flexibility:

• The same option can be displayed in more than one place

on the ballot.

• Options can be rearranged by rearranging the references

from option areas to options.

Pvote 119

Page 133 of 324
Page 134 of 324

The rearrangement of options, also known as “candidate

rotation,” helps to reduce the bias inherent in displaying a

particular candidate first. Without the extra layer of indirection,

candidate rotation would be difficult to automate reliably

because there would be no distinction between a reference to an

option area and a reference to an option. This distinction is

important because indirect references to options via option

areas should change when options are shuffled, whereas direct

references to options should not change when options are

shuffled. When candidates are rotated, their screen position

and order of audio presentation should change, but the set of

candidates belonging to a party for a straight-party vote should

not change.

This design feature makes it easy to rotate candidates by a

simple manipulation of the ballot file. Rearranging the

references from option areas to options does not change the

option number assigned to each candidate. Thus, candidate

rotation has no effect on the way voter selections are recorded,

which helps to avoid the possibility of confusion in interpreting

recorded votes.

One could produce several rotated variants of a ballot

before the election and publish them all; it is straightforward to

verify that two ballot definition files represent the same ballot

except for reordering of the candidates. Alternatively, the voting

machine could even perform candidate rotation on the fly for

each voter, though the Pvote implementation does not do this.

Pvote 120

Page 134 of 324
Page 135 of 324

Ballot definition format

Figure 7.2 depicts the complete ballot definition format for

Pvote. Just as in Ptouch, the ballot definition describes a state

machine. Each state transition is triggered by a user action or

by an idle timeout. Executing a transition can cause options to

be selected or deselected. Audio feedback can be associated

with states and with transitions between states. The ballot

definition contains three main sections:

• Ballot model: structure of the ballot and interaction flow of

the user interface.

• Audio data: sound clips to play over the headphones.

• Video data: images to display on the screen, the locations at

which to display them, and locations of touch-sensitive

screen regions.

These three sections are separated so that each one can be

supplied to a distinct module of the VM with distinct

responsibilities. In addition, they can be separately updated—

for example, one can translate the audio interface into a

different language by recording audio clips for a new audio data

section while leaving the other sections unchanged.

In Pvote, which is written specifically for a text-based

electronic ballot printer, the ballot definition also includes a

fourth section, the text data, which contains textual descriptions

of the contests and candidates for the printer to print.

Audio data. The audio data section specifies the sample rate at

which all audio is to be played and provides an array of sound

clips. Other parts of the ballot definition refer to these clips by

supplying indices into this array. The audio clips are

uncompressed and monophonic, and each sample is a 16-bit

signed integer. The clips can contain recordings of actual

speech or of prerendered synthesized speech.

Video data. The video data section specifies the resolution of

the video screen and includes an array of layouts and an array

Pvote 121

Page 135 of 324
Page 136 of 324

ballot model

page

int timeout_ms

counter area

int group_i

int sprite_i

state

timeout action

int sprite_i

audio segment

binding

audio segment

group

int max_sels

int max_chars

int option_clips

option

int sprite_i

int clip_i

intn writein_group_i

binding

intn key

intn target_i

condition

audio segment

step

enum op

intn group_i

int option_i

intn next_page_i

int next_state_i

audio segment

condition

enum type

int clip_i

intn group_i

int option_i

condition

enum predicate

intn group_i

int option_i

bool invert

definitions of

substructures (small

dotted rectangles) used

in the ballot model

intn timeout_page_i

int timeout_state_i

option area

int group_i

int option_i

review area

int group_i

intn cursor_sprite_i

binding

text data

text group

str name

bool writein

str[] options

audio data

clip

sample[] samples

int sample_rate

video data

layout

target rectangle

int left

int top

int width

int height

screen image

int width

int height

pixel[width × height] pixels

int width

int height

slot rectangle

int left

int top

int width

int height

sprite image

int width

int height

pixel[width × height] pixels

Figure 7.2. The Pvote ballot definition data structure. Stacked boxes represent arrays. This

is the second line of the caption.

Pvote 122

Page 136 of 324
Page 137 of 324

of sprites. A sprite is an image, smaller than the size of the

entire screen, that will be pasted on the screen somewhere. A

layout consists of a full-screen image, an array of targets, and

an array of slots. A target is a rectangular region of the screen

where a touch will have an effect; a slot is a rectangular region

where a sprite can be pasted. Image data is stored

uncompressed, with 3 bytes per pixel (red, green, and blue

colour values).

group

int max_sels

int max_chars

int option_clips

option

int sprite_i

int clip_i

intn writein_group_i

Ballot model. The ballot model is the main specification of the

state machine. It contains an array of groups and an array of

pages. It also specifies an idle timeout in milliseconds.

Groups and options. A group is a set of choices from which the

voter makes selections. There are two kinds of groups: contest

groups and write-in groups. A contest group represents a race

in which the options are candidates or a referendum question

with options such as “yes” and “no”. A write-in group

represents the text entered in a write-in area within a contest, in

which the options are the characters used to spell out the name

of the write-in candidate. In the array of options within each

group, images and sound clips are specified to represent each

option by providing indices into the arrays of audio clips and

sprites. Within a contest group, an option can also specify that

it is a write-in option and identify the write-in group containing

its write-in text.

Each group specifies its capacity (the maximum number of

selections allowed in the group); for contest groups this

prevents overvotes, and for write-in groups this limits the

length of the entered text. All the write-in options within a

contest must have the same maximum length for text entry.

Pages and states. The page is the basic unit of visual

presentation; within each page is an array of states. The pages

correspond, one-to-one, to the layouts in the video data. At any

given moment, there is a current page and a current state. The

user interface always begins on page 0 in state 0; when the VM

Pvote 123

Page 137 of 324
Page 138 of 324

executes a transition to the last page in the array of pages, the

ballot is printed or cast with the voter’s current selections. In

addition to the array of states, each page contains arrays of

option areas, counter areas, review areas, and bindings.

state

timeout action

int sprite_i

audio segment

binding

audio segment

intn timeout_page_i

int timeout_state_i

The states in a page are states in the state machine of the

user interface. Each state specifies a sprite to be pasted over the

main page image while the state is current. (For example, a page

could show a list of several options, and the states within that

page could display a focus highlight that moves from option to

option. Each state would paste a focus highlight for its option

over the page image.) Each state also has an array of audio

segments to be played upon entering the state, and an array of

its own bindings.

A state can also specify audio segments to be played upon a

timeout and/or an automatic transition to another state upon a

timeout. A timeout occurs when the audio has stopped playing

and there has been no user activity for the timeout duration

specified in the ballot model.

page

counter area

int group_i

int sprite_i

option area

int group_i

int option_i

review area

int group_i

intn cursor_sprite_i

binding

state

An option area is a screen region where an option will be

displayed. Its fields identify the option that will appear there.

A counter area is a screen region that will indicate the

number of options currently selected in a contest; this enables

the interface to provide feedback on undervoting. A counter

area is associated with a group and points to an array of sprites.

The number of currently selected options in the group is used

as an index to select a sprite from the array to display.

A review area is a screen region where currently selected

options will be listed; it has a field to indicate the group whose

selections will be shown. The review area must provide enough

room for up to j options to be displayed, where j is the capacity

of the group. A review area can also specify a “cursor sprite” to

be displayed in the space for the next option when the group is

not full. This allows a review area for a write-in group to serve

as a text entry area, in which a cursor appears in the space

where the next character will be added.

The screen locations for pasting all these sprites (overlays

for states, options for option areas and review areas, and sprites

Pvote 124

Page 138 of 324
Page 139 of 324

for counter areas) are not given in the ballot model; they are

specified in the array of slots in the page’s corresponding layout.

Each state, option area, and counter area uses one slot. Each

review area uses j × (1 + k) slots, where j is the capacity of the

group and k is the capacity of write-ins for options in the group.

(A write-in group cannot itself contain write-in options; thus, for

a review area for a write-in group, k is zero.) Each block of 1 + k

slots is used to display a selected option: the option’s sprite

goes in the first slot, and if the option is a write-in, the

characters of the entered text go in the remaining k slots, which

are typically positioned within the first slot. If there are i

currently selected options in the group, option sprites appear in

the first i of the j blocks. If there is a cursor sprite, it is pasted

into the first slot of block i + 1 when the group is not full.

binding

intn key

intn target_i

condition

audio segment

step

enum op

intn group_i

int option_i

intn next_page_i

int next_state_i

enum predicate

intn group_i

int option_i

bool invert

Bindings. The lists of bindings in pages and states specify

behaviour in response to user input. Each binding consists of

three parts: stimulus, conditions, and response.

There are two kinds of stimuli: a keypress, which is

represented as an integer key code, and a screen touch, which is

translated into a target index by looking up the screen

coordinates of the touch point in the layout’s list of targets. A

binding can specify either a key code or a target index or both.

Each binding can have a list of associated conditions; the

binding applies only if all the conditions are satisfied. A

condition can test whether a particular group is empty or full or

whether a particular option is selected.

The response consists of three parts, all optional: selection

operations, audio feedback, and navigation. The selection

operations are specified as a series of steps, where a step selects

or deselects an option, appends a character to a write-in, deletes

the last character, or clears a group. The audio feedback is

given as an array of audio segments to play. Navigation is

specified as the index of a new page and state.

Bindings for the current state take precedence over bindings

for the current page. When the user provides a stimulus, at

most one binding is invoked: the bindings for the state and

Pvote 125

Page 139 of 324
Page 140 of 324

then the page are scanned in order, and the response is carried

out for the first binding that matches the stimulus and has all

its conditions satisfied.

audio segment

enum type

int clip_i

intn group_i

int option_i

condition

enum predicate

intn group_i

int option_i

bool invert

Audio segments. Audio feedback is specified as a list of

segments. A segment can play a fixed clip, the clip associated

with a specified option, all the clips associated with the options

that are selected in a specified group, or a clip chosen based on

the number of options that are selected in a specified group.

When a clip associated with an option is played, if the option is

a write-in option, the clip for each character in the contents of

the write-in field is also played. More than one clip can be

associated with an option (for example, each candidate could

have a short description and a long description).

At any given moment, at most one clip can be playing at a

time; there is a play queue for clips waiting to be played next.

Whenever a clip finishes playing, the next clip from the queue

immediately begins to play, until the queue is empty. Invoking a

binding always interrupts any currently playing clip and clears

the play queue. The audio segments for the binding, if any, are

queued first; if a state transition occurs, the audio segments for

the newly entered state are queued next.

Each segment has a list of conditions (the same as in a

binding) that must all be satisfied in order for the segment to be

queued; otherwise, the segment is skipped. The conditions are

evaluated when the segment list is being queued (i.e.,

immediately after carrying out the selection steps of a binding,

immediately after entering a new state, or when a timeout

occurs).

Pvote 126

Page 140 of 324
Page 141 of 324

Software design

The virtual machine is composed of five software modules: the

navigator, the audio driver, the video driver, the event loop, and

the vote recorder (Figure 7.3). Each component has limited

responsibilities, and there are limited data flows between

components. Two additional components not visible in

Figure 7.3 are the ballot loader, which deserializes the ballot

definition into memory, and the ballot verifier, which checks the

ballot definition. The loader and verifier complete their work

before the voting session begins (i.e., before any interaction

with the voter). The verifier is responsible for ensuring that the

ballot definition is sufficiently well-formed that the VM will not

crash or become unresponsive during the voting session.

The event loop maintains no state and handles all incoming

events, which are of four types:

• Keypresses: Upon receiving a keypress event, the event loop

sends a press message to the navigator.

video data

paste(sprite_i, slot_i)

goto(layout_i) navigator vote

recorder

video

driver frame buffer write(selections)

touch sensor x, y

locate(x, y)

slot_i

touch(target_i)

press(key)

timeout() storage device

or printer keypad event loop key

audio

driver headphones next()

play(clip_i)

stop()

audio data ballot model

LEGEND

one-way data flow

ballot

definition

hardware

device

software

module

start playing

audio finished set timer timer expired

Figure 7.3. Block diagram of the Pvote virtual machine. The five software modules in

bold generate and run the user interface. The arguments clip i, layout i, sprite i,

target i, key, x, and y are integers; selections is an array of arrays of integers.

Pvote 127

Page 141 of 324
Page 142 of 324

• Screen touches: Upon receiving a touch event, the event loop

sends a locate message to the video driver to translate the

touch coordinates into a target index, then passes this

target index to the navigator in a touch message.

• Audio notifications: Upon receiving notification that a

sound clip has finished playing, the event loop sends a next

message to the audio driver.

• Timer notifications: Upon receiving notification that the

timer has expired, if no sound clip is currently playing, the

event loop sends a timeout message to the navigator to

indicate that the ballot’s specified timeout has passed with

no activity.

Whenever it receives any event, the event loop reschedules a

timer notification event according to the timeout duration in

the ballot definition.

The navigator keeps track of the current page and state and the

current selections in each group, and has no other state. The

navigator responds to three messages:

• touch(target i): Find the first operative binding for the

video data

paste(sprite_i, slot_i)

goto(layout_i) navigator vote

recorder

video

driver frame buffer write(selections)

touch sensor x, y

locate(x, y)

slot_i

touch(target_i)

press(key)

timeout() storage device

or printer keypad event loop key

audio

driver headphones next()

play(clip_i)

stop()

audio data ballot model

LEGEND

one-way data flow

ballot

definition

hardware

device

software

module

start playing

audio finished set timer timer expired

Figure 7.3. Block diagram of the Pvote virtual machine. The five software modules in

bold generate and run the user interface. The arguments clip i, layout i, sprite i,

target i, key, x, and y are integers; selections is an array of arrays of integers.

Pvote 128

Page 142 of 324
Page 143 of 324

current state or page that matches the given target, and

invoke it.

• press(key): Find the first operative binding for the current

state or page that matches the given keypress, and invoke it.

• timeout(): Add the current state’s timeout audio segments

to the play queue, and follow the current state’s timeout

transition, if one is specified.

The navigator sends five messages to other modules:

• goto(layout i) is sent to the video driver upon transition

to a page. The layout index is the same as the page index

(the array of layouts in the video data parallels the array of

pages in the ballot model).

• paste(sprite i, slot i) is sent to the video driver to

paste sprites into slots as necessary for states, option areas,

counter areas, and review areas. sprite i is the index of a

sprite in the array of sprites in the video data; slot i is the

index of a slot in the current layout.

• play(clip i) is sent to the audio driver to queue a clip to

be played on the headphones. clip i is the index of an

audio clip in the array of clips in the audio data.

video data

paste(sprite_i, slot_i)

goto(layout_i) navigator vote

recorder

video

driver frame buffer write(selections)

touch sensor x, y

locate(x, y)

slot_i

touch(target_i)

press(key)

timeout() storage device

or printer keypad event loop key

audio

driver headphones next()

play(clip_i)

stop()

audio data ballot model

LEGEND

one-way data flow

ballot

definition

hardware

device

software

module

start playing

audio finished set timer timer expired

Figure 7.3. Block diagram of the Pvote virtual machine. The five software modules in

bold generate and run the user interface. The arguments clip i, layout i, sprite i,

target i, key, x, and y are integers; selections is an array of arrays of integers.

Pvote 129

Page 143 of 324
Page 144 of 324

• stop() is sent to the audio driver to stop the currently

playing clip.

• write(selections) is sent to the vote recorder to record

the user’s selections. selections is an array of arrays of

integers: one array for each group, listing the indices of the

selected options in that group.

The audio driver maintains a queue of audio clips to be played,

and has no other state. It responds to three messages:

• play(clip i): If nothing is currently playing, immediately

begin playing the specified clip; otherwise queue the

specified clip to be played.

• next(): If there are any clips waiting in the queue, start

playing the next one.

• stop(): Stop whatever is currently playing and clear the

queue.

The audio driver sends no messages to other modules, but

whenever it starts playing a clip, it schedules a notification

event for the event loop to receive when the clip finishes

playing. The audio driver also exposes a flag that the event loop

reads to check whether audio is currently being played.

video data

paste(sprite_i, slot_i)

goto(layout_i) navigator vote

recorder

video

driver frame buffer write(selections)

touch sensor x, y

locate(x, y)

slot_i

touch(target_i)

press(key)

timeout() storage device

or printer keypad event loop key

audio

driver headphones next()

play(clip_i)

stop()

audio data ballot model

LEGEND

one-way data flow

ballot

definition

hardware

device

software

module

start playing

audio finished set timer timer expired

Figure 7.3. Block diagram of the Pvote virtual machine. The five software modules in

bold generate and run the user interface. The arguments clip i, layout i, sprite i,

target i, key, x, and y are integers; selections is an array of arrays of integers.

Pvote 130

Page 144 of 324
Page 145 of 324

The video driver maintains just one piece of state, the index of

the current layout. It responds to three messages:

• goto(layout i): Copy the full-screen image for the given

layout into the video display’s frame buffer and remember

this as the current layout.

• paste(sprite i, slot i): Copy the given sprite into the

frame buffer at the position specified by the given slot in

the current layout.

• locate(x, y): Find and return the index of the first target

that contains the given point in the current layout’s list of

targets, or an error code if the point does not fall within any

target.

The video driver sends no messages to other modules.

The vote recorder maintains no state and responds to only one

message:

• write(selections): Record the voter’s selections.

The vote recorder records votes as appropriate for the type of

voting machine (e.g., printing a ballot, marking a ballot, or

directly recording votes in electronic storage).

video data

paste(sprite_i, slot_i)

goto(layout_i) navigator vote

recorder

video

driver frame buffer write(selections)

touch sensor x, y

locate(x, y)

slot_i

touch(target_i)

press(key)

timeout() storage device

or printer keypad event loop key

audio

driver headphones next()

play(clip_i)

stop()

audio data ballot model

LEGEND

one-way data flow

ballot

definition

hardware

device

software

module

start playing

audio finished set timer timer expired

Figure 7.3. Block diagram of the Pvote virtual machine. The five software modules in

bold generate and run the user interface. The arguments clip i, layout i, sprite i,

target i, key, x, and y are integers; selections is an array of arrays of integers.

Pvote 131

Page 145 of 324
Page 146 of 324

Implementation

Pvote is a Python [63] implementation of the design

described here. Pvote can run on Linux, MacOS, and Windows.

Graphics and sound are handled by Pygame [62], an

open-source multimedia library for Python. Touchscreen input

is simulated using the mouse, and hardware button input is

simulated using the keyboard.

Pvote is written to be deployed as an electronic ballot

printer. In Pvote, the vote recorder prints out a textual

description of the voter’s selections. Each time Pvote runs, it

prints at most one ballot (to standard output) and then enters a

terminal state. The source code for Pvote is included in

Appendix B. The code is also available online at

http://pvote.org/, together with a sample ballot definition

file in the Pvote format. The sample ballot definition is

described in detail in Appendix C.

Pvote 132

Page 146 of 324
Page 147 of 324

Evaluation

Size. The entire Pvote implementation is 460 lines long, not

counting comments and blank lines. The breakdown of module

sizes is as follows:

ballot loader 137 lines

ballot verifier 96 lines

subtotal (pre-voting) 233 lines

event loop 25 lines

navigator 120 lines

audio driver 35 lines

video driver 22 lines

subtotal (voting) 202 lines

vote recorder 25 lines

total 460 lines

Dependencies. Pvote is written in a small subset of Python 2.3,

called Pthin, which is specified in the Pvote Assurance

Document [92]. Pvote uses only one built-in collection type, the

Python list, and only the following built-in functions:

• open and read to read the ballot definition file.

• chr and ord to convert integers to/from characters.

• list to convert strings to lists of characters.

• enumerate and range to iterate over lists.

• len, append, remove, and pop to manipulate lists.

The ballot loader imports the built-in SHA module and uses it to

verify a SHA-1 hash of the ballot definition. The audio and

video driver use various Pygame functions: init and stop in

the audio mixer module, play on the Sound object, init and

set mode in the video display module, fromstring in the

image module for loading images, and blit on the Surface

object to paste images onto the screen. Aside from these, Pvote

imports no other library modules.

Pvote 133

Page 147 of 324
Page 148 of 324

File size. Pvote was tested with a sample ballot definition file

generated by a ballot compiler, also written in Python. The

ballot compiler takes a textual description of the contests and

options and produces the necessary images using the

open-source ReportLab toolkit [65] for drawing, text rendering,

and page layout. To construct the audio clips for the ballot

definition, the compiler uses the same textual description to

select fragments from a library of clips of recorded speech and

concatenates the fragments together as needed. The audio clips

in this sample ballot are recorded from live speech, which is

usually preferred over synthesized speech.1

The inclusion of screen images and audio recordings in the

ballot definition yields a large file. See Appendix C for details

on the sample ballot. It contains five contests: two are

single-selection races with six candidates each, one is a

multiple-selection race with five candidates, and two are

propositions. An audio description of about 100 words for each

proposition is included in the ballot. The result is a

69-megabyte ballot definition file, containing 17 pages at a

resolution of 1024 × 768 pixels and 8 minutes of audio

sampled at 22050 Hz. As a rough estimate, a ballot with 20 or

30 contests might occupy a few hundred megabytes.

File sizes this large might seem unwieldy in practice.

However, files can be compressed for transmission (bzip2

compresses this 69-megabyte ballot to 12.5 megabytes, which is

better than a factor of 5), and ballot definitions can be loaded

onto voting machines using inexpensive SD flash memory cards

(one-gigabyte SD cards can be purchased for about US$10).

Functionality. Pvote achieves the functionality goals that were

listed at the end of Chapter 6. Pvote can support a wide range

of features in the voting user interface, including multimodal

input and output and virtually complete flexibility in the style

of audio and visual presentation. Because Pvote uses

1The National Council on Disability wrote, “Voting systems that provide digitized human speech are

preferable to systems with synthesized speech because digitized speech is ‘more readily comprehensible’ and

more likely to contain the correct pronunciation of candidate names” [51].

Pvote 134

Page 148 of 324
Page 149 of 324

prerecorded audio and prerendered images, the ballot can be

presented in any language.

With its generalized actions and conditions, Pvote offers

much more flexibility in the handling of user input than Ptouch,

its touchscreen-only predecessor. Unlike Ptouch, Pvote can

handle straight-party voting, dependencies among contests

(e.g., in a recall election, voting for a replacement candidate

conditional on voting “yes” for recalling the incumbent), and

conditional navigation (e.g., displaying an undervote warning

page when the voter has not made any selections in a contest).

The ballot designer also has more freedom to define the

interaction for selection and text entry.

To get a rough sense of Pvote’s coverage of ballot design

features, I examined NIST’s collection of sample ballots [56],

consisting of 373 ballots from 40 U. S. states for elections from

1998 to 2006. The longest was a 2004 ballot from Chicago that

had 15 elected offices, 74 judicial confirmations, and one

referendum. The following table summarizes the features used

on these ballots. All these features, and hence all the ballots in

the collection, are supported by Pvote’s ballot definition format.

Ballot feature Ballots

Vote for 1 of n 373

Vote for up to k of n (k > 1) 195

Vote for an image (e.g., a state flag) 2

Vote yes/no (referendum, confirmation) 251

Ranked choice (up to 3 choices) 7

Write-in candidate 318

Straight-party vote 60

Cross-endorsed candidates 8

Multi-party primary 5

Party logos 21

The collection also includes ballots in Chinese, Ilokano,

Japanese, Korean, Spanish, and Vietnamese. Pvote can present

ballots in any language, though for write-in candidates voters

must spell out the name using an alphabetic language.

Pvote 135

Page 149 of 324
Page 150 of 324

8 Security review

How was Pvote’s security evaluated? 137

What were Pvote’s security claims? 139

How was Pthin defined? 143

What flaws did the reviewers find? 145

What improvements did the reviewers suggest? 146

Did the reviewers find the inserted bugs? 148

What ideas did reviewers have on programming languages? 149

What ideas did reviewers have on conducting reviews? 151

What lessons were learned from the review? 153

136

Page 150 of 324
Page 151 of 324

How was Pvote’s security evaluated?

My overall purpose in creating Pvote was to design and write

voting software whose security could be easily verified. To test

whether it had achieved this purpose, I invited several security

researchers to all-day meetings at the University of California,

Berkeley to review the Pvote design and source code. Reviewers

met from March 29 to March 31, 2007 and also on May 20, 2007.

David Wagner and I were on hand for all three days in March

to explain Pvote’s design, answer the reviewers’ questions, and

provide any assistance they requested in their investigation. On

May 20, I attended but David Wagner did not.

The reviewers examined and discussed Pvote for a total of

about 90 reviewer-hours over the four days of reviewing.

Participants. On March 29 and 30, these reviewers were

present:

• Matt Bishop, UC Davis

• Mark Miller, HP Labs

• Dan Sandler, Rice University

• Dan Wallach, Rice University

On March 31, these reviewers were present:

• Tadayoshi Kohno, University of Washington

• Mark Miller, HP Labs

• Dan Sandler, Rice University

On May 20, these reviewers were present:

• Ian Goldberg, University of Waterloo

• Tadayoshi Kohno, University of Washington

The assurance document. Before the review, I prepared a

77-page document to provide the reviewers with detailed

information about Pvote. This document [92] presents the ballot

definition format, the software design, and the source code of

Pvote itself. The source code is displayed with annotations

justifying the validity of each line, shown on the facing page

opposite each page of code.

Security review 137

Page 151 of 324
Page 152 of 324

Not all the reviewers had previous experience with the

Python programming language. To ensure that everyone had a

common understanding of the code, I had to provide a

definition of the language in which it was written. I chose to

define a small subset of Python called Pthin, containing just the

syntactic constructs and functions used by Pvote. With the

language semantics clearly specified, we could exclude flaws in

the language implementation from the security review, and

focus on Pvote itself.

The assurance document defined the scope of the review by

stating assumptions about how Pvote would be used and listing

the security properties that Pvote was supposed to uphold

under those conditions. These properties were drawn from the

assurance tree given in Chapter 2 and the security goals given

in Chapter 6. For each claimed security property, I gave an

assurance argument.

The review process. I spent most of the first day presenting

the software design of Pvote and walking the reviewers through

the implementation. For the rest of the first day and the second

day, the reviewers examined the software, mostly by hand, and

asked us questions. We discussed various aspects of Pvote,

voting security, and software reviewing in general.

By the end of the second day, David Wagner and I realized

that, because the reviewers had not found any bugs and we did

not know of any bugs in the code, we could not conclude

anything about how effective they were at finding bugs or

whether any bugs were actually present. Therefore, to motivate

the reviewers and observe their effectiveness at finding bugs,

we decided to intentionally insert some bugs into the code. On

the third and fourth days, we announced that the code

contained at least one bug, and asked the reviewers to find it.

On the fourth day we also asked the reviewers to try inserting

their own bugs, hoping this would motivate them to understand

the code in more depth.

Security review 138

Page 152 of 324
Page 153 of 324

What were Pvote’s security claims?

Pvote was evaluated against a set of responsibilities, under a set

of assumptions about how it is deployed for an election. Both of

these are listed below.

Since several possible vote-recording mechanisms can be

used with Pvote, I had to coin a generic term to refer to the

recording step. Thus, the term committed means that voter

selections are finalized as far as the machine is concerned—this

occurs on a DRE when votes are recorded, but on an EBM or EBP

when votes are printed. The following lists also use the term

voting session, which lasts from when a voting machine starts

interacting with a particular voter (e.g., when the first screen of

the voting user interface comes up) until the ballot is committed

or the voter abandons the machine. This does not include

per-voter initialization steps by pollworkers.

Assumptions. The reviewers were asked to assume that:

A1. The voting machine software (ostensibly Pvote) is

handed over for review before the election.

A2. The software that runs on the voting machines on

election day is exactly what was reviewed.

A3. Pvote is started once per voting session.

A4. Only authorized voters are allowed to carry out voting

sessions.

A5. Ballot definition files are published for review and

testing before the election.

A6. The correct ballot definition is selected and used for

each voting session.

A7. The ballot definitions used on election day are intact,

exactly as they were reviewed.

A8. The programming language implementation functions

correctly.

A9. The operating system and software libraries function

correctly.

A10. The voting machine hardware functions correctly.

Security review 139

Page 153 of 324
Page 154 of 324

Responsibilities. Under the above conditions, Pvote must:

R1. Never abort during a voting session. (For any given

ballot definition, Pvote should either (a) always reject it

as invalid and never start voting sessions, or (b) always

accept it as valid and never abort during any session

with that ballot definition.)

R2. Remain responsive during a voting session.

R3. Become inert after a ballot is committed.

R4. Display a completion screen when and only when a

ballot is committed, and continue to display this screen

until the next session begins.

R5. Exhibit behaviour in each session independent of any

previous sessions.

R6. Exhibit behaviour independent of which parts of buttons

are touched (all touch points within a target region

should be equivalent).

R7. Exhibit behaviour that is determined entirely by the

ballot definition and the stream of user input events and

their timing.

R8. Commit valid selections (no overvotes and no invalid

candidates or contests).

R9. Commit the ballot when and only when so requested by

the voter.

R10. Correctly and unambiguously commit the selections the

voter made.

R11. Present instructions, contests, and options as specified

by the ballot definition.

R12. Navigate among instructions, contests, and options as

specified by the ballot definition.

R13. Select and deselect options according to user actions as

specified by the ballot definition.

R14. Correctly indicate which options are selected, when

directed to do so by the ballot definition.

R15. Correctly indicate whether options are selected, when

directed to do so by the ballot definition.

R16. Correctly indicate how many options are selected, when

directed to do so by the ballot definition.

Security review 140

Page 154 of 324
Page 155 of 324

Examples of threats. The above set of assumptions placed

certain threats out of scope for the review, such as:

• Insiders among pollworkers. We assumed that pollworkers

would not give voters multiple sessions (A3), would not let

unauthorized people vote (A4), and would select the correct

ballot style for each voter (A6).

• Tampering with the software distribution. We assumed that

the voting machine software would not be altered between

review and use (A1, A2).

• Tampering with the ballot definition. We assumed that the

ballot definition would not be altered between review and

use (A5, A7).

• Tampering with cast vote records. We assumed that other

mechanisms would protect the integrity of paper or

electronic vote records produced by Pvote.

• Faulty or subverted non-voting-specific software. We

assumed that the software components that are not specific

to voting function correctly (A8, A9). The assurance

document describes the proper behaviour of the library

functions and operating system.

• Faulty or subverted hardware. The review focused only on

software (A10).

• Poor ballot design. It was specifically not claimed that using

Pvote would eliminate accessibility or usability problems,

even though testing with the published ballot definitions

might help reveal some of these problems in time to

address them.

The review focused on threats of the following four kinds:

• Voters. Voters can interact with Pvote using the touchscreen

and keypad. Is there any sequence of interactions that can

cause Pvote to violate voting rules (R3, R4, R8) or violate

voter privacy (R5)?

• Bugs. Can any valid ballot definition, in combination with

any sequence of user interactions, ever cause Pvote to

behave incorrectly (R1, R2, R6, R7, R8, R9, R10, R11, R12,

R13, R14, R15, R16)?

Security review 141

Page 155 of 324
Page 156 of 324

• Insiders among voting software suppliers. An insider might

modify Pvote to contain backdoors or hidden weaknesses

before being handed over for review and installation. Could

an attacker make effective changes that would go unnoticed

by reviewers and testers?

• Insiders among election officials. An insider might design or

alter a ballot definition to contain the wrong information or

bias the vote. Could an attacker subvert ballot definitions in

a way that would go unnoticed by reviewers and testers?

Insider threats were an area of particular attention because

Pvote was designed specifically to address the problem that

software is complex and hard to trust. One of the things I

hoped to learn from the review was the effect of Pvote’s novel

design approach on the difficulty of performing or detecting an

insider attack.

Security review 142

Page 156 of 324
Page 157 of 324

How was Pthin defined?

Pthin is a subset of the Python language; that is, all Pthin

programs are valid Python programs. The following is just an

overview of the Python features that are included in Pthin, for

readers familiar with Python. For a complete Pthin specification,

see the assurance document [92].

Features. In Pthin, values have types, but variables do not; any

variable can be assigned a value of any type. There is a unique

special value called None whose only supported operation is

comparison to None. Aside from this, there are six types of

values in Pthin:

• Integers are signed and unlimited in size.

• Strings contain 8-bit bytes.

• Lists have variable length and can contain values of any type

as elements.

• Functions may take arguments of any type and always return

a value (which is None if no value is explicitly returned).

• Classes contain method definitions; invoking a class (like a

function) instantiates an object.

• Objects are instances of classes. Each object has its own

public namespace of fields, accessed with a dot.

Pthin includes the following operators from Python:

• = for assignment to variables and object fields

• . for accessing object fields (as in x.y = 5)

• +, -, *, /, % for doing arithmetic on integers

• + for concatenating strings or lists

• [] for indexing strings and lists (as in x[3])

• [:] for slicing strings and lists (as in x[i:j])

• ==, !=, <, <=, >, >= for comparing integers

• ==, != for comparing strings and comparing to None

• and, or, not for Boolean operations (these accept operands

of any type and yield the integer values 0 or 1)

• in for testing if an element is in a list (as in a in b)

Security review 143

Page 157 of 324
Page 158 of 324

Pthin includes the following kinds of Python statements:

• print prints out a string

• assert causes a fatal error if a condition is not met

• if executes a block conditionally

• for iterates over the elements of a list

• while iterates on a condition

• import imports code from other modules

• class declares a class (but there is no inheritance in Pthin)

• def defines a function or a method

• return returns a value from a function

Pthin includes the following built-in Python functions:

• range(i) makes a list of the integers from 0 to i - 1

• chr(i) converts an integer to a one-byte string

• ord(s) converts the first byte of a string to an integer

• len(x) gets the length of a string or list

• list(s) breaks a string into a list of one-byte strings

• enumerate(l) turns a list l into a list of [i, x] pairs for

each element x and its index i

• open(s) opens a file for reading

Pthin lists support the append(), remove(), and pop()

methods from Python. Pthin includes list comprehension

expressions, of the form [x*x for x in range(5)], which

evaluate an expression once for each element of a list to yield a

new list containing all the results.

Properties. Pthin is a completely deterministic language, which

is of critical significance for reviewing and testing. There is no

access to clocks or sources of randomness. The only ways that

a Pthin program can be influenced by the outside world are by

reading from files and by receiving Pygame events.

The definition of Pthin eliminates some of the more

complex features of Python, such as inheritance and exception

handling. Exceptional conditions in Pthin cause fatal errors,

since they cannot be caught.

Security review 144

Page 158 of 324
Page 159 of 324

What flaws did the reviewers find?

The reviewers did not find any bugs in the original Pvote source

code. However, they did find some errors and omissions in the

assurance document. I will describe the most significant ones

here; all of the reviewers’ findings are explained in detail in

Appendix E.

Correctness claim for R1 (non-termination). Pvote is supposed

to “never abort during a voting session” (R1), and the assurance

document presents a supporting argument for this claim. The

presented argument is incomplete because it neglects to rule

out one way that Pvote could run out of memory. Nonetheless,

it is still possible to show that memory usage has an upper

limit; Appendix E provides the missing part of the argument.

Correctness claim for R9 (ballot casting). Pvote is supposed to

“commit the ballot when and only when so requested by the

voter” (R9). However, a ballot definition can direct Pvote to

automatically cast the ballot (by jumping to the last page) after

some amount of time has passed with no user activity, in

violation of this requirement. One of the assumptions is that

the ballot definition file must be checked before the election

(A5). To ensure that R9 is met, the pre-election check has to

ensure that no automatic transition goes to the last page.

Missing requirement for voter privacy. The assurance

document doesn’t state an explicit requirement for preserving

the voter’s privacy once his or her ballot has been committed.

Pvote is restarted afresh for each new voter (A3), but what about

the interval from when the voter walks away until the machine

is reset? A ballot definition that displays the voter’s selections

on the last page (i.e., after committing the ballot) might violate

the voter’s privacy. So the pre-election check must also prohibit

such ballot definitions; the assurance document neglected to

make this clear.

Security review 145

Page 159 of 324
Page 160 of 324

What improvements did the reviewers

suggest?

The following are the main recommendations on which all the

reviewers could agree; Appendix E lists all their suggestions in

more detail, including those that were less conclusive.

Assurance document. The reviewers recommended including a

detailed breakdown of all the properties to be verified about the

ballot definition, divided into three categories:

• properties checked by Pvote’s verifier,

• properties checked by other automated tools, and

• properties checked by humans.

This would address two of the three flaws mentioned in the last

section (the problem with the correctness claim for R9 and the

voter privacy concern about the last page).

The reviewers also recommended:

• adding a section that enumerates all causal connectivity

between Pvote and the outside world;

• stating explicit preconditions about the state of the audio

driver when the navigator’s timeout() method is called;

• mentioning that cursor sprites need to be checked to ensure

they can’t be confused with any option sprites or character

sprites; and

• cautioning that, if an exception occurs during a voting

session, Python will emit a stack trace that might reveal

something about the voter’s choices.

Pthin. The reviewers recommended these changes to Pthin, to

simplify the language and facilitate reviewing:

• prohibiting all unprintable characters except newline;

• prohibiting all identifiers containing double-underscores,

except init ;

• prohibiting nested class or function definitions; and

• prohibiting chained assignments of the form x = y = z.

Security review 146

Page 160 of 324
Page 161 of 324

Ballot definition format. The reviewers recommended:

• offering ballot definition analysis tools to help reviewers

check ballot definitions; (e.g., to ensure that all the pages

can be reached from the starting page, to ensure that option

areas don’t overlap each other, and so on);

• defining an alternate textual representation of the ballot

definition that is easier for humans to examine and edit,

and providing tools to translate between the text form and

the binary form;

• developing a translator that turns a ballot definition into a

set of HTML pages or a Flash animation so that voters can

preview the voting experience in a Web browser.

• renaming the int type to nat to make it clearer that no

negative numbers are allowed, only natural numbers;

• placing digital signatures on ballot definitions and having

Pvote check the signatures; and

• including the 8-byte file header in the input for computing

the hash that appears at the end of the file.

Implementation. The reviewers recommended several changes

to the Pvote code to improve its clarity and reviewability. Their

suggestions and comments are described in the presentation of

the code in Appendix B, as well as in Appendix E.

Security review 147

Page 161 of 324
Page 162 of 324

Did the reviewers find the inserted bugs?

David Wagner and I decided to insert three bugs into Pvote to

see if the reviewers would find them. We inserted what we

thought would be an “easy” bug, a “medium” bug, and a “hard

bug” to find, and chose each bug individually in such a way that

an insider could conceivably exploit the bug to influence the

results of an election. These bugs are detailed in Appendix E.

We decided to insert all of these bugs in a 100-line region of

a single file, lines 11 to 109 of Navigator.py, and told the

reviewers to look in this region. We did this both because the

navigator was the most interesting in terms of the program

logic and because we knew the reviewers would have limited

time. The new version of the code that we gave the reviewers

contained all three bugs, but we did not tell the reviewers how

many bugs there were.

Yoshi Kohno, Mark Miller, and Dan Sandler participated as

reviewers on the third day of the review. Dan was very familiar

with Python and found the “easy” and “medium” bugs quickly,

within about 70 minutes. Yoshi Kohno and Mark Miller found

the “easy” bug after about four hours of reviewing. None of the

reviewers found the “hard” bug.

Ian Goldberg and Yoshi Kohno participated as reviewers on

the fourth day of the review. Ian Goldberg also found the “easy”

bug within about two hours; none of the other bugs were found

on the fourth day.

The reviewers spent a total of about 20 reviewer-hours

focused on the task of finding the bugs in this 100-line section

of Navigator.py.

Security review 148

Page 162 of 324
Page 163 of 324

What ideas did reviewers have on

programming languages?

The effect of programming language design on adversarial code

review was a prominent topic of discussion. These are some of

the main issues we discussed.

Mistyped or confusing identifiers. There are a few common

ways that variable names and other identifiers can lead to

problems in a software review:

• In Python, misspelled identifiers can lead to errors while the

program is running.

• Identifiers that are too similar can confuse reviewers

(intentionally or unintentionally).

• The same name can be used to refer to different things in

different scopes.

We discussed several possible language restrictions that would

help avoid these problems, such as requiring variable

declarations, forbidding the shadowing of variables, forbidding

the use of a field and a variable with the same name (e.g.,

self.foo and foo) in the same context, or forbidding variables

with names that are too similar.

Language subsetting. Another way to reduce the burden on

reviewers would be to let programmers choose restricted

subsets of the language in which to write sections of the

program. For example, suppose the programmer could declare

that a particular function is written in a side-effect-free subset

of the language, and a static verification tool could check that

only allowed syntax is used. This restriction would make it

easier for reviewers to audit the function and understand other

functions that call it.

E [89] and Joe-E [45] are especially interesting examples of

modern languages that support language subsetting, since they

offer an extensible auditing feature that lets programmers

define their own subsets of the language.

Security review 149

Page 163 of 324
Page 164 of 324

Static types. Types can be a powerful mechanism for statically

checking program correctness. I chose to write Pvote in Python,

a language without static type-checking, because of Python’s

agility and conciseness. On the other hand, static verification

could have reduced some of the burden on reviewers at the cost

of a longer and harder-to-read program.

Mutability. If the programming language supported a way of

making variables immutable, this would be one fewer thing for

reviewers to worry about (for example, the ballot definition

could become immutable after it has been loaded and verified).

Security review 150

Page 164 of 324
Page 165 of 324

What ideas did reviewers have on conducting

reviews?

Looking at source code. One reviewer remarked that he was

much more effective at comprehending someone else’s code

when all the code was spread out on the wall in front of him, on

paper. He found this surprising because he had spent the last

20 years editing code on computer screens.

This suggested to me that there might be significant value to

keeping the code size below a threshold at which it is physically

possible to lay out all of the code in front of a single person.

Trust in the adversary. The reviewers mentioned that it was

difficult to maintain the requisite level of distrust in me as the

author of the code, especially when we were interacting directly.

On a few occasions, the reviewers found they were inclined to

make unjustified assumptions about the good intent or

competence of the author, and they later suggested that

preventing social interaction between the reviewers and the

author might make such reviews more effective.

Reviewer fatigue. The reviewers generally felt that the point

where a reviewer becomes tired of inspecting a piece of code

comes long before the code has been subjected to enough

scrutiny. This suggests that it might be more effective for code

to be reviewed by many reviewers each for a limited length of

time, rather than a single reviewer for an extended length of

time.

One-line change test. Mark Miller proposed a test for

determining the size of the TCB (trusted computing base) for a

particular security requirement—that is, the amount of code on

which that requirement relies. His test consists of a series of

trials with someone playing the role of the attacker. For each

trial, one line of the program is chosen at random and the

attacker is allowed to change just that line to do as much

Security review 151

Page 165 of 324
Page 166 of 324

damage as possible. The fraction of trials in which the attacker

succeeds in violating the security requirement yields an

estimate of the fraction of the program that constitutes the TCB

for that requirement. Looking at the degree of vulnerability in

these terms allowed us to talk about the potential value of a

particular design change to Pvote or Pthin.

The read-write review. Dan Sandler proposed a new type of

software review he called the “read-write review,” in which

reviewers are asked to insert their own bugs. He conjectured

that this process would:

• Motivate reviewers to find “hot spots” in the code that were

especially vulnerable to small changes, thereby leading

them to scrutinize places where malicious bugs were likely

to have been inserted.

• Force reviewers to modify and run the program with the

intention of producing a specific change in behaviour, thus

requiring them to develop a deeper understanding of how

the program works than they would get from merely

reading the code.

• Yield a program with known bugs that could then be passed

on to another group of reviewers to inspect. The existence

of the known bugs would motivate the next group, and the

fraction of those bugs they found could offer some measure

of their effectiveness.

On the fourth day of the review, I asked the reviewers to try

inserting their own bugs. Their experience led them to comment

that being required to insert bugs might actually reduce a

reviewer’s chances of finding bugs, because it would encourage

reviewers to stick to the parts of code they already understand

well, instead of diving deep into unfamiliar parts of the code.

Security review 152

Page 166 of 324
Page 167 of 324

What lessons were learned from the review?

Conducting software reviews.

• Intentionally inserting bugs motivates reviewers. The

bug-insertion experiment created a dramatic difference in

the review process. The reviewers became much more

focused and motivated once they knew there was at least

one bug to find, and the exercise became a lot more fun.

• Set goals. Ask the reviewers specific questions, if you want

answers. Initially I assumed that the main outcome of the

review would be an evaluation of the security and

correctness of Pvote, and that the reviewers would arrive at

some level of confidence that would raise or lower my level

of confidence in Pvote’s design and implementation.

However, the review produced much broader discussion at

many different levels: how to design programs to facilitate

review, how to choose programming languages (or restricted

subsets thereof) to facilitate review, and how to conduct

reviews to maximize bug-finding effectiveness.

• Static analysis, testing, and code review can make a good

combination. Each of these techniques alone has

weaknesses: static analysis cannot enforce high-level

requirements; testing cannot cover all possible inputs; and

code review is tedious and error-prone. But in combination,

they complement each other. Static analysis can reduce the

tedium of code review by giving reviewers powerful starting

assumptions. And testing—even cursory walkthroughs of

the software—can quickly rule out flaws that break

commonly used functionality. A bug that can get past both

static analysis and live testing is a bug that causes trouble

only in certain specific situations. It is likely to be nontrivial

to write a bug that only causes misbehavior in specific

situations, has a significant and intended effect on the

outcome, and yet doesn’t appear obviously unusual to a

code reviewer.

Security review 153

Page 167 of 324
Page 168 of 324

Writing software to be reviewed.

• Sometimes it is better to spell things out, even if it means

more code. Minimizing the number of lines of code was a

high priority for me when I wrote the Pvote code. Although

less code often means less work for reviewers, we

discovered a few examples of the opposite. Minimizing

complexity is not always the same as minimizing code.

• The choice of language or language subset is important. The

language in which you write code heavily determines the

amount of work that reviewers must do. The language

design dictates the assumptions that reviewers are allowed

to make. The choice of language also affects whether

reviewers have tools to help them examine and analyze code

more effectively.

Programming language design.

• Supporting adversarial review is a new goal for

programming languages. Adversarial code review has

demands that go beyond those of a typical code review.

When the authors of the code are potentially malicious, they

have a considerable home-turf advantage, as evidenced by

the ability of an inserted bug to evade 20 reviewer-hours

focused on just 100 lines of code.

• Help programmers restrict parts of a program to subsets of

the language. Sometimes more language power is needed,

sometimes less; sometimes different kinds of language

features are needed for different purposes. Allowing the

programmer to choose which subset of the language to use

for each purpose can dramatically reduce the range of

possible vulnerabilities that a reviewer has to consider.

• Support for local reasoning is essential to adversarial review.

When reviewers are trying to verify a particular

application-level property, they need ways to quickly rule

out most of the program from being relevant to the

assurance of that property. Any language feature that helps

them perform local reasoning, or that lets the programmer

create parts of the program where local reasoning is valid,

Security review 154

Page 168 of 324
Page 169 of 324

will make reviewing easier. Capability-style design is a

promising approach, since it leverages lexical scope to

support local reasoning [47].

Voting systems.

• Pvote probably has fewer accidental bugs than most voting

systems. With 20 reviewer-hours focused on 100 lines (12

reviewer-minutes per line) and 90 reviewer-hours in total on

the entire program, Pvote may be one of the most closely

inspected pieces of voting software in existence, in terms of

effort per line of code. (It would take ten person-years to

review 100 000 lines of code with this much effort per line.

Consider that most commercial voting systems contain

hundreds of thousands of lines of code— in some cases over

a million. Moreover, the complexity of code review probably

increases more than linearly in the size of the code.) Since

no bugs were found in the Pvote code, we can have some

confidence that it meets a higher standard of code quality

than the typical commercial voting system.

• Detecting malicious code in a code review is extremely

difficult. Pvote was designed specifically to be minimal and

written with code reviewing in mind. The reviewers had

access to detailed documentation, as well as an environment

that allowed them to modify and execute the program.

Despite these things, and the high effort expended per line,

an inserted bug went undetected. Though many of us

expected that finding bugs would be difficult, we were still

surprised by how hard it was.

• Commercial voting systems are reviewed nowhere near

enough to detect insider attacks. Since the Pvote source code

was probably reviewed more intensely than the source code

of commercial voting systems has been reviewed, and since

even this was insufficient to find a maliciously inserted bug,

we can conclude that commercial voting systems almost

certainly have not been subjected to the degree of review

that would be necessary to declare it free of maliciously

inserted bugs.

Security review 155

Page 169 of 324
Page 170 of 324

9 Complexity

Does prerendering actually eliminate complexity? 157

What is achieved by shifting complexity? 158

Why do software reviews assume trust in compilers? 160

How far back can the derivation of a program be traced? 161

What affects the tolerance of complexity in a component? 164

How does Pvote reallocate complexity? 167

What is gained by using interpreted languages? 173

156

Page 170 of 324
Page 171 of 324

Does prerendering actually eliminate

complexity?

A theme running throughout this work is the management of

complexity. The major unaddressed software threat is the

insider threat from programmers; our only defense against it is

assurance of software correctness. Complexity is the chief

enemy of assurance, but it cannot be completely avoided.

Prerendering the user interface is fundamentally a strategy for

mobilizing complexity. The designer of the ballot definition

language gains the freedom to move complexity that normally

resides in the voting machine among three components:

• the tool that generates the ballot definition file,

• the ballot definition file, and

• the VM in the voting machine.

The allocation of complexity among these parts depends on

design choices in the ballot definition language. For instance, in

Pvote, the task of laying out buttons on the screen is no longer

the job of the voting machine; it is in the ballot generation tool.

The logic that decides when to play which audio message is no

longer part of the voting machine; it is in the ballot definition.

Thus, prerendering does not, in itself, eliminate complexity;

rather, it enables a designer to reallocate complexity. It is

worthwhile to ask what this reallocation accomplishes. Does

shifting complexity in this way make a real difference, or is it

merely a shell game—a way of hiding complexity in

components that I’ve conveniently chosen to ignore?

Complexity 157

Page 171 of 324
Page 172 of 324

What is achieved by shifting complexity?

I argue that the reallocation of complexity does make a real

difference. It matters where complexity resides because

components differ in the way they are vulnerable, in the degree

to which they are vulnerable, and in the people to whom they

are vulnerable. Also, changing the allocation of complexity in a

system has a significant effect because of the dependency

relationships among the components.

To explain what I mean, I’ll focus on just one of these

relationships for a moment. The relationship I’m about to

describe happens to be particularly important to the security of

all software, not just voting machine software. When a software

program runs, the instructions that the computer carries out

are in an executable file. A compiler translates the source code

into the executable file. The following figure depicts this

relationship. The executable file is drawn as a larger box than

the source code because it is usually larger and more complex.

Typical compilers are enormously complex, so the compiler is

the largest of all.

source code compiler executable file

Figure 9.1. A compiler turns source code into an executable file. The sizes of the boxes

(very roughly) indicate relative complexity.

When software undergoes a security review, the reviewers

usually ask to look at the source code of the software, not the

actual executable files. Source code is certainly easier to review

than executable code. That’s why programming languages were

invented—so that humans would have something easier to deal

with than low-level machine instructions. But convenience is

not a reason for confidence.

Complexity 158

Page 172 of 324
Page 173 of 324

If a thorough review of the executable file discovers no

bugs, it directly offers (at least some) confidence that the

executable file is correct. But if a thorough review of the source

code discovers no bugs, it does not assure the correctness of

the executable file unless the compiler is also correct.

Generative relationships like this exist throughout software

systems. Whenever there is such a relationship, with an input, a

transform, and an output, reviewers have a choice: they can

inspect the output, or they can inspect the input and the

transform instead. But it is necessary to establish that both the

input and the transform are correct in order to establish that

the output is correct.

In this example, the burden of establishing confidence in

the executable is traded for the burden of establishing

confidence in both the source code and the compiler. But a

compiler is a massive piece of software—so why is this trade

considered a good idea? In particular, why do software reviews

typically skip inspection of the compiler? The next section

looks at this question.

Complexity 159

Page 173 of 324
Page 174 of 324

Why do software reviews assume trust in

compilers?

Maybe they shouldn’t. Not all computer scientists would agree

that it is safe to assume a trustworthy compiler. In a famous

essay on trust [76], Ken Thompson argued that compilers

cannot be trusted, and gave a compelling demonstration of how

to construct a deviously misbehaving compiler that would

compile programs (including itself) incorrectly.

Despite Thompson’s essay, much of current computer

security practice (and even research) implicitly makes this

assumption. One conceivable justification for this is that the

compiler has a general purpose— it is designed to compile all

sorts of programs—whereas the source code is written for a

specific application. Perhaps those who trust compilers believe

that the compiler is likely to be more mature and more

thoroughly tested than a newly written program. Or perhaps

they believe that, since the compiler is used to compile many

different kinds of programs, someone would notice if it made

compilation mistakes. Or perhaps—more depressingly—they

simply think there is no hope of ever verifying compilers.

My purpose here is not to argue that corrupting a compiler

in such a way would be impossible; clearly, as Thompson

showed, it can be done. I aim only to offer some basis for the

plausibility of the commonly held idea that corruption of a

software program through subversion of the compiler is more

difficult than directly corrupting the software’s source code.

In choosing to review source code, reviewers trade an

application-specific component with high complexity (the

executable) for a component that is highly complex but

general-purpose (the compiler), and a component that is

application-specific but less complex (the source code).

Complexity 160

Page 174 of 324
Page 175 of 324

How far back can the derivation of a program

be traced?

What happens if you keep tracing where each component came

from? The compiler is itself a piece of software; in Figure 9.1 it

is shown as a mysterious box. What is that box, exactly? Is it the

source code of the compiler or the executable file?

Actually, it is neither. The thing that actually performs the

transformation of source code into an executable file is a

running instance of the compiler. The transformation depicted

by the “compiler” box is a process, not a static entity. So the

following figure is a bit more accurate.

running

compiler

process

source code executable file

Figure 9.2. The middle box represents a compilation process, not a static piece of data.

The behaviour of that process is indeed derived from the

executable file of the compiler program, but that is not all.

Something has to turn that executable file (which is a static

piece of data) into a running process; let us call this thing the

operating platform on which it runs. The operating platform

consists of all the software and hardware that makes it possible

to run computer programs. It includes the operating system,

software libraries, CPU, memory, storage, and so on—which

makes it quite a bit bigger and more complex than the compiler.

running

compiler

process

operating

platform

compiler

executable Figure 9.3. An operating platform turns an executable file into a process.

Complexity 161

Page 175 of 324
Page 176 of 324

The compiler executable was also derived from source

code—the source code of the compiler—by an earlier

compilation process. This earlier compilation may have been

carried out by the same compiler or a different compiler.

Putting all these relationships together gives us a fuller picture

of how the executable program was derived.

compiler

source code

source code

running

compiler

process

executable file

operating

platform

compiler

executable

running

compiler

process

Figure 9.4. A small derivation map for a compiled program.

This diagram could continue indefinitely. The compiler

process at the top of the diagram was itself produced by

running a compiler executable on an operating platform, and

that executable was the output of a compiler, and so on in a

long chain of compilation steps running back through history.

Ultimately the chain ends at an executable program that was

created without the help of a compiler.

Malicious code that was introduced at any point in this

chain could affect the final executable file. The program could

be vulnerable to an insider attack that occurred many, many

steps earlier—this is the point Thompson made in his essay.

Complexity 162

Page 176 of 324
Page 177 of 324

There’s still more to the picture—what about the operating

platform? That, too, is constructed through a long chain of

dependencies. It consists of operating system software

compiled by a compiler, running on hardware produced by

manufacturing processes that are also controlled by software.

I call these diagrams derivation maps because they show

how a security-critical artifact is derived from other

components. Each arrow represents a step in a hierarchical

decomposition of the system. The purpose of this kind of

analysis is to identify sources of vulnerability to insider attacks.

Derivation maps can help you make an effective assurance

argument or analyze an assurance argument to tell whether it is

complete.

As a reviewer of the system, your challenge would be to cut

away these sources of vulnerability. Each arrow in the diagram

corresponds to a choice you could make: between reviewing the

component at the head of the arrow and reviewing the two

components at the tail and shaft of the arrow. Reviewing,

testing, or otherwise establishing confidence in a particular

component lets you ignore the arrowhead leading to it, and cut

away the part of the diagram behind that arrowhead.

You may have noticed that some of the boxes in these

diagrams have sharp corners and some have rounded corners.

The reason for this is to indicate the distinction I mentioned

earlier: general-purpose components have rounded corners,

whereas application-specific components have sharp corners.

This distinction is but one of many possible factors that could

affect the degree to which one is willing to tolerate software

complexity in a given component.

Complexity 163

Page 177 of 324
Page 178 of 324

What affects the tolerance of complexity in a

component?

Here are some of the ways in which you might evaluate a

component with respect to the detectability of insider

corruption. Classifying components according to these factors

could help you identify ways that a shift in complexity can

increase confidence.

• User choice. Are relying parties forced to use a particular

implementation of the component, or do they have the

freedom to choose their own? Shifting complexity from a

dictated component to a freely chosen component reduces

barriers to confidence. For example, anyone can choose or

write their own tools to deconstruct and analyze ballot

definition files. In contrast, voters cannot choose to vote on

any equipment they want; they must use the equipment

provided by election administrators.

• Disclosure. Is the component hidden or disclosed? The

wider the audience to whom the component is disclosed, the

harder it is for malicious code to go unnoticed. Components

that are undisclosed, or inherently undisclosable (such as

live running processes) are riskier because their correctness

cannot be externally verified. Shifting complexity to a

disclosed component reduces barriers to confidence.

• Number of developers. How many people have access to the

component during development? If the component is

authored by multiple people, corrupting it may require a

conspiracy rather than just an individual attacker. Shifting

complexity to a component with a larger development team

might reduce barriers to confidence.

• Specificity of purpose. Shifting complexity from

application-specific components to general-purpose

components sometimes reduces barriers to confidence.

Undetected bugs and backdoors may be less likely if the

component is widely used and used in a variety of

environments for a variety of purposes.

Complexity 164

Page 178 of 324
Page 179 of 324

• Testing. Shifting complexity to components that have been

thoroughly tested can reduce barriers to confidence, if the

testing parallels the intended use.

• Maturity. How mature is the component? A component that

has been stable, used, and developed for a long time has

had more time to have its problems found and fixed.

Shifting complexity to a more mature component could

reduce barriers to confidence.

• Release date. When was the component released, relative to

other components? Suppose, for example, that every time a

particular compiler development team releases a new

version of their compiler, the released version is reliably

and indelibly archived. And suppose it can be verified that

the compiler used to compile a particular program exactly

matches the one released and archived on a particular date

in the past. If the compiler was released before the program

was even conceived, it is harder to imagine how an insider

could have subverted the compiler to meaningfully

influence the outcome of the program.

• Reviewing resources. There may be more reviewers or better

reviewers available for certain types of components. For

example, it might be easier to gain confidence in a

component written in a more popular programming

language because there is a larger community of people

available who can understand and inspect the code.

Any of these factors could constitute a reason that shifting

complexity from one component to another helps achieve better

confidence.

While individual factors may not be enough to justify

confidence, they can have stronger effects when combined. For

example, even if a component has been tested thoroughly, there

is still the possibility that it was written specifically to evade

testing. But such evasion is likely to require some suspicious- looking code, which is less likely to escape notice if the code

also happens to be disclosed to the public.

Complexity 165

Page 179 of 324
Page 180 of 324

For a concrete example, consider Pvote. Suppose that Pvote

will be run on a voting machine using version 2.3.5 of the

Python interpreter, which was released in February 2005, before

I started my research work on electronic voting. Python 2.3.5 is

a mature open-source implementation of the language: it passes

an extensive suite of functional tests, it has been widely used all

over the world, and hundreds of programmers have contributed

to its development.

Pvote’s source code is also open to the public. If it were to

be used for a real election, chances are good that it would be

downloaded and examined by many people. Python is a

well-known programming language with a large community of

users who would be able to understand the Pvote code.

Given this context, how trustworthy is the Python

interpreter? There are two ways that misbehaviour of the

Python interpreter could be used in an insider attack:

• The Pvote program could be crafted to take advantage of a

latent bug in the interpreter. The interpreter bug would

have to be one that is not commonly triggered, since it

would have survived years of open-source development and

testing, as well as use with all kinds of Python programs. Yet

at the same time, the Pvote code that triggers this unusual

bug would also have to avoid looking out of the ordinary to

the many Python programmers who inspect Pvote.

• The interpreter could be crafted to misbehave when running

Pvote. To avoid detection in other contexts, the interpreter

bug would have to be specific to the Pvote code in some

way. But someone would have had to plant this bug in the

interpreter before Pvote was designed and developed. The

more specific the bug is to Pvote, the harder it is to see how

the attacker could have predicted Pvote’s implementation.

When it comes to software bugs, nothing is 100% certain. But

when many positive factors come together in a context like this,

they can constitute a basis for trust.

Complexity 166

Page 180 of 324
Page 181 of 324

How does Pvote reallocate complexity?

Figure 9.5 shows a derivation map for Pvote together with a

derivation map of a conventional electronic voting machine for

comparison. The ultimate product in each case is the user

experience of the voter using the voting machine, which is

determined by the voting machine software’s interpretation of

the ballot definition file. Both derivation maps omit the

derivation of the compiler and operating platform.

Although the relative differences in size in the diagram are

meant to roughly express relative differences in complexity,

they are not to scale. For example, there is actually about 100

times as much source code in conventional voting machine

software than there is in Pvote. Pvote is 460 lines of Python,

whereas the Diebold AccuVote-TSx and the Sequoia Edge (two

widely used touchscreen machines) run software consisting of

66 000 and 124 000 lines of code respectively [12, 7]. The

complexity of a C compiler is many times larger still.

When you compare the two derivation maps, the two main

complexity shifts are evident:

• Ballot definition. In Pvote, the ballot definition is more

complex and the running instance of the voting VM is less

complex than its counterpart in a conventional system, the

running instance of the voting software. Also, the ballot

definition is publicly disclosed.

• Python interpreter. In Pvote, the voting software runs on a

Python interpreter rather than directly on the voting

machine’s operating platform. The source code to the voting

VM is much smaller than that of the voting software in a

conventional system; on the other hand, Pvote introduces

the Python interpreter, a large additional component.

Whereas the source code and executable for the voting

machine software in a conventional system are

application-specific and secret, the source code and

executable for the Python interpreter used by Pvote are

general-purpose and publicly disclosed.

Complexity 167

Page 181 of 324
Page 182 of 324

running instance

of Python interpreter

voting

machine

source code

voting machine

executable file

running

compiler

process

voting machine

operating platform

running instance

of voting software

ballot definition

generator

electronic voting

user experience

Python