The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

What you describe here, Abhishek, is a social problem that I do not think can be 
solved by technology. In fact I think it is made worse by technology (see e.g. 
https://en.wikipedia.org/wiki/2004_United_States_election_voting_controversies).

For me, it makes little difference whether voting computers (or voting machines, 
as they are often called when the manufacturer wants to distract from the fact 
that these are general-purpose computers we are talking about) are formally 
verified. Sure, if the choice is between an unverified and a verified voting 
computer, I will prefer the verified option, but this is a marginal difference. 
I still can't know that the computer I am voting with actually runs the code 
that has been verified. And only very few people can actually understand the 
arguments on which the integrity and correctness of this process is based.

I agree with the others who said that one of the most important criteria of a 
voting system is that everyone can understand it and be convinced that it works 
as intended. I believe this criteria to be fundamentally unsatisfiable for any 
form of electronic voting.

Regarding what Marco 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. 

I am a big believer in formal verification, but I think there are problems 
formal verification cannot solve, and voting is one of them.

Kind regards,
Ralf

On 30.04.22 23:41, Abhishek Anand wrote:
> > It doesn't seem to be an argument for formally-verified EVMs, tho, since
> > in this circumstance the "goons" could just connect another machine to
> > the central server.
>
> Not necessarily. There are cryptographic remote voting schemes that are coercion 
> ("goon") resistant (as long as goons don't interfere with voter registration) 
> yet cryptographically verifiable by everybody, e.g. 
> https://www.cs.cornell.edu/projects/civitas/papers/clarkson_civitas.pdf (I am not a 
> crypto expert and I hope I did not mischaracterize the work of crypto voting geniuses)
>
> Andrew Appel has some criticisms about similar systems 
> (https://freedom-to-tinker.com/2018/11/05/end-to-end-verifiable-elections/), 
> which I mostly agreed with just 2-3 years ago.
> But with what happened to the US in the last few years (1. proliferation of mail-in voting 2. 
> extreme polarization and isolation: the "2" sides don't talk to each other and consider 
> the other side as completely evil and/or uninformed and each side thinks the world will end if 
> the other side wins), I don't anymore trust the people involved in the election process, e.g. 
> mail delivery people carrying mail-in ballots, to steadfastly adhere to the electoral specs and 
> not succumb to the "ends justify the means" attitude. Now, IMO, a system that ensures 
> that at least the votes of the tech-literate people were properly accounted for would be better 
> than the status quo. I don't think tech-illiterate are unworthy of voting and I wish there was a 
> better solution other than the daunting challenge of educating them on crypto fundamentals.
>
> I think such crypto voting schemes should be implemented and verified. Even 
> if they cannot be used for voting on governments, they have many other 
> applications. One application close to my heart is to reduce the chances of 
> dishonesty in clinical trials, especially those conducted by pharmaceutical 
> companies. Clinical trials are in many ways isomorphic to voting in that the 
> objective is to produce a correct tally: you have 2 groups (experiment and 
> control/placebo) and the main outcome is the tallies (totals) of various 
> outcomes (e.g. deaths/heart-attacks/infections) in both groups. If heart 
> attacks are much lower in the experiment group and the group was randomly 
> chosen, it is strong evidence or effectiveness of a pharma product. A problem 
> though is that the pharma companies cannot be trusted to honestly produce the 
> tallies: they produce the tallies with almost no oversight from people not 
> having a financial COI with the outcome: a situation much worse than 
> political voting. This is not just a theoretical concern: there are many many 
> instances of fraud, e.g.:
> https://www.ncbi.nlm.nih.gov/pmc/articles/PMC1779871/ (Merck hid reports of 3 
> heart attacks in the trial of vioxx, which was later found to cause heart 
> attacks)
> My suspicion lately is that the known instances of fraud are just a tip of 
> the iceberg: it is very common to see pharma products perform much worse in 
> the field and in trials not sponsored by the manufacturers than that in the 
> manufacturer-sponsored trials.

--
Website: https://ralfj.de/research