The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

Formal verification don't need to provide a solution to all problems
to be valuable.  Especially in situations where, by construction,
ordinary people are exactly on the same foot as experts.

My 2 cts,
JF


On Wed, Apr 27, 2022 at 04:27:50AM -0400, Mario Carneiro 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
>    <[1]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
>      <[2]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
> 
> References
> 
>    Visible links
>    1. mailto:jean-francois.monin AT univ-grenoble-alpes.fr
>    2. mailto:monnier AT iro.umontreal.ca

-- 
Jean-Francois Monin
Verimag
Universite Grenoble Alpes