[seanwilson]

Seems like a decent place to apply formal verification as well to show the machines are bug free. Voting machines are critically high impact if they have bugs and (famous last words) the complexity of the software seems low.

[kijin]

The counting app itself might be low-complexity, but I'm pretty sure the app runs on some kind of off-the-shelf OS with hundreds of millions of lines of code and at least a few known vulnerabilities.

A somewhat outdated version of Windows is a common choice, as is some random non-LTS version of Ubuntu. I don't think OpenBSD is particularly popular among self-serve kiosk manufacturers.

[DSMan195276]

I think it's worth adding that if it doesn't use some off-the-shelf OS, then the complexity of the software just jumped a few levels because you're talking about writing a lot more lower-level components to make it work. Using an off-the-shelf OS is almost definitely the better way to go unless there's some obvious reason that it won't work (Like architecture issues). I would also add that the choice of OS matters a lot less then configuration - If you do your configuration carefully and strip down the active components in the system, then you can make any of them secure enough for this task. And if you do a poor job of it, then even OpenBSD isn't going to save you.

That said, while I do agree the voting software should be open-source in principle, I'm not really as concerned with hackable bugs in that software that can only be exploited through physical means. If they have physical access to the machine like in this video then you're already shot - ideally you have preventive measures that will make it obvious when physical access has occurred. If you don't physically secure the machine, then it doesn't really matter how good the code is.