Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Electronic Voting Machines in French Elections

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Electronic Voting Machines in French Elections


Chronological Thread 
    < Chronological >      < Thread >
  • From: Mario Carneiro <di.gama AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Electronic Voting Machines in French Elections
  • Date: Wed, 27 Apr 2022 04:27:50 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=di.gama AT gmail.com; spf=Pass smtp.mailfrom=di.gama AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f179.google.com
  • Ironport-data: A9a23:rPk346gdTZSgv4L3ZTnpyoRWX161UhYKZh0ujC45NGQN5FlHY01je htvXWGDOqqLNjTzKYolOtiy/R5UvJTcmNdmTwFr+SkyRXhjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKieUsxIbVcMpB0J0HqPoMZkxN8w6TSFK1nV4 4mq/5eBYATNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ NplibCXdlg2Nfb2vM8iSEZDOCxcOpdmweqSSZS/mZT7I0zudnLtx7B3EBhzM9RHq6B4BmZB8 fFeIzcIBvyBr7jukfTrF6812JxldZa6VG8ckikIITXxAfdgTpnGSo3F4NZZ2HE7gcUm8fP2P pBEMmMwPEuojxtnZGdJOYwDzdWUj3TnVjd8o06JgvNm7D2GpOB2+OG1bIC9lsaxbc5ShwOTo n/M13/oBwkTct2Z0zuMtHy27tIjhgv+UYMWUaSkr7tk2QLCgGMUDxISWB2wpvzRZlOCt8x3F 2AzxXUxpvMI0GeUVYbmdBCap0Skh0tJMzZPKNES5AaIw6vSxg+WAGkYUzJMAODKUudmFFTGM XfZz7vU6SxTXK69Ei3Cq+/Fxd+mEW1Ecj9YPH5soR4tuoG7+OkOYgTzosGP+ZNZY/XwEDD0h imW9W0w3upCy8EM0Kq/8BbMhDfESnn1ouwdtlm/soGNtFkRiGuZi2qAtwCzARFoct7xc7V5l CJY8/VyFchXZX13qASDQf8WAJai7OufPTvXjDZHRsd8r2X2oi79IN8PvVmSwXuF1O5UKFcFh 2eD6WtsCGN7YRNGkIcsM9nhVJ96pUQePY29DaCFNrKinaSdhCfepH00DaJh92/ql0conMkC1 WSzIK6R4YIhIf0/llKeHr9DuZdyn3xW7T6NGPjTkkv/uZLDNSb9YepUazOmM7FphIva+lm92 4gEbKOilU4PONASlwGNrub/23hRfSZlbX03wuQLHtO+zv1ORT9xVqeNke9wE2Gn9owM/tr1E riGchcw4DLCabfvc21ms1hvN+HiW4hRt3U+MXB+NFqkwSlxboOm7aNZfJwyJOF1+OtmxP9yb v8EZ8TQWqQVGmqbo2wQPcvnsYhvVBW3ngbRbSeoZT4IeZQ/FQHE/9nTeBTiqXsVBS2tuMpi+ LCtj1uJQZcKSwl4ItzRbfajkwG4sXQHybB9WkLJJp9Yf0C1qNpmLCn4j/kWJcAQKEWblmHKi VrOWRpB/LvDuY449tXNlJuolYbxHrssBFdeEkna8a2yanvX82+l9olKD7SFcDXbY2Xrofnwa OhQycb8B/0JhlN9tYRxTuRwxqUk6tqz/rJXw1g2HHjPaFj3WLpsLmPcgZtKv6xJg6ZF4E64A x3evNZdPrqNNYXuF1tIfFgpaeGK1Pc1nDjO7KRqfB+runcvpLfXA19POxSsiTBGKOcnOo0Sx +p86tUd7Bayi0Z3P9va3DpY8X+Aci4JX6k97M1IBYbqjk8y1ggHb8WDW2n555aAb9gKOU4ve 2fGiK3HjrVa50zDb3tjSiSXjLQF3cwD6EJQ0VsPB1WVgd6Z1PU56xtcrGYsRQNPwxQbju9+N wCH7aGuyXliItupuCRCY4xoMwRIBRnc41CojlVQyzyfQE6vWWjAamY6PI5hOazfH310JlBmE HOwkQ4JkgoGuOn+2yIzXQhurPmLoRlZ6FjZgM7+dyiaN8BSXNcm65NCoUIHrhLmBYU6g0ivS SyGOgpvQfWTCBP8aJHXx2VXOXr8hfxEyKF/rSldwZ40
  • Ironport-hdrordr: A9a23:Z5pJGqM7LunL9sBcTvijsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZEmPHPP+VQssTQb6LO90cq7IE80l6QFhbX5VI3KNGLbUSmTTL2KhrGSpAEIdReOkNK1Fp 0NT0G9MrDN5JRB4voSKTPXL+od
  • Ironport-phdr: A9a23:kWwMnRMgSMp2tKnkTocl6nZQBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv64r1QKCBdyTq6odzbaM6ea4AS1IyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf71/I A+roQjRucUanZZuIbs1xhfVv3dEYetbyX12KV6Jgxrw+sK894N//ipNvP4s69ROWrjgcaQiS rxYAjUmM2Qr68DuqBLOUwiB6GYCX2sPihZHDBTL4x/8Xpfqryv1rfF91zWAPc33Vr87RzKv5 Lp2RRDyiScHMzk58HzLisF1kalWrg6tqwB5zoXJZoyeKfhwcb7Hfd4CSmVBUMReWSxPDI2/c oUBEfYOMP1CoIXhvVYDtweyCRWuCe7p1zRGhmX23ao/0+k5Fg/JxhYgH9MJsH/Jstj6Lr0SU earw6nJ1zXDaO5d1DDg54jJaBwhruuDXbdqfsfKxkkvEhnKjlSUqYD/IzyV0eENvnGd4uF9W u2hl3QppBttojiz2MgskI/Ji5oaxF3a9ih0xIY4KNO8RUN4btOoDJVeuzyGOoV5XM4vTGVlt Tg0x7AJp5O3YicHxZU7yhPCd/GKfImF7g79WOiRJzpzmXFreKqnihqs7UStzvfwW8q03VpQs yZIk8XAumoQ2xHR7sWKTOZ28F271jaVzQ/T7/lJIUAqmqrfLJ4s2rswmYASsUTHByP2gVn2g LKPekUq5+Sl6eDqbq/ppp+bMI90hQX+Pbo0lsOjBuQ4NxACX2md+euiyL3u5VP1TKlOg/Esk aTUsIrWKdkaq6KlGQNZz4Qu5hKnAzejytsYnH0HLFxfeBKAiojkI0zBIPHiAfewmVuslS1ky uvJPr3kGJrNL3zDnK39crZ67k5Q0AwzwstH6JJOFr4BOO7zWlP2tNHAExM1Kxa0zPr/CNVhy oMeXnqCDbOeMKPLqFOH+uYvI/SXa4IOozb8K/0l5+b0gnMjmF8de7Op3ZoNZ3yiEPRmORbRX X25idAYVGwOowAWTerwiVTEXyQASWy1WvcZ7ys6D8qNBJ3FS4G3h/TV0Cb9EZRTb0hJD1mNF THjcIDSCKREUz6bPsI0ym9MbrOmUYJ0jXlG1Sf/wrtjda/P/zEA8InkzJ5z7vHSkhc78Xp1C d6c2ieDVTI8hXsGEhkx2q03uklh0hGby6Etj/0eGtVW7ttGVw47MdjXyOkpQ8vqVFf5d8ySA E2jXs3gBDgwStwrxNpbb0c7FNynhzjM2iOrB/kekLnYTIcs/Pf62H78b914126A1KQliAw+R dBTMGS9mqNl3w3aBoqMilnA0qjzKvVa0ynK+2OOi2GJuSm0SSZWVqPIFTAab0rS9pHi41/aC qSpEfIhOxdAzsiLLu1LbMfohBNIXqWrPtOWeG+3l2qqYHTAjrqRcIrnfXkc1yTBGQAFlQ4U5 3OPKQk5AG+ovWvfCDVkEV+nbVnr9KFyr3ayT0l8yA/vDQUp27vz9RcQjNSTTvoS2vQPvyJg4 zR4EVCh3s7HXsKarlkpd6FdbNUhpVZfgDiB5kotY9r5cfgk3wFPIGEV9wv02h56C5tNi50vp XIul09pLL6AlUhGb3We1IzxPbveLi/z+gquYujYwAK7sp7e96ER5fA/s1imshuuEx9o/3Qh3 NBQ2lOT45zLCEwZVpe7ASNVv1Bq4qrXZCUw/dae2XwqPqCxuxfN3tsoAK0uzRPqLJ9PdaiDE gH1CcgTAcOjffcrl1aeZRUBJOlO9aQwMqtKbtO+0bWwdKZllTOi1iFc5Zxll1mL72x6Q/LJ2 JAMx7eZ2BGGXnHylgXpvsfykIFCLTYcewj3gSTlQoFYY6RacoMCCGPoKMqyjtlznJ/iXXdE+ UXrXQtXnp/0P0PMNxqkglwY3F9fuXG9nCqk0zF49lNh5rGS2iDD2aWqdRYKPHJKWHg3iF7tJ YauiNVJFEOsbgUviF6k/ROgn/kd9Pk5djeLBx4XLnuTTSkqSKa7u7ucbtQa7ZoptX4SS+Gge RWBTaa7pRIG0iTlFm8YxTYhdjjstI+q+n4ywG+bMnt3q2LUPM9qwhKKrtDdA/FY2zMuSyxxi D2RDV+5dYrMn53ch9LYv+ayWnj0HJFSNybiyIqouy6y5GksChq61aP7ipjsFg401jX+3t9hW HDTrRryVYLs0ryzLeNtekQ7YT20o9o/AIx1lZE8wY0BwXVPzIvA5mIJyC2gecUew6/1a2ABA CIG08KAqhaww1Vtdxfrj8r4TinPmZYnPojiJDlKhWRlqJoWQKaMsO4awW0v+QH+9FyJJ6A6x 2ZVyONyuiBExbhR4kx1iH3aWOh3fwEQPDSwxUrWqYri/eMHPCD3NuLonEtmwYL+Vvfb/kcFC Sy/ItB7TWdx9pktbw6KiSeurNmiIJ6JM7dx/lWVi0uS1rAFbstuybxaw3IgYzu1vGV5mbdk1 lo3jM385M7fbDwztKOhXkwCbmyzN55Vo2u9y/4Zx5nzvcjnH409SG9SAt21HbTxQWhU7bO+Z k6PCGFu8C7FX+CETEnEsgE+6CueW4aiM3XdTJUA5fNlQhTVZElWgQRPGS4/goZ8DQeygsrob EZ+4DkVoF/+sBpFjOxyZVH5VS/EqQGkZy1RKtDXJQdK7gxE+0beMNCPpuN1ESZC+5S9rQuLY mWFbgVMBGsNVwSKHVfmdrWp4NDB9aCfCI/cZ7PWZq6SrOVFS/qS7Zem048j5irVc8vWYSgkA Po81U5OG3t+HoWRmjkCTTAWizOYb8Ofo0TZmGU/pcS+/fL3HQP3sNHXWv0CbJM2pUjw2PjSZ IvyzG5jJD1V140B3yrNwbkbhxsJjj12MiKqCfIGvDLMS6TZnulWCQQaYmV9Lpgtjep00w9TN Mrckt6w2KR/i6t/B1YDWlXkk+mmYMULJye2M1aNVyPpfPyWYCbGxc36e/b2UbpLkOBdrAG9o x6eGk7ney2fznznDk/+d+5Liy6fMVpVv4T3IXMPQSDzCdnhbBO8Ktp+izY7lKY1in39PmkZK TFgcklJo9V4AgtXh/x+HypK6X83dIFsfg6W6uDZLtAdtv45Wkycdspf6XU+jqJJtWRKHaMk3 iTVqdFqrhetlezdklJa
  • Ironport-sdr: 86c1gFr5dVhliaN51Psd06YIzu8jym7GGdJOZJ/rcfxei3y55bJCrTnb7/Vh/gvudKOEuvh8rZ j/x+Fg9xjNG8U9kWG46xpfnnX8B9KyB3KTf2qGOPZt26DjqFTeuJBbtLCPtwTTw0zLc1Pi7FuA ZfvKBivJiwPg54g1U3hk0wY8RcGQd5J0c3GF2PfKdChbLBEfXqrtBFkvV3tJ3DUX02eNL8hokf 0Ut199XKPleB3zVdwATzGJe+yWNB6hoUISwWefne6GCqhEAybKE+aSjN+LMMQkokSBU+ciuIqC mySPlZblCGhD0vE6S62mzAQm
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

Archive powered by MHonArc 2.6.19+.

Top of Page