But with IoT I'm not necessarily after one person. I'm going after a million people who all have the same garbage device. If the payoff is bigger the incentive to keep pushing past obstacles is very high.
You CAN write proven bug free code, but only if you are willing to accept a long series of limitations.
It could still be the case that for all practically relevant programs there is a proof in each case that they are secure, even if there is no automatic way to find it.
It makes it impossible to say whether certain things can be proven to be secure.
If you use a finite state machine, You can control the states and make mathematical assurances that your program terminates.
The solution to the halting problem is that you work backwards, instead of forwards. You don't let a program run forever and hope for the answer. We also don't give infinite memory to programs to eventually exit/halt or not - My machines have 8 GB and 32GB ram. And oomkiller does its job rather well.
Tests work because they are arranged by humans to verify the system under test for validity, but only for one specific system at a time.
The halting problem is basically an admission that one is unable to write a test to verify arbitrary programs on arbitrary, Turing complete hardware. You must be 10% smarter than the piece of equipment in short.
Killing something for taking too long or eating too much memory makes no substantive judgement on whether the computation at hand is ready to return or not, You (or your OS) just unilaterally made the decision that the computation wasn't worth continuing.
The Halting problem depends on a turing machine. As stated by Wikipedia, a turing machine is:
"a mathematical model of computation that defines an abstract machine, which manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, given any computer algorithm, a Turing machine capable of simulating that algorithm's logic can be constructed."
The first description how to build one is, "The machine operates on an infinite memory tape divided into discrete cells."
Infinite memory? Well, that's already trivial to dismiss then.
And I also said that things that need to be proved should be using finite state machines. Using an FSM means a dimensionality reduction to a thing that doesn't suffer from the halting problem. One can make complicated graphs, yet still not introduce the same pitfalls as a turing machine has.
And, here's a paper arguing that FSM's dont suffer from halting problem. https://pdfs.semanticscholar.org/025b/97d66265dfbcb02d9dd1a2...
I'm kinda holding my breath that they turn out to be right.
Programmers only care about three numbers: zero, one, and "out of memory"Compilers have plenty of bugs, so do operating systems and CPUs as we have seen in recent years.
Only when "code" is thought of as an abstract notion existing in isolation from inputs, outputs, real systems, etc.
That‘s the point, isn‘t it? No system will ever be 100% secure, so all we can try to achieve is to deter attackers.