The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

+1

I am convinced that formal verification could protect ourselves of 
unintended bugs in software and hardware. But, not against malicious 
bugs. The "trusted computing base" will remain too big and too complex.

A few references on the subject:

* Andrew Appel's papers on the subject:
  https://www.cs.princeton.edu/~appel/voting/index.html

* Jie Zhang, Feng Yuan, and Qiang Xu. “DeTrust: Defeating Hardware Trust 
Verification with Stealthy Implicitly-Triggered Hardware Trojans.”
  https://dl.acm.org/doi/10.1145/2660267.2660289

* Ken Thompson. “Reflections on Trusting Trust.”
  https://dl.acm.org/doi/10.1145/358198.358210


In contrast, there are very trustable low tech solutions.

A real issue with French voting system is that the result do not reflect 
what people really want (and institutions are poorly democratic).

Solutions like https://en.wikipedia.org/wiki/Majority_judgment are 
well-known, but politicians who would have the power to change the 
system do not want to change it, because they benefit from the current 
system.

Sylvain.

Le 27/04/2022 à 09:48, Jean-Francois Monin a écrit :
> +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