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 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.