1. 12

  2. 6

    “No one doubts that the companies take security seriously.” I doubt it and everybody reading this article should doubt. Saying that the companies take security seriously is a huge joke but not a really funny one. (I’m french and we are “happy” to allow abroad citizen to vote online)

    1. 2

      I liked the article, and I’m not super keen on auditless voting machines, but there’s a bit of FUD and alarmism mixed in here too.

      The seven minute hack involved Appel climbing behind a machine, picking a lock and replacing a bunch of ROM chips unobserved. There are 425 (minimum, some precincts may have more than one) such machines in montco. 7 minutes times 425 means this is at least a two day hack. :)

      1. 3

        But do you need to hack them all? Just hack a few machines in carefully-chosen precincts and you’re golden. You don’t need to determine the exact outcome or override every single vote, you just need to nudge things in your chosen direction. In fact, a properly-timed DoS attack against the machines might be all that is required, especially in a country like the US where most people have to work on election day.

        1. 2

          Well, how many machines need to be disabled for the Kremlin to swing the election for trump?

      2. 1

        Best vid on this stuff with examples and people that tried to do something about it:


        Far as Appel, he and others' work on verified software are their greatest contribution to safety/security as we’ll likely use them to prove out the tools to solve all kinds of problems. Example of how that might play out is Esterel’s SCADE system for modeling & generating code for embedded systems. High-integrity systems like that have to work every time. It was written in Ocaml, rigorously quality checked, and the source to object code translation checked. Work like Appel’s on ML could enhance vetting the source side via types/analysis and/or source-to-object checking via verified compilation. That would let both developers and evaluators spend more time on other features. Another example is their work on verifying C programs and compilers that might have lots of impact given all the stuff written in it.

        Edit to add list of their papers: