[EM] CORRECTING Black box voting repost re how HAVA imploded

[Ka-Ping Yee]

On Thu, 1 Feb 2007, Michael Poole wrote:
> Some companies have done rigorous proofs of software correctness for
> applications like money-holding smart cards (including proofs for the
> related protocols).  This is a more-constrained problem than
> electronic voting -- primarily in the complexity of I/O channels.
> Proving correctness for the money cards still required a lot of
> research in formal methods, and a lot of time and money to apply the
> formal methods to the software.  The last time I looked at the
> literature on software proofs, something on the scale of DRE voting
> could not be verified by proof.

I'm working on this.  It's still at the research stage, but you might
be interested in checking it out.  Last year i developed very small
software for running a touchscreen voting machine, aiming for something
small and simple enough to be verifiable.  See:

    http://zesty.ca/voting/

Diebold's code is over 31000 lines of C++.  My prototype weighed in at
less than 300 lines of Python -- small enough that one might actually
reasonably consider verification.

That prototype is only for sighted voters (touchscreen input and
output).  I'm now working on a new prototype with both video and audio,
to provide greater accessibility.  It's looking like this won't exceed
twice the size of the first prototype.


-- ?!ng