SoylentNews is people
SoylentNews
from the newer-is-not-necessarily-better dept.
The Intercept reports
The nation's secretaries of state gathered for a multi-day National Association of Secretaries of State (NASS) conference in Washington, D.C., this weekend, with cybersecurity on the mind.
Panels and lectures centered around the integrity of America's election process, with the federal probe into alleged Russian government attempts to penetrate voting systems a frequent topic of discussion.
[...] One way to allay concerns about the integrity of electronic voting machine infrastructure, however, is to simply not use it. Over the past year, a number of states are moving back towards the use of paper ballots or at least requiring a paper trail of votes cast.
For instance, Pennsylvania just moved to require all voting systems to keep a paper record of votes cast. Prior to last year's elections in Virginia, the commonwealth's board of elections voted to decertify paperless voting machines--voters statewide instead voted the old-fashioned way, with paper ballots.
[...] Oregon is one of two states in the country to require its residents to vote by mail, a system that was established via referendum in 1998. [Oregon Secretary of State Dennis] Richardson argued that this old-fashioned system offers some of the best defense there is against cyber interference.
"We're using paper and we're never involved with the Internet. The Internet is not involved at all until there's an announcement by each of our 36 counties to [the capital] Salem of what the results are and then that's done orally and through a confirmation e-mail and the county clerks in each of the counties are very careful to ensure that the numbers that actually are posted are the ones that they have," he said. "Oregon's in a pretty unique situation."
[...] In New Hampshire, the state uses a hybrid system that includes both paper ballots and machines that electronically count paper ballots with a paper trail.
Karen Ladd, the assistant secretary of state for New Hampshire, touted the merits of the system to The Intercept. "We do a lot of recounts, and you can only have a recount with a paper ballot. You can't do a recount with a machine!" she said.
America's paper ballot states may seem antiquated to some, but our neighbors to the north have used paper ballots for federal elections for their entire history. Thanks to an army of officials at 25,000 election stations, the integrity of Canada's elections is never in doubt.
(Score: 2) by TheRaven on Tuesday February 20 2018, @02:07PM (5 children)
It's a problem of trust. How many people have enough mathematics to follow a formal proof of correctness of a voting system? Let's say ten thousand. Now, to trust the election, every voter who is not one of these people has to trust at least one of these people. Unfortunately, the people in that group are all highly educated, with a strong bias towards current and retired university employees. If you are voting for a party that mostly represents working class voters with a maximum of high school education, do you trust verification carried out by a group whose interests may be diametrically opposed to yours? Are you willing to bet your country on the idea that foreign nationals with no vested interest in your wellbeing would rather point out the flaw than keep quiet while people like them run your country?
sudo mod me up
(Score: 2) by Wootery on Tuesday February 20 2018, @03:53PM (4 children)
I probably would, yes. The world's a big place, we're talking about an Open Source project, and it only takes one objector to kick up about a flaw.
Compare: the Soviets' Cuban missile project. There were no leaks there and the USA only discovered the sites through U2 reconnaissance missions. Because the (doubtless numerous) people who knew of the project were all working on the same side, and would have taken on enormous risk exposing the project anyway (which, again, they were not motived to do in the first place).
That's not how crypto works, though. When a researcher finds a problem, they publicise it. It's adversarial scholarship in action. It would be the same here. Deliberate maliciousness in FOSS is pretty rare even in obscure projects (though I'm aware people have tried it with the kernel).
It would certainly be a damn sight better than those amateur-hour Diebold trainwrecks.
Again though, I'm still against electronic voting. Even with such a software system, you can't trust the final deployment. More compellingly still, there's just not enough reason to move away from paper ballot in the first place. Digital isn't always better.
(Score: 2) by TheRaven on Wednesday February 21 2018, @02:51PM (3 children)
But it also takes one objector to have the time and expertise to conduct a full review. How long did vulnerabilities like Heartbleed stay in OpenSSL, when companies had a big financial incentive to care that it was secure? If they find a flaw a year after the election, what do you do, re-run the whole thing?
And then, a decade later, something is declassified and you learn that the NSA and / or GCHQ knew about that vulnerability 20 years earlier and were using it for all of that time. If you're working for the FSB and you find a vulnerability in the US election code, do you publish it? My guess is that you either tamper with the election, or you wait for a year after the election and then leak evidence that you knew about the vulnerability and pretend that you tampered with the election and undermine trust in the process. And, actually, if you don't find a flaw, then leaking that you did and tampered with the election will have a similar effect - and how does the government then prove that there wasn't a flaw in the formal verification of the voting system in a way that the majority of the population would trust?
sudo mod me up
(Score: 2) by Wootery on Wednesday February 21 2018, @04:59PM (2 children)
Indeed, I'm putting some faith in formal methods making this considerably easier. I presume it would be a good deal harder to conceal a malicious 'feature' in a formal spec (from which the imperative code is then refined) than in a typical ball-of-mud C codebase.
To your second paragraph: all good points. I don't know formal methods well enough to know how much real help they'd be in all of this. Perhaps my point boils down a With a sufficiently approachable formal system... pipe-dream.
(Again though, the impossibility of trustable deployment renders our whole exercise insignificant.)
(Score: 2) by TheRaven on Wednesday February 21 2018, @06:39PM (1 child)
If anything, they make it harder. To check a formally verified program you need to understand both the problem domain and the mathematical tools. That dramatically reduces the set of people that can do it. You can machine check the proof, but you can't check that the proof is actually telling you anything useful. seL4 is a great example here: all of their proofs are probably fine, but it was about 6 hours between their initial public release and the first security vulnerability being found, because the security vulnerability wasn't as a result of a property that was checked.
The problem with security proofs is that you need to define what security means before you can prove that a system has that property. You can't exhaustively enumerate security requirements, the next attack always comes from the thing that you didn't consider.
sudo mod me up
(Score: 2) by Wootery on Wednesday February 21 2018, @10:03PM
True, but I still think it'd be harder to conceal a deliberate defect.
Sure you can - it tells you the program fulfils the formal spec. Of course you still have to worry about side-channel attacks and anything not covered by the formal spec, but it's not as if the assured properties are worthless.
Side-channel attacks can be an issue with formal systems, sure, such as Haskell programs leaking secrets by having more predictable timings than the equivalent C code. Oops, wasn't part of the formal model, and the type-safety didn't help.
I missed the seL4 bug - what did they miss?
I'm not sure how that would manifest with a voting system, but that might just be proof that I'm not that imaginative.