Idea: write a formally proven voting machine

For those having some spare time and who are willing to dig into tricky (but interesting) areas, I have a nice idea of project to do: write the (free) software of a voting machine where all (or at least most of) the code is formally proven.

The voting machine I consider would be a very classical one: no network connection (so no remote electronic voting), a touch screen with the different voting options, votes are stored on a local hard drive. One can use a standard PC as reference hardware (with for example a graphical screen with mouse click to emulate the touch screen), even if for a real voting machine a temper-proof hardware would be mandatory.

The purpose of the software would be:

• Before the vote phase, to take the set of vote option and the list of voters identifiers (an unique random integer for each one of them, that would emulate the use of a smartcard);
• During the vote itself, authenticate a voter (through his/her unique identifier), take his/her vote and store it;
• After the vote phase, output the vote result.

The software would be written in plain C, using information (and maybe code) from Simple Operating System (SOS) for hardware interface (mouse and screen control). Using Why proof obligation producer, one would produce the formal version of the program for the Coq proof assistant, that would be used for the formal proofs.

Of course, all of those software are available as free software and the resulting code and formal proofs should be also available as free software. The net result of such a project would not be a complete voting machine (this is much more complex than that) but a first step towards a trustable voting machine.

What do you think of it?

2006-01-25T18:03:05Z [] permanent link