The Coq mailing list

[Sam Kuper <sampablokuper AT posteo.net>]

On Tue, Apr 26, 2022 at 07:22:10PM -0400, Stefan Monnier wrote:
>> But imagine that voting machines are formally verified from hardware
>> to software,
> 
> What problem do electronic voting machines solve?

Some ballot boxes (intended for use with paper ballots) are not secure.

Example:

Some of them have zip closures: the slider on the zip is lockable (e.g.
with a padlock), the idea being that once the zip is closed and the
slider is locked, the contents are "secure" from being stolen/replaced.
Tamper-evidence can be added by applying tapes/seals to parts of the zip
or the lock.

However, in some jurisdictions that use these ballot boxes, election
officials fail to apply tamper-evidence mechanisms properly, meaning
that the ballot boxes' contents can be accessed/replaced by picking the
lock or by forcing the zip open/closed away from the slider, leaving no
obvious evidence of tampering.

Even if the election officials apply tamper-detection seals/tapes/etc
properly, those seals/tapes/etc themselves may in fact be undetectably
defeatable - again allowing surreptitious access/replacement of ballot
box contents.

Therefore, where ballot boxes are, as above, not themselves robust
against access, and if they are also stored (between the time of the
ballot and the time of the count) in a place where an attacker can
tamper with their contents away from observation and cover their tracks,
then the attacker may be able to affect the outcome of the ballot
without anyone else being the wiser.

Source: I unofficially observed the procedures followed, for several
national and local elections, at a particular polling station in a
European electoral district.  I noted several ballot boxes were
vulnerable to tampering, and were temporarily stored (long enough for
tampering to potentially occur) in a location not sufficiently under
guard to ensure intruders would be noticed.  I did not see anyone
actually try to tamper with the ballots - but due to the vulnerabilities
noted above, this was not wholly reassuring.


Would formally-verified voting machines solve these problems?  Possibly,
depending on implementation.

Sam