Kevin Hartnett writes in Quanta Magazine about the High-Assurance Cyber Military Systems (HACMS) project, which has achieved very significant strides in formally verified code. He reports on their signature achievement, securing the software of a robot helicopter.
“At the end of eighteen months, the Red Team was not able to hijack the newly-minted SMACCMCopter running high-assurance HACMS code, despite being given six weeks and full access to the source code of the copter.” .
Wow! We wanted to do this stuff back when I was in school (and Ronald Reagan was President), so I certainly appreciate the significance and quality of this work. This is an outstanding and nearly unprecedented result. As Professor Fischer says, “People can’t really have the excuse anymore that it’s too hard.”
(A cynic might say, “In a historic first, after seventy years, researchers have written the first correct computer program.” I mean, it’s a continuing miracle that software works as well as it does, given how poorly we write it.)
Hartnett called this “Hacker-Proof Code”, though I would be a lot more cautious before declaring invulnerability.
“Hacker-proof” sounds like “unsinkable” to me. You know it probably isn’t.
I can’t find too much detailed information on either the code or the testing. As far as I can tell, they have secured software operating the UAV, making it much harder for unauthorized parties to destroy or take over the device. This is done by writing logical specifications of the correct operation and proving that the software precisely follows the specification.
This is awesome and awesomely difficult, but hardly “hacker-proof”.
- The specification may be wrong and/or hacked
- The logical prover or the proof may be broken and/or hacked
- The humans who operate the system may be wrong and/or hacked
- The hardware may be broken and/or hacked
- During operation, input data may be broken and/or hacked
Very nice work, indeed! But “hacker-proof”? It takes a lot more than a bug free software module.
- Kathleen Fisher, Using formal methods to enable more secure vehicles: DARPA’s HACMS program, in Proceedings of the 19th ACM SIGPLAN international conference on Functional programming. 2014, ACM: Gothenburg, Sweden. p. 1-1.
- Kevin Hartnett, (2016) Hacker-Proof Code Confirmed. Quanta Magazine, https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/