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
interpreter
source code
Python interpreter
executable file
running
compiler
process
voting machine
operating platform
running instance
of voting software
ballot definition
generator
electronic voting
user experience
voting VM
source code
ballot
definition
pre- rendered
ballot
definition
LEGEND
live process,
general-purpose
live process,
voting-specific
undisclosed,
voting-specific
disclosed,
voting-specific
undisclosed,
general-purpose
disclosed,
general-purpose
inspectability
generality
Shape indicates generality. Shading indicates inspectability.
Arrows indicate transformation.
Size indicates relative complexity.
input transform output
Conventional approach
(compiled code + runtime-generated user interface)
Pvote approach
(interpreted code + prerendered user interface)
Figure 9.5. Derivation maps of a conventional voting system and of Pvote.
Complexity 168
Page 182 of 324
Page 183 of 324
The effect of these architectural changes is to reduce the
complexity of the critical, voting-specific componentsāthe
sharp-cornered boxes in the derivation map. Figure 9.5
highlights three factors about each component: complexity
(size), generality of purpose (round or sharp corners), and
disclosure (shading). In Pvote, the only voting-specific
components that have to be inspected to gain confidence in the
voting machine are the voting machineās operating platform, the
voting VM source code, and the prerendered ballot definition,
and all three are disclosed.
Both changes are similar in character: in each case, a
high-level interpreted language is introduced. Pvote replaces C
with Python, and then replaces some of the Python code with a
specialized ballot definition language. And in each case, the
design of the high-level language dictates the balance of
complexity between a pair of components in the diagram.
The following figure focuses on the relevant two pairs of
components.
running instance
of voting VM
electronic voting
user experience
ballot
definition ballot
definition
language
Python language
running instance
of Python interpreter
voting VM
source code
Figure 9.6. The two trade-offs introduced by Python and the ballot definition language.
The two boxes on the left trade off complexity according to
how high-level the Python language isāthat is, how much of
the behaviour of the voting machine is specified by the Python
interpreter as opposed to the source code it interprets. The
diagrams on the next page explore what it would be like to
move along the spectrum between using a low-level language
and using a high-level language.
Complexity 169
Page 183 of 324
Page 184 of 324
If the Python language were replaced with an extremely
low-level language, the diagram would look like this:
running instance
of voting VM
electronic voting
user experience
ballot
definition
voting VM
source code
running instance
of interpreter
Figure 9.7. Python is replaced with a very low-level interpreter.
In the ultimate extreme, the interpreter would disappear
and the input would no longer be source code; it would be an
executable file running directly on the operating platform.
If the Python language were replaced with a higher-level
language, the diagram would look like this:
running instance
of voting VM
electronic voting
user experience
ballot
definition
running instance
of interpreter
voting VM
source code
Figure 9.8. Python is replaced with a very high-level interpreter.
In the extreme, the input would disappear and the
interpreter would subsume all the duties of the voting machine
softwareā in effect, becoming the voting machine software.
The two extremes yield the same result: a specialized
executable file running on the operating platformāexactly the
situation of the conventional voting machine.
Complexity 170
Page 184 of 324
Page 185 of 324
The two boxes at the top right trade off complexity according to
the level of abstraction in the ballot definition language. With a
very low-level ballot definition language, the diagram would
look like this:
electronic voting
user experience
running instance
of Python interpreter
ballot
definition
running instance
of voting VM
voting VM
source code
Figure 9.9. A low-level ballot definition language means a larger ballot definition.
In the extreme case, the VM would shrink to nothing at all,
and the ballot definition would just be an executable file
running on the voting machine.
With a very high-level ballot definition language, you get the
following picture:
electronic voting
user experience
running instance
of Python interpreter
voting VM
source code
running instance
of voting VM
ballot
definition
Figure 9.10. A high-level ballot definition language means a smaller ballot definition.
This is pretty much what happens in a conventional voting
machine. Most of the voting user experience is defined by the
voting machine software; the ballot definition only contains
miminal information about the contests and candidates.
Complexity 171
Page 185 of 324
Page 186 of 324
The conventional voting machine approach is about as far
as itās possible to go in the direction of a high-level ballot
definition language. Thatās because there has to be a way to
configure the voting machine for the candidates and contests in
a particular election; if we went any further, a specialized
version of the voting machine software would have to be
released for each ballot style.
Compared to conventional voting machine software, Pvote
moves in the direction of a low-level ballot definition language.
Giving the ballot definition language more power is beneficial
because:
ā¢ it exposes more of the behaviour of the voting machine to
public review,
ā¢ it exposes more of the behaviour of the voting machine to
control by designers instead of programmers, and
ā¢ it allows the software in the voting machine to change less
often. (Recall that back in Chapter 6, I said that greater
generality in the ballot definition language helps to
future-proof the voting VM software.)
But why not go so far as to shift all the complexity to the ballot
definition, and eliminate the voting VM entirely? How do you
choose the best balance between a high-level or low-level ballot
definition, or between a high-level or low-level interpreted
language for the voting machine software? The next section
addresses these questions.
Complexity 172
Page 186 of 324
Page 187 of 324
What is gained by using interpreted languages?
The purpose of programming language design is to offer
high-level abstractions with which to express desired behaviour.
The interpreter implements and enforces those abstractions.
For example, the Python interpreter gives a guarantee of
memory safety: in general, a Python program cannot arbitrarily
corrupt memory. (There are extension modules designed
specifically to allow arbitrary memory access, but the Pthin
language definition excludes the use of such modules.) This
both simplifies code written in Python and allows a reviewer of
such code to make useful assumptions about its behaviour.
As another example, the ballot definition language contains
no concept of the current time and date, and in general, no way
to express behaviour that will be different at testing time than
on election day itself. This property is essential to the
effectiveness of ālogic and accuracy testing,ā in which behaviour
observed in live pre-election testing is assumed to reflect the
machineās actual behaviour on election day. This restriction
significantly reduces the amount of code that has to be reviewed
to establish that the entire system has deterministic behaviour.
This is the answer to the question of balancing complexity
between an interpreter and the code it interprets. Shifting
complexity into a high-level programming language is useful
only insofar as the target language provides security-relevant
restrictions on what can be expressed. As long as a solid
assurance argument can be made for the interpreter, itās a good
idea to make the interpreter responsible for abstractions that
enforce useful correctness properties. In Pythonās case, the
argument is that Python is a general-purpose language; in the
ballot definition languageās case, the argument is that the voting
VM is small. My experience with Pvote suggests that restricted
domain-specific languages and languages that support
programming in restricted subsets are powerful tools for
verifiable secure system design.
Complexity 173
Page 187 of 324
Page 188 of 324
10 Related work
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
174
Page 188 of 324
Page 189 of 324
Do any other voting systems use
prerendering?
Yes, there is some precedent for using prerendered images in
electronic voting machines.
The Open Voting Consortiumās EVM2003 project [59, 58]
used a full-screen bitmap image for displaying an electronic
ballot.1 This use of a prerendered image was also motivated by
a desire for software simplicity.
The ES&S iVotronic supports the use of ābitmap ballotsā for
displaying ballots in foreign languages [36].2 These ballots
contain graphical images for the candidateās names and other
text, so that text in arbitrary languages can be shown.
To the best of my knowledge, Pvote is the first voting
system that uses a prepared description of the entire user
interface, including full-screen images, prerecorded audio, and a
specification of behaviour. This extension of the concept of
prerendering is significant for all the reasons identified in
Chapter 4: it further simplifies the software in the voting
computer, enables more thorough public review, creates a more
complete public record, gives designers control over ballot
design, and reduces the need to change the voting computer
software.
1According to David Mertz of the OVC, this idea was originally proposed for use in EVM2003 by Fred McLain.
2My thanks are due to Dan Wallach for mentioning this precedent to me.
Related work 175
Page 189 of 324
Page 190 of 324
What other voting proposals reduce reliance
on software?
Many voting researchers have recognized the difficulty of
testing and verifying software, and sought to reduce the
vulnerability of elections to software bugs or maliciously
crafted software. The prerendering approach is motivated by
the desire to reduce the size and complexity of the trusted base
on which the security of the voting system rests. In the
following sections, Iāll discuss other major proposals that share
the same motivation:
ā¢ The āfrogā voting scheme
ā¢ āSoftware independenceā (and a common implementation of
SI, the voter-verified paper audit trail)
ā¢ End-to-end verification schemes
Related work 176
Page 190 of 324
Page 191 of 324
What are āfrogā voting systems?
In 2001, researchers from CalTech and MIT proposed a voting
procedure based on āfrogsā [10]. They coined the term āfrogā to
mean a small and cheap device, such as a memory card, that
permanently stores a single voterās votesāthe electronic
equivalent of an individual marked paper ballot.
The frog proposal separates the voting process into two
steps, vote selection and vote casting, each carried out with a
separate machine. The voter first selects their votes on the
vote-selection machine, which stores them on a frog. The voter
then puts the frog into the vote-casting machine, which displays
the contents of the frog for the voter to check, and upon
confirmation by the voter, casts the votes. The frog is kept as a
permanent record in case a recount is needed later.
The idea behind this proposal is to separate the more
complicated operation of selecting votes from the
security-sensitive operation of casting the votes. According to
the proposers, the trusted base of software is reduced because
responsibility for security now rests only on the simpler
vote-casting machine; the vote-selection machine will have āno
need for high securityā [10].
Related work 177
Page 191 of 324
Page 192 of 324
Do frogs solve the electronic voting problem?
Not entirely. The central claim of the frog schemeāthat it
excludes the vote-selection software from the trusted baseā
relies on two significant assumptions:
ā¢ that voters will check their frogs carefully before casting
them, and
ā¢ that voters will know what to expect when the contents of
the frog are displayed.
Some voters may give the vote-casting machine only a cursory
glance, and most are likely to be influenced by confirmation
bias [55]. Thus, it is possibleāperhaps even likelyāthat votes
recorded incorrectly by the vote-selection machine could go
unnoticed. The susceptibility of an election to incorrect
recording by the vote-selection machine also depends on how
election administrators respond when voters report problems,
and how many complaints are needed to trigger such response.
Even if voters do check the votes on their frogs carefully,
the vote-selection machine remains in a position to influence
voters during the selection processāthus violating the
principle that an election should be an unbiased measurement.
For example, the vote-selection machine could present the
candidates in a biased way. It could change the wording of a
ballot measure to make an option seem more appealing or even
invert the sense of the question, swapping the implications of
āyesā and ānoā. It could even give misleading instructions to
voters, such as telling them to ignore the vote-casting machine
or to go to a different polling place to vote on certain contests.
The prerendered approach therefore targets a broader
security goal: to secure the entire voting user interface
including the vote selection process, in order to avoid bias in
the electionās measurement of the will of the electorate.
Prerendering the user interface does not rule out the possibility
of further partitioning the user interface into two steps as
proposed in the frog voting architecture.
Related work 178
Page 192 of 324
Page 193 of 324
What is āsoftware independenceā (SI)?
āSoftware independenceā is a prominent concept in the next
version of U. S. federal standards for voting systems, the ā2007
VVSG.ā A draft of the 2007 VVSG [81] has been unanimously
adopted by the standards committee, but remains open for
public comment before adoption. Section 2.4 of that draft
introduces the term like this:
Software independence means that an undetected error or
fault in the voting systemās software is not capable of causing
an undetectable change in election results.
The draft declares that āAll voting systems must be software
independent to conform to the VVSG.ā The draft goes on to
explain the concept like this:
There are essentially two issues behind the concept of
software independence, one being that it must be possible to
audit voting systems to verify that ballots are being recorded
correctly, and the second being that testing software is so
difficult that audits of voting system correctness cannot rely
on the software itself being correct.
According to the draft:
ā¢ Hand-counted paper ballots and optically scanned paper
ballots are software independent, since they leave a paper
record that can later be recounted by hand to check that the
original counts are correct.
ā¢ DRE machines with a VVPAT feature are also software
independent, since the VVPAT records are on paper and can
also be recounted by hand.
ā¢ DRE machines without paper trails are not software
independent (even though some DREs offer a ārecountā
function, this is carried out by just another software
program and so fails to be software independent).
Related work 179
Page 193 of 324
Page 194 of 324
The name and concept of āsoftware independenceā were
introduced in a white paper by Rivest and Wack [66] written for
the committee that was working on the VVSG. In addition to
giving a definition of āsoftware independenceā (essentially the
same as the one quoted above), this paper identified a
distinction between āstrong software-independenceā and āweak
software-independence.ā A strongly software-independent
voting system is one for which changes in outcome due to
software errors are not only detectable but also correctable
without re-running the election. A weakly software-independent
voting system is one that has the detection property (i.e.,
satisfies the above definition of āsoftware independenceā)
without a recovery mechanism. Essentially, āstrong software
independenceā is āsoftware independenceā plus a recovery
mechanism.
Related work 180
Page 194 of 324
Page 195 of 324
Does SI make software reliability irrelevant?
No. Requiring all voting systems to provide a software- independent audit capability is certainly an important
improvement, but this alone is far from what would be
necessary to achieve confidence in a voting system.
To explain why, I need to go into a bit of detail about how
the term āsoftware independenceā is used in the VVSG draft.
The VVSG draft defines the term with one meaning and then
uses it with a second meaningāand unfortunately, neither of
these two meanings actually constitute independence from
software. There are three main problems with the VVSG
definition and the use of the name āsoftware independenceā for
the concept:
1. The VVSG definition does not describe systems that are
actually independent of software, just systems that are less
than totally dependent on software.
2. The meaning of the VVSG definition depends on detection
procedures that are unspecified.
3. The use of the term in the VVSG focuses on auditing the
counting of recorded votes, but elections can be influenced
in many ways other than miscounting or altering recorded
votes.
Less-than-total dependence is not independence. The initial
definition of āsoftware independenceā given in Section 2.4 of
the VVSG draft requires that software faults be ānot capable of
causing an undetectable changeā in the election outcome. If the
software can cause an undetectable change, then the election is
100% reliant upon the software to be correct. But as long as any
software-caused change is detectable in principle, no matter how
vanishingly small the probability of detection, the voting system
will meet the definition. Even a voting system that has only a
0.1% chance of error detection (and is thus, in a sense, 99.9%
dependent on software) would meet the VVSG definition of
āsoftware independent.ā
Related work 181
Page 195 of 324
Page 196 of 324
The detection procedures are unspecified. By using the word
āundetectable,ā the VVSG definition presumes the existence of
some procedures by which errors could be detected. However, it
does not specify whether those procedures need to be realistic
or practical.
For example, the VVSG draft says that DRE machines
without paper trails fail to be āsoftware independent.ā Consider
for the sake of argument a DRE machine with no VVPAT that
stores vote records on a cassette tape (as old microcomputers
like the TRS-80 and Apple II used to do). In principle one could
stop the machine and examine the electronic records after each
ballot is cast, thereby detecting incorrectly recorded votes; this
examination would require some electronic equipment but
could be performed without software. Does such a DRE machine
therefore meet the definition, despite lacking a paper trail?
As another example, consider a DRE machine that produces
a paper audit trail with the vote information printed as a
barcode. Is it āsoftware independentā? If recounts of the paper
audit trail are performed using a barcode scanner, then the
recount would depend on the software that processes the
barcodes. Yet, in principle, a human being with enough patience
could examine the stripes in the barcode, decode them by hand,
and thus conduct a software-independent audit. Whether this
machine meets the definition of āsoftware independenceā
depends on assumptions about what one uses to perform the
detection.
Further, what constitutes successful detection? In some
analyses of the probability of software fault detection, detection
by a single voter constitutes detection. But a complaint from a
single voter is unlikely to stop an election, cause machines to be
taken out of service, or launch an investigation. This is for good
reason: if election administrators made it their policy to take
any machine out of service based on a complaint from a single
voter, just a few dishonest voters could effectively shut down
polling stations and cause havoc on election day. Thus election
officials must choose some threshold of voter complaints they
deem necessary to trigger remedial action.
Related work 182
Page 196 of 324
Page 197 of 324
How should the proper threshold be determined? If the
threshold is too low, the election will be vulnerable to
fraudulent complaints. If the threshold is too high, the election
will be vulnerable to undetected faults. It may even be the case
that there is no acceptable threshold of voter complaints
because these two ranges of unacceptable thresholds overlap.
The likelihood of recovery from a software fault is intimately
dependent on the policies for response and escalation when
problems are reported.
It should be clear from the preceding analysis that software
independence is necessarily a property of an entire election
administration system, including policies and procedures as
well as technology. I propose the following definition:
True software independence (TSI) means there is a
negligible probability that an error or fault in the voting
systemās software will change the outcome of the election.
For clarity, I will use āVSIā to refer to the VVSG definition:
VVSG software independence (VSI) means an undetected
error or fault in the voting systemās software cannot cause
an undetectable change in the outcome of the election.
Although the definitions are similar, the difference between āa
negligible probability of changeā and āno undetectable changeā
is significant. The first describes something that can be
estimated and measured; the second does not, and depends on
unstated assumptions about what is detectable, what detection
procedures are performed, and what constitutes successful
detection.
āStrong software independenceā (SSI) as defined by Rivest
and Wack [66] and TSI are both stronger versions of the VSI
concept, but they strengthen the concept in different ways. SSI
adds recovery to VSI, but a voting system can still meet SSI even
if the probability of detection and recovery is minimal. TSI
requires that the probability of detection and recovery be high.
Related work 183
Page 197 of 324
Page 198 of 324
Altering recorded votes is not the only way to influence an
election. Immediately after presenting the VSI definition, the
VVSG draft then explains the term āsoftware independenceā
with a different meaning: namely, the capability to audit the
counting of votes without relying on software. Here is the
relevant excerpt from the VVSG draft (emphasis added):
There are essentially two issues behind the concept of
software independence, one being that it must be possible to
audit voting systems to verify that ballots are being
recorded correctly, and the second being that testing
software is so difficult that audits of voting system
correctness cannot rely on the software itself being correct.
… [P]revious versions [of the VVSG] permitted voting systems
that are software dependent, that is, voting systems whose
audits must rely on the correctness of the software.
I will use the term āsoftware-independent audit capabilityā to
refer to this concept:
A voting system has software-independent audit capability
(SIAC) if it provides a procedure for verifying that votes were
recorded and counted correctly without relying on the
correctness of any software.
SIAC has a narrower meaning than VSI, because it is only
concerned with the counting of votes after they are recorded.
Faulty voting machines can influence elections in many other
waysāfor example, by presenting the candidates in a biased
fashion, omitting contests from the ballot, misleading the voter
with false instructions, printing incorrect paper audit trails, or
crashing and preventing voters from casting votes at all.
A DRE with a voter-verified paper audit trail (VVPAT) can
influence an election in all of these ways, and so it fails to be
TSI even though it has SIAC. All of these are ways that an
election would, in fact, depend on software, despite being called
āsoftware independentā according to the VVSG draft.
Related work 184
Page 198 of 324
Page 199 of 324
It can even be argued that a DRE with a VVPAT fails to meet
the VSI definition, depending on the interpretation of the word
āundetectable.ā Consider, for example, a DRE with a VVPAT,
which is programmed to occasionally skip a particular contest
on the first time through the ballot. The contest is only skipped
the first time through, and the contest is still printed on the
VVPAT as usual.
Imagine the typical voterās experience with this machine.
After going through all the pages of the ballot, the voter might
or might not read the VVPAT carefully. The VVPAT will show
that no selection was made for the skipped contest; the voter
has no way to tell whether the software maliciously skipped the
contest, the voter missed a page due to double-tapping on the
ānext pageā button by mistake, or the voter just forgot to fill in
that contest. In any case, if the voter goes back and fills in the
missing vote, everything behaves normally.
A malicious DRE such as this can exert significant influence
on an election. Yet it leaves no evidence that would show that
the software is at fault; that is, no amount of forensic analysis
after the election would be able to establish that a contest was
unfairly skipped. The emphasis on auditing in the VVSG draftās
use of the term āsoftware independenceā suggests that
recorded evidence is centrally important. If āundetectableā in
the VSI definition means ānot detectable by examination of
recorded evidence,ā then DREs with VVPATs fail to be VSI.
If DREs with VVPATs are VSI, it seems strange to define
āsoftware independentā such that machines with software in a
position to mislead voters qualify as āsoftware independent.ā
Why software reliability still matters. Even if a voting system
qualifies as SIAC or even VSI according to the definitions Iāve
identified here, there are still many ways that the election can
be vulnerable to software faultsāfor example, crashing more
frequently for voters of a particular political party. If software
presents the ballot to the voter, then software is in a position to
mislead or otherwise influence the voter. Therefore, software
reliability and correctness remain vital to election integrity.
Related work 185
Page 199 of 324
Page 200 of 324
What is end-to-end (E2E) verification?
As mentioned in Chapter 3, āend-to-end verificationā is the
name for a family of techniques that enable each individual
voter to verify that his or her votes were properly counted in
the final total. The main challenge of end-to-end verification is
to provide enough information for voters to perform this check,
yet not enough information for voters to sell their votes.
The general approach of E2E schemes is to publish a
complete but anonymous record of all the votes so that anyone
can check the count; where the schemes differ is in how they
assure voters that their individual votes are included in the
published record of votes.
ā¢ Some schemes publish a set of encrypted, identifiable vote
records in addition to the complete set of plaintext,
anonymous vote records. These include VoteHere [54],
Scratch & Vote [1], PrĆŖt-Ć -Voter [13], and Punchscan [26].
Voters receive an encrypted record of their votes to take
home, which they can check against a published encrypted
record. Some other mathematical procedure is used to
verify that the two sets of vote records correspond.
ā¢ Some schemes give each voter a record with only partial
information about his or her votes to take home. The
information is enough to check against the published
records but insufficient as sellable evidence of his or her
votes. ThreeBallot [68] and VAV [67] fall into this category.
ā¢ Twin [67] is an unusual end-to-end scheme. In Twin, each
voter receives a receipt for a randomly selected other voterās
ballot. Thus, while the posted records can be matched with
receipts, they canāt be identified as belonging to any
particular voter.
Related work 186
Page 200 of 324
Page 201 of 324
Does E2E verification make software reliability
irrelevant?
End-to-end verification schemes let voters ensure their votes are
counted without relying on software. Voters using an E2E voting
system have all the information they need to perform this check
themselvesāunlike voters using a voting system with a VVPAT,
who must rely on election administrators to conduct a hand
count of the VVPATs in order for the paper record to matter.
Thus, E2E schemes provide the potential for stronger voter
verifiability, as long as voters are willing to carry out a more
involved procedure to verify their votes.
However, E2E schemes do not address the problems of
ballot presentation and crashing software. Purely paper-based
E2E schemes avoid the use of computers for vote entry, but may
limit access for voters with some kinds of disabilities. On the
other hand, if the ballot is presented by a computer or votes are
entered on a computer, the problems of reliable ballot
presentation and vote entry remain; it is these issues that
prerendering addresses. Programs like Pvote can provide the
reliable vote-entry functionality needed for computer-based E2E
voting systems.
Related work 187
Page 201 of 324
Page 202 of 324
What are other approaches to high-assurance
software?
Automated proof. The desire to prove software programs to be
correct has existed pretty much since programmable computers
were invented. As early as 1961, John von Neumann sought to
mathematically prove the correctness of computer
programs [30]. Since that time, researchers have investigated a
variety of ways to automatically construct a proof that a
program meets a formal specification.
ā¢ Verification conditions. In 1969, James King developed an
automatic program verifier [42] based on associating
verification conditions with execution paths through the
program. Each verification condition is the proposition that
if an initial predicate (i.e., a precondition) holds at the
beginning of the execution path, then a final predicate (i.e.,
a postcondition) will hold when the end of the execution
path is reached. The correctness of the entire program is
established by proving that all these verification conditions
hold, and showing that their paths can be chained together
to cover all possible execution paths from where the
program starts to where the program halts.
A modern example of this approach is Java Modelling
Language (JML). Programmers can embed JML annotations in
comments in Java code to specify assertions such as
invariants, preconditions, and postconditions. A static
checking tool called ESC/Java [27] can then analyze the
program and verify the consistency of these assertions.
ā¢ Weakest precondition methods. The weakest precondition
approach works in the opposite direction. It begins with the
desired postcondition and works backwards through the
program to determine the weakest precondition that would
be necessary to imply the postcondition.
ā¢ Abstract interpretation. Abstract interpretation [16] (also
known as symbolic execution) consists of executing the
statements of a program using an abstract representation of
Related work 188
Page 202 of 324
Page 203 of 324
the programās state. That is, instead of giving concrete
values to variables, an abstract interpreter keeps track of an
expression representing each variableās value in terms of
the input. These expressions evolve as variables are
manipulated, and may take on a disjunction of the values
produced by conditional branching. Proofs of properties
about these expressions are then used to establish the
correctness of the program.
ā¢ Model checking. In the model checking approach, software
engineers must first construct a model of their program
design or requirements in a formal modelling lamguage.
Then an automatic prover checks that the model meets a set
of desired properties, which also have to be specified in a
formal notation.
Each of the above techniques has to rely on an automated
theorem prover to show that symbolic logical statements about
the program imply the desired properties to be verified. One of
the earliest theorem provers used for checking programs was
the Boyer-Moore theorem prover, also known as NQTHM. A
review article by Boyer and Moore [8] reports that NQTHM has
been used to check large systems such as a microprocessor
design, an assembler, and a small operating system kernel.
ACL2 [39], the successor to NQTHM, is one of the best known
modern theorem provers. Simplify [19] is another well-known
automatic theorem prover that serves as the proving engine for
ESC/Java.
The prerendering technique does not compete with these
formal approaches; instead, it augments their power. All of the
above methods require a formal specification against which to
check the program and, in the case of model checking, a formal
model of the program itself. A formally verified program is only
as correct as the specification against which it was verified.
Creating such specifications and models correctly is a tricky
task. A smaller and simpler original program makes the
specifications, models, and resulting proofs less likely to
contain mistakes.
Related work 189
Page 203 of 324
Page 204 of 324
During the Pvote security review, we discussed the
possibility of translating Pvote into a language where there is
support for formal verification, and adding the necessary
annotations for preconditions and postconditions. The two
main options we talked about were Java (which has JML and
ESC/Java) and SPARK Ada [6], a commercially developed variant
of Ada specifically designed for high assurance and verification.
Proof-carrying code. In the proof-carrying code (PCC)
technique [53], the supplier of an application constructs a
formal proof that it satisfies a security policy, and includes this
proof (in encoded form) in the distributed application binary.
The host system on which the application will be run can then
check the proof for itself, without relying on any other trusted
parties, to ensure that the program is safe to run.
In the context of electronic voting, the PCC approach would
require the voting machine to run a proof checker. PCC proof
checkers have been built as small as 2 700 lines [4] (about 30%
of which are in C and the rest in Twelf, a logic specification
language), but this is still substantially larger than Pvote.
Formal code generation. Instead of applying machine analysis
to check the correctness of human-written code, an alternative
is to machine-generate code in such a way that the code must be
correct. This is the concept behind formal code generation [86].
A human-written specification still has to direct the machine
generation of code, but this specification could be written at a
higher level, in a declarative rather than a procedural manner.
Large-scale program analysis. Several tools have been
developed for analyzing large programs for bugs. These tools
make no attempt to prove correctness; they are mainly intended
to catch specific kinds of common errors that the programmer
may have missed. A recent example of such a project is Oink
(based on CQual++ [28]), which has been used to scan the
Debian Linux codebase for format string vulnerabilities [14].
Related work 190
Page 204 of 324
Page 205 of 324
Conclusion
In this dissertation, Iāve examined the problem of electronic
voting, starting from an analysis of the requirements for a
democratic election and the different kinds of voting systems
used in practice and proposed by researchers. This analysis led
me to focus on the correctness and simplicity of the software in
the voting computer, a challenge Iāve addressed through the
technique of user interface prerendering. This concept led to
two iterations of design and implementation, culminating in the
creation of Pvote, a vote-entry program that supports
synchronized audio and video, touchscreen input, and
accessible device input.
Pvote is implemented in just 460 lines of Pythonāa tiny
amount of code compared to existing voting machines such as
the Diebold AccuVote-TSx (66 000 lines of code) or the Sequoia
Edge (124 000 lines of code)āyet it allows a high degree of
flexibility in the design of the user interface. With Pvote, the
user interfaces of voting computers can finally be designed by
experts in information design, interaction design, and
accessibility instead of voting system programmers. The
security review of Pvoteās design and source code is reason for
optimism about Pvoteās correctness. Although the results
showed that Pvote was not reviewed enough to be positive that
it lacks flaws, the review also found no bugs in Pvote despite
intense scrutiny. Pvote validates the prerendered user interface
approach by demonstrating that it can meet both accessibility
and security goals.
The quest to create reliable voting machine software has
yielded some results that can be applied to high-assurance
software of other kinds. This work focused specifically on
defending against the insider attack, a long-standing and
191
Page 205 of 324
Page 206 of 324
difficult problem in computer security that has rarely been
addressed. User interface prerendering is an effective technique
whenever a general-purpose computer is used for a specialized
purpose and high reliability is required despite periodic
changes in the user interface. Derivation maps are helpful for
analyzing and mitigating potential sources of vulnerability to
insider attacks. The experience with the Pvote security review
yielded insights into language and design features that would
support the adversarial code review process, and redoubled my
respect for how difficult it can be to review code written by a
potential adversary. The review experience has convinced me
that small teams and short timeframes are inadequate for
adversarial review, and suggests that true confidence in voting
system software is likely to require source code disclosure to
the public or a large community of reviewers, for an extended
period of time before use in an election.
Will we ever create electronic voting machines are truly
worthy of trusting with our votes? I canāt predict whether we
will, but at least one thing is established: Pvote puts a stake in
the ground to show just how small voting machine software can
be. There is simply no good reason to rely on voting machine
software thatās hundreds of times larger.
Conclusion 192
Page 206 of 324
Page 207 of 324
Bibliography
[1] Ben Adida and Ronald L. Rivest (2006). Scratch & vote: self-contained paper-based
cryptographic voting. In Proceedings of the 5th ACM Workshop on Privacy in the
Electronic Society, pages 29ā40. ACM Press.
[2] Alan Agresti and Brett Presnell (2002). Misvotes, Undervotes and Overvotes: The
2000 Presidential Election in Florida. Statistical Science, 17(4):436ā440 (Voting and
Elections, November 2002). Institute of Mathematical Statistics.
[3] Edward G. Amoroso (1994). Fundamentals of Computer Security Technology.
Prentice Hall.
[4] Andrew W. Appel, Neophytos G. Michael, Aaron Stump, and Roberto Virga (2002).
A Trustworthy Proof Checker. Technical Report TR-648-02, Department of
Computer Science, Princeton University. Available at
http://www.cs.princeton.edu/research/techreps/TR-648-02.
[5] Jonathan Bannet, David W. Price, Algis Rudys, Justin Singer, and Dan S. Wallach
(2004). Hack-a-Vote: Security Issues with Electronic Voting Systems. IEEE Security &
Privacy, 2(1):32ā37 (January/February 2004).
[6] John Barnes (1997). High Integrity Ada: The SPARK Approach. Addison-Wesley.
[7] Matt Blaze, Arel Cordero, Sophie Engle, Chris Karlof, Naveen Sastry, Micah Sherr,
Till Stegers, and Ka-Ping Yee (2007). Source Code Review of the Sequoia Voting
System. Available at http://www.sos.ca.gov/elections/voting_systems/
ttbr/sequoia-source-public-jul26.pdf.
[8] Robert S. Boyer and J. Strother Moore (1990). A Theorem Prover for a
Computational Logic. Lecture Notes in Computer Science, (449):1ā15 (July 1990).
193
Page 207 of 324
Page 208 of 324
[9] Steven J. Brams and Peter C. Fishburn (1998). Approval Voting. The American
Political Science Review, 72(3):831ā847 (September 1998).
[10] Shuki Bruck, David Jefferson, and Ronald L. Rivest (2001). A Modular Voting
Architecture (āFrogsā). Presented at the Workshop on Trustworthy Elections (WOTE
2001). Available at http://www.vote.caltech.edu/wote01/pdfs/amva.pdf
(retrieved on June 7, 2007).
[11] Darren Burton and Mark Uslan (2002). Cast a Vote by Yourself: A Review of
Accessible Voting Machines. AccessWorld, November 2002. Available at
http://www.afb.org/afbpress/pub.asp?docid=aw030603.
[12] Joseph A. Calandrino, Ariel J. Feldman, J. Alex Halderman, David A. Wagner, Harlan
Yu, and William P. Zeller (2007). Source Code Review of the Diebold Voting System.
Available at http://www.sos.ca.gov/elections/voting_systems/ttbr/
diebold-source-public-jul29.pdf.
[13] David Chaum, Peter Ryan, and Steve A. Schneider (2004). A Practical,
Voter-verifiable Election Scheme. Technical Report CS-TR-880, School of
Computing Science, University of Newcastle upon Tyne, UK.
[14] Karl Chen and David A. Wagner (2007). Large-Scale Analysis of Format String
Vulnerabilities in Debian Linux. In Proceedings of the 2007 ACM SIGPLAN
Workshop on Programming Languages and Analysis for Security (PLAS 2007),
pages 75ā84. ACM Press.
[15] Lillie Coney (2004). Statement Before the U. S. Election Assistance Commission,
Technical Guidelines Development Committee, September 22, 2004. Available at
http://vote.nist.gov/voting_statement.pdf (retrieved on December 4,
2007).
[16] Patrick Cousot and Radhia Cousot (1977). Abstract interpretation: A unified lattice
model for static analysis of programs by construction or approximation of
fixpoints. In Proceedings of the 4th Conference on Principles of Programming
Languages, pages 238ā252. ACM Press.
[17] Theo de Raadt. OpenBSD Security. Available at
194
Page 208 of 324
Page 209 of 324
http://www.openbsd.org/security.html (retrieved on December 13, 2007).
[18] Stephanie Delaune, Steve Kremer, and Mark Ryan (2006). Coercion-resistance and
Receipt-freeness in Electronic Voting. In Proceedings of the 19th Computer Security
Foundations Workshop (CSFW). IEEE Computer Society Press.
[19] David Detlefs, Greg Nelson, and James B. Saxe (2003). Simplify: A Theorem Prover
for Program Checking. Technical Report 2003-148, Hewlett-Packard Labs. Available
at http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html.
[20] Diebold Election Systems. Welcome to Diebold Election Systems.
http://www.dieboldes.com/ as of January 24, 2004. Archived copy available at
http://web.archive.org/web/20040209133249/www2.diebold.com/
dieboldes/default.htm.
[21] Christopher Drew (2007). U. S. Bars Lab From Testing Electronic Voting. New York
Times, January 4, 2007.
[22] Election Data Services (2004). Overview of Voting Equipment Usage in United
States, Direct Recording Electronic (DRE) Voting. Statement of Kimball Brace to the
United States Election Assistance Commission, May 5, 2004. Available at
http://www.electiondataservices.com/EDSInc_DREoverview.pdf.
[23] Election Reform Information Project (2007). Voter-Verified Paper Audit Trail
Legislation & Information. Available at
http://www.electionline.org/Default.aspx?tabid=290 (retrieved on
December 13, 2007).
[24] Sarah P. Everett, Michael D. Byrne, and Kristen K. Greene (2006). Measuring the
usability of paper ballots: Efficiency, effectiveness, and satisfaction. In Proceedings
of the Human Factors and Ergonomics Society 50th Annual Meeting. Human Factors
and Ergonomics Society.
[25] Sarah P. Everett (2007). The Usability of Electronic Voting Machines and How Votes
Can Be Changed Without Detection. Ph. D. dissertation, Department of Psychology,
Rice University. Available at
http://chil.rice.edu/alumni/petersos/EverettDissertation.pdf.
195
Page 209 of 324
Page 210 of 324
[26] Kevin Fisher, Richard Carback, and Alan T. Sherman (2006). Punchscan:
Introduction and System Definition of a High-Integrity Election System. In
Proceedings of the IAVoSS Workshop On Trustworthy Elections (WOTE 2006).
[27] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe,
and Raymie Stata (2002). Extended static checking for Java. ACM SIGPLAN Notices,
37(5):234ā245 (May 2002).
[28] Jeffrey S. Foster (2002). Type Qualifiers: Lightweight Specifications to Improve
Software Quality. Ph. D. dissertation, Computer Science Division, University of
California, Berkeley.
[29] Laurin Frisina, Michael C. Herron, James Honaker, and Jeffrey B. Lewis (2007).
Ballot Formats, Touchscreens, and Undervotes: A Study of the 2006 Midterm
Elections in Florida. Available at
http://www.dartmouth.edu/~herron/cd13.pdf (retrieved on June 7, 2007).
[30] H. Goldstine and John Von Neumann (1961). Planning and Coding Problems. In
A. H. Taub, editor, John Von Neumann Collected Works, number V, pages 80ā152.
Pergamon Press.
[31] Rop Gonggrijp and Willem-Jan Hengeveld (2007). Studying the Nedap/Groenendaal
ES3B Voting Computer: A Computer Security Perspective. In Proceedings of the
USENIX/ACCURATE Electronic Voting Technology Workshop (EVT 2007). USENIX
Press.
[32] Bev Harris (2004). Black Box Voting: Ballot Tampering in the 21st Century. Talion
Publishing. Available at http://www.blackboxvoting.org/book.html.
[33] Harri Hursti (2006). Diebold TSx Evaluation: Critical Security Issues with Diebold
TSx, May 11, 2006. Available at
http://www.blackboxvoting.org/BBVtsxstudy.pdf (retrieved on June 7,
2007).
[34] Information Technology Association of America, Election Technology Council
(2006). Comments submitted on behalf of the ITAA ETC to the members of the
State of California Senate Committee on Elections, Reapportionment and
196
Page 210 of 324
Page 211 of 324
Constitutional Amendments, February 8, 2006. Archived at
http://web.archive.org/web/20060622084803/http://www.electiontech.
org/downloads/ITAA+ETC+CA+OSS+TESTIMONY+-+FINAL.pdf.
[35] Srinivas Inguva, Eric Rescorla, Hovav Shacham, and Dan S. Wallach (2007). Source
Code Review of the Hart InterCivic Voting System. Available at http://www.sos.
ca.gov/elections/voting_systems/ttbr/Hart-source-public.pdf.
[36] Douglas W. Jones (2004). Recommendations for the Conduct of Elections in
Miami-Dade County using the ES&S iVotronic System. Available at
http://www.cs.uiowa.edu/~jones/voting/miami.pdf (retrieved on December
13, 2007).
[37] Douglas W. Jones (2006). Connecting Work on Threat Analysis to the Real World.
Presented at Threat Analyses for Voting System Categories: A Workshop on Rating
Voting Methods (VSRW 2006). Available at
http://www.cs.uiowa.edu/~jones/voting/VSRW06.pdf (retrieved on
December 19, 2007).
[38] Ari Juels, Dario Catalano, and Markus Jakobsson (2005). Coercion-Resistant
Electronic Elections. In Proceedings of the 2005 ACM Workshop on Privacy in the
Electronic Society, pages ā61ā70. ACM Press.
[39] Matt Kaufmann and J. Strother Moore (1996). ACL2: An Industrial Strength Version
of Nqthm. In Procedings of the Eleventh Annual Conference on Computer
Assurance, Systems Integrity, Software Safety, and Process Security, pages 23ā34.
[40] Arthur Keller (2007). Experiences with Sequoia AVC Edge with VeriVote Printer as
Precinct Inspector in Santa Clara County.
[41] Tim P. Kelly (1998). Arguing Safety ā A Systematic Approach to Managing Safety
Cases. Ph. D. dissertation, Department of Computer Science, University of York.
Available at http://www-users.cs.york.ac.uk/~tpk/tpkthesis.pdf.
[42] James C. King (1969). A program verifier. Ph. D. dissertation, Department of
Computer Science, Carnegie Mellon University.
197
Page 211 of 324
Page 212 of 324
[43] Tadayoshi Kohno, Adam Stubblefield, Aviel D. Rubin, and Dan S. Wallach (2004).
Analysis of an Electronic Voting System. In Proceedings of the 2004 IEEE
Symposium on Security and Privacy. IEEE Computer Society Press.
[44] Samuel Merrill (1988). Making Multicandidate Elections More Democratic. Princeton
University Press.
[45] Adrian Mettler and David A. Wagner. Joe-E (open source software project).
Available at http://joe-e.org/.
[46] Joanne M. Miller and Jon A. Krosnick (1998). The Impact of Candidate Name Order
on Election Outcomes. Public Opinion Quarterly, 62(3):291ā330.
[47] Mark S. Miller (2006). Robust Composition: Towards a Unified Approach to Access
Control and Concurrency Control. Ph. D. dissertation, Department of Computer
Science, Johns Hopkins University. Available at
http://erights.org/talks/thesis.
[48] David Molnar, Tadayoshi Kohno, Naveen Sastry, and David A. Wagner (2006).
Tamper-Evident, History-Independent, Subliminal-Free Data Structures on PROM
Storage -or- How to Store Ballots on a Voting Machine. In Proceedings of the 2006
IEEE Symposium on Security and Privacy. IEEE Computer Society Press.
[49] Moni Naor and Vanessa Teague (2001). Anti-persistence: History Independent Data
Structures. In Proceedings of the 33rd Annual ACM Symposium on the Theory of
Computing, pages 492ā501. ACM Press.
[50] National Conference of State Legislatures. Straight Ticket Voting States (2007).
Available at
http://www.ncsl.org/programs/legismgt/elect/straight_ticket.htm
(retrieved on December 13, 2007).
[51] National Council on Disability (2006). NCD Statement: Voluntary Voting System
Guidelines. Available at
http://www.ncd.gov/newsroom/publications/2006/voluntary_voting.htm
(retrieved on December 13, 2007).
198
Page 212 of 324
Page 213 of 324
[52] National Institute of Standards and Technology (1995). FIPS 180-1: Secure Hash
Standard. Available at http://www.itl.nist.gov/fipspubs/fip180-1.htm
(retrieved on December 13, 2007).
[53] George C. Necula (1997). Proof-Carrying Code. In Proceedings of the 24th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL
1997), pages 106ā119. ACM Press.
[54] C. Andrew Neff and Jim Adler (2003). Verifiable e-voting. Available at
http://votehere.com/vhti/documentation/VH_VHTi_WhitePaper.pdf
(retrieved on December 13, 2007).
[55] Raymound S. Nickerson (1998). Confirmation Bias: A Ubiquitous Phenomenon in
Many Guises. Review of General Psychology, 2(2):175ā220.
[56] Richard G. Niemi and NIST (2005). Sample State and Local Ballots. Available at
http://vote.nist.gov/ballots.htm (retrieved on December 13, 2007).
[57] Nokia Corporation. Python for Series 60 (open source software project). Available
at http://opensource.nokia.com/projects/pythonfors60.
[58] Open Voting Consortium. EVM2003 (open source software project). Available at
http://evm2003.sourceforge.net/.
[59] Open Voting Consortium (2007). Ballot Prerendering. Available at
http://www.openvotingconsortium.org/ballot-prerendering.html
(retrieved on December 18, 2007).
[60] Thea Peacock and Peter Ryan (2006). Coercion-resistance as Opacity in Voting
Systems. Technical Report CS-TR-959, School of Computing Science, University of
Newcastle upon Tyne, UK.
[61] Elliot Proebstel, Sean Riddle, Francis Hsu, Justin Cummins, Freddie Oakley, Tom
Stanionis, and Matt Bishop (2007). An Analysis of the Hart Intercivic DAU eSlate. In
Proceedings of the USENIX/ACCURATE Electronic Voting Technology Workshop (EVT
2007). USENIX Press.
199
Page 213 of 324
Page 214 of 324
[62] Pygame (open source software project). Available at http://pygame.org/.
[63] Python Software Foundation. Python (programming language). Available at
http://www.python.org/.
[64] RABA Technologies (2004). Trusted Agent Report: Diebold AccuVote-TS Voting
System, January 20, 2004. Available at
http://www.raba.com/press/TA_Report_AccuVote.pdf (retrieved on
December 19, 2007).
[65] ReportLab, Inc. ReportLab Toolkit (open source software project). Available at
http://www.reportlab.org/.
[66] Ronald L. Rivest and John P. Wack (2006). On the notion of āsoftware
independenceā in voting systems. Available at
http://vote.nist.gov/SI-in-voting.pdf (retrieved on December 5, 2007).
[67] Ronald L. Rivest and Warren D. Smith (2007). Three Voting Protocols: ThreeBallot,
VAV, and Twin. In Proceedings of the USENIX/ACCURATE Electronic Voting
Technology Workshop (EVT 2007). USENIX Press.
[68] Ronald L. Rivest (2006). The ThreeBallot Voting System. Available at http://
people.csail.mit.edu/rivest/Rivest-TheThreeBallotVotingSystem.pdf
(retrieved on June 7, 2007).
[69] Noel H. Runyan (2007). Improving Access to Voting: A Report on the Technology
for Accessible Voting Systems. D Ģemos and Voter Action. Available at
http://demos.org/pubs/improving_access.pdf (retrieved on June 7, 2007).
[70] Bruce Schneier (1999). Attack Trees: Modeling security threats. Dr. Dobbās Journal,
24(12):21ā29 (December 1999).
[71] Markus Schulze (2003). A New Monotonic and Clone-Independent Single-Winner
Election Method. Voting Matters, (17):9ā19 (October 2003).
[72] Science Applications International Corporation (2003). Risk Assessment Report:
Diebold AccuVote-TS Voting System and Processes, September 2, 2003. Available at
200
Page 214 of 324
Page 215 of 324
http://www.elections.state.md.us/pdf/risk_assessment_report.pdf
(retrieved on November 14, 2007).
[73] Ted Selker (2005). Voting Technology: Election Auditing is an End-to-End
Procedure. Science, 308(5730):1873ā1874 (June 2005).
[74] Warren D. Smith (2000). Range Voting. Available at
http://math.temple.edu/~wds/homepage/rangevote.pdf (retrieved on
December 13, 2007).
[75] Molly F. Story (1998). Maximizing Usability: The Principles of Universal Design.
Assistive Technology, 10(1):4ā12.
[76] Ken Thompson (1984). Reflections on Trusting Trust. Communications of the ACM,
27(8):761ā763 (August 1984).
[77] T. Nicolaus Tideman (1987). Independence of Clones as a Criterion for Voting
Rules. Social Choice and Welfare, 4(3):185ā206 (September 1987).
[78] United States: 107th Congress (2002). Help America Vote Act of 2002. Available at
http://www.fec.gov/hava/law_ext.txt.
[79] United States: 110th Congress (2007). H. R. 811: Voter Confidence and Increased
Accessibility Act of 2007. Available at
http://thomas.loc.gov/cgi-bin/bdquery/z?d110:h.r.00811:.
[80] United States Election Assistance Commission (2005). 2005 Voluntary Voting
System Guidelines. Available at http://www.eac.gov/voting%20systems/
voluntary-voting-guidelines/2005-vvsg.
[81] United States Election Assistance Commission (2007). Draft 2007 Voluntary Voting
System Guidelines. Available at
http://www.eac.gov/files/vvsg/Final-TGDC-VVSG-08312007.pdf (retrieved
on November 17, 2007).
[82] Verified Voting Foundation (2004). Election 2004 E-Voting Incidents from the
Election Incident Reporting System. Available at
201
Page 215 of 324
Page 216 of 324
http://www.verifiedvotingfoundation.org/article.php?id=5331.
[83] William E. Vesely, F. F. Goldberg, N. H. Roberts, and D. F. Haasl (1981). Fault Tree
Handbook (NUREG-0492). United States Nuclear Regulatory Commission.
[84] David A. Wagner, David Jefferson, Matt Bishop, Chris Karlof, and Naveen Sastry
(2006). Security Analysis of the Diebold AccuBasic Interpreter, February 14, 2006.
Available at http://www.cs.berkeley.edu/~daw/papers/accubasic.pdf
(retrieved on June 7, 2007).
[85] Jonathan N. Wand, Kenneth W. Shotts, Jasjeet S. Sekhon, Jr. Walter R. Mebane,
Michael C. Herron, and Henry E. Brady (2001). The Butterfly Did It: The Aberrant
Vote for Buchanan in Palm Beach County, Florida. American Political Science
Review, 95(4):793ā810 (December 2001).
[86] Michael W. Whalen and Mats P. E. Heimdahl (1999). On the Requirements of High
Integrity Code Generation. In Proceedings of the 4th IEEE International Symposium
on High-Assurance Systems Engineering. IEEE Computer Society Press.
[87] S. P. Wilson, Tim P. Kelly, and John A. McDermid (1996). Safety Case Development:
Current Practice, Future Prospects. In Safety and Reliability of Software-Based
Systems, page 135. Springer-Verlag New York.
[88] Alec Yasinsac, David A. Wagner, Matt Bishop, Ted Baker, Breno de Medeiros, Gary
Tyson, Michael Shamos, and Mike Burmester (2007). Software Review and Security
Analysis of the ES&S iVotronic 8.0.1.2 Voting Machine Firmware. Florida
Department of State.
[89] Ka-Ping Yee and Mark Miller (2002). Auditors: An Extensible, Dynamic Code
Verification Mechanism. Available at
http://www.erights.org/elang/kernel/auditors/ (retrieved on December
13, 2007).
[90] Ka-Ping Yee (2006). Prerendered User Interfaces for Higher-Assurance Electronic
Voting. In Proceedings of the USENIX/ACCURATE Electronic Voting Technology
Workshop (EVT 2006). USENIX Press.
202
Page 216 of 324
Page 217 of 324
[91] Ka-Ping Yee (2007). Extending prerendered-interface voting software to support
accessibility and other ballot features. In Proceedings of the USENIX/ACCURATE
Electronic Voting Technology Workshop (EVT 2007). USENIX Press.
[92] Ka-Ping Yee (2007). Pvote Software Review Assurance Document. Technical Report
EECS-2007-40, Department of Electrical Engineering and Computer Sciences,
University of California, Berkeley, CA. Available at
http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-40.html.
[93] Ka-Ping Yee (2007). Report on the Pvote security review. Technical Report
EECS-2007-136, Department of Electrical Engineering and Computer Sciences,
University of California, Berkeley. Available at
http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-136.html.
203
Page 217 of 324
Page 218 of 324
A Ptouch source code
The following pages present the source code of Ptouch,
consisting of five modules:
ā¢ main.py
ā¢ Ballot.py
ā¢ Navigator.py
ā¢ Video.py
ā¢ Recorder.py
Each line of code is numbered and printed in monospaced type.
36 flags = [0 for c in m.contests]
Defining occurrences of classes, methods, and functions appear
in bold.
123 def getlist(ballot, stream, Class):
Lines marked with a triangle are entry points into a module,
called from other modules. Functions and methods without a
triangle are called only from within the same module.
. 45 def activate(self, slot i):
The code is broken into sections, with explanatory text in grey
preceding each section.
Explanatory text looks like this.
204
Page 218 of 324
Page 219 of 324
main.py
This is the main Ptouch program. It initializes the other software
components with the provided ballot definition file and then processes
incoming Pygame events in a non-terminating loop.
1 import Ballot, Navigator, Recorder, Video
2 from pygame import display, event, MOUSEBUTTONDOWN, KEYDOWN
The following lines load and verify the ballot definition, then instantiate
the other parts of Ptouch with their corresponding sections of the ballot
definition.
3 ballot = Ballot.Ballot(āballotā)
4 video = Video.Video(ballot.imagelib)
5 recorder = Recorder.Recorder(ballot)
6 navigator = Navigator.Navigator(ballot.model, video, recorder)
This is the main event loop. The loop begins by updating the display to
match the framebuffer in memory, so that any display changes made
during the last iteration appear onscreen. The loop never exits.
7 while 1:
8 display.update()
On each iteration, one event is retrieved from Pygameās event queue. The
only type of event Ptouch handles is a mouse click. The coordinates of
the mouse click are translated into a slot index. If the click corresponds
to a slot, it is passed to the navigatorās activate() method for further
handling.
9 e = event.wait()
10 if e.type == MOUSEBUTTONDOWN:
11 slot = video.locate(*e.pos)
12 if slot is not None:
13 navigator.activate(slot)
Ptouch source code 205
Page 219 of 324
Page 220 of 324
Ballot.py
The Ballot module defines the ballot definition data structure. The
main program instantiates a Ballot object to deserialize the ballot data
from a file stream and construct the ballot definition data structure. All
the other classes in this module represent parts of the ballot definition;
each one deserializes its contents from the stream passed to its
constructor.
1 class Ballot:
. 2 def init (self, filename):
3 self.data = open(filename).read()
4 stream = open(filename)
sprite n is a counter that keeps track of the next sprite index. Each
instance of the Option, Writein, Subpage, and Subtarget classes
contains a local field called sprite i that points to its associated sprite.
This field is set by the init method of the class, which picks up the
sprite index by accessing and incrementing the sprite n field of the
Ballot during loading. subpage n is a local counter of subpages that is
only used during verification after the ballot is loaded.
5 self.sprite n = subpage n = 0
6 self.model = m = Model(self, stream)
7 self.imagelib = il = Imagelib(self, stream)
8 assert stream.read(1) == āā
At this point the ballot definition has been fully loaded into memory.
The rest of the init method verifies that the ballot definition is
well-formed. If it is not well-formed, the program should be aborted with
a fatal error to prevent the possibility that Ptouch will crash after
starting a voting session.
The following lines ensure that there is at least one page and one contest,
and that the arrays of layouts and sprites have the proper sizes.
9 assert m.pages and m.contests
10 assert len(m.pages) + len(m.subpages) == len(il.layouts)
11 assert len(il.sprites) == self.sprite n
items contains one list corresponding to each contest; it will collect all
the slots and sprites for the options in the contest. chars also contains
one line corresponding to each contest; it will collect all the slots and
sprites for the write-in characters in the contest. These lists will later be
checked to ensure that the sizes of all sprites match the sizes of the slots
into which they could be pasted.
12 items = [[] for c in m.contests]
13 chars = [[] for c in m.contests]
For each page, the targets, options, write-ins, and reviews are checked to
ensure their fields have valid values.
14 for i, p in enumerate(m.pages):
15 for t in p.targets:
16 assert t.action in [0, 1, 2]
17 assert 0 <= t.page i < len(m.pages)
18 for x in p.targets + p.options + p.writeins + p.reviews:
19 assert 0 <= x.contest i < len(m.contests)
Ptouch source code 206
Page 220 of 324
Page 221 of 324
The slot variable keeps track of the slot index during checking of the
slots associated with each page.
20 slots = il.layouts[i].slots
21 slot = len(p.targets)
The slots and sprites for all the option areas are gathered into the
appropriate arrays for later size checking.
22 for i, o in enumerate(p.options):
23 items[o.contest i] += [slots[slot + i], il.sprites[o.sprite i]]
The slots and sprites for all the write-ins are gathered into the
appropriate arrays for later size checking.
24 slot += len(p.options)
25 for w in p.writeins:
26 items[w.contest i] += [slots[slot], il.sprites[w.sprite i]]
27 max chars = m.contests[w.contest i].max chars
28 chars[w.contest i] += slots[slot + 1:slot + 1 + max chars]
29 slot += 1 + max chars
The slots and sprites for all the review areas are gathered into the
appropriate arrays for later size checking.
30 for r in p.reviews:
31 max chars = m.contests[r.contest i].max chars
32 for i in range(m.contests[r.contest i].max sels):
33 items[r.contest i] += [slots[slot]]
34 chars[r.contest i] += slots[slot + 1:slot + 1 + max chars]
35 slot += 1 + max chars
The flags array indicates which contests contain write-in options.
36 flags = [0 for c in m.contests]
37 for p in m.pages:
38 for w in p.writeins:
39 flags[w.contest i] = 1
For each contest with write-in options, the associated write-in subpage is
checked to ensure it has the right number of slots and all of its
subtargets have fields with valid values. The slots for write-in characters
are gathered into the appropriate arrays for later size checking. In this
loop, subpage n keeps track of the index of the associated subpage.
40 for i, c in enumerate(m.contests):
41 if flags[i]:
42 c.subpage i, subpage n = subpage n, subpage n + 1
43 p = m.subpages[c.subpage i]
44 slots = il.layouts[len(m.pages) + c.subpage i].slots
45 assert len(p.subtargets) + c.max chars == len(slots)
46 chars[i] += slots[len(p.subtargets):]
47 for t in p.subtargets:
48 assert t.action in [0, 1, 2, 3, 4, 5]
49 if t.action in [0, 1]:
50 chars[i] += [il.sprites[t.sprite i]]
51 chars[i] += [il.sprites[p.cursor i]]
The number of subpages in the ballot model should match the number of
contests with write-in options, which were counted in the preceding loop.
52 assert len(m.subpages) == subpage n
Ptouch source code 207
Page 221 of 324
Page 222 of 324
Each layout is checked to ensure that its background image matches the
screen size and all its slots are positioned within the screen bounds.
53 for l, b in [(l, l.background) for l in il.layouts]:
54 assert (b.width, b.height) == (il.width, il.height)
55 for slot in l.slots:
56 assert 0 <= slot.left < slot.left + slot.width < il.width
57 assert 0 <= slot.top < slot.top + slot.height < il.height
Finally, the sprites and slots that have been collected for each group are
checked to ensure they all have properly matching sizes.
58 for list in items + chars:
59 for x in list:
60 assert (x.width, x.height) == (list[0].width, list[0].height)
Each remaining class loads its contents from the stream in a constructor
that parallels its data structure. These constructors instantiate other
classes to read single components from the stream, call getlist() to
read a variable-length list of components from the stream, or call
getint() to deserialize an integer from the stream.
61 class Model:
62 def init (self, ballot, stream):
63 self.contests = getlist(ballot, stream, Contest)
64 self.pages = getlist(ballot, stream, Page)
65 self.subpages = getlist(ballot, stream, Subpage)
66 class Contest:
67 def init (self, ballot, stream):
68 self.max sels = getint(stream)
69 self.max chars = getint(stream)
70 class Page:
71 def init (self, ballot, stream):
72 self.targets = getlist(ballot, stream, Target)
73 self.options = getlist(ballot, stream, Option)
74 self.writeins = getlist(ballot, stream, Writein)
75 self.reviews = getlist(ballot, stream, Review)
76 class Target:
77 def init (self, ballot, stream):
78 self.action = getint(stream)
79 self.page i = getint(stream)
80 self.contest i = (self.action == 1 and [getint(stream)] or [0])[0]
81 class Option:
82 def init (self, ballot, stream):
83 self.contest i = getint(stream)
84 self.sprite i, ballot.sprite n = ballot.sprite n, ballot.sprite n + 1
85 class Writein:
86 def init (self, ballot, stream):
87 self.contest i = getint(stream)
88 self.sprite i, ballot.sprite n = ballot.sprite n, ballot.sprite n + 1
89 class Review:
90 def init (self, ballot, stream):
91 self.contest i = getint(stream)
Ptouch source code 208
Page 222 of 324
Page 223 of 324
92 class Subpage:
93 def init (self, ballot, stream):
94 self.subtargets = getlist(ballot, stream, Subtarget)
95 self.cursor i, ballot.sprite n = ballot.sprite n, ballot.sprite n + 1
96
97 class Subtarget:
98 def init (self, ballot, stream):
99 self.action = getint(stream)
100 if self.action in [0, 1]:
101 self.sprite i, ballot.sprite n = ballot.sprite n, ballot.sprite n + 1
102 class Imagelib:
103 def init (self, ballot, stream):
104 self.width = getint(stream)
105 self.height = getint(stream)
106 self.layouts = getlist(ballot, stream, Layout)
107 self.sprites = getlist(ballot, stream, Image)
108 class Layout:
109 def init (self, ballot, stream):
110 self.background = Image(ballot, stream)
111 self.slots = getlist(ballot, stream, Slot)
112 class Slot:
113 def init (self, ballot, stream):
114 self.left = getint(stream)
115 self.top = getint(stream)
116 self.width = getint(stream)
117 self.height = getint(stream)
An Image object contains the pixel data for an image, which resides in a
single Python string. In serialized form, the imageās width and height are
stored preceding the pixel data, which contains three bytes per pixel (one
byte each for the red, green, and blue components).
118 class Image:
119 def init (self, ballot, stream):
120 self.width = getint(stream)
121 self.height = getint(stream)
122 self.pixels = stream.read(self.width * self.height * 3)
The getlist() function reads a variable-length list of data structures
from the stream, all of a particular given class. In Python (and Pthin),
classes are first-class objects and can be passed as arguments. In
serialized form, the list is preceded by a 4-byte integer indicating how
many elements to read.
123 def getlist(ballot, stream, Class):
124 return [Class(ballot, stream) for i in range(getint(stream))]
The getint() function reads an unsigned 4-byte integer from the
stream, serialized with the most significant byte first.
125 def getint(stream):
126 bytes = [ord(char) for char in stream.read(4)]
127 return (bytes[0]<<24) + (bytes[1]<<16) + (bytes[2]<<8) + bytes[3]
Ptouch source code 209
Page 223 of 324
Page 224 of 324
Navigator.py
The navigator is initialized with access to the ballot model data
structure, the video driver, and the vote recording module. It saves these
references locally, initializes an empty selection state, and begins the
voting session by transitioning to page 0. The selections member
contains a list of selections for each contest. The elements of these lists
are themselves lists: an ordinary selected option is represented by a list
of a single integer, the optionās sprite index; a selected write-in option is
represented by a list containing the write-in optionās sprite index
followed by the indices of the character sprites entered for the write-in.
1 class Navigator:
. 2 def init (self, model, video, recorder):
3 self.model, self.video, self.recorder = model, video, recorder
4 self.selections = [[] for contest in model.contests]
5 self.goto(0)
6 self.update()
The goto() method transitions to a given page. If the transition goes to
the last page, the voterās selections are recorded. Any page transition
clears the writein and chars members, which are set only when a
subpage is active (writein points to the current write-in object, and
chars contains the write-in characters entered so far).
7 def goto(self, page i):
8 if page i == len(self.model.pages) - 1:
9 self.recorder.write(self.selections)
10 self.page i, self.page = page i, self.model.pages[page i]
11 self.writein, self.chars = None, []
The update() method updates the video display based on the current
page and selections.
12 def update(self):
When the writein member is not None, this means the user is currently
on a subpage. The video driver is told to paste the subpageās background
over the entire screen, then paste any entered characters into the
character slots of the subpage, in order. If the character slots are not all
full, the cursor sprite is also pasted into the next available character slot.
13 if self.writein:
14 contest = self.model.contests[self.writein.contest i]
15 subpage = self.model.subpages[contest.subpage i]
16 self.video.goto(len(self.model.pages) + contest.subpage i)
17 offset = len(subpage.subtargets)
18 for i, sprite i in enumerate(self.chars):
19 self.video.paste(sprite i, offset + i)
20 if len(self.chars) < contest.max chars:
21 self.video.paste(subpage.cursor i, offset + len(self.chars))
Ptouch source code 210
Page 224 of 324
Page 225 of 324
When the writein member is None, no subpage is active. The video
driver is told to paste the current pageās background over the entire
screen, then fill in the options, write-ins, and reviews on the page
according to the current selections. The indices of the corresponding
slots are assumed to be arranged in sequential order, as described in
Chapter 5; hence the variable slot i is incremented in each loop and
carried forward to the next loop.
22 else:
23 self.video.goto(self.page i)
To check whether an option is selected, the elements of the contestās
selection list are scanned for a one-element list containing the optionās
sprite index.
24 slot i = len(self.page.targets)
25 for option in self.page.options:
26 if [option.sprite i] in self.selections[option.contest i]:
27 self.video.paste(option.sprite i, slot i)
28 slot i += 1
To check whether a write-in is selected, the elements of the contestās
selection list are scanned for a list whose first element is the write-in
optionās sprite index. If such a list is found, the rest of the elements in
the list are the sprite indices of the entered characters, so all the sprites
in the list can be pasted into the write-inās slots in the order they appear.
(The cursor is not shown on ordinary pages, only on subpages.)
29 for writein in self.page.writeins:
30 for selection in self.selections[writein.contest i]:
31 if selection[0] == writein.sprite i:
32 for j, sprite i in enumerate(selection):
33 self.video.paste(sprite i, slot i + j)
34 slot i += 1 + self.model.contests[writein.contest i].max chars
To display a review, the selections in the contestās selection list are
pasted into the reviewās slots in the order they appear. Since write-in
selections are represented by a list beginning with the write-in sprite
index followed by the entered character sprites, these sprites will fit into
the 1 + contest.max chars slots corresponding to the review. The
inner loop always executes contest.max sels times so that slot i will
be incremented by the correct amount.
35 for review in self.page.reviews:
36 contest = self.model.contests[review.contest i]
37 selections = self.selections[review.contest i]
38 for i in range(contest.max sels):
39 if i < len(selections):
40 for j, sprite i in enumerate(selections[i]):
41 self.video.paste(sprite i, slot i + j)
42 slot i += 1 + contest.max chars
Ptouch source code 211
Page 225 of 324
Page 226 of 324
The activate() method activates a slot when a user touches the
touchscreen within the slot. The triggered behaviour depends on whether
the slot corresponds to a subtarget, a target, an option, or a write-in.
. 43 def activate(self, slot i):
When the writein member is not None, this means the user is currently
on a subpage. The touched slot index is treated as a subtarget index. The
action field of the subtarget determines the action to take: the values
from 0 through 5 correspond to APPEND, APPEND2, DELETE, CLEAR, CANCEL,
and ACCEPT.
44 if self.writein:
45 contest = self.model.contests[self.writein.contest i]
46 subpage = self.model.subpages[contest.subpage i]
47 subtarget = subpage.subtargets[slot i]
APPEND appends the selected character. APPEND2 appends the selected
character only if the write-in is not empty. In both cases the character is
only appended if the maximum length will not be exceeded.
48 if subtarget.action == 0 or subtarget.action == 1 and self.chars:
49 if len(self.chars) < contest.max chars:
50 self.chars += [subtarget.sprite i]
DELETE deletes the last entered character.
51 if subtarget.action == 2:
52 self.chars[-1:] = []
CLEAR clears all the entered characters.
53 if subtarget.action == 3:
54 self.chars = []
CANCEL cancels the write-in and exits the subpage. The write-in option
was already removed from the selection list upon entry to the subpage
(see line 85), so upon return to the original page, the write-in option will
be cleared and deselected.
55 if subtarget.action == 4:
56 self.goto(self.page i)
ACCEPT accepts the write-in and exits the subpage. The write-in sprite
and entered character sprites are placed into a list, and this list is added
to the selection list for this contest.
57 if subtarget.action == 5 and self.chars:
58 self.selections[self.writein.contest i] += [
59 [self.writein.sprite i] + self.chars]
60 self.goto(self.page i)
Ptouch source code 212
Page 226 of 324
Page 227 of 324
The rest of the cases cover user actions when the user is on an ordinary
page. The first case covers targets; the action field of the target can be
0, 1, or 2, corresponding to a plain transition, a transition with clearing
the selections in a contest, and a transition with clearing all the
selections in the entire ballot.
61 elif slot i < len(self.page.targets):
62 target = self.page.targets[slot i]
63 if target.action == 1:
64 self.selections[target.contest i] = []
65 if target.action == 2:
66 self.selections = [[] for contest in self.model.contests]
67 self.goto(target.page i)
The next case handles options. Touching an option toggles whether it is
selected, unless this would exceed the selection limit indicated by the
contestās max sels field.
68 elif slot i < len(self.page.targets) + len(self.page.options):
69 option = self.page.options[slot i - len(self.page.targets)]
70 selections = self.selections[option.contest i]
71 contest = self.model.contests[option.contest i]
72 if [option.sprite i] in selections:
73 selections.remove([option.sprite i])
74 elif len(selections) < contest.max sels:
75 selections += [[option.sprite i]]
The only remaining case is that the user has touched a write-in. In this
case, slot i is used to find the appropriate write-in, and its contestās
selection list is searched to see whether the write-in is already selected.
76 else:
77 slot i -= len(self.page.targets) + len(self.page.options)
78 for writein in self.page.writeins:
79 contest = self.model.contests[writein.contest i]
80 if slot i < 1 + contest.max chars:
81 selections = self.selections[writein.contest i]
82 for i, selection in enumerate(selections):
If the write-in is already selected, the write-in characters that were
previously entered need to be moved into the chars buffer so they will
appear on the subpage. The entry for this write-in in the selection list is
removed upon entry to the subpage; it will be added back if the user
decides to accept the write-in (see line 58).
83 if selection[0] == writein.sprite i:
84 self.writein, self.chars = writein, selection[1:]
85 selections[i:i + 1] = []
86 break
87
If the write-in is not selected, its subpage is simply activated.
88 else:
89 if len(selections) < contest.max sels:
90 self.writein = writein
91 break
92 slot i -= 1 + contest.max chars
The display is then updated to reflect the selection changes and/or
transition that were enacted in response to the userās touch.
93 self.update()
Ptouch source code 213
Page 227 of 324
Page 228 of 324
Video.py
Video display control is provided by the pygame library.
1 from pygame import display, image, FULLSCREEN
The loadimage() function converts a string containing uncompressed
pixel data into a Pygame Image object.
2 def loadimage(i):
3 return image.fromstring(i.pixels, (i.width, i.height), āRGBā)
The Video class is responsible for pasting full-screen images and sprites
onto the display, as well as translating touch locations into slot indices.
4 class Video:
The video driver is initialized with access to the image library section of
the ballot definition. It initializes the Pygame display and converts all the
images from raw data into Pygame Image objects.
. 5 def init (self, il):
6 display.init()
7 self.screen = display.set mode((il.width, il.height), FULLSCREEN)
8 self.backgrounds = [loadimage(l.background) for l in il.layouts]
9 self.layouts = [l.slots for l in il.layouts]
10 self.sprites = [loadimage(sprite) for sprite in il.sprites]
11 self.goto(0)
The goto() method switches to a given layout, which involves pasting
the layoutās background image over the entire screen. The slots
member always points to the current layoutās slots.
. 12 def goto(self, layout i):
13 self.slots = self.layouts[layout i]
14 self.screen.blit(self.backgrounds[layout i], (0, 0))
The paste() method pastes a given sprite into a given slot. The slot
coordinates come from the current layout.
. 15 def paste(self, sprite i, slot i):
16 slot = self.slots[slot i]
17 self.screen.blit(self.sprites[sprite i], (slot.left, slot.top))
The locate() method finds the slot index corresponding to a given
touch location. It returns the index of the first enclosing slot in the
current layout.
. 18 def locate(self, x, y):
19 for i, slot in enumerate(self.slots):
20 if slot.left <= x < slot.left + slot.width:
21 if slot.top <= y < slot.top + slot.height:
22 return i
Ptouch source code 214
Page 228 of 324
Page 229 of 324
Recorder.py
This Recorder module is responsible for recording the voterās selections
in a tamper-evident, history-independent format.
1 import sha
2 class Recorder:
3
The Recorder object is initialized with access to the ballot definition so
it can compute a hash of the ballot data.
. 4 def init (self, ballot):
5 self.hash = sha.new(ballot.data).hexdigest()
The write() method does the real work of writing out the selections.
. 6 def write(self, selections):
7 file = open(āvotesā, ār+ā)
First, the erased portion of the file is skipped. The four-byte sentinel
ā\xff\xff\xff\xffā signals the beginning of the unerased area.
8 while file.read(4) != ā\xff\xff\xff\xffā:
9 pass
Then all of the currently stored items are read into the items list. Each
item is stored as a block of data preceded with the length of the block as
a 4-byte unsigned integer. A zero signals that there are no more items.
10 items = []
11 size = getint(file)
12 while size:
13 items += [file.read(size)]
14 size = getint(file)
Each selection to be written is then encoded as a string of 4-byte
integers, preceded by the hash of the ballot definition. These strings are
gathered into the items list.
15 for i, contest in enumerate(selections):
16 for selection in contest:
17 item = self.hash + putint(i)
18 for n in selection:
19 item += putint(n)
20 items += [item]
Sorting the items list guarantees a history-independent result.
21 items.sort()
Ptouch source code 215
Page 229 of 324
Page 230 of 324
Next, the size of the region to erase is computed by adding up the
maximum possible lengths that each item could have used up, if the
items were each added one at a time.
22 start = 0
23 maxlength = max([len(item) for item in items] or [āā])
24 for i, item in enumerate(items):
25 start += 4 + (4 + maxlength)*i + 4
26
The file pointer is then moved to the correct starting location and the
new data is written, with the sentinel in front and a zero at the end.
27 file.write(ā\0ā*(start - file.tell()))
28 file.seek(start)
29 file.write(ā\xff\xff\xff\xffā)
30 for item in items:
31 file.write(putint(len(item)) + item)
32 file.write(putint(0))
After the new data has been successfully written, the region in front of
the new data is erased, ensuring an atomic transition from the old data
to the new data.
33 file.seek(0)
34 file.write(ā\0ā*start)
The getint() function deserializes an unsigned 4-byte integer from a
stream.
35 def getint(stream):
36 bytes = [ord(char) for char in stream.read(4)]
37 return (bytes[0]<<24) + (bytes[1]<<16) + (bytes[2]<<8) + bytes[3]
The putint() function serializes an unsigned integer into a 4-byte
string.
38 def putint(n):
39 char = lambda n: chr(n & 255)
40 return char(n>>24) + char(n>>16) + char(n>>8) + char(n)
Ptouch source code 216
Page 230 of 324
Page 231 of 324
B Pvote source code
The following pages present the source code of Pvote,
consisting of seven modules:
ā¢ main.py
ā¢ Ballot.py
ā¢ verifier.py
ā¢ Navigator.py
ā¢ Audio.py
ā¢ Video.py
ā¢ Printer.py
Each line of code is numbered and printed in monospaced type.
42 self.bindings = get list(stream, Binding)
Defining occurrences of classes, methods, and functions appear
in bold.
127 def get enum(stream, cardinality):
Lines marked with a triangle are entry points into a module,
called from other modules. Functions and methods without a
triangle are called only from within the same module.
.48 def press(self, key):
The code is broken into sections, with explanatory text in grey
preceding each section.
Explanatory text looks like this.
Reviewersā comments, from the Pvote security review, are
marked with bullets and shown in grey italic text after the
section to which they refer.
ā¢ Reviewersā notes look like this.
217
Page 231 of 324
Page 232 of 324
main.py
This is the main Pvote program. It initializes the other software
components with the provided ballot definition file and then processes
incoming Pygame events in a non-terminating loop.
1 import Ballot, verifier, Audio, Video, Printer, Navigator, pygame
These two constants are the type IDs of user-defined events. An
AUDIO DONE event signals that an audio clip has finished playing. A
TIMER DONE event signals that a timed delay has elapsed.
2 AUDIO DONE = pygame.USEREVENT
3 TIMER DONE = pygame.USEREVENT + 1
ā¢
ā¢
ā¢
Reviewers suggested that all constants be moved into a separate
module; thus, for example, both main.py and Audio.py would refer to
the same AUDIO DONE constant instead of redundantly defining it in
both files.
The following lines load the ballot definition, verify it, and then
instantiate the other parts of Pvote with their corresponding sections of
the ballot definition.
4 ballot = Ballot.Ballot(open(”ballot”))
5 verifier.verify(ballot)
6 audio = Audio.Audio(ballot.audio)
7 video = Video.Video(ballot.video)
8 printer = Printer.Printer(ballot.text)
9 navigator = Navigator.Navigator(ballot.model, audio, video, printer)
Pvote source code 218
Page 232 of 324
Page 233 of 324
This is the main event loop. The loop begins by updating the display to
match the framebuffer in memory, so that any display changes made
during the last iteration appear onscreen. The loop never exits.
10 while 1:
11 pygame.display.update()
On each iteration, one event is retrieved from Pygameās event queue. A
timeout is scheduled before waiting for the event, so that if no events
occur in timeout ms milliseconds, a TIMER DONE event will be posted.
This timeout is then cancelled so that a timer event cannot occur while
other processing is taking place.
12 pygame.time.set timer(TIMER DONE, ballot.model.timeout ms)
13 event = pygame.event.wait()
14 pygame.time.set timer(TIMER DONE, 0)
Keypresses are handled by the navigatorās press() method. Touches on
the touchscreen are handled by looking for a corresponding target; if one
is found, the event is handled by the navigatorās touch() method.
15 if event.type == pygame.KEYDOWN:
16 navigator.press(event.key)
17 if event.type == pygame.MOUSEBUTTONDOWN:
18 [x, y] = event.pos
19 target i = video.locate(x, y)
20 if target i != None:
21 navigator.touch(target i)
The audio driver schedules an AUDIO DONE event to be posted whenever
an audio clip finishes playing. Upon receipt of such an event, the audio
driverās next() method is called so that any audio clips waiting to be
played next can start playing.
22 if event.type == AUDIO DONE:
23 audio.next()
If a TIMER DONE event was received, that means there has been no user
activity for timeout ms milliseconds. It also means that no AUDIO DONE
event has occurred for timeout ms milliseconds, which means that
either the audio is silent or that a clip has been playing for longer than
timeout ms milliseconds. If the playing flag on the audio driver is
zero, that means the timeout period has elapsed since the last user input
occurred or last audio clip finished.
24 if event.type == TIMER DONE and not audio.playing:
25 navigator.timeout()
Pvote source code 219
Page 233 of 324
Page 234 of 324
Ballot.py
The Ballot module defines the ballot definition data structure. The
main program instantiates a Ballot object to deserialize the ballot data
from a file stream and construct the ballot definition data structure. All
the other classes in this module represent parts of the ballot definition;
each one deserializes its contents from the stream passed to its
constructor.
1 import sha
2 class Ballot:
. 3 def init (self, stream):
4 assert stream.read(8) == “Pvote\x00\x01\x00″
5 [self.stream, self.sha] = [stream, sha.sha()]
In order to produce a SHA-1 hash of all the ballot data, the Ballot object
passes self as the stream object to the other constructors. Its read
method allows it to proxy for the original stream, allowing it to
incorporate all the data into the hash as it passes through. After all four
parts of the ballot definition have been loaded, the last 20 bytes of the
stream are checked to ensure they match the hash.
6 self.model = Model(self)
7 self.text = Text(self)
8 self.audio = Audio(self)
9 self.video = Video(self)
10 assert self.sha.digest() == stream.read(20)
11 def read(self, length):
12 data = self.stream.read(length)
13 self.sha.update(data)
14 return data
ā¢
ā¢
ā¢
Reviewers suggested that the read() method would make more sense
if moved into a separate object playing the role of the stream proxy,
instead of using the Ballot itself as the stream proxy. This change
would also prevent the sub-objects from having access to the
incompletely constructed Ballot object during construction.
Each remaining class loads its contents from the stream in a constructor
that parallels its data structure. These constructors instantiate other
classes to read single components from the stream, call get list() to
read a variable-length list of components from the stream, or call
get int(), get enum(), or get str() to deserialize primitive data
types from the stream.
15 class Model:
16 def init (self, stream):
17 self.groups = get list(stream, Group)
18 self.pages = get list(stream, Page)
19 self.timeout ms = get int(stream, 0)
20 class Group:
21 def init (self, stream):
22 self.max sels = get int(stream, 0)
23 self.max chars = get int(stream, 0)
24 self.option clips = get int(stream, 0)
25 self.options = get list(stream, Option)
Pvote source code 220
Page 234 of 324
Page 235 of 324
26 class Option:
27 def init (self, stream):
28 self.sprite i = get int(stream, 0)
29 self.clip i = get int(stream, 0)
30 self.writein group i = get int(stream, 1)
31 class Page:
32 def init (self, stream):
33 self.bindings = get list(stream, Binding)
34 self.states = get list(stream, State)
35 self.option areas = get list(stream, OptionArea)
36 self.counter areas = get list(stream, CounterArea)
37 self.review areas = get list(stream, ReviewArea)
38 class State:
39 def init (self, stream):
40 self.sprite i = get int(stream, 0)
41 self.segments = get list(stream, Segment)
42 self.bindings = get list(stream, Binding)
43 self.timeout segments = get list(stream, Segment)
44 self.timeout page i = get int(stream, 1)
45 self.timeout state i = get int(stream, 0)
46 class OptionArea:
47 def init (self, stream):
48 self.group i = get int(stream, 0)
49 self.option i = get int(stream, 0)
50 class CounterArea:
51 def init (self, stream):
52 self.group i = get int(stream, 0)
53 self.sprite i = get int(stream, 0)
54 class ReviewArea:
55 def init (self, stream):
56 self.group i = get int(stream, 0)
57 self.cursor sprite i = get int(stream, 1)
58 class Binding:
59 def init (self, stream):
60 self.key = get int(stream, 1)
61 self.target i = get int(stream, 1)
62 self.conditions = get list(stream, Condition)
63 self.steps = get list(stream, Step)
64 self.segments = get list(stream, Segment)
65 self.next page i = get int(stream, 1)
66 self.next state i = get int(stream, 0)
67 class Condition:
68 def init (self, stream):
69 self.predicate = get enum(stream, 3)
70 self.group i = get int(stream, 1)
71 self.option i = get int(stream, 0)
72 self.invert = get enum(stream, 2)
73 class Step:
74 def init (self, stream):
75 self.op = get enum(stream, 5)
76 self.group i = get int(stream, 1)
77 self.option i = get int(stream, 0)
Pvote source code 221
Page 235 of 324
Page 236 of 324
78 class Segment:
79 def init (self, stream):
80 self.conditions = get list(stream, Condition)
81 self.type = get enum(stream, 5)
82 self.clip i = get int(stream, 0)
83 self.group i = get int(stream, 1)
84 self.option i = get int(stream, 0)
85 class Text:
86 def init (self, stream):
87 self.groups = get list(stream, TextGroup)
88 class TextGroup:
89 def init (self, stream):
90 self.name = get str(stream)
91 self.writein = get enum(stream, 2)
92 self.options = get list(stream, get str)
93 class Audio:
94 def init (self, stream):
95 self.sample rate = get int(stream, 0)
96 self.clips = get list(stream, Clip)
The Clip type contains the waveform data for an audio clip, which
resides in a single Python string. In a serialized ballot definition, the
number of samples is stored preceding the audio data. Since each sample
is a 16-bit value, the number of bytes to read is twice the number of
samples.
97 class Clip:
98 def init (self, stream):
99 self.samples = stream.read(get int(stream, 0)*2)
100 class Video:
101 def init (self, stream):
102 self.width = get int(stream, 0)
103 self.height = get int(stream, 0)
104 self.layouts = get list(stream, Layout)
105 self.sprites = get list(stream, Image)
106 class Layout:
107 def init (self, stream):
108 self.screen = Image(stream)
109 self.targets = get list(stream, Rect)
110 self.slots = get list(stream, Rect)
An Image object contains the pixel data for an image, which resides in a
single Python string. In serialized form, the imageās width and height are
stored preceding the pixel data, which contains three bytes per pixel (one
byte each for the red, green, and blue components).
111 class Image:
112 def init (self, stream):
113 self.width = get int(stream, 0)
114 self.height = get int(stream, 0)
115 self.pixels = stream.read(self.width*self.height*3)
116 class Rect:
117 def init (self, stream):
118 self.left = get int(stream, 0)
119 self.top = get int(stream, 0)
120 self.width = get int(stream, 0)
121 self.height = get int(stream, 0)
Pvote source code 222
Page 236 of 324
Page 237 of 324
The get int() function reads an unsigned 4-byte integer from the
stream. The allow none argument is a flag specifying whether the
returned value can be None, which is represented by the sequence
“\xff\xff\xff\xff”. This function ensures that the data meets the
constraints given in the assurance documentānamely, that the value is
between 0 and 231 ā 1 inclusive, or None only for fields that allow it.
122 def get int(stream, allow none):
123 [a, b, c, d] = list(stream.read(4))
124 if ord(a) < 128:
125 return ord(a)*16777216 + ord(b)*65536 + ord(c)*256 + ord(d)
126 assert allow none and a + b + c + d == “\xff\xff\xff\xff”
ā¢ Reviewers suggested that it would be clearer to have two separate
methods (for reading an integer and reading an integer-or-None)
instead of using get int() for both purposes.
ā¢ Reviewers agreed that there should be an explicit return None
statement to show that None is the intended return value.
The get enum() function reads an enumerated type from the stream,
which is represented the same way as an integer. The second argument
gives the cardinality of the enumeration, which is used to ensure the
validity of the returned value.
127 def get enum(stream, cardinality):
128 value = get int(stream, 0)
129 assert value < cardinality
130 return value
ā¢ Reviewers suggested that it would be clearer to have two separate
methods for reading Boolean values and enumerated values, instead of
using get enum(stream, 2) to read Boolean values.
The get str() function reads a string from the stream, which is
represented as a sequence of bytes prefixed by the length as a 4-byte
integer. This function checks that all the characters in the string fall in
the printable ASCII range, so they will print out in a predictable way. The
tilde character (number 126) is specifically excluded to avoid any
ambiguity in the printed output, because the tilde is used as a delimiter.
131 def get str(stream):
132 str = stream.read(get int(stream, 0))
133 for ch in list(str):
134 assert 32 <= ord(ch) <= 125
135 return str
ā¢
ā¢
Reviewers suggested that the condition in line 134 would be easier to
understand if it were written isprint(ch) and ch != ā~ā.
The get list() function reads a variable-length list of data structures
from the stream, all of a particular given class. In Python (and Pthin),
classes are first-class objects and can be passed as arguments. In
serialized form, the list is preceded by a 4-byte integer indicating how
many elements to read.
136 def get list(stream, Class):
137 return [Class(stream) for i in range(get int(stream, 0))]
Pvote source code 223
Page 237 of 324
Page 238 of 324
verifier.py
The verifier module contains only one entry point, verify(), whose
responsibility is to abort the program if the ballot definition is not
well-formed. The intention is that, if execution continues after a call to
verify(), it should never abort thereafterāthat is: (a) verify() checks
all the assumptions about the ballot definition upon which the rest of
Pvote relies; and (b) the contents of the ballot definition data structures
are never changed after verify() is called.
. 1 def verify(ballot):
2 [groups, sprites] = [ballot.model.groups, ballot.video.sprites]
option sizes contains one list corresponding to each group; it will
collect all the sprites for the options in that group and all the slots in
which such options could be pasted (in option areas and review areas).
char sizes also contains one list for each group; it will collect all the
sprites for characters corresponding to write-in options in the group, as
well as all the slots in which such characters could be pasted (in review
areas). These lists will later be checked to ensure that the sizes of all
sprites match the sizes of all the slots into which they could be pasted.
3 option sizes = [[] for group in groups]
4 char sizes = [[] for group in groups]
The following lines ensure that the parallel arrays have matching size. It
also makes sure that they are also nonempty; for example, the navigator
assumes that there is at least one page when it starts up with a transition
to page 0.
5 assert len(ballot.model.groups) == len(ballot.text.groups) > 0
6 assert len(ballot.model.pages) == len(ballot.video.layouts) > 0
For each page, the list of bindings are checked. Each page also has to
have at least one state.
7 for [page i, page] in enumerate(ballot.model.pages):
8 layout = ballot.video.layouts[page i]
9 for binding in page.bindings:
10 verify binding(ballot, page, binding)
11 assert len(page.states) > 0
For each state, the segments and bindings are checked. The sprite is
checked to make sure it exactly fills its slot, and the timeout transition is
also checked for validity.
12 for [state i, state] in enumerate(page.states):
13 verify size(sprites[state.sprite i], layout.slots[state i])
14 verify segments(ballot, page, state.segments)
15 for binding in state.bindings:
16 verify binding(ballot, page, binding)
17 verify segments(ballot, page, state.timeout segments)
18 verify goto(ballot, state.timeout page i, state.timeout state i)
19 slot i = len(page.states)
Pvote source code 224
Page 238 of 324
Page 239 of 324
Each option area is checked for a valid option reference, and the option
slots are gathered into the appropriate array for later size checking.
20 for area in page.option areas:
21 verify option ref(ballot, page, area)
22 option sizes[area.group i].append(layout.slots[slot i])
23 slot i = slot i + 1
For each counter area, all the possible sprites that could be pasted are
checked to ensure they exactly fill the slot.
24 for area in page.counter areas:
25 for i in range(groups[area.group i].max sels + 1):
26 verify size(sprites[area.sprite i + i], layout.slots[slot i])
27 slot i = slot i + 1
For each review area, the slots for options and characters are gathered
into the appropriate array for later size checking. If there is a cursor
sprite, its size is expected to match the option slots as well.
28 for area in page.review areas:
29 for i in range(groups[area.group i].max sels):
30 option sizes[area.group i].append(layout.slots[slot i])
31 slot i = slot i + 1
32 for j in range(groups[area.group i].max chars):
33 char sizes[area.group i].append(layout.slots[slot i])
34 slot i = slot i + 1
35 if area.cursor sprite i != None:
36 option sizes[area.group i].append(sprites[area.cursor sprite i])
The sprites for all the options and characters are gathered into the
appropriate arrays. The audio clip indices for the options are ensured to
be within range. For write-in options, the number of allowed write-in
characters in the parent group is checked to ensure it matches the
number of allowed selections in the write-in group; thus, all the write-in
options in a group are required to accept the same number of characters.
Write-in groups are not themselves allowed to contain write-ins.
37 for [group i, group] in enumerate(groups):
38 for option in group.options:
39 option sizes[group i].append(sprites[option.sprite i])
40 option sizes[group i].append(sprites[option.sprite i + 1])
41 assert group.option clips > 0
42 ballot.audio.clips[option.clip i + group.option clips - 1]
43 if option.writein group i != None:
44 writein group = groups[option.writein group i]
45 assert writein group.max chars == 0
46 assert writein group.max sels == group.max chars > 0
47 for option in writein group.options:
48 char sizes[group i].append(sprites[option.sprite i])
The sprites and slots that have been collected for each group are now
checked to ensure they all have matching sizes.
49 for object in option sizes[group i]:
50 verify size(object, option sizes[group i][0])
51 for object in char sizes[group i]:
52 verify size(object, char sizes[group i][0])
Pvote source code 225
Page 239 of 324
Page 240 of 324
The text section is checked to ensure that every option has a name, and
ensure that the group names and option names have reasonable lengths
that will print properly.
53 for [group i, group] in enumerate(ballot.text.groups):
54 assert len(group.name) <= 50
55 assert len(group.options) == len(groups[group i].options)
56 for option in group.options:
57 assert len(option) <= 50
Every audio clip is checked to ensure that it has nonzero length. There is
no Pvote code that relies on this property; Pygame has the an
unfortunate limitation that the audio system will abort if asked to play a
zero-length sound.
58 for clip in ballot.audio.clips:
59 assert len(clip.samples) > 0
Finally, the video section is checked. The background images must match
the screen size, all the slots and targets must fit entirely onscreen, and
the image data for each sprite must match the spriteās claimed
dimensions.
60 assert ballot.video.width*ballot.video.height > 0
61 for layout in ballot.video.layouts:
62 verify size(layout.screen, ballot.video)
63 for rect in layout.targets + layout.slots:
64 assert rect.left + rect.width <= ballot.video.width
65 assert rect.top + rect.height <= ballot.video.height
66 for sprite in ballot.video.sprites:
67 assert len(sprite.pixels) == sprite.width*sprite.height*3 > 0
The verify binding() function checks that a binding is well-formed by
inspecting each of its parts: its list of conditions, its list of steps, its list
of audio segments, and its transition.
68 def verify binding(ballot, page, binding):
69 for condition in binding.conditions:
70 verify option ref(ballot, page, condition)
71 for step in binding.steps:
72 verify option ref(ballot, page, step)
73 verify segments(ballot, page, binding.segments)
74 verify goto(ballot, binding.next page i, binding.next state i)
The verify goto() function checks that the page index and state index
for a transition are within range. None is an allowed value for the page
index.
75 def verify goto(ballot, page i, state i):
76 if page i != None:
77 ballot.model.pages[page i].states[state i]
Pvote source code 226
Page 240 of 324
Page 241 of 324
The verify segments() function checks that a list of segments is
well-formed. It inspects each segmentās list of conditions and, based on
the segment type, ensures that all the possible corresponding indices of
audio clips are within range.
78 def verify segments(ballot, page, segments):
79 for segment in segments:
80 for condition in segment.conditions:
81 verify option ref(ballot, page, condition)
82 ballot.audio.clips[segment.clip i]
83 if segment.type in [1, 2, 3, 4]:
84 group = verify option ref(ballot, page, segment)
85 if segment.type in [1, 2]:
86 assert segment.clip i < group.option clips
87 if segment.type in [3, 4]:
88 ballot.audio.clips[segment.clip i + group.max sels]
ā¢
ā¢
ā¢
ā¢
Reviewers wanted to see meaningfully named constants here for the
enumerated values. They recommended that all the enumerated value
constants should be pulled out into a separate moduleāthus, for
example, the above code and the navigator code would refer to the
same set of SG * constants.
The verify option ref() function checks the validity of an (indirect
or direct) option reference in a condition, step, or segmentāall of these
types have a group i field and an option i field. If the group i field is
None, then option i must be the index of a valid option area on the
current page. Otherwise, group i and option i must be valid group
and option indices respectively. The group object is returned as a
convenience for verify segments(), which uses the group object for
other checks.
89 def verify option ref(ballot, page, object):
90 if object.group i == None:
91 area = page.option areas[object.option i]
92 return ballot.model.groups[area.group i]
93 ballot.model.groups[object.group i].options[object.option i]
94 return ballot.model.groups[object.group i]
The verify size() function ensures that two objects (sprites or slots)
have the same dimensions.
95 def verify size(a, b):
96 assert a.width == b.width and a.height == b.height
Pvote source code 227
Page 241 of 324
Page 242 of 324
Navigator.py
The first three lines set up constants corresponding to the three
enumerated types in the ballot model definition: OP * for step types,
SG * for audio segment types, and PR * for predicates in conditions.
1 [OP ADD, OP REMOVE, OP APPEND, OP POP, OP CLEAR] = range(5)
2 [SG CLIP, SG OPTION, SG LIST SELS, SG COUNT SELS, SG MAX SELS] = range(5)
3 [PR GROUP EMPTY, PR GROUP FULL, PR OPTION SELECTED] = range(3)
The navigator is initialized with access to the ballot model data
structure, audio driver, video driver, and printing module. It saves these
references locally, initializes an empty selection state, and begins the
voting session by transitioning to state 0 of page 0.
4 class Navigator:
. 5 def init (self, model, audio, video, printer):
6 self.model = model
7 [self.audio, self.video, self.printer] = [audio, video, printer]
8 self.selections = [[] for group in model.groups]
9 self.page i = None
10 self.goto(0, 0)
The goto() method transitions to a given state and page. It is called by
invoke() and timeout(). If the transition goes to the last page, the
voterās selections are committed. Any state transition (even a transition
back to the current state) triggers the playback of the stateās audio
segments; the play() method queues the audio instantaneously for later
playback. In the ballot definition, page i can be None to indicate that no
transition should occur; that case is accepted and handled here. Other
methods rely on goto() to always update the video display with a call to
update(), even if no state transition occurs.
11 def goto(self, page i, state i):
12 if page i != None and self.page i != len(self.model.pages) - 1:
13 if page i == len(self.model.pages) - 1:
14 self.printer.write(self.selections)
15 [self.page i, self.page] = [page i, self.model.pages[page i]]
16 [self.state i, self.state] = [state i, self.page.states[state i]]
17 self.play(self.state.segments)
18 self.update()
ā¢
ā¢
Reviewers found the logic of line 12 confusing, as it combines the āno
transitionā condition with the āalready committedā condition. They all
agreed that the navigator should have a flag that indicates whether
the votes have already been committed, and a separate method that
commits the votes and sets the flag. They also suggested that, to make
the commit condition more obvious, the navigator should start on page
1 and always commit on page 0.
Pvote source code 228
Page 242 of 324
Page 243 of 324
The update() method updates the video display based on the current
page, state, and selections. It tells the video driver to paste the pageās
background image over the entire screen, then lay the stateās sprite on
top of that, and finally fills in any option areas, counter areas, and review
areas on the page, in that order. The indices of the slots are assumed to
be arranged in sequential order, as described in Chapter 7; hence the
variable slot i is incremented in each loop and carried forward to the
next loop. Because review areas occupy a variable number of slots
depending on their group, the review area loop relies on the review()
method to return an appropriately incremented value for slot i.
19 def update(self):
20 self.video.goto(self.page i)
21 self.video.paste(self.state.sprite i, self.state i)
22 slot i = len(self.page.states)
23 for area in self.page.option areas:
24 unselected = area.option i not in self.selections[area.group i]
25 group = self.model.groups[area.group i]
26 option = group.options[area.option i]
27 self.video.paste(option.sprite i + unselected, slot i)
28 slot i = slot i + 1
29 for area in self.page.counter areas:
30 count = len(self.selections[area.group i])
31 self.video.paste(area.sprite i + count, slot i)
32 slot i = slot i + 1
33 for area in self.page.review areas:
34 slot i = self.review(area.group i, slot i, area.cursor sprite i)
The review() method fills in the appropriate sprites for a review area.
The arguments group i and cursor sprite i are parameters of the
review area; slot i should be the index of the review areaās first slot.
The main loop always runs group.max sels times to ensure that
slot i cannot go out of range, and that slot i is incremented by the
correct amount: max sels Ć (1 + max chars). Each selected option is
pasted into a slot, and then, if the option is a write-in option, a recursive
call to review() fills in the characters of the write-in. If a cursor sprite is
given, it is pasted into the slot just after the last selected option.
35 def review(self, group i, slot i, cursor sprite i):
36 group = self.model.groups[group i]
37 selections = self.selections[group i]
38 for i in range(group.max sels):
39 if i < len(selections):
40 option = group.options[selections[i]]
41 self.video.paste(option.sprite i, slot i)
42 if option.writein group i != None:
43 self.review(option.writein group i, slot i + 1, None)
44 if i == len(selections) and cursor sprite i != None:
45 self.video.paste(cursor sprite i, slot i)
46 slot i = slot i + 1 + group.max chars
47 return slot i
ā¢ The reviewers generally found this method to be the most confusing
part of the source code, because of its use of recursion and the
arithmetic involved in determining slot i. They suggested splitting
this into two methods such as review contest() and
review writein(); review contest() would call
review writein() when necessary. Even though there would be
substantial duplication between the two methods, the reviewers felt
that eliminating recursion was more important.
Pvote source code 229
Page 243 of 324
Page 244 of 324
The press() and touch() methods handle incoming events from the
main loop: press() handles keypresses and touch() handles screen
touches. Both methods scan through the bindings of the current state
and page, searching for a binding that matches the pressed key or
touched target and whose conditions are all satisfied. The first such
binding (and only the first such binding) is invoked with a call to the
invoke() method.
. 48 def press(self, key):
49 for binding in self.state.bindings + self.page.bindings:
50 if key == binding.key and self.test(binding.conditions):
51 return self.invoke(binding)
. 52 def touch(self, target i):
53 for binding in self.state.bindings + self.page.bindings:
54 if target i == binding.target i and self.test(binding.conditions):
55 return self.invoke(binding)
ā¢ Reviewers felt the method names press() and touch() were too
similar and could be made clearer.
The test() method evaluates a list of conditions and returns 1 only if all
the conditions are met. Each of the three predicate types is evaluated in a
separate clause; the cond.invert flag indicates whether to invert the
sense of an individual predicate.
56 def test(self, conditions):
57 for cond in conditions:
58 [group i, option i] = self.get option(cond)
59 if cond.predicate == PR GROUP EMPTY:
60 result = len(self.selections[group i]) == 0
61 if cond.predicate == PR GROUP FULL:
62 max = self.model.groups[group i].max sels
63 result = len(self.selections[group i]) == max
64 if cond.predicate == PR OPTION SELECTED:
65 result = option i in self.selections[group i]
66 if cond.invert == result:
67 return 0
68 return 1
ā¢
ā¢
ā¢
Reviewers felt the comparison of Boolean values on line 66 was ājust
too clever for its own good.ā They agreed that lines 66 and 67 could
have been more clearly written as
if cond.invert:
result = not result
if not result:
return 0
to show that cond.invert reverses the sense of the condition and that
the loop body returns 0 only when the condition is not met.
The invoke() method invokes a binding. The steps of the action are
carried out, then the audio for the binding is queued, and finally the
state transition, if any, takes place. (The goto() method handles the case
where next page i is None.) Invoking a binding always interrupts any
currently playing audio.
69 def invoke(self, binding):
70 for step in binding.steps:
71 self.execute(step)
72 self.audio.stop()
73 self.play(binding.segments)
74 self.goto(binding.next page i, binding.next state i)
Pvote source code 230
Page 244 of 324
Page 245 of 324
The execute() method executes a single step, which operates on the
selection state. It is responsible for ensuring that invalid selection states
are never reached.
75 def execute(self, step):
76 [group i, option i] = self.get option(step)
77 group = self.model.groups[group i]
78 selections = self.selections[group i]
79 selected = option i in selections
80 if step.op == OP ADD and not selected or step.op == OP APPEND:
81 if len(selections) < group.max sels:
82 selections.append(option i)
83 if step.op == OP REMOVE and selected:
84 selections.remove(option i)
85 if step.op == OP POP and len(selections) > 0:
86 selections.pop()
87 if step.op == OP CLEAR:
88 self.selections[group i] = []
ā¢
ā¢
Reviewers felt the Boolean expression on line 80 should be clarified
with parentheses.
ā¢ Reviewers found the execute() method more confusing than
necessary because it uses both the list self.selections and a local
variable selections that aliases a part of it. Mixing these two ways of
accessing the list makes it harder to reason about the code, because
each could have side-effects on the other. The method would be easier
to verify if it always accessed the list through just self.selections
or just selections.
ā¢ Reviewers felt the method names invoke() and execute() were too
similar and could be made clearer.
The timeout() method handles an inactivity timeout. It is called by the
main event loop.
. 89 def timeout(self):
90 self.play(self.state.timeout segments)
91 self.goto(self.state.timeout page i, self.state.timeout state i)
Pvote source code 231
Page 245 of 324
Page 246 of 324
The play() method plays a list of audio segments. Its job is to translate
a list of segments into a sequence of audio clip indices, and send these
indices to the audio driver to be queued for playing. Each segmentās
conditions are checked; if the conditions are met, the corresponding clip
index (or indices) are sent to the audio driver. After the clips are queued,
play() returns immediately; it does not wait for the audio to finish
playing, or even to start playing.
92 def play(self, segments):
93 for segment in segments:
94 if self.test(segment.conditions):
95 if segment.type == SG CLIP:
96 self.audio.play(segment.clip i)
97 else:
98 [group i, option i] = self.get option(segment)
99 group = self.model.groups[group i]
100 selections = self.selections[group i]
101 if segment.type == SG OPTION:
102 self.play option(group.options[option i], segment.clip i)
103 if segment.type == SG LIST SELS:
104 for option i in selections:
105 self.play option(group.options[option i], segment.clip i)
106 if segment.type == SG COUNT SELS:
107 self.audio.play(segment.clip i + len(selections))
108 if segment.type == SG MAX SELS:
109 self.audio.play(segment.clip i + group.max sels)
The play option() method sends audio clips for a given option to the
audio driver. There can be multiple clips associated with each option, as
dictated by the option clips field of its containing group; the offset
argument selects which one to play. For a write-in option, this entails
playing, in sequence, all the audio clips for the characters in the write-in.
Write-in characters are assumed to have only one clip each.
110 def play option(self, option, offset):
111 self.audio.play(option.clip i + offset)
112 if option.writein group i != None:
113 writein group = self.model.groups[option.writein group i]
114 for option i in self.selections[option.writein group i]:
115 self.audio.play(writein group.options[option i].clip i)
The get option() method is used by test(), execute(), and play()
to determine the specific group and option for a condition, step, or
segment respectively. Conditions, steps, and segments all have fields
named group i and option i that can refer to an option either directly
or indirectly. When group i is None, itās an indirect reference: option i
is the index of an option area on the current page. When group i is not
None, itās a direct reference: group i and option i specify the intended
option.
116 def get option(self, object):
117 if object.group i == None:
118 area = self.page.option areas[object.option i]
119 return [area.group i, area.option i]
120 return [object.group i, object.option i]
Pvote source code 232
Page 246 of 324
Page 247 of 324
Audio.py
Audio playback is provided by the pygame library.
1 import pygame
Pygame is based on an event-loop control model. Instead of invoking
callbacks, Pygame queues events for processing by the application. Each
event has an integer type ID, and Pygame supports user-defined events
with type IDs equal to pygame.USEREVENT or higher. This module uses
AUDIO DONE for signalling when an audio clip has finished playing.
2 AUDIO DONE = pygame.USEREVENT
ā¢
ā¢
Reviewers suggested that constants like these all be collected in a
separate module, and that main.py and Audio.py refer to the same
AUDIO DONE constant instead of redundantly defining it in both files.
The Audio class is responsible for maintaining a queue of audio clips and
causing them to be played in sequence. It ensures that only one clip is
playing at a time, and that all the clips are played back one after another
until the queue is empty.
3 class Audio:
The audio driver is initialized with access to the audio section of the
ballot definition. It initializes the Pygame audio mixer and converts all
the audio clips from raw data into Pygame Sound objects. The playing
flag is exposed to the main program; it indicates whether or not audio is
currently playing.
. 4 def init (self, audio):
5 rate = audio.sample rate
6 pygame.mixer.init(rate, -16, 0)
7 self.clips = [make sound(rate, clip.samples) for clip in audio.clips]
8 [self.queue, self.playing] = [[], 0]
The play() method puts a single audio clip on the queue. If nothing is
currently playing, playback of the given audio clip immediately begins.
. 9 def play(self, clip i):
10 self.queue.append(clip i)
11 if not self.playing:
12 self.next()
The next() method takes the next available audio clip off of the queue
and starts playing it. The AUDIO DONE event is scheduled to be posted
when the audio clip finishes playing. The playing member is set to a
nonzero value if and only if an audio clip is playing.
. 13 def next(self):
14 self.playing = len(self.queue)
15 if len(self.queue):
16 self.clips[self.queue.pop(0)].play().set endevent(AUDIO DONE)
The stop() method stops audio playback and cancels pending audio.
. 17 def stop(self):
18 self.queue = []
19 pygame.mixer.stop()
Pvote source code 233
Page 247 of 324
Page 248 of 324
The make sound() function converts a string of audio data into a
Pygame Sound object. Because Pygame only knows how to load sounds
from files, and the only uncompressed sound format that Pygame
accepts is the Microsoft WAVE format, we have to construct a fake file
object with a WAVE file header. The header always specifies no
compression, monaural audio, and signed 16-bit samples.
20 def make sound(rate, data):
21 [comp channels, sample size] = [”\x01\x00\x01\x00″, “\x02\x00\x10\x00″]
22 fmt = comp channels + put int(rate) + put int(rate*2) + sample size
23 file = chunk(”RIFF”, “WAVE” + chunk(”fmt “, fmt) + chunk(”data”, data))
24 return pygame.mixer.Sound(Buffer(file))
The chunk() function creates a RIFF chunk, which consists of a 4-byte
type code and a 4-byte length followed by a string of data.
25 def chunk(type, contents):
26 return type + put int(len(contents)) + contents
The put int() function converts an integer into a 4-byte big-endian
representation.
27 def put int(n):
28 [a, b, c, d] = [n/16777216, n/65536, n/256, n]
29 return chr(d % 256) + chr(c % 256) + chr(b % 256) + chr(a % 256)
The Buffer class is a thin wrapper that makes a string look like a
readable file. make sound() wraps this class around the WAVE formatted
audio data so it can be passed to Pygame to create a Sound object.
30 class Buffer:
31 def init (self, data):
32 [self.data, self.pos] = [data, 0]
33 def read(self, length):
34 self.pos = self.pos + length
35 return self.data[self.pos - length:self.pos]
Pvote source code 234
Page 248 of 324
Page 249 of 324
Video.py
Video display control is provided by the pygame library.
1 import pygame
The make image() function converts a string containing uncompressed
pixel data into a Pygame Image object.
2 def make image(im):
3 return pygame.image.fromstring(im.pixels, (im.width, im.height), “RGB”)
The Video class is responsible for pasting full-screen images and sprites
onto the display, as well as translating touch locations into target indices.
4 class Video:
The video driver is initialized with access to the video section of the
ballot definition. It initializes the Pygame display and converts all the
images from raw data into Pygame Image objects. The video driver keeps
a pointer to the current layout in its layout member so it can look up
slots and targets for the current page.
. 5 def init (self, video):
6 size = [video.width, video.height]
7 self.surface = pygame.display.set mode(size, pygame.FULLSCREEN)
8 self.layouts = video.layouts
9 self.screens = [make image(layout.screen) for layout in video.layouts]
10 self.sprites = [make image(sprite) for sprite in video.sprites]
11 self.goto(0)
The goto() method switches to a given layout, which involves pasting
the layoutās background image over the entire screen.
. 12 def goto(self, layout i):
13 self.layout = self.layouts[layout i]
14 self.surface.blit(self.screens[layout i], [0, 0])
The paste() method pastes a given sprite into a given slot. The slot
coordinates are looked up in the current layout.
. 15 def paste(self, sprite i, slot i):
16 slot = self.layout.slots[slot i]
17 self.surface.blit(self.sprites[sprite i], [slot.left, slot.top])
The locate() method finds the target index corresponding to a given
touch location. It returns the index of the first enclosing target in the
current layout.
. 18 def locate(self, x, y):
19 for [i, target] in enumerate(self.layout.targets):
20 if target.left <= x and x < target.left + target.width:
21 if target.top <= y and y < target.top + target.height:
22 return i
Pvote source code 235
Page 249 of 324
Page 250 of 324
Printer.py
The Printer class commits the voterās selections by printing them out.
(Other vote-recording mechanisms could be substituted for this module.)
It is initialized with access to the text section of the ballot definition.
1 class Printer:
2 def init (self, text):
3 self.text = text
The write() method does the printing, assuming that the standard
output stream is connected to a printer. To prevent any possibility of
ambiguous output, the first character of every printed line indicates its
purpose, and lines never wrap. An asterisk (*) marks a contest, and a
minus sign (-) marks an option. A plus sign (+) marks a write-in group,
and an equals sign (=) marks the text of the write-in. A tilde (~) is printed
after the name of each write-in character because characters can have
names of any length (a feature intended to let ASCII printouts describe
write-ins containing non-ASCII characters.) A tilde on a line by itself
marks the end of the printout. Here is an example of a printout:
* Governor
- Peter Miguel Camejo
* Secretary of State ~ NO SELECTION
* Member of City Council
- William “Bill” G. Glynn
- Write-in 1
+ Member of City Council, Write-in 1
= S~T~E~P~H~E~N~ ~H~A~W~K~I~N~G~
* Proposition 1A
- Yes
~
. 4 def write(self, selections):
5 for [group i, selection] in enumerate(selections):
6 group = self.text.groups[group i]
7 if group.writein:
8 if len(selection):
9 print “\n+ ” + group.name
10 line = “”
11 for option i in selection:
12 if len(line) + len(group.options[option i]) + 1 > 60:
13 print “= ” + line
14 line = “”
15 line = line + group.options[option i] + “~”
16 print “= ” + line
17 else:
18 if len(selection):
19 print “\n* ” + group.name
20 for [option i, option] in enumerate(group.options):
21 if option i in selection:
22 print “- ” + option
23 else:
24 print “\n* ” + group.name + ” NO SELECTION”
25 print “\n~\f”
Pvote source code 236
Page 250 of 324
Page 251 of 324
C Sample Pvote ballot definition
This appendix describes the construction of a ballot definition
file for Pvote (the same ballot file mentioned on page 133). It is
based on ballot style #167 for the November 2006 election in
Contra Costa County, California. The paper ballot has 16
elected offices, 12 judicial confirmations, and 16 referenda.
This ballot definition just contains the first two state offices
(Governor and Secretary of State), one local office (City Council),
and two state measures (Propositions 1A and 1B).
This sample ballot definition is not intended to serve as an
example of optimally usable or optimally accessible ballot
design. It is merely intended to demonstrate a few different
interaction models that are achievable with Pvote, and to make
a plausible case that it is possible to design a single ballot
definition file that works for voters who use only the visual
interface, voters who use only the audio interface, or voters who
use the visual and audio interfaces together.
Audio messages are shown in a sans-serif typeface. Boxes
indicate variable parts of the message. When a series of boxes
are joined by dashes, one box in the series is played depending
on the voterās current selections. A box can also contain text in
italics describing the message to be played. Here is an example:
Please vote for one. No choices are currently selected.
Your current selection is list of selected options .
The above describes an audio message consisting of:
ā¢ First, the spoken message āPlease vote for one.ā
ā¢ Then, either the spoken message āNo choices are currently
selected.ā or the message āYour current selection is.ā
ā¢ Finally, a spoken list of the selected options.
237
Page 251 of 324
Page 252 of 324
There are 10 groups and 17 pages in this ballot definition. The groups are as follows.
Group 0. This is the contest for Governor, with max sels = 1, max chars = 25, and
option clips = 2. It contains 7 options. There are two sprites for each option:
Each option has two associated audio clips, for a short and a long spoken description. For
example, option 0 has the two clips:
ā¢ Phil Angelides
ā¢ Phil Angelides. Democratic Party. Treasurer of the State of California.
The last option, option 6, has writein group = 1; the rest have writein group = None.
Group 1. This is the write-in group for the Governor contest, with max sels = 25,
max chars = 0, and option clips = 1. It has 29 options, with the sprites:
Each option has one associated audio clip with the name of the character (the names of
the letters of the alphabet and the spoken words āhyphenā, āapostropheā, and āspaceā).
Sample Pvote ballot definition 238
Page 252 of 324
Page 253 of 324
Group 2. This is the contest for Secretary of State, with max sels = 1, max chars = 25,
and option clips = 2. It contains 7 options, with two sprites for each option:
Just as in group 0, each option has two associated audio clips giving a short and a long
spoken description. The last option, option 6, has writein group = 3; the rest have
writein group = None.
Group 3. This is the write-in group for the Secretary of State contest, with max sels = 25,
max chars = 0, and option clips = 1. It has the same options as group 1.
Group 4. This is the contest for City Council, with max sels = 3, max chars = 25, and
option clips = 2. It contains 8 options, with two sprites for each option:
Sample Pvote ballot definition 239
Page 253 of 324
Page 254 of 324
Just as in groups 0 and 2, each option has two associated audio clips giving a short and a
long spoken description. Each of the last three options has its own write-in group: option
5 has writein group = 5, option 6 has writein group = 6, and option 7 has
writein group = 7. The rest of the options have writein group = None.
Groups 5, 6, and 7. These are the write-in groups for the three write-in options in the City
Council contest. All of them have max sels = 25, max chars = 0, option clips = 1, and
the same options as group 1.
Group 8. This is the contest for Proposition 1A, with max sels = 1, max chars = 0, and
option clips = 2. It contains 2 options, with two sprites for each option:
Option 0 has two audio clips that both say āyesā; option 1 has two audio clips that both
say ānoā. (The redundant audio clips are unnecessary; this is just due to the current ballot
compilerās assumption that every option has a short and a long audio description.) Both
options have writein group = None.
Group 9. This is the contest for Proposition 1B, with max sels = 1, max chars = 0, and
option clips = 2. It contains the same options as group 8.
Sample Pvote ballot definition 240
Page 254 of 324
Page 255 of 324
Page 0. This is the screen image for layout 0.
Page 0 has just one state, state 0, with the following audio message:
This is the General Election for Tuesday, November 7, 2006, Contra Costa County,
California. To begin, touch NEXT in the lower-right corner of the screen. There is also
a number keypad directly below the screen. The numbers are arranged like a
telephone, with 1, 2, and 3 in the top row, 4, 5, and 6 in the second row, 7, 8, and 9 in
the third row, and 0 in the bottom row. To begin, press 6.
There is a target positioned over the NEXT button; the 6 key and this target are both
bound to a transition to page 1. (When no state is mentioned, state 0 is implied.)
Throughout the ballot, the arrangement of keypad controls is loosely associated with
directional movement. The 4 and 6 keys (left and right) always navigate to the previous
and next page; the 2 and 8 keys (up and down) navigate to the previous and next item on
the page; and the 5 key (in the center) selects or activates the current item.
Sample Pvote ballot definition 241
Page 255 of 324
Page 256 of 324
Page 1. This is the screen image for layout 1.
Page 1 has just one state, state 0, with the following audio message:
Touch the screen to make your selections. Use the NEXT and PREVIOUS buttons below
to move from page to page. To continue, touch NEXT or press 6 on the number
keypad.
There are targets positioned over the PREVIOUS and NEXT buttons. The 6 key and the
NEXT target are bound to a transition to page 2. The 4 key and the PREVIOUS target are
bound to a transition to page 0.
Sample Pvote ballot definition 242
Page 256 of 324
Page 257 of 324
Page 2. This is the screen image for layout 2.
Page 2 demonstrates one possible way to present a single-selection contest. Touching any
item changes the selection to that item, automatically deselecting any previous selection.
The voter can also step through the options one by one. using the audio interface and
keypad buttons. For voters who are using the visual and audio interfaces together,
selecting an option by touchscreen also produces audio confirmation, and the options are
also visually highlighted when the keypad buttons are used to step through them.
Page 2 has 8 states. State 0 has the following audio message:
State. Governor. There are 6 candidates. Please vote for one.
No choices are currently selected. Your current selection is list of selected options .
Touch the screen to make selections or press 8 to hear the choices. To skip to the
next contest, press 6.
The number of selections determines whether No choices… or Your current… is played.
Sample Pvote ballot definition 243
Page 257 of 324
Page 258 of 324
In state 0, the 8 key is bound to a transition to state 1. States 1 through 7 correspond to
the seven options for Governor. Each state highlights an option with a dotted red box. For
example, state 1 places this sprite over the first option:
Each of the states 1 through 6 has an audio message of the form:
candidate name . This choice is currently selected. To select this choice, press 5.
To hear the next choice, press 8. To hear your current selections for Governor, press
3. To clear your selections for Governor, press 1.
This choice… or To select… is played depending on whether the option is selected. In
these states, the 8 and 2 keys transition to the next and previous states. The 5 key clears
groups 0 and 1, selects the highlighted option, and plays the audio message:
Selected candidate name for Governor.
State 7, in which the last option is highlighted, has the audio message:
Write-in candidate.
This choice is currently selected. To edit or cancel this write-in, press 5.
To write in a name, press 5. To hear all the choices again, press 4. To hear your
current selections for governor, press 3. To clear your selections for governor, press 1.
This choice… or To write in… is played depending on whether the option is selected. In
this state, the 5 key transitions to page 11, which is the write-in page for Governor.
Page 2 has 7 option areas, located over the 7 choices for governor. Each of the first six
option areas has a corresponding target that clears groups 0 and 1 and then selects the
option. There is a target positioned over the last option that transitions to page 11, which
is the write-in entry page for Governor. The page also has a review area for group 1, with
25 small slots arranged in a row over the last option. This review area displays the entered
text for the write-in candidate. When the write-in candidate has been selected, the
highlighted sprite (with the check mark and green background) is pasted over the last
option, and the review area causes the entered characters to be pasted on top of that.
Sample Pvote ballot definition 244
Page 258 of 324
Page 259 of 324
There is a page-wide binding for the 1 key that clears groups 0 and 1 and plays the audio
message:
The selections for Governor are now cleared.
There is also a page-wide binding for the 3 key that triggers the audio message:
Governor. No choices are currently selected. Your current selection is
list of selected options .
There are targets positioned over the PREVIOUS and NEXT buttons. The 6 key and the
NEXT target are bound to a transition to page 3. The 4 key and the PREVIOUS target are
bound to a transition to page 1.
The page also has one counter area, positioned over the NEXT button. This is a counter
area for group 0, and its sprites look like this:
This counter area demonstrates one way of alerting voters when they proceed to the next
contest without making a selection. When the number of selections is zero, the NEXT
button is visually replaced with the SKIP CONTEST image; its behaviour is unchanged.
Sample Pvote ballot definition 245
Page 259 of 324
Page 260 of 324
Page 3. This is the screen image for layout 3.
Page 3 has 8 states. State 0 has the following audio message:
State. Secretary of State. There are 6 candidates. Please vote for one.
No choices are currently selected. Your current selection is list of selected options .
Touch the screen to make selections or press 8 to hear the choices. To skip to the
next contest, press 6. To go back to the previous contest, press 4.
The structure of the page is the same as page 2: states 1 through 7 highlight each of the
options, and they have the similar bindings and audio messages to those on page 2. There
are 7 option areas with corresponding targets that select them, and a review area for the
write-in characters in group 3, positioned over the last option. Selecting the write-in
option transitions to page 12, the write-in page for Secretary of State. There are targets
positioned over the PREVIOUS and NEXT buttons, with a counter area over the NEXT
button to replace it with a SKIP CONTEST image. The 6 key and the NEXT target go to
page 4; the 4 key and the PREVIOUS target go to page 2.
Sample Pvote ballot definition 246
Page 260 of 324
Page 261 of 324
Page 4. This is the screen image for layout 4.
Page 4 demonstrates a possible way of presenting a multiple-selection contest. Touching
an option toggles whether it is selected or not, except that overvoting is prevented;
attempting to overvote yields an audio explanation.
Page 4 has 9 states. State 0 has the following audio message:
City of Pittsburg. Member of City Council. There are 5 candidates. Please vote for up
to 3. No choices are currently selected. Your current selection is
Your current selections are list of selected options . Touch the screen to make
selections or press 8 to hear the choices. To skip to the next contest, press 6. To go
back to the previous contest, press 4.
The current number of selections determines which of the three clips are played:
No choices… , Your current selection is , or Your current selections are . In state 0, the 8
key is bound to a transition to state 1.
Sample Pvote ballot definition 247
Page 261 of 324
Page 262 of 324
States 1 through 8 correspond to the eight options. Because up to three selections are
allowed in this contest, there are three write-in options. Each state highlights an option
with a dotted red box, just like the pages for Governor and Secretary of State.
Each of the states 1 through 5 has an audio message of the form:
candidate name . To select this choice, press 5.
This choice is currently selected. To deselect it, press 5.
The maximum number of choices is currently selected. If you want to select more
choices, you must first deselect a choice.
If you are done with this contest, press 6. To hear the next choice, press 8. To hear
your current selections for Member of City Council, press 3. To clear your selections
for Member of City Council, press 1.
To select… is played if the option is not selected and the group is not full; This choice…
is played if the option is selected; and The maximum… is played if the option is not
selected and the group is full. In these states, the 8 key goes to the next state and the 2
key goes to the preceding state. If the highlighted option is selected, the 5 key deselects it
and plays the message:
Deselected candidate name for Member of City Council.
If the option isnāt selected and the group is not full, the 5 key selects it and plays:
Selected candidate name for Member of City Council.
If the option isnāt selected and the group is full, the 5 key plays the audio message:
You may only vote for up to 3 choices for Member of City Council. To vote for this
choice, you must deselect another choice first. Your current selections are
list of selected options .
States 6, 7, and 8, which correspond to the write-in options, have the audio message:
Write-in candidate. To write in a name, press 5.
This write-in is currently selected. To edit or cancel this write-in, press 5.
The maximum number of choices is currently selected. If you want to select more
choices, you must first deselect a choice.
Sample Pvote ballot definition 248
Page 262 of 324
Page 263 of 324
If you are done with this contest, press 6. To hear the next choice, press 8. To hear
your current selections for Member of City Council, press 3. To clear your selections
for Member of City Council, press 1.
As with states 1 through 5, To write in… is played if the option is not selected and the
group is not full; This choice… is played if the option is selected; and The maximum… is
played otherwise. The 8 and 2 keys navigate between states. If the option is selected, or if
it isnāt selected and the group is not full, the 5 key jumps to the corresponding write-in
page (page 13, 14, or 15). If the option isnāt selected and the group is full, the 5 key
produces the same message as in states 1 through 5:
You may only vote for up to 3 choices for Member of City Council. To vote for this
choice, you must deselect another choice first. Your current selections are
list of selected options .
Page 4 has 8 option areas, located over the 8 choices for City Council. Each of the option
areas has a target with a page-wide binding just like the binding described above for the 5
key in states 1 through 8. The page has 3 review areas located over the last three options;
these are for groups 5, 6, and 7, the write-in groups for this contest.
Just like pages 2 and 3, there are targets positioned over the PREVIOUS and NEXT buttons,
with a counter area over the NEXT button to replace it with a SKIP CONTEST image. The 6
key and the NEXT button go to page 5; the 4 key and the PREVIOUS button go to page 3.
Sample Pvote ballot definition 249
Page 263 of 324
Page 264 of 324
Page 5. This is the screen image for layout 5.
Page 5 demonstrates one way to present a contest with a small, fixed number of choices.
This example is a referendum with only two choices, so itās possible to map them directly
to two buttons instead of highlighting each choice in a separate state. A non-touchscreen
user can choose an option just by pressing the button for that option, instead of stepping
through the options to find the desired one.
Page 5 has 3 states. State 0 has the following audio message:
State Measures. Proposition 1A. No choices are currently selected.
Your current selection is list of selected options . To hear the full text of this
proposition, press 8. Touch your selection on the screen, or, to select yes, press 7; to
select no, press 9.
In state 0, the 8 key transitions to state 1.
Sample Pvote ballot definition 250
Page 264 of 324
Page 265 of 324
State 1 has the audio message:
Transportation funding protection. Legislative constitutional amendment. Protects
transportation funding… text of paragraph describing proposition …in 2007 and
thereafter. To hear the text of this proposition again, press 8. Touch your selection on
the screen, or, to select yes, press 7; to select no, press 9.
In state 1, the 8 key transitions back to state 1, which causes the audio message to repeat.
There are two option areas on the page, one for YES and one for NO. There are two
targets, one located over each option, and page-wide bindings for the 7 and 9 keys. The 7
key and the YES target clear the contest (group 9) and select option 0 for yes; the 9 key
and the NO target clear the contest (group 9) and select option 1 for no. Both keys and
both targets trigger the audio message:
Selected option name on Proposition 1A.
As on the preceding pages, there are targets positioned over the PREVIOUS and NEXT
buttons, with a counter area over the NEXT button to replace it with a SKIP CONTEST
image. The 6 key and the NEXT target go to page 6; the 4 key and the PREVIOUS target go
to page 4.
Sample Pvote ballot definition 251
Page 265 of 324
Page 266 of 324
Page 6. This is the screen image for layout 6.
Page 6 has 2 states. State 0 has the following audio message:
State Measures. Proposition 1B. No choices are currently selected.
Your current selection is list of selected options . To hear the full text of this
proposition, press 8. Touch your selection on the screen, or, to select yes, press 7; to
select no, press 9.
The structure of the page is the same as page 5: the 8 key transitions to state 1, with an
audio message that reads out the text of the onscreen description. The 7 and 9 keys and
YES and NO buttons work as on page 5. There are targets positioned over the PREVIOUS
and NEXT buttons, with a counter area over the NEXT button to replace it with a SKIP
CONTEST image. The 6 key and the NEXT target go to page 7; the 4 key and the
PREVIOUS target go to page 5.
Sample Pvote ballot definition 252
Page 266 of 324
Page 267 of 324
Page 7. This is the screen image for layout 7.
Pages 7, 8, and 9 allow the voter to review selections before casting the ballot. A voter
using the audio interface can step through all the contests (automatically skipping from
the end of one page to the beginning of the next) by repeatedly pressing the 8 key.
Page 7 has 3 states. State 0 has the following audio message:
Review your selections before casting your ballot. To change your selections for any
contest, touch that contest on the screen. Use the NEXT and PREVIOUS buttons to
move from page to page. Or, to hear your selections read back to you, press 8.
In state 0, the 8 key transitions to state 1, which has the audio message:
Governor. You have not made a selection for this contest. Your current selection is
list of selected options . To make a selection To change your selection , press 5. For
the next contest, press 8.
Sample Pvote ballot definition 253
Page 267 of 324
Page 268 of 324
State 1 highlights the Governor contest with a dotted red box by placing this sprite over it:
In state 1, the 5 key transitions to state 0 of page 2, and the 8 key transitions to state 2 of
page 7. State 2 has the audio message:
Secretary of State. You have not made a selection for this contest.
Your current selection is list of selected options . To make a selection
To change your selection , press 5. For the next contest, press 8. For the previous
contest, press 2.
State 2 highlights the second contest with its sprite:
In state 2, the 5 key transitions to state 0 of page 3, the 8 key transitions to state 1 of page
8, and the 2 key transitions to state 1 of page 7.
The page has two review areas: one for group 0, positioned to overlay the box under
āGovernorā, and one for group 2, positioned to overlay the box under āSecretary of State.ā
Thus, when there is no selection, the NO SELECTION MADE message shows through from
the background; when there is a selection, it covers up the NO SELECTION MADE
message. There is a target positioned over each of the two contests; these targets
transition to pages 2 and 3 respectively. There are also targets positioned over the
PREVIOUS and NEXT buttons. The 6 key and the NEXT target go to page 8; the 4 key and
the PREVIOUS target go to page 6.
Sample Pvote ballot definition 254
Page 268 of 324
Page 269 of 324
Page 8. This is the screen image for layout 8.
Page 8 shows just one contest. (On a larger ballot, there could be many contests on each
review page.)
Page 8 has 2 states. State 0 has the same audio message as page 7:
Review your selections before casting your ballot. To change your selections for any
contest, touch that contest on the screen. Use the NEXT and PREVIOUS buttons to
move from page to page. Or, to hear your selections read back to you, press 8.
In state 0, the 8 key transitions to state 1, which has the audio message:
Member of City Council. You have not made a selection for this contest.
Your current selection is Your current selections are list of selected options .
To make a selection To change your selection , press 5. For the next contest, press
8. For the previous contest, press 2.
Sample Pvote ballot definition 255
Page 269 of 324
Page 270 of 324
State 1 highlights the City Council contest with its sprite:
In state 1, the 5 key transitions to state 0 of page 4, the 8 key transitions to state 1 of page
9, and the 2 key transitions to state 2 of page 7.
The page has one review area for group 4, with its three slots positioned to overlay the
three boxes under āMember of City Council.ā When there are fewer than three selections
in group 4, one of the NO SELECTION MADE messages will show through. There is one
target positioned over this review area that transitions to page 4, as well as two targets
positioned over the PREVIOUS and NEXT buttons. The 6 key and the NEXT target go to
page 9; the 4 key and the PREVIOUS target go to page 7.
Sample Pvote ballot definition 256
Page 270 of 324
Page 271 of 324
Page 9. This is the screen image for layout 9.
Page 9 has 3 states. State 0 has the same audio message as the previous two pages. States
1 and 2 correspond to the two propositions; each one highlights a proposition and reads
back the selection for that proposition, similar to the previous two pages. In state 1, the 5
key transitions to state 0 of page 5, the 8 key transitions to state 2 of page 9, and the 2
key transition to state 1 of page 8. In state 2, the 5 key transitions to state 0 of page 6, the
2 key transitions to state 1 of page 9, and the 8 key produces the audio message:
This is the last contest. To proceed with casting your ballot, press 6.
The page has two review areas positioned over the two boxes for Propositions 1A and 1B,
for group 8 and group 9 respectively, and targets over these regions that transition to
page 5 and page 6 respectively. For the whole page, the 6 key and the NEXT target go to
page 10; the 4 key and the PREVIOUS target go to page 8.
Sample Pvote ballot definition 257
Page 271 of 324
Page 272 of 324
Page 10. This is the screen image for layout 10.
Page 10 is the final confirmation page before casting the ballot; it has just one state. State
0 has the audio message:
This is your last chance to review your selections before casting your ballot. To review
your selections, press 1. To cast your ballot now, press 0.
The 1 key and the REVIEW button transition to page 7. The 0 key and the CAST BALLOT
button transition to page 16. The 4 key and the PREVIOUS button transition to page 9.
Sample Pvote ballot definition 258
Page 272 of 324
Page 273 of 324
Page 11. This is the screen image for layout 11.
Pages 11 through 15 are pages for entering write-in candidates, corresponding to the
write-in options in the Governor contest (1 write-in option), the Secretary of State contest
(1 write-in option), and the City Council contest (3 write-in options). The voter can enter
characters either by touching them on the screen or by using the keypad to step through
the alphabet. The voter leaves the write-in page by either accepting or cancelling the
write-in, which selects or deselects the corresponding write-in option.
Page 11 has 30 states. State 0 has the audio message:
Write-in candidate for Governor. This write-in is empty. This write-in contains
list of selected characters . To write in a name, touch the letters on the screen.
To edit this write-in, touch the letters on the screen. To delete the last letter, touch
BACKSPACE or press 1.
Touch ACCEPT when you are finished, or touch CANCEL to cancel this write-in. Or, to
advance through the alphabet using the keypad, press 6.
Sample Pvote ballot definition 259
Page 273 of 324
Page 274 of 324
Whether the write-in is empty determines whether This write-in is empty. or
This write-in contains is played, and also whether To write in a name… or
To edit this write-in… is played. The 6 key advances to state 1.
State 1 highlights the A button with this sprite:
and has the audio message:
A. To add this letter to the write-in, press 5. To delete the last letter, press 1. To
advance to the next letter of the alphabet, press 6. For the previous letter, press 4. To
read back the letters you have entered, press 3. To accept this write-in, press 7. To
cancel this write-in, press 9.
The name of the letter is spoken first so that the voter can quickly scan through the
alphabet using the 6 and 4 keys to interrupt the message and navigate to the next and
previous letters. The 7 and 9 keys express affirmative and negative actions, somewhat
consistent with their use to select YES and NO on pages 5 and 6. the 1 key is used for
deletion, somewhat consistent with its use to clear selections in other contests. And the 3
key is used to request a playback of selections, as it does on other pages.
States 2 through 29 highlight each of the other character buttons from B through SPACE,
and they have similar audio messages. In all of these states, the 5 key appends the
character to the group, the 1 key removes the last character, and the 6 and 4 keys
transition to the next and previous state. In state 1, the 4 key goes to state 29; in state 29,
the 6 key goes to state 1. If the group is not full, the 5 key appends the highlighted
character to the group and plays the name of the character. If the group is full, the 5 key
produces the audio message:
There is no room for more letters.
The page has one review area with 25 slots in a row over the green box at the top of the
page. This review area shows the characters selected in group 1 and has a cursor sprite:
Sample Pvote ballot definition 260
Page 274 of 324
Page 275 of 324
There are targets for each of the 29 letter buttons; each target is bound to the same action
as the 5 key for that button (either it appends the character or notifies the voter that there
is no more room).
There are targets over the CLEAR and BACKSPACE buttons. The CLEAR button clears the
group and plays the audio message:
Clear.
If the group is empty, the 1 key and the BACKSPACE target just play the message:
This write-in is empty.
Otherwise, the 1 key and the BACKSPACE target remove the last character from the group.
There is a page-wide binding for the 3 key that plays the audio message:
This write-in is empty. This write-in contains list of selected characters .
There are also targets over the ACCEPT and CANCEL buttons. If the group is empty, the 7
key and the ACCEPT target just play the message:
This write-in is empty.
Otherwise, they clear group 0 (the contest for Governor) and select option 6 in group 0
(the write-in option for Governor), transition back to page 2, and play the message:
Selected write-in candidate list of characters for Governor.
The 9 key and the CANCEL target clear group 1 (this write-in group) remove option 6 from
group 0 (the write-in option for Governor), transition back to page 2, and play the
message:
Cancelled write-in.
Sample Pvote ballot definition 261
Page 275 of 324
Page 276 of 324
Page 12. This is the screen image for layout 12.
Page 12 has 30 states, like page 11. State 0 has the audio message:
Write-in candidate for Secretary of State. This write-in is empty.
This write-in contains list of selected characters .
To write in a name, touch the letters on the screen.
To edit this write-in, touch the letters on the screen. To delete the last letter, touch
BACKSPACE or press 1.
Touch ACCEPT when you are finished, or touch CANCEL to cancel this write-in. Or, to
advance through the alphabet using the keypad, press 6.
The page has the same structure as page 11, except that it corresponds to group 3 (the
write-in group for Secretary of State) and to option 6 of group 2 (the write-in option for
Secretary of State), and transitions back to page 3 when the write-in is accepted or
cancelled.
Sample Pvote ballot definition 262
Page 276 of 324
Page 277 of 324
Page 13. This is the screen image for layout 13.
Page 13 has 30 states, like the other write-in pages. State 0 has the audio message:
Write-in candidate for Member of City Council. This write-in is empty.
This write-in contains list of selected characters .
To write in a name, touch the letters on the screen.
To edit this write-in, touch the letters on the screen. To delete the last letter, touch
BACKSPACE or press 1.
Touch ACCEPT when you are finished, or touch CANCEL to cancel this write-in. Or, to
advance through the alphabet using the keypad, press 6.
This page has the same structure as pages 11 and 12, except that it corresponds to group
5 (the first write-in group for Member of City Council) and to option 5 of group 4 (the first
write-in option for Member of City Council), and transitions back to page 4 when the
write-in is accepted or cancelled. When the write-in is accepted, group 4 is not cleared;
option 5 is just added to the selections for group 4 since there can be multiple selections.
Sample Pvote ballot definition 263
Page 277 of 324
Page 278 of 324
Page 14. This is the screen image for layout 14.
Page 14 is identical to page 13 except that it corresponds to group 6 (the second write-in
group for Member of City Council) and to option 6 of group 4 (the second write-in option
for Member of City Council).
Sample Pvote ballot definition 264
Page 278 of 324
Page 279 of 324
Page 15. This is the screen image for layout 15.
Page 15 is identical to pages 13 and 14 except that it corresponds to group 7 (the third
write-in group for Member of City Council) and to option 7 of group 4 (the third write-in
option for Member of City Council).
Sample Pvote ballot definition 265
Page 279 of 324
Page 280 of 324
Page 16. This is the screen image for layout 16.
Page 16 is the last page; transitioning here casts the ballot. There is just one state, and it
has the audio message:
Thank you for voting. Your ballot has been recorded. sound of applause
There are no bindings on this page.
Sample Pvote ballot definition 266
Page 280 of 324
Page 281 of 324
D Sample Pvote ballot designs
This appendix presents a few other possible designs for
electronic ballots that could work with Pvote, to illustrate the
flexibility of Pvote to handle other visual appearances and
interaction styles.
267
Page 281 of 324
Page 282 of 324
An alternate visual design.
This is an example of a selection page with a different ālook and feelā than the sample
ballot in Appendix C. The video display has a different resolution (640 Ć 480 pixels), and
the buttons appear shiny instead of flat. Square buttons are used for options and rounded
buttons are used for navigation.
In Pvote, this design can be implemented just by drawing different full-screen images
for each page and providing option sprites that match the new ālook and feel.ā For
example, when the YES and NO options are selected, they can be overlaid with these
sprites:
Sample Pvote ballot designs 268
Page 282 of 324
Page 283 of 324
Random-access navigation.
This design offers a high-level overview of the ballot, always visible on the left third of the
display. The overview region allows the voter to jump directly to any contest on the ballot,
and also provides an indication of which contests are undervoted at all times. The right
two-thirds of the display are similar to the ballot design in Appendix C.
In Pvote, this design can be implemented by including the overview pane with its YOU
ARE HERE arrow as part of the full-screen image for each page. The undervote indicators
next to each contest in the overview pane can be implemented with counter areas for each
contest.
Sample Pvote ballot designs 269
Page 283 of 324
Page 284 of 324
Persistent review.
This design is a variant of the previous random-access design. Instead of merely showing
which contests are undervoted, the overview pane now shows the selection that the voter
made. Thus, the overview pane functions as an everpresent review screen.
In Pvote, this design can be implemented by adding an āindicator groupā to
correspond to each contest group. Each indicator group would contain āindicator optionsā
with small indicator-size sprites representing each option. Every operation that selects or
deselects an option would also select or deselect the corresponding indicator option. Then
the review indicators in the overview pane would be implemeneted as review areas for the
indicator groups corresponding to each contest group.
The tediousness and redundancy in such a ballot definition suggests that Pvote could
be improved by extending the ballot definition format to allow each option to be
represented by an arbitrary number of sprites of different sizes, instead of just two
sprites (selected and unselected) of the same size. Such an extension would also improve
Pvoteās support for ballots that accommodate vision-impaired users (see page 104) or
ballots that allow the voter to switch languages in mid-session.
Sample Pvote ballot designs 270
Page 284 of 324
Page 285 of 324
Imitation paper ballot.
This design emulates a paper ballot in its appearance and behaviour, offering a familiar
interface for voters who are used to optically scanned ballots. The voter touches the
candidates to fill in the bubbles and uses the arrow buttons at the bottom of the screen to
flip through the ballot. Reviewing selections before casting the ballot consists of flipping
back through the same pages and checking the marked bubbles, just as one would do with
a paper ballot.
In Pvote, this design can be implemented by using empty and filled bubbles as the
option sprites. The targets that select options can be large (covering the entire candidate
name and description) while the corresponding option sprites are small (covering just the
bubble).
Sample Pvote ballot designs 271
Page 285 of 324
Page 286 of 324
E Pvote security review findings
This appendix presents the findings from the code review of
Pvote, taken from the āReport on the Pvote security reviewā [93].
272
Page 286 of 324
Page 287 of 324
Correctness
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.
Correctness claim for R1 (non-termination). Pvote is supposed
to ānever abort during a voting sessionā (R1). As part of the
supporting argument for this claim, Section 7.11 of the
assurance document describes how an upper bound on Pvoteās
memory usage can be statically determined from the ballot
definition. The memory usage argument identifies strings and
lists as the only kinds of values with variable size, and
establishes limits on how long they can possibly grow. But since
Python (and Pthin) integers have unlimited range, a single
integer can also have a variable size. The argument for R1 is
incomplete because it neglects to establish any upper limit on
the integer values used by Pvote.
However, the missing part of the argument can be filled in
by examining all the expressions in the Pvote code that yield
new integers. There are only four built-in functions that return
integers, and all of them return values that are known to be
bounded:
ā¢ range() yields a list of integers between 0 and its
argument.
ā¢ ord() yields an integer between 0 and 255.
ā¢ len() yields the length of the list or string argument, and
the argument in the assurance document already
establishes that lists and strings have bounded size.
ā¢ enumerate() yields lists containing integers all between 0
and the length of the list, and the argument in the assurance
document already establishes that list lengths are bounded.
Aside from built-in functions, the only other way to produce a
new integer value is by performing arithmetic. Arithmetic
expressions occur in the Pvote source code on the following
lines:
Pvote security review findings 273
Page 287 of 324
Page 288 of 324
ā¢ Ballot.py line 125: This line always yields an integer less
than 231
.
ā¢ verifier.py lines 23, 27, 31, 34; Navigator.py lines 28,
32, 46: These lines all increment an integer loop index by a
constant or a quantity fixed in the ballot definition. The
iteration count in each of these loops is determined by a
fixed value in the ballot definition.
ā¢ main.py line 3; verifier.py lines 40, 42, 60, 64, 65, 67, 88;
Navigator.py lines 12, 13, 27, 31; Video.py lines 20, 21;
Printer.py line 12; Audio.py lines 28, 29, 35: These lines
all perform arithmetic and do not store the result. The
operands to the arithmetic expressions are all bounded
values (constants, Boolean values such as 0 or 1, values
fixed in the ballot definition, list lengths, or string lengths).
ā¢ Navigator.py lines 107, 109, 111: These lines perform
arithmetic and pass the result to the Audio.play()
method. The operands to the arithmetic expressions are all
bounded values. The audio driver stores the clip indices,
but does not perform any arithmetic on them.
ā¢ Audio.py line 22: This line performs arithmetic on rate,
which is fixed in the ballot definition, and passes it to
put int(), which converts it to a string without storing it.
ā¢ Audio.py line 34: This line increments the stored integer
self.pos by a passed-in value. In order for this integer to
remain bounded, Pvote relies on Pygameās Sound
constructor to stop calling read() after it returns an empty
string to signal that the end of the file has been reached.
Correctness claim for R9 (ballot casting). Pvote is supposed to
ācommit the ballot when and only when so requested by the
voterā (R9). By design, a Pvote ballot definition can specify a
page transition to occur automatically after some amount of
time has passed with no response from the user. Because a
transition to the last page commits the ballot, this automatic
timeout transition can be made to commit the ballot without
explicit voter action, in violation of R9. A timeout transition
could also prevent the user from committing by jumping to a
Pvote security review findings 274
Page 288 of 324
Page 289 of 324
page with no escape; or it could indirectly force the user to
commit by jumping to a page with no escape except to cast the
ballot (the user has no way to go back and change selections).
Pvoteās design assumes that the ballot definition file will be
checked before an election (A5). Pvote should ensure that the
ballot file will not cause Pvote to crash; the pre-election checks
should ensure that the ballot does not mislead or misrepresent
the voter. To uphold R9, one of these checks must ensure that
no timeout transition deprives the user of the ability to cast the
ballot or the ability to change their selections before casting the
ballot. The assurance document failed to mention that such a
check is necessary.
Missing requirement for voter privacy. The assurance
document states no explicit requirement for preserving a
voterās privacy once the voterās ballot has been committed.
Although Pvote is restarted afresh for each new voter (A3), there
is no assurance of privacy for the interval from when the voter
walks away until the machine is reset. For example, a ballot
definition with a review area on the last page might reveal the
voterās choices to the pollworker or the next voter, without
violating any requirements stated in the assurance document.
There needs to be an assurance argument or a ballot definition
audit requirement to ensure that the images and audio shown
on the final page are independent of all prior choices. In
combination with R3 (Pvote should become inert after a ballot is
committed), this would ensure that the voterās choices will not
be revealed after the voter commits the ballot.
Negative integers. The assurance document (in Section 7.1)
makes an argument that negative integers are never used in
Pvote. This argument claims to list all the uses of the
subtraction operator in Pvote, but neglects to mention the
expression len(self.model.pages) - 1, which appears on
lines 12 and 13 of Navigator.py. Nonetheless, the claim that
negative integers are never used still holds, since the verifier
ensures that model.pages always has a length of at least 1.
Pvote security review findings 275
Page 289 of 324
Page 290 of 324
Pthin specification. Pthin was intended to be a subset of
Python in that any valid Pthin program is a valid Python
program with the same behaviour. However, the Pthin
specification does not accurately describe how a Pthin program
would behave when run under a Python interpreter.
In some cases where Pthin specifies that a fatal error should
occur, Python will not raise an exception. This is significant for
Pvote because Pvote relies on fatal errors to ensure that invalid
ballot definitions never make it past the verifier.
1. According to the Pthin specification, substring slicing
s[i:j] should cause a fatal error unless 0 ā¤ i ā¤ j < n,
where n is the length of s, but Python actually accepts any
integers for the starting and stopping indices.
2. According to the Pthin specification, list indexing l[i]
should cause a fatal error unless 0 ā¤ i < n, where n is the
length of the list, but Python actually allows -n ā¤ i < n. The
same holds for string indexing as well.
3. According to the Pthin specification, any type violation or
illegal argument to a built-in operation causes a fatal error.
But, if Pvote were to pass a callback function to Pygame, and
that function were to throw an exception inside Pygame,
then Pygame could catch the exception and thereby deviate
from the Pthin specification.
The Pthin specification also deviates from the behaviour of the
Python interpreter in the following ways:
4. The Pthin specification neglects to mention that and and or
have short-circuit evaluation, as in Python.
5. The Pthin specification documents the pop() method with
no arguments, but doesnāt document pop() with one
argument, which is used on line 16 of Audio.py.
Although the Pthin specification is in error, it does not appear
that any of the above five deviations would cause Pvote to
function incorrectly:
1. The verifier does not use the slicing operator, so there is no
risk that the slicing operator will fail to produce a fatal error
when it should.
Pvote security review findings 276
Page 290 of 324
Page 291 of 324
2. Section 7.1 of the assurance document establishes that a
negative integer never appears as a string or list index.
3. Pvote never passes any callback functions to Pygame.
4. The and and or operators are used at main.py line 24,
verifier.py line 96, Ballot.py line 126, Navigator.py
lines 12, 44, 50, 54, 80, 83, and 85, and Video.py lines 20
and 21. None of the operands cause side effects; among all
these expressions, the only function calls are to the
Navigator.test() method, and this method has no side
effects.
5. This is simply a documentation error; no security claims
rely on it.
Figure 6.1. A causal connection is missing from the diagram in
Figure 6.1 of the assurance document. There should be a dotted
line leaving the event loop to indicate that it schedules timer
events, and another dotted line entering the event loop for the
timer events it receives.
Pvote security review findings 277
Page 291 of 324
Page 292 of 324
Consensus recommendations
This section describes recommendations made by reviewers on
ways that Pvote or its assurance document could be improved
to make Pvote easier to deploy, use, or review.
Assurance document. The reviewers agreed that the document
should give a detailed breakdown of all the properties that need
to be verified about a ballot definition, in three categories:
those checked by human review, those checked by automated
tools outside of Pvote, and those checked by Pvoteās verifier.
The reviewers recommended that a section of the document
should separately enumerate all causal connectivity with the
outside world (e.g., primitives or library calls that have external
effects, such as the print statement or the open() function).
The reviewers suggested that the assurance document
should explicitly state, on line 89 of Navigator.py, the
precondition that audio.playing has to be false by that point,
and that if the program reaches this point, it has been false for
at least the last ballot.model.timeout ms milliseconds.
The reviewers recommended that the assurance document
explicitly state that cursor sprites need to be checked to make
sure they are not confusable with a candidate or a character.
The reviewers noted that Python dumps a stack trace when
an exception is thrown. If an exception occurs during a voting
session, a record of the corresponding stack trace could
conceivably violate voter privacy. The reviewers recommended
that the assurance document mention this issue and propose
ways to deal with it.
Pthin. The reviewers recommended that the Pthin specification
should prohibit all unprintable characters in source code except
newline, and specifically should prohibit tab characters to avoid
ambiguity in indentation levels. (It was confirmed that the Pvote
source code contains no unprintable characters except newline.)
The reviewers recommended that Pthin should prohibit all
Pvote security review findings 278
Page 292 of 324
Page 293 of 324
identifiers containing double-underscores except init , to
avoid the possibility of triggering any special or implicit
behaviours in Python.
The reviewers suggested that Pthin explicitly forbid nested
class definitions and function definitions, for simplicity.
The reviewers suggested that Pthin could avoid some bugs
caused by one-character changes from == to = by excluding
chained assignments of the form x = y = z.
Ballot definition. The reviewers recommended that ballot
definition analysis tools should be distributed with Pvote to
help reviewers check commonly desired properties of ballot
definitions. Some examples of such properties are reachability
of all pages from the starting state, reachability of the commit
page from any page, and reachability of all the selection pages
from any page.
The reviewers suggested that the ballot definitionās int type
be renamed nat to make it more clear that this type excludes
negative numbers.
The reviewers suggested that ballot definitions be digitally
signed and that Pvote check the signature. The reviewers also
agreed that the ballot definition fileās 8-byte header should be
included in the computation of the hash at the end of the file.
Serialization format. Some reviewers, concerned that the binary
format of the ballot definition file would make it difficult for
humans to examine, initially suggested XML as an alternative
serialization format, with images and audio stored in auxiliary
files. Other reviewers objected that XML is also unreadable. The
reviewers reached the consensus that the ballot definition
should remain the current binary format, so that the Pvote code
for reading it can remain simple and elegant; a separate, textual
ballot definition format should be specified so that the textual
form can be put in a one-to-one correspondence with the binary
form. The Pvote system should include a disassembler (that
converts the binary form into the textual form together with any
auxiliary binary files) and an assembler (that does the opposite).
Pvote security review findings 279
Page 293 of 324
Page 294 of 324
No one has the option to write their own voting software and
vote on it, but anyone who wants to verify a correct conversion
has the option to write their own assembler and disassembler.
The reviewers thought it would also be nice to have a
one-way translator that produces interactive HTML pages or a
Flash animation, so that voters can visit a web page and preview
the voting experience in a browser.
Implementation. The changes suggested by the reviewers are
described here and also noted in the code listing in Appendix B.
Navigator. The reviewers agreed that the navigator should have
something like a self.committed flag to indicate that the
ballot has been committed, together with a commit() method
that commits the ballot and sets the committed flag.
The reviewers felt that some method names in the navigator
could be clarified, such as press(), touch(), invoke(),
execute().
The reviewers felt that lines 66 to 67 of Navigator.py were
just ātoo clever for its own good.ā The intent of these lines
could be expressed more clearly by writing:
if cond.invert:
result = not result
if not result:
return 0
to show that cond.invert reverses the sense of the condition
and that 0 is returned the only when the condition is not met.
The reviewers agreed that line 80 of Navigator.py could
use some parentheses to clarify the Boolean expression.
The reviewers suggested eliminating the recursion in
review() by duplicating the body of the method in two
specialized methods, review contest() and
review writein(). review contest() would call
review writein() and there would be no recursive calls,
making it easier for reviewers to understand.
Pvote security review findings 280
Page 294 of 324
Page 295 of 324
The reviewers found Navigator.execute() more
confusing than necessary because it uses both the list
self.selections and a local variable selections that aliases
a part of it. Mixing these two ways of accessing the list makes it
harder to reason about the code, because each could have
side-effects on the other. The method would be easier to verify
if it always accessed the list through just self.selections or
just selections.
Some reviewers were uncomfortable with the get option()
method, whose parameter is not limited to a specific type; it
accepts any object with members named group i and
option i (thus, any Condition, Step, or Segment).
Ballot. The reviewers suggested that the Ballot module would
be easier to understand if the hashing were performed by a
separate object, not the Ballot itself. This would also prevent
other objects from having access to the incompletely
constructed Ballot object during construction.
Verifier. The reviewers suggested that the verifier have separate
methods get bool() and get enum() instead of get enum()
for both purposes, and separate methods get int() and
get intn() instead of get int() for both purposes.
The reviewers suggested that get str() would be clearer if
it checked isprint(ch) and ch != ā~ā rather than 32 <=
ord(ch) <= 125.
General style. The reviewers suggested that all the constants be
moved to a single module and that each enumerated type be
defined as a class that consolidates the cardinality of the
enumeration, the symbolic names of the elements, and the
values of the elements. The reviewers noted that, for example,
AUDIO DONE is assigned in two separate files, with no condition
that they be assigned the same value.
The reviewers suggested that explicit return None
statements be inserted where None is an intentionally returned
value, instead of relying on None to be returned by default.
Pvote security review findings 281
Page 295 of 324
Page 296 of 324
Inconclusive recommendations
This section contains recommendations made during the review
that did not reach general agreement, were disputed, or were
ultimately withdrawn.
Ballot definition. Some reviewers were concerned that each
write-in option needs its own separate write-in text entry page,
with the text entry state machine duplicated on each page.
Thus, for example, for a ballot with two single-selection
contests and two three-selection contests, if all the contests
allow write-ins (in English letters), there will be eight nearly
identical write-in pages with about 30 states each. This is
because the VM doesnāt have a stack, doesnāt support
subroutines, and canāt pass parameters. It was suggested that
ballot definition complexity could be substantially reduced by
turning the VM from a finite-state machine to a pushdown
automaton. Call-return semantics would also be useful not only
for write-ins, but also for displaying help pages and revisiting
contests from a review screen.
Other reviewers were not convinced that this duplication
was that important. They felt that 30 states was not enough of
an explosion of states to justify additional complexity in the
ballot definition language. Ultimately there was no consensus
that call-return should be added.
A possible compromise might be to create a deterministic
compiler that translates from a language with a call-return
feature to the current language without call-return, and then
publish its input and output for verification.
Image format. Adding an alpha channel to images was
suggested as a way of increasing flexibility in the design of the
ballot definition. However, this would add a little more code to
the voting machine and make human review of ballot
definitions harder. The true appearance of the ballot might be
hidden from human reviewers using alpha compositing tricks
Pvote security review findings 282
Page 296 of 324
Page 297 of 324
(for instance, a sprite with an alpha channel could appear
normal over one background but contain a hidden message that
appears when it is composited over another background).
Programming language. Some reviewers objected to the use of
chained-inequality expressions such as x == y > z because
they were potentially misleading for a reader used to the C
interpretation; they recommended that this syntactic shorthand
be removed from the Pthin specification and that the clauses be
written out separately as x == y and y > z. Others found
such expressions sensible and concise.
Pvote security review findings 283
Page 297 of 324
Page 298 of 324
Observations
This section documents other notable observations that
reviewers made.
Single source vs. multiple sources. The reviewers agreed that
the most critical code is code that:
ā¢ has to be in the voting machine,
ā¢ has to be correct, and
ā¢ cannot be multiply sourced.
Pthin. Some reviewers noted Pthinās simplicity and readability,
and mentioned that they were impressed at their ability to read
and understand a language they didnāt know.
The definition of Pthin implies that a Pthin program has no
access to information about its environment other than explicit
user inputs, and therefore no way to distinguish a real election
from a test. The assurance document could state explicitly that
the Pthin language is deterministic and that it has no
implementation-dependent or compiler-dependent features
other than memory capacity limits (which, if exceeded, can only
cause fatal errors).
The definition of Pthin helps support some of the assurance
requirements:
ā¢ R5 says that Pvoteās behaviour in each session should be
independent of any previous sessions. Satisfying this
requirement doesnāt depend on the code of Pvote; it relies
upon Pthinās definition (e.g., no arbitrary access to the
filesystem), together with the design choice that the
pollworker resets the voting station.
ā¢ R7 says that Pvoteās behaviour should be determined
entirely by the ballot definition and the stream of user input
events. This also doesnāt depend on the code of Pvote; it is
ensured by the interfaces to Pvote and the fact that Pthin is
deterministic. Neither Pthin nor Pygame provide any access
to clocks or sources of randomness.
Pvote security review findings 284
Page 298 of 324
Page 299 of 324
Terminology. The definition of Pthin misuses the term
āprecondition.ā A precondition is something that is assumed to
be true, and if the precondition is violated then the resulting
behaviour is undefined. However, in the Pthin definition, the
word āpreconditionā is used to describe any condition whose
violation is required to cause a fatal error. This distinction is
important because such fatal errors are necessary to the
assurance arguments that are made in the annotations on the
Pvote source code.
Separation of concerns. The separation between the video
driver and the navigator is a separation of space and time: the
video driver knows about space but has no concept of time (no
history); the navigator knows about time but knows nothing of
space (screen layout).
A claim worth stating and verifying is that once the video
driver receives a goto message, it should be history-insensitive
about all prior state, as if a new video driver was freshly
instantiated on each page transition.
Temporal categories of variables. One reviewer noted that
many variables are intended to describe the state of the world
at a particular time, either past, future, or present. For example,
the navigator uses self.page i to refer to the current page
and the parameter page i refers to what will become the
current page. It would be helpful to have a naming convention
to reflect this, so it is easy to tell what point in time a variable
refers to. For example, the parameter page i could be named
new page i or next page i.
Something similar may also be useful in the audio module,
which has to distinguish between what Pvote thinks the audio
state is (busy or available) and what the Pygame audio driver
thinks the audio state is.
Printer output. Some reviewers found the printer output
unfriendly for human readers; in particular, they felt the
insertion of markers after each write-in character was ugly.
Pvote security review findings 285
Page 299 of 324
Page 300 of 324
Arithmetic. Some reviewers commented that arithmetic is
difficult to reason aboutā itās something humans are especially
bad at, compared to computers. In particular, the
Navigator.review() method was harder to verify than it
could have been, because it relies on arithmetic to establish a
correspondence between the array of slots and various other
structures. The reviewers found the incrementing of slot i
and the passing of slot i recursively to review() tricky to
understand (and hence suspicious).
Design consistency. The reviewers noticed that certain features
of Pvote violated the design heuristic of prioritizing the
simplicity of the ballot format:
ā¢ The SG MAX SELS audio segment type is not strictly
necessary. Since the maximum number of selections in each
contest is statically known, every instance of SG MAX SELS
could be replaced by SG CLIP. The ballot definition might
be slightly harder to audit as a result.
ā¢ States are also not strictly necessary and could be
eliminated. Each state could be turned into a separate page,
at the cost of duplicating all the common information that
states currently share.
Fleeing voters. Some local policies require that fleeing voters
should have their ballots automatically cast for them. One way
to implement this for Pvote would be to provide a special
button on the machine (perhaps behind a locked door) that
pollworkers could press to cast the ballot of a fleeing voter.
Code annotations. The assurance document presented a
precondition/postcondition analysis as a set of annotations to
the source code. This analysis was extremely tedious to
perform by hand, even for less than 500 lines of code, and
would also be extremely tedious for reviewers to verify by hand.
The reviewers were concerned that annotations kept separate
from the code would be difficult to maintain, and would be
better expressed directly in the source code. The reviewers felt
Pvote security review findings 286
Page 300 of 324
Page 301 of 324
that, to be practical, verification support based on annotations
has to be cheap and has to require few annotations to be added
by the programmer.
In a statically typed language, many or most of the
annotations in the assurance document would have been
unnecessary, and would be automatically checked by a
compiler. In many reviewersā opinion, this affirmed the value of
type systems for secure and reliable code.
Pvote security review findings 287
Page 301 of 324
Page 302 of 324
Open issues
This section describes other unresolved issues and ideas that
were discussed at the review concerning Pvote or software
auditing in general.
Ballot definition. We discussed the following topics concerning
the ballot definition.
Validity. How much should Pvote constrain the ballot
definition? There is a trade-off between the strictness of the
constraints enforced by Pvoteās verifier and the length of time
that the Pvote software goes unchanged between revisions. With
too many constraints, we run the risk that unanticipated
changes in laws and regulations (or differences in regulations
among jurisdictions) may invalidate Pvoteās assumptions and
force Pvote to change frequently; this would argue for
minimizing these constraints. New laws could also require
Pvote to support new features, which similarly could require
less constrained ballot definitions. On the other hand, too few
constraints on the ballot definition would make it harder to
ensure that Pvote doesnāt crash.
There is also a trade-off between the ease of auditing a
published ballot definition file and the size of the TCB. A
higher-level ballot definition is easier for humans to audit, but
is also likely to mean more code in Pvote.
Auditing. Instead of reviewing the ballot definition directly,
assurance could be gained by publishing the input to the ballot
layout tool and the code of the ballot layout tool. If the ballot
layout tool is deterministic, anyone should be able to run it to
regenerate the ballot definition file.
For auditing the ballot definition, it could also be helpful to
be able to start from the ballot definition file and
unambiguously recover the original input to the ballot layout
tool (for example, by performing OCR on the images, perhaps
Pvote security review findings 288
Page 302 of 324
Page 303 of 324
with some hints from the ballot layout tool). This might be a
requirement to impose on the ballot layout tool.
Programming language. The effect of programming language
design on source code review was another prominent topic.
Mistyped or confusing identifiers. Python automatically creates a
new binding when you make a local assignment; thus, assigning
to a misspelled variable name will just silently create another
variable. The same is true for assignment to member variables.
The reviewers considered this error-prone and suggested some
ways to address the problem:
ā¢ Use a tool to check identifiers that are suspiciously similar.
ā¢ Use a tool to check for variables that are assigned but then
unused.
ā¢ Require all functions to declare their local variables in
comments or decorators and statically check these
declarations.
ā¢ Require constructors to initialize all member variables, and
forbid self from escaping the constructor before all fields
are assigned.
One way for code to be (inadvertently or intentionally)
confusing is to reuse the same identifier names in different
scopes. The reviewers suggested that Pthin could forbid
shadowing of identifiers, and perhaps even forbid using
self.foo and foo in the same context. For example,
Navigator.execute() uses both self.selections and
selections, which some reviewers found tricky to follow.
One reviewer suggested the principle of never reusing a
variable name for two different purposes. For example,
Navigator.play() uses the local variable option i for
different purposes on lines 98 and 104. This particular violation
could be found by a static analysis that requires all loop
counters to be unbound before the loop begins.
A possible language feature that would reduce this problem
would be a requirement that the first binding of any variable be
preceded with a keyword (such as var as in JavaScript). This
Pvote security review findings 289
Page 303 of 324
Page 304 of 324
would force programmers to declare whether they expect each
variable to be already bound or not.
Subsetting. The reviewers noted that it is useful for a
programming language to provide easy ways to enforce that a
given portion of a program is in a particular subset of the
language. Examples of this are the extensible auditing features
in E and Joe-E. If reviewers can rely on static checkers to ensure
that parts of a program are in declared subsets of the language,
that can make their job as reviewers much easier.
Type distinctions. Python has no truly separate Boolean type;
Boolean values behave in almost all respects like the integers 0
and 1. The reviewers suggested that it might be good for Pthin
to treat integers and Boolean values as separate types and
statically check that they are used in a type-safe way. There are
a few places in the current Pvote code that would violate such a
type restriction, such as Navigator.py line 27.
One reviewer noted difficulty in telling whether a variable
name such as group i stood for an nullable or non-nullable
integer. This could be addressed by a type distinction or a
naming convention. One suggested naming convention uses the
prefix opt for optional (i.e., nullable) variables.
Mutability. The reviewers suggested that it would be useful to
be able to declare some variables āeventually read-only.ā Such
variables would be initially mutable, but at some later point
irreversibly become immutable (either upon exiting a particular
scope or upon being marked immutable by the Pthin program).
These could be used to ensure that the ballot definition is
read-only after it is loaded and verified. An alternative would be
to construct the ballot definition only out of immutable objects.
Another potentially useful behaviour that the reviewers
suggested was a variant on Javaās final keyword: a variable
that, after initialization, can only be set to None. Thus, it would
be possible to āthrow awayā the variable as a way of divesting
authority, but not to change it.
Pvote security review findings 290
Page 304 of 324
Page 305 of 324
The reviewers also suggested that Pthin might require
constructors to set all the member variables of the object being
constructed.
Compilation. The reviewers suggested that instead of verifying
the compiler, auditors could verify that the assembly-language
output from the compiler is a valid compilation of the source
code input to the compiler.
If Pthin were small enough, perhaps it could be reliably
mechanically translated to a variety of target languages.
Other languages. The following other programming languages
were suggested for implementing Pvote:
ā¢ BitC
ā¢ CCured
ā¢ Cyclone
ā¢ Java
ā¢ Joe-E (subset of Java)
ā¢ Ada
ā¢ SPARK Ada (subset of Ada)
ā¢ ML
In addition, JML (Java Modelling Language) declarations could
be added to an implementation in Java or Joe-E, and verified by
a static checker such as ESC/Java2.
Porting Pvote to Joe-E would help reviewers reason about
statelessness and determinism (e.g., statelessness of the
Ballot constructor or determinism of the verifier).
There is a trade-off here between choosing a well-known
language (with a large community of potential code reviewers)
and a more obscure language with verification features. The
importance of public confidence in the election affects this
trade-off.
Other language features. The reviewers mentioned that static
typing and explicit control over memory allocation could be
potentially helpful language features for the design and review
of Pvote.
Pvote security review findings 291
Page 305 of 324
Page 306 of 324
The reviewers wondered if it might be possible to further
reduce Pthin by eliminating negative integers and strings,
thereby making it easier to translate into other languages.
Also, there are a few places where Pthin had to be a slightly
larger language in order to accommodate an existing API. An
alternative to this would be to create an abstraction around the
API, implement the abstraction in Python, and use a call to the
Python function in the Pthin program. (This example illustrates
the benefits of flexibility in choosing language subsets.)
Memory usage. Section 7.11 of the assurance document
attempts to provide an argument that the memory usage of
Pvote is bounded. How would an actual upper bound on
memory usage be calculated given a particular ballot definition?
How might Pvoteās design and Pthinās specification be changed
in order to make such a calculation straightforward?
Hardware. For a voting machine that emits audio via a typical
headphone port, there is a risk that the audio may be recorded
in violation of voter privacy. In particular, if audio is enabled by
default and most voters donāt use audio, a cable running from
the audio port to a recording device may go unnoticed [61].
Accessibility. The only user input events Pvote understands are
screen touches and button presses, not including their duration,
movement, velocity, pressure, or release. In particular, Pvote
cannot distinguish long and short presses or detect
double-clicks. We need to identify the norms for input devices
in the accessibility community; if timed features like this are
needed, Pvote may have to be altered to support them. (One
reviewer pointed out that some support for such features could
also be provided by hardware, such as hardware that translates
a long button press into one keycode and a short button press
into a different keycode.)
One-button or other low-bandwidth input interfaces could
require Pvote to be more aware of timing. One example would
be an interface where āpauseā is an input event; another would
Pvote security review findings 292
Page 306 of 324
Page 307 of 324
be an interface where options are read off slowly one at a time,
and the user signals when he hears the desired option. For
these designs, we would want to be able to specify a separate
timeout length for each state, and potentially also an arbitrary
action (not just a transition) to be triggered on a timeout.
Use of pointers. The reviewers debated whether it would be an
improvement to have the verifier, as it goes through the ballot
definition checking array indices, replace the integer array
indices with pointers to the referenced array elements. This
would make it easier to be sure that the preconditions checked
in the verifier match the preconditions on which the rest of
Pvote relies. However, there is a good rationale for using indices
instead of pointers, since passing indices transfers no authority.
For example, other modules can pass indices into the printer
module that will be used as indices into the text data, even
though these other modules donāt have access to the text data.
One reviewer suggested that rights amplification might be a
possible solution (bringing together an opaque array object and
an opaque index object would yield an array element). It might
be tricky to make this work for parallel arrays, which Pvote uses.
Output. The reviewers discussed the possibility of declaring the
output module to be a replaceable component, separate from
Pvote. Thus the interface to Pvote would be: take a ballot
definition file as input, produce a cast vote record as output.
The output module would print or record the cast vote in
whatever appropriate manner. There was no consensus on how
the output interface should be defined.
Printing. The reviewers were concerned that the printing
module is based around 7-bit ASCII, thus restricting candidate
names to 7-bit ASCII. Alternatively, if the printing module were
to print images instead of text, problems related to text
encoding would go away. Several options were discussed:
ā¢ Print numeric identifiers instead of strings; the numbers
would refer to the ballot definition. (But one useful purpose
Pvote security review findings 293
Page 307 of 324
Page 308 of 324
of a printed record is to allow votes to be counted even if all
electronic records are lost; this option lacks that feature.)
ā¢ Allow Unicode strings; pass them through opaquely to the
printer. The printer module should export a validation
method that checks whether strings are printable by the
printer hardware (e.g., the printer might support only 7-bit
ASCII, or it might provide a font that supports some subset
of Unicode). This validation would be performed on all
strings at ballot loading time to ensure they will be safely
printable.
ā¢ Just print sprites; eliminate all strings from the ballot
definition and from Pthin. Some possibilities:
ā¢ For each sprite to be shown on the display, provide a
corresponding black-and-white sprite for printing.
ā¢ Restrict all displayed sprites to 1-bit black-and-white
bitmaps, so the printer output can match it exactly.
(This also has the fairness advantage that colour-blind
voters will perceive exactly the same ballot as other
voters.)
ā¢ Allow both of the above approaches and add a flag to
the ballot definition to let the ballot designer choose one
of them.
ā¢ Specify an algorithm for converting a colour image to a
black-and-white image for printing. If the ballot designer
chooses to use a colour sprite, it is their responsibility to
make sure that its black-and-white conversion is legible.
System platform. The reviewers pondered what a minimal
platform for Pvote would look like, and sketched out the
following:
ā¢ Audio driver (hardware that plays from a memory-mapped
buffer, with software that keeps the buffer full)
ā¢ Interrupts for all input devices (including touchscreen
touches)
ā¢ Printer driver
ā¢ Storage driver (SD card, etc.)
ā¢ Single-threaded program
Pvote security review findings 294
Page 308 of 324
Page 309 of 324
Code documentation. The Pvote code was presented to the
reviewers without comments, for fear that comments might bias
their evaluation. Some reviewers had opinions about this:
ā¢ Some reviewers felt that it would be nice to see comments in
the code, and that leaving comments out of the code didnāt
make their job easier.
ā¢ One reviewer was glad that the comments were separated,
because (a) more code fits on fewer pages, and (b) he was
not being influenced by comments he could not trust. He
felt that he was getting more benefit by being forced to
reconstruct for himself the argument for why the code was
correct.
ā¢ One reviewer would prefer to see the meaning of fields
described in comments right in the code (like Javadoc).
ā¢ āCode that needs no documentationā is a myth; the code
says how, but the comments say why.
A possible compromise would be to include comments in the
code, and also offer a way for the reviewers to view the code
with the comments hidden.
Tests. Adding a suite of unit tests and regression tests might
help the reviewers perform testing, though it would constitute
more code for them to audit.
Pvote security review findings 295
Page 309 of 324
Page 310 of 324
Bug insertion
This section describes the bug insertion experiment that we
conducted. On the third and fourth days of the review, the
reviewers were given a new hardcopy of the source code
containing bugs that David Wagner and I had inserted. We told
the reviewers that we had inserted at least one bug in the code,
and asked them to try to find it.
Since insider attacks are a major unaddressed threat in
existing systems, we specifically wanted to experiment with this
scenario. Therefore, we warned the reviewers to treat us as
untrusted adversaries, and that we might not always tell the
truth. However, since it was in everyoneās interest to use our
limited time efficiently, we settled on a time-saving convention.
We promised to truthfully answer any question about a factual
matter that the reviewers could conceivably verify mechanically
or by checking an independent sourceāfor example, questions
about the Python language, about static properties of the code,
about its runtime behaviour, and so on.
As we sought to craft bugs on the evening of March 30,
David Wagner and I chose the following criteria to make the
experiment more realistic:
ā¢ The bug had to conceivably enable an attack that would
affect election results. We assumed that the attacker also
had the ability to distribute a maliciously designed ballot
definition.
ā¢ The bug had to conceivably escape detection in a live
walkthrough test, such as a āLogic and Accuracy Testā for an
election, which typically consists of going through the whole
casting process for several ballots so that at least one vote is
cast for each candidate.
ā¢ The bug could not violate the Pthin language definition.
We only considered bugs that individually met all these criteria.
David and I devised and inserted three bugs with varying levels
of subtlety:
Pvote security review findings 296
Page 310 of 324
Page 311 of 324
1. Easy: Lines 83ā84 in Navigator.py are as follows.
83 if step.op == OP REMOVE and selected:
84 selections.remove(option i)
We removed and selected from line 84. The consequence
is that an attempt to deselect an option using OP REMOVE
will crash if the option is not already selected. A ballot
definition could use this bug to selectively crash the
machine in a particular situation (e.g., to disenfranchise
those who vote for a particular party). The ballot definition
could still pass a walkthrough test and avoid crashing under
normal circumstances by using a condition to prevent
OP REMOVE from being executed when the option is not
selected.
2. Medium: Lines 78ā79 in Navigator.py are as follows.
78 selections = self.selections[group i]
79 selected = option i in selections
We changed selections to self.selections in the
second line (line 79). The consequence is that selected will
always be 0, because self.selections is a list of lists, not
a list of integers. The consequence is that OP ADD will keep
adding a selection to the list even after it has already been
selected. So, in a contest with a max sels of 3, for example,
a voter could cast three votes for the same candidate. (Note
that this bug could be caught by a static type checker.)
3. Hard: Lines 42ā43 in Navigator.py are as follows.
42 if option.writein group i != None:
43 self.review(option.writein group i, slot i + 1, None)
This is the recursive call within the review() method. The
recursion only goes one level deep: the outer call displays
the selected options within a contest, and the inner call
displays the selected characters within a write-in. Thus, the
outer call passes the write-in group to the inner call. We
changed None to cursor sprite i in the recursive call on
line 43. This takes the cursor sprite i index that was
passed in (which would be a sprite the size of an option)
Pvote security review findings 297
Page 311 of 324
Page 312 of 324
and passes it on to the inner call (which would attempt to
paste it into a slot the size of a character). The ballot
definition could set up a situation in which this size
mismatch caused a sprite to exceed the bounds of the
screen, causing the program to crash.
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.
March 31. Three reviewers were present on March 31:
Tadayoshi Kohno, Mark Miller, and Dan Sandler. Dan was
already very familiar with Python; he worked separately. He
found the āmediumā bug about 35 minutes after he started his
search, purely by manual inspection, saying the line ālooked
suspicious.ā He then found the āeasyā bug about 35 minutes
later (70 minutes after starting). He hypothesized that the
condition was incomplete by reading the code, then tested his
hypothesis by running Pvote and finding a way to make the
program crash.
The other two reviewers, Mark and Yoshi, worked together.
They were less familiar with Python; one had spent the
preceding two days learning about Pvoteās design and
inspecting the code, and the other was encountering Pvote for
the first time with the bugs embedded. About four hours into
the review (not including a lunch break), they expressed some
concern about the code near the āeasyā bug. About ten minutes
later, they noticed that the annotations to the left of line 83
didnāt match the code. Another ten minutes later, they declared
that they had found a bug (the āeasyā bug). Part of what had
caused them to inspect this region of code carefully was an
attempt to systematically verify, one by one, each of the
Pvote security review findings 298
Page 312 of 324
Page 313 of 324
assurance arguments given in Chapter 7 of the assurance
document. They did not find the āmediumā bug.
By the time the reviewers quit late in the day, none had
found the āhardā bug, although there had been some questions
about ways that cursor sprites could be used to conduct an
attack. They had spent a total of about 20 reviewer-hours
examining the version of the code with the three inserted bugs.
May 20. Two reviewers were present on May 20: Ian Goldberg
and Tadayoshi Kohno. Ian found the āeasyā bug about 130
minutes after starting his search, despite being new to Pvote.
About 90 minutes later, after no more bugs were found, we
decided to switch strategies. To test out the āread-write reviewā
idea that Dan Sandler had previously proposed (see Section E),
both reviewers would try to insert bugs into the code, and we
would see if this helped them find the bugs that David and I
had inserted earlier.
Yoshi spent the next 50 minutes inserting bugs into the
code. I examined his altered code and, by manual inspection
alone, was able to find the three bugs he inserted in about 30
minutes. (Of course, as the author of the code, I was uniquely
familiar with it, so this doesnāt reveal much about the subtlety
of the inserted bugs.) No more bugs were discovered for the
rest of the day. By the end of the day, the reviewers had
inspected the code for about 13 reviewer-hours.
Pvote security review findings 299
Page 313 of 324
Page 314 of 324
Review process
This section describes ideas and suggestions regarding the
software review process that came up during the review.
Viewing 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.
Analysis tools. The reviewers mentioned that these tools would
have been helpful to them:
ā¢ a static checker to verify that Pvote is written in the Pthin
subset
ā¢ a checker for suspiciously similar (possibly mistyped)
identifiers
ā¢ an information flow analyzer
ā¢ a static analyzer to determine the maximum possible call
depth
Trust in the adversary. The reviewers mentioned on several
occasions that it was difficult to maintain the requisite level of
distrust in the programmer, especially when the programmer
was present in the room and was a friendly face. The
significance of the social relationship between programmer and
reviewer is an important difference between code review for
accidental mistakes and code review for intentional malice. The
reviewers agreed that in an adversarial review, programmers
should not socialize with the reviewers; perhaps they should
even not be physically in the same room, or communicate only
over a text-based communication channel. The reviewers
believed that measures like theseāto ādehumanize the
enemyāāwould help them maintain the necessary distrust of
the programmer.
One reviewer noted that, although his suspicions were
Pvote security review findings 300
Page 314 of 324
Page 315 of 324
raised during the bug-finding test by a missing annotation, he
would have been easily tricked by a bogus annotation. He would
not have bothered to check that the annotation was correct,
since it appeared that the programmer had thought about the
issue and claimed to offer some justification, and since every
other time he had checked out an annotation, it did turn out to
be valid. This weakness resulted from a combination of the
tediousness of checking annotations and insufficient distrust in
the programmer.
Reviewer fatigue. The reviewers generally felt that the point
where one becomes tired of inspecting code comes long before
one has subjected it to enough scrutiny. It might be a good idea
to limit the amount of time spent per reviewer: the more
familiar one becomes with it, the more confident and
comfortable one becomes at making assumptions of
correctness. One reviewer suggested that, since reviewers
shouldnāt ever become complacent with the code being
reviewed, the review process should follow a āprinciple of most
surpriseā to keep reviewers on their toes.
One-line change test. Mark Miller proposed the following test:
suppose that, as an attacker, you had the ability to change just
one line of code. How much damage could you do (i.e., which
assurance requirements could you cause the program to
violate)? Figuring out which lines are the most sensitive would
provide a map of the āhot spotsā in the programāthe places
that require especially close attention during a code review. For
example, changing - 1 to + 1 on line 12 of Navigator.py is
sufficient to make Pvote keep printing out ballots repeatedly if
left unattended. Therefore, this line is part of the TCB for R3
(become inert after a ballot is commtited) and also for R9
(commit the ballot only when so requested by the voter).
In a variant of this test, there are a series of trials. For each
trial, one line of the program is chosen at random and the
attacker is allowed to change just that line. With enough trials,
one could estimate the size of the TCB for each assurance
Pvote security review findings 301
Page 315 of 324
Page 316 of 324
requirement. For example, if the attacker is able to violate a
particular requirement in 1/4 of the trials, then the TCB for that
requirement is probably about 1/4 the size of the program.
By changing almost any single line, one can trivially cause
the program to crash. It is more of a challenge to cause a
meaningful effect on an election without failing a simple
operational test.
Our discussion of the one-line change test highlighted the
benefits of read-only types. Without read-only restrictions,
almost any line in Pvote can be changed to one that maliciously
modifies the ballot data in memory.
The read-write review. Dan Sandler suggested the possibility
of taking the bug insertion experiment one step further by
encouraging the reviewers to insert their own bugs, a process he
called the āread-write review.ā He conjectured that being tasked
to insert bugs 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.
One could imagine several groups of reviewers performing a
multi-round review, in which each group inserts some bugs and
then passes on the code to the next group.
Other tasks might also improve code understanding by
getting reviewers to modify and interact with the code.
Reviewers could be asked to translate it to another
Pvote security review findings 302
Page 316 of 324
Page 317 of 324
programming language, or to rewrite parts of the code they find
hard to understand, and then verify that their rewritten or
translated code produces equivalent behaviour.
The idea of the read-write review was inspired by Danās
experience with the Hack-a-Vote class exercise, in which more
bugs were found by students while inserting bugs than while
looking for bugs. The insight was that although Hack-a-Vote was
conceived as a test of the students doing the hacking, it is also a
test of the Hack-a-Vote softwareās resistance to undetected
tampering.
Ideally, if reviewers find most or all of the planted bugs,
while finding few or no bugs in the original code, this might be
grounds for confidence in the original code. However, we noted
several ways that an actual attacker (the original, possibly
malicious programmer who initially wrote the software) might
be a stronger adversary than a fake attacker (a code reviewer
asked to insert bugs into the software):
ā¢ A real attacker could simply be smarter.
ā¢ A real attacker may be more motivated or have more at
stake.
ā¢ A real attacker may have more time and resources than a
team of reviewers would have in one round of the review.
ā¢ A real attacker would be more familiar with the code, and
could have chosen the design and implementation
specifically to enable particular malicious bugs.
On the fourth day of the review, reviewers were asked to
insert their own bugs. They commented:
ā¢ Itās possible that inserting bugs may reduce a reviewerās
chances of finding bugs. Inserting bugs under time
constraints may encourage reviewers to stick to the parts of
code they already understand well, instead of diving deep
into unfamiliar parts of the code.
ā¢ The code can be divided into three classes: (a) parts you
understand, (b) parts you donāt understand, and (c) parts
you donāt understand but think you do. Reviewers will tend
to insert bugs in types (a) and (c), but not (b).
Pvote security review findings 303
Page 317 of 324
Page 318 of 324
Post-review survey
After the conclusion of the first three-day meeting, we
informally surveyed the reviewers by e-mail. Their responses
are paraphrased here.
Thoroughness of review . How thorough was this review,
compared to other security reviews you have participated in, or
other reviews of voting software?
ā¢ This was comparable to other code reviews, though very
different from reviewing commercial voting software
because Pvote is so much smaller.
ā¢ Other reviews expended more total effort, but this review
spent more effort per line of code.
ā¢ This did not go into as much depth as other security reviews
because we were focused on just the Pvote component.
ā¢ For me, not that thorough.
General confidence. After this review, how much confidence do
you have have in Pvote, compared to other voting systems you
are familiar with?
ā¢ Much more confidence in Pvote than any commercial voting
system; however, Pvote is only one component and many of
the security flaws in other voting systems occur in parts
outside of Pvoteās scope. āComparing Pvote to the
comparable portions of commercial systems is no contest.
Pvote kills them.ā
ā¢ For what Pvote does, much better than any of the other
systems I have seen.
ā¢ Iām not familiar with other voting systems.
ā¢ I canāt give a confidence level about Pvote, though I am
confident it would be easier to argue the security of Pvote
than other designs.
Lack of accidental bugs. How confident are you that Pvote is
free of accidental bugs? In other words, if you assume that Ping
Pvote security review findings 304
Page 318 of 324
Page 319 of 324
is not malicious and was trying his best to make Pvote
trustworthy, how confident are you that you would have found
any inadvertent bugs in Pvote?
ā¢ Reasonably confident.
ā¢ Rather highly.
ā¢ Confident due to the efforts of the group as a whole, though
not very confident I would have found them on my own.
ā¢ Itās hard to say.
Lack of malicious bugs. How confident are you that Pvote is
free of malicious code? In other words, if you assume that Ping is
malicious and may have been trying his best to introduce a
backdoor, how confident are you that you would have found it?
ā¢ Not at all confident.
ā¢ Poorly.
ā¢ Confident due to the efforts of the group as a whole, though
not very confident I would have found them on my own.
ā¢ Not very confident.
Pvote security review findings 305
Page 319 of 324
Page 320 of 324
GNU Free Documentation License
1.2, November 2002
Copyright Ā© 2000, 2001, 2002 Free Software Foundation, Inc.
51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
Everyone is permitted to copy and distribute verbatim copies of this license document, but changing it is not
allowed.
Preamble
The purpose of this License is to make a manual, textbook, or other functional and useful document āfreeā in
the sense of freedom: to assure everyone the effective freedom to copy and redistribute it, with or without
modifying it, either commercially or noncommercially. Secondarily, this License preserves for the author and
publisher a way to get credit for their work, while not being considered responsible for modifications made by
others.
This License is a kind of ācopyleftā, which means that derivative works of the document must themselves
be free in the same sense. It complements the GNU General Public License, which is a copyleft license
designed for free software.
We have designed this License in order to use it for manuals for free software, because free software
needs free documentation: a free program should come with manuals providing the same freedoms that the
software does. But this License is not limited to software manuals; it can be used for any textual work,
regardless of subject matter or whether it is published as a printed book. We recommend this License
principally for works whose purpose is instruction or reference.
1. Applicability and definitions
This License applies to any manual or other work, in any medium, that contains a notice placed by the
copyright holder saying it can be distributed under the terms of this License. Such a notice grants a
world-wide, royalty-free license, unlimited in duration, to use that work under the conditions stated herein.
The āDocumentā, below, refers to any such manual or work. Any member of the public is a licensee, and is
addressed as āyouā. You accept the license if you copy, modify or distribute the work in a way requiring
permission under copyright law.
A āModified Versionā of the Document means any work containing the Document or a portion of it,
either copied verbatim, or with modifications and/or translated into another language.
A āSecondary Sectionā is a named appendix or a front-matter section of the Document that deals
exclusively with the relationship of the publishers or authors of the Document to the Documentās overall
subject (or to related matters) and contains nothing that could fall directly within that overall subject. (Thus,
if the Document is in part a textbook of mathematics, a Secondary Section may not explain any mathematics.)
The relationship could be a matter of historical connection with the subject or with related matters, or of
legal, commercial, philosophical, ethical or political position regarding them.
The āInvariant Sectionsā are certain Secondary Sections whose titles are designated, as being those of
Invariant Sections, in the notice that says that the Document is released under this License. If a section does
not fit the above definition of Secondary then it is not allowed to be designated as Invariant. The Document
may contain zero Invariant Sections. If the Document does not identify any Invariant Sections then there are
none.
The āCover Textsā are certain short passages of text that are listed, as Front-Cover Texts or Back-Cover
Texts, in the notice that says that the Document is released under this License. A Front-Cover Text may be at
most 5 words, and a Back-Cover Text may be at most 25 words.
306
Page 320 of 324
Page 321 of 324
A āTransparentā copy of the Document means a machine-readable copy, represented in a format whose
specification is available to the general public, that is suitable for revising the document straightforwardly
with generic text editors or (for images composed of pixels) generic paint programs or (for drawings) some
widely available drawing editor, and that is suitable for input to text formatters or for automatic translation
to a variety of formats suitable for input to text formatters. A copy made in an otherwise Transparent file
format whose markup, or absence of markup, has been arranged to thwart or discourage subsequent
modification by readers is not Transparent. An image format is not Transparent if used for any substantial
amount of text. A copy that is not āTransparentā is called āOpaqueā.
Examples of suitable formats for Transparent copies include plain ASCII without markup, Texinfo input
format, LaTeX input format, SGML or XML using a publicly available DTD, and standard-conforming simple
HTML, PostScript or PDF designed for human modification. Examples of transparent image formats include
PNG, XCF and JPG. Opaque formats include proprietary formats that can be read and edited only by
proprietary word processors, SGML or XML for which the DTD and/or processing tools are not generally
available, and the machine-generated HTML, PostScript or PDF produced by some word processors for output
purposes only.
The āTitle Pageā means, for a printed book, the title page itself, plus such following pages as are needed
to hold, legibly, the material this License requires to appear in the title page. For works in formats which do
not have any title page as such, āTitle Pageā means the text near the most prominent appearance of the workās
title, preceding the beginning of the body of the text.
A section āEntitled XYZā means a named subunit of the Document whose title either is precisely XYZ or
contains XYZ in parentheses following text that translates XYZ in another language. (Here XYZ stands for a
specific section name mentioned below, such as āAcknowledgementsā, āDedicationsā, āEndorsementsā, or
āHistoryā.) To āPreserve the Titleā of such a section when you modify the Document means that it remains a
section āEntitled XYZā according to this definition.
The Document may include Warranty Disclaimers next to the notice which states that this License applies
to the Document. These Warranty Disclaimers are considered to be included by reference in this License, but
only as regards disclaiming warranties: any other implication that these Warranty Disclaimers may have is
void and has no effect on the meaning of this License.
2. Verbatim copying
You may copy and distribute the Document in any medium, either commercially or noncommercially,
provided that this License, the copyright notices, and the license notice saying this License applies to the
Document are reproduced in all copies, and that you add no other conditions whatsoever to those of this
License. You may not use technical measures to obstruct or control the reading or further copying of the
copies you make or distribute. However, you may accept compensation in exchange for copies. If you
distribute a large enough number of copies you must also follow the conditions in section 3.
You may also lend copies, under the same conditions stated above, and you may publicly display copies.
3. Copying in quantity
If you publish printed copies (or copies in media that commonly have printed covers) of the Document,
numbering more than 100, and the Documentās license notice requires Cover Texts, you must enclose the
copies in covers that carry, clearly and legibly, all these Cover Texts: Front-Cover Texts on the front cover, and
Back-Cover Texts on the back cover. Both covers must also clearly and legibly identify you as the publisher of
these copies. The front cover must present the full title with all words of the title equally prominent and
visible. You may add other material on the covers in addition. Copying with changes limited to the covers, as
long as they preserve the title of the Document and satisfy these conditions, can be treated as verbatim
copying in other respects.
If the required texts for either cover are too voluminous to fit legibly, you should put the first ones listed
(as many as fit reasonably) on the actual cover, and continue the rest onto adjacent pages.
If you publish or distribute Opaque copies of the Document numbering more than 100, you must either
include a machine-readable Transparent copy along with each Opaque copy, or state in or with each Opaque
copy a computer-network location from which the general network-using public has access to download using
public-standard network protocols a complete Transparent copy of the Document, free of added material. If
you use the latter option, you must take reasonably prudent steps, when you begin distribution of Opaque
copies in quantity, to ensure that this Transparent copy will remain thus accessible at the stated location until
GNU Free Documentation License 307
Page 321 of 324
Page 322 of 324
at least one year after the last time you distribute an Opaque copy (directly or through your agents or
retailers) of that edition to the public.
It is requested, but not required, that you contact the authors of the Document well before redistributing
any large number of copies, to give them a chance to provide you with an updated version of the Document.
4. Modifications
You may copy and distribute a Modified Version of the Document under the conditions of sections 2 and 3
above, provided that you release the Modified Version under precisely this License, with the Modified Version
filling the role of the Document, thus licensing distribution and modification of the Modified Version to
whoever possesses a copy of it. In addition, you must do these things in the Modified Version:
A. Use in the Title Page (and on the covers, if any) a title distinct from that of the Document, and from those
of previous versions (which should, if there were any, be listed in the History section of the Document).
You may use the same title as a previous version if the original publisher of that version gives permission.
B. List on the Title Page, as authors, one or more persons or entities responsible for authorship of the
modifications in the Modified Version, together with at least five of the principal authors of the Document
(all of its principal authors, if it has fewer than five), unless they release you from this requirement.
C. State on the Title page the name of the publisher of the Modified Version, as the publisher.
D. Preserve all the copyright notices of the Document.
E. Add an appropriate copyright notice for your modifications adjacent to the other copyright notices.
F. Include, immediately after the copyright notices, a license notice giving the public permission to use the
Modified Version under the terms of this License, in the form shown in the Addendum below.
G. Preserve in that license notice the full lists of Invariant Sections and required Cover Texts given in the
Documentās license notice.
H. Include an unaltered copy of this License.
I. Preserve the section Entitled āHistoryā, Preserve its Title, and add to it an item stating at least the title,
year, new authors, and publisher of the Modified Version as given on the Title Page. If there is no section
Entitled āHistoryā in the Document, create one stating the title, year, authors, and publisher of the
Document as given on its Title Page, then add an item describing the Modified Version as stated in the
previous sentence.
J. Preserve the network location, if any, given in the Document for public access to a Transparent copy of
the Document, and likewise the network locations given in the Document for previous versions it was
based on. These may be placed in the āHistoryā section. You may omit a network location for a work that
was published at least four years before the Document itself, or if the original publisher of the version it
refers to gives permission.
K. For any section Entitled āAcknowledgementsā or āDedicationsā, Preserve the Title of the section, and
preserve in the section all the substance and tone of each of the contributor acknowledgements and/or
dedications given therein.
L. Preserve all the Invariant Sections of the Document, unaltered in their text and in their titles. Section
numbers or the equivalent are not considered part of the section titles.
M. Delete any section Entitled āEndorsementsā. Such a section may not be included in the Modified Version.
N. Do not retitle any existing section to be Entitled āEndorsementsā or to conflict in title with any Invariant
Section.
O. Preserve any Warranty Disclaimers.
If the Modified Version includes new front-matter sections or appendices that qualify as Secondary Sections
and contain no material copied from the Document, you may at your option designate some or all of these
sections as invariant. To do this, add their titles to the list of Invariant Sections in the Modified Versionās
license notice. These titles must be distinct from any other section titles.
You may add a section Entitled āEndorsementsā, provided it contains nothing but endorsements of your
Modified Version by various partiesāfor example, statements of peer review or that the text has been
approved by an organization as the authoritative definition of a standard.
You may add a passage of up to five words as a Front-Cover Text, and a passage of up to 25 words as a
Back-Cover Text, to the end of the list of Cover Texts in the Modified Version. Only one passage of Front-Cover
Text and one of Back-Cover Text may be added by (or through arrangements made by) any one entity. If the
Document already includes a cover text for the same cover, previously added by you or by arrangement made
GNU Free Documentation License 308
Page 322 of 324
Page 323 of 324
by the same entity you are acting on behalf of, you may not add another; but you may replace the old one, on
explicit permission from the previous publisher that added the old one.
The author(s) and publisher(s) of the Document do not by this License give permission to use their names
for publicity for or to assert or imply endorsement of any Modified Version.
5. Combining documents
You may combine the Document with other documents released under this License, under the terms defined
in section 4 above for modified versions, provided that you include in the combination all of the Invariant
Sections of all of the original documents, unmodified, and list them all as Invariant Sections of your combined
work in its license notice, and that you preserve all their Warranty Disclaimers.
The combined work need only contain one copy of this License, and multiple identical Invariant Sections
may be replaced with a single copy. If there are multiple Invariant Sections with the same name but different
contents, make the title of each such section unique by adding at the end of it, in parentheses, the name of
the original author or publisher of that section if known, or else a unique number. Make the same adjustment
to the section titles in the list of Invariant Sections in the license notice of the combined work.
In the combination, you must combine any sections Entitled āHistoryā in the various original documents,
forming one section Entitled āHistoryā; likewise combine any sections Entitled āAcknowledgementsā, and any
sections Entitled āDedicationsā. You must delete all sections Entitled āEndorsementsā.
6. Collections of documents
You may make a collection consisting of the Document and other documents released under this License, and
replace the individual copies of this License in the various documents with a single copy that is included in
the collection, provided that you follow the rules of this License for verbatim copying of each of the
documents in all other respects.
You may extract a single document from such a collection, and distribute it individually under this
License, provided you insert a copy of this License into the extracted document, and follow this License in all
other respects regarding verbatim copying of that document.
7. Aggregation with independent works
A compilation of the Document or its derivatives with other separate and independent documents or works,
in or on a volume of a storage or distribution medium, is called an āaggregateā if the copyright resulting from
the compilation is not used to limit the legal rights of the compilationās users beyond what the individual
works permit. When the Document is included in an aggregate, this License does not apply to the other works
in the aggregate which are not themselves derivative works of the Document.
If the Cover Text requirement of section 3 is applicable to these copies of the Document, then if the
Document is less than one half of the entire aggregate, the Documentās Cover Texts may be placed on covers
that bracket the Document within the aggregate, or the electronic equivalent of covers if the Document is in
electronic form. Otherwise they must appear on printed covers that bracket the whole aggregate.
8. Translation
Translation is considered a kind of modification, so you may distribute translations of the Document under
the terms of section 4. Replacing Invariant Sections with translations requires special permission from their
copyright holders, but you may include translations of some or all Invariant Sections in addition to the
original versions of these Invariant Sections. You may include a translation of this License, and all the license
notices in the Document, and any Warranty Disclaimers, provided that you also include the original English
version of this License and the original versions of those notices and disclaimers. In case of a disagreement
between the translation and the original version of this License or a notice or disclaimer, the original version
will prevail.
If a section in the Document is Entitled āAcknowledgementsā, āDedicationsā, or āHistoryā, the
requirement (section 4) to Preserve its Title (section 1) will typically require changing the actual title.
GNU Free Documentation License 309
Page 323 of 324
Page 324 of 324
9. Termination
You may not copy, modify, sublicense, or distribute the Document except as expressly provided for under this
License. Any other attempt to copy, modify, sublicense or distribute the Document is void, and will
automatically terminate your rights under this License. However, parties who have received copies, or rights,
from you under this License will not have their licenses terminated so long as such parties remain in full
compliance.
10. Future revisions of this license
The Free Software Foundation may publish new, revised versions of the GNU Free Documentation License
from time to time. Such new versions will be similar in spirit to the present version, but may differ in detail to
address new problems or concerns. See http://www.gnu.org/copyleft/.
Each version of the License is given a distinguishing version number. If the Document specifies that a
particular numbered version of this License āor any later versionā applies to it, you have the option of
following the terms and conditions either of that specified version or of any later version that has been
published (not as a draft) by the Free Software Foundation. If the Document does not specify a version number
of this License, you may choose any version ever published (not as a draft) by the Free Software Foundation.
Addendum: How to use this License for your documents
To use this License in a document you have written, include a copy of the License in the document and put the
following copyright and license notices just after the title page:
Copyright Ā© YEAR YOUR NAME. 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 section entitled āGNU Free Documentation Licenseā.
If you have Invariant Sections, Front-Cover Texts and Back-Cover Texts, replace the āwith . . . Texts.ā line with
this:
with the Invariant Sections being LIST THEIR TITLES, with the Front-Cover Texts being LIST, and with the
Back-Cover Texts being LIST.
If you have Invariant Sections without Cover Texts, or some other combination of the three, merge those two
alternatives to suit the situation.
If your document contains nontrivial examples of program code, we recommend releasing these
examples in parallel under your choice of free software license, such as the GNU General Public License, to
permit their use in free software.
310
Page 324 of 324
yee-phd.pdf
Page 321 of 324
