The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

On Sun, May 1, 2022 at 3:51 AM Stefan Monnier <monnier AT iro.umontreal.ca> 
wrote:

> That's why I referred to e-voting, which is different from formally
> verified voting machines.
>
> e-voting relies on a cryptographic communication protocol and doesn't
> make particular assumptions about the trustworthiness of the machines
> used by the remote voters.
>
> Formally verified EVMs on the other hand rely on correctness of the code
> running on the actual voting machine (and correctness of the hardware,
> etc...).

Formal verification of EVMs is nice to, or I would say must, have, but 
elections
require independent verification/auditing of results. To achieve independent
verification in case of EVMs, we can use VVPAT [1]. Every voter can verify 
that
machine captures their intention (individual verifiability), and
everyone can verify
that the final tally is produced based on cast ballots (universal
verifiability). This chain
of verification, individual and universal, eliminates the chances of fraud.

My rationale for verifying the EVMs is that India is not going back to
paper based
elections (in fact, I conjecture that most of the countries conducting
elections in some
electronic form are not going back to paper based elections).
Therefore, it is better to
make sure that these machines are verified, open sourced, etc. EVMs
used in India is
closed source, the source code for conducting election in Australian
Capital Territory (ACT)
Canberra, is closed source and proprietary [2] (you need to sign 
confidentiality
agreement), and even sometimes, in a very rare event, you can be denied to
inspect the source code [3]. If you dig more, you find secrecy is widespread
phenomena, either it is EVMs (simple machines) or e-voting (general purpose
computers).  The horrifying part is that many companies involved in
e-voting (general purpose computer voting) simply write the software
programs  to conduct elections in C/C++/Java and establish
the correctness by testing! Ideally, I would like a voting-machine whose
hardware is formally verified and open sourced, the software running on
it is formally verified and open sourced.  Moreover, it has gone through
some very challenging stress testing something like this [4] (Btw, this
system was running on SeL4, a formally verified operating system
developed in Data61, Australia, but unfortunately CSIRO, the parent
body of Data61, dismantled the formal verification group. This group
literally achieved impossible!). If DARPA can achieve the impossible [4]
using formal verification, there is a lot of hope for democracy as well.


Best,
Mukesh


[1] https://en.wikipedia.org/wiki/Voter-verified_paper_audit_trail
[2] 
https://www.elections.act.gov.au/elections_and_voting/electronic_voting_and_counting
[3] https://www.aec.gov.au/information-access/foi/2014/files/ls4912-1.pdf
[4] https://www.311institute.com/hack-proof-code-defeats-darpa-hackers/



>
> They both involve computers and voting but they are quite different, AFAIK.
>
>
>         Stefan
>