Election Abnormalities
The election of 2020 is the strangest I’ve ever seen: I stayed up fairly late, seeing Donald Trump in the lead and then woke up to a ‘miraculous’ turnaround setting Biden as the victor… and then reports came out about vote-switching, vans at 3 AM, networking anomalies, and more.
There were legal challenges, which I thought had the feel of being designed to lose — “taking a dive” — and that’s only on Trump’s legal team’s part. The entirety of the Judiciary seemed unconcerned with Justice, culminating when the Supreme Court declined to hear the case with Texas and 20 other States in their original jurisdiction. (This alone would be reason to support judicial reform, as I have thought for decades, but that’s a rant for another time.)
Then came January 6th, the certification of the electors and their votes. What we saw there was disappointing: not only was the judiciary unconcerned with a just election, but the Congress certified these questionable votes — the whole ‘riot’ seeming to be perfectly engineered to give an excuse for doing so, while simultaneously setting the stage for the oppression of patriotic Americans under the guise of fighting “white-nationalism” and “domestic-terrorism”… despite the clear difference between the events at D.C. and the so-called “peaceful-protests” of the last year which left many buildings ash, and destroyed small businesses.
So, this opens up an uncomfortable question: how many of our elections have been subverted? How many policies were snuck in, shoved down our throats by subterfuge? — A friend told me that up in Maryland the first vote with electronic-voting machines had homosexual marriage as one of the items, it passed, but nobody he talked to had voted for it. Even California, via it’s Proposition 8, decided to reject homosexual marriage. (Proposition 8 was thrown out by a single federal judge as ‘unconstitutional’ and the US Supreme Court refused to hear the appeal, letting the judge’s pronouncement stand.)
The Design of a Secure Voting Machine
- No ethernet-, USB-, FireWire, RS-232, parallel or other such ports;
- An exception for a single read-only mechanism for tabulation; preferably something standardized but uncommon, like GPIB;
- No radios: WiFi, Bluetooth, etc;
- Custom CPU, eliminating all unnecessary opcodes;
- No Operating System;
- Use of formally provable software: custom bare-metal vote-counting program;
- Use of formal proving on the CPU.
- At least two write-only records for the purpose of auditing.
Auditing
The inclusion of auditing information is essential for rebuilding trust in our elections, and thanks to the miracle of the technology of the 1970s, we can have two audit trails just like grocery stores across the nation: print one copy of the ‘receipt’ for the store internally, and another for the ‘customer’.
Formal Proof
While traditionally the usage of formal proof in large software projects has generally been seen as ‘cost-prohibitive’ by the management in charge of software development, there are some exceptions: NASA’s spacecraft, Aeronautics (Airframes & Air-Traffic Control), and Medical Devices. — Why not the software used in our elections?
The cornerstone of formal proof is the ability to (a) prove that given some precondition, some postcondition must follow; (b) ensure that certain properties are met, typically in service to (a), but sometimes; (3) ensuring the functional correctness of the underlying object, be it code or electronics-systems… twenty or twenty-five years ago doing this in a cost-effective way may have been impractical, but the Department of Defense commissioned the programming language Ada in part to be formally provable given static analyzers. That tooling has been upgraded and incorporated into a toolset operating on a restricted subset of Ada such that you are able to prove the functional-correctness of the code [generally] automatically. — The Department of Defense also commissioned a similar project for hardware, which later became VHDL.
It’s beyond ridiculous that these two technologies haven’t been used to ensure the provable correctness of both the software and hardware involved in handling our elections.
Restricted Hardware
The purpose of restricting hardware via elimination is obvious: it reduces both the opportunity to subvert the system, as well as reduces the amount of time & effort required to verify as correct. — After all, there can be no internet breach if there is no ethernet-port, network-stack, or even the circuitry to operate it!
GPIB, as mentioned above, is a standard from the 1960/70s and is commonly found in automated test equipment; it should be simple enough to implement in hardware so as to provide read-only access to the votes tallied on the voting machine.
While I have other, more specific, thoughts on the matter, I think this should impress on you not only how feasible a provably correct voting system is, but how the current voting machines are, to put it bluntly, optimized for election fraud.
