We’re Doomed If We Don’t Secure Teslas and Infrastructure
forbes.com
forbes.com
Systems that show that reasonable security is possible includes NaCl, seL4, and CHERI, the last two of which are based on the work of Mark Miller and his colleagues like Jonathan Shapiro. Possibly O'Dowd has written similarly robust systems, without being able to show them publicly; possibly not. But plainly it is possible to do so.
The evidence suggests that O'Dowd has not written similarly robust systems, because several serious vulnerabilities have been found in the INTEGRITY RTOS sold by Green Hills Software, a company he founded, of which he was CEO, and of which he is still president. These vulnerabilities are of precisely the type that secure development practices would trivially prevent: https://www.cvedetails.com/vulnerability-list/vendor_id-2260...
O'Dowd did correctly identify the impossibility of making Linux secure in his controversial 02004 series of white papers, "Linux Security Controversy", now memory-holed from Green Hills's website but still present on the Internet Archive: https://web.archive.org/web/20040610165447/https://www.ghs.c...:
> Since Linux, UNIX, and Windows were not originally designed for security, they are unlikely designed for security, they are unlikely to ever exceed Common Criteria EAL4. They all have millions of lines of insecure code that can't be fixed.
> Our INTEGRITY real-time operating system was designed from day one to meet the highest levels of software security. The only way to come close to the level of security that INTEGRITY has already attained is to start over from scratch. But if such an effort were to result in a secure operating system, it would not be Linux, it would be something else.
However, he also touts the benefits of security through obscurity:
> Secrecy is an Important Component of Security
Consequently the above-mentioned vulnerabilities in INTEGRITY seem to have been found by analyzing the binary without access to the source code; presumably the number of such vulnerabilities that are undetected is enormously larger.
Reading O'Dowd's 02004 white paper demonstrates the reason: the security of INTEGRITY is said to rely on formal code review and verification tests, not ruthlessly simple design and formal proofs (though he does say that the FAA safety certifications done of INTEGRITY were done by formal-methods mathematicians and that one of its virtues is that it is small, "a few thousand lines of privileged-mode code", similar in size to the seL4 kernel).
A potential difficulty is that there's an important difference between "making a system not vulnerable to any attackers" and "making a system vulnerable only to its author", but as long as its author is not attacking it, the difference is not observable in the system's behavior. (O'Dowd himself makes this point in part II of his white papers: "A clever subversion will never cause the operating system to work incorrectly except when it is being exploited by its inventor. Even then, only the inventor usually sees the incorrect operation.") You have to look at the proofs or other evidence used to demonstrate the system's security. For the public to do this requires that they be publicly available. And, as Miller correctly points out, it's possible for the author to still possess information about flaws that the proofs fail to address.
Still, I think it's possible for someone who isn't the author to know everything there is to know about the security of a system, which would guarantee that they know at least as much about it as the author (the "agent" Miller mentions). Miller's own work is one of the most important tools for making this possible.
O'Dowd mentions the Karger–Thompson attack (using a compiler backdoored with a self-reproducing backdoor) which the reproducible-builds and https://bootstrapping.miraheze.org/wiki/Main_Page efforts are working toward preventing, claiming that it "irrefutably proved that an open source process couldn’t find clever subversions". But seL4 is not vulnerable to the Karger–Thompson attack because its security proofs verify the compiled binary, not just the source code, so it is not vulnerable to compiler backdoors unless they backdoor the proof checker or the hardware or OS it's running on.
However, the situation with Tesla is at the opposite extreme. Not only is Tesla's code not proven correct, not only is even the source code not available to the public, in fact not even the binaries are officially available to the public. The information asymmetry is nearly as extreme as it is possible for it to be; Tesla's users lack all of the information they would need to mitigate the risks of the principal-agent problem. (INTEGRITY is slightly better because although the source code is not available to the public, it is at least provided to its users.)
And this is probably true of any system in which cars or other systems are receiving security updates from headquarters, as Templeton says Teslas do; for the updates themselves not to pose a backdoor threat to users, the car must receive the updates from the user, not from headquarters, so that the user has the opportunity to vet the update, or delegate its vetting to a trusted third party. Consider, for example, what would be required for Russian or Chinese officials to have confidence their Tesla wasn't surreptitiously recording their conversations at the behest of the US government.
Frequent security updates (multiple times per decade) not only expose users to extreme vulnerability to their software provider, they also imply that the security proofs were incorrect and thus that the process that produced them was flawed.