The Coq mailing list

[Dominic Mulligan <dominic.p.mulligan AT googlemail.com>]

I don't see what harm there is in applying formal verification techniques to voting machines.  However, I also don't see it as some killer application of formal verification: ultimately, as a voter, even if I go along with the idea of verifying the tabulating code installed on these machines, why should I trust that verified tabulating code is indeed installed on the voting machine that I am about to use?  Sure, there are technical ways you could do this (using e.g., trusted hardware, cryptographic code measurement, open and freely auditable code, and reproducible builds of the verified code).  However, this hints at a problem common to all proposals, that I have seen anyway, for "provably secure" electronic voting: they quickly explode in complexity, bringing in baroque combinations of cryptography, formal specification and verification, and trusted hardware.  Not only is this a nightmare to explain to the generally technically savvy, but the layperson unwilling or incapable of understanding these proposals ultimately has to trust a relatively small number of people that the entire system is safe.  Even worse, we already have access to a known technique, in manual counting, that is easy to understand by all, trivial to perform and audit, efficient enough for its intended application, and with little evidence of widespread fraud (at least in the type of society that would likely deploy formally verified voting machines).

On Wed, 27 Apr 2022 at 09:28, Mario Carneiro <di.gama AT gmail.com> wrote:

I think that as long as people feel this way (including formal methods experts), then we haven't really accomplished our job as formal verification researchers. Electronic voting is a perfect example of a system that really puts the purported advantages of formal verification and TCB concerns to the test: if we can't convince ourselves that this can be done safely and securely, then it seems hypocritical to advocate for formal methods elsewhere in safety-critical and security-critical areas.

An effective solution to the problem requires many things:

* Software and hardware with open and accessible specification and implementation (except for cryptographic keys, of course)

* Formal verification of the implementation (also publicly available)

* Simple documentation of the process, not written for experts

* Public support by experts and government officials

The consequences of a failure in electronic voting systems are much more severe than paper ballot processes, but human error and collusion are also a thing, and it is clear to me that the local optimum of paper voting is not as good as the local optimum of electronic voting, but there is a huge gulf of bad implementations in between and formal verification is a necessary (but not sufficient) component to actually avoid the failure cases.

Mario Carneiro

On Wed, Apr 27, 2022 at 3:48 AM Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr> wrote:

+1

Low-tech paper solutions are robust and easily understood by everybody,
as well as attacks and countermeasures, so much better for confidence
and democracy.
Complicated technologies are just the opposite.

JF

On Tue, Apr 26, 2022 at 11:19:09PM -0400, Stefan Monnier wrote:
>
> The way I see it, the more people who participate (i.e. more eyes),
> the safer.
>
>
>         Stefan
>
>
> > On Tue, Apr 26, 2022, 18:22 Stefan Monnier <monnier AT iro.umontreal.ca> wrote:
> >
> >> > But imagine that voting machines are formally verified from hardware
> >> > to software,
> >>
> >> What problem do electronic voting machines solve?
> >>
> >>
> >>         Stefan
> >>
> >>
>

--
Jean-Francois Monin
Verimag
Universite Grenoble Alpes