Today, Microsoft announced our joint work on ElectionGuard and the upcoming release of the software development kit. This SDK will be freely available, and can be used to enable end-to-end verifiable (E2E-V) elections around the world. An E2E-V election uses cryptography to produce proofs that an election has been run correctly. In a properly implemented E2E-V system, it is impossible for the voting system to cheat without detection. E2E-V puts the power to fully check election correctness into the hands of the public, allowing us all to independently confirm election accuracy.
We are thrilled to be taking part in the design and implementation of the ElectionGuard SDK. Collaborating with Dr. Josh Benaloh, Microsoft Research, and Microsoft’s Defending Democracy Program team has been ideal in bringing such a wide-ranging vision to light. We hope that today’s announcement will kick off an even bigger collaboration, one that we expect will involve the entire elections community, including other cryptographic researchers, accessibility experts, hackers, elections vendors, and everyone in between.
One of the most incredible aspects of the ElectionGuard SDK is that it will be usable by anyone. The SDK can be used as the core of most of today’s election systems. It will be designed for a wide range of hardware, operating systems, and election configurations. Our documentation and API design methodologies will make it straightforward to convert existing systems to use ElectionGuard. The same approaches also serve to make ElectionGuard hard to misuse; the API design makes entire classes of misuse impossible.
Moreover, ElectionGuard will encourage the kind of open source ecosystem where hobbyist programmers can easily develop and share open election systems. The SDK will be easy enough to use that a class of high-school programmers might develop an election system for use by their own school. Those elections can then be run on software that the school already owns, and by the nature of end-to-end verifiability, the results can be checked with as much certainty as they can in any other E2E-V election in the world.
The presence of end-to-end verifiability is not a reason to let down our guard. Every day, Galois works to secure the world’s most critical systems, and we are using the best we have on ElectionGuard. We have already started building up layered evidence of the correctness of ElectionGuard, starting with rigorous specification languages, and continuing with formal verification, cryptographically secure logging, and constant internal consistency checks. Thorough and formal specifications of the E2E-V protocol are being developed in collaboration with Microsoft Research and other top cryptographers from around the world. On top of all of this, ElectionGuard will support risk limiting audits as yet another independent way to confirm the validity of election results.
As the summer progresses we will release our cryptographic specifications, system designs and documentation, and eventually a usable SDK. Each of these releases will provide opportunities for the elections community to provide feedback on ElectionGuard. Our work on building correct and secure systems is meant to inspire trust, but our techniques will only inspire confidence if they can be understood. We intend to take the time to explain our entire assurance case, to give those concerned with system correctness the ability to read our formal documents in order to decide for themselves if the properties we prove of our software are appropriate. ElectionGuard represents an opportunity to change the way that the world view elections, and we can’t wait to share this experience with all of you.