>
Yeah, let's just ask the engineers who are solving one of the toughest robotics problems ever to rewrite the entire house of cards that is their technology stack without any vulnerabilities.I did say "very expensive". But yes, if we're serious about correctness, safety, and security, I don't see any other choice. We should scrap the crap and spend the $billions necessary to rebuild it right.
Ideally. We don't really need to go that far. Isolation is possible and not that hard, see Qmail: http://hillside.net/plop/2004/papers/mhafiz1/PLoP2004_mhafiz...
> Of course even machine checked proofs will have trouble finding vulnerabilities that creep in during the specifications stage or exist in the realm of hardware.
I'm no hardware specialist, but you can still prove the correctness of the design of such and such hardware. The actual chips can still fail the specifications, but that's easier to test once you know the design itself is correct.
Also, specifications themselves can be checked. Only the high-level properties must ultimately be decided and reviewed by hand. Not that they won't be complicated or numerous, but that's still much smaller and easier to deal with than the entire implementation.
> How do you isolate your sensors from external input and expect to do anything?
I wasn't talking about the normal sensor input, which of course can be tricked the same way human sensory input can (for instance with a big flash or something). I was thinking about sensor command, such as which way they should be oriented or something. Though I expect most sensors will have no such input, and will only output to the system.