Re:Formal Verification Creates Hacker-Proof Code
by nickpsecurity on Friday October 21, 2016 @01:11PM
(#12762323)
It's true but that's a specification problem. The hardware should be in the model since it's in the TCB. The earliest tools used for high-assurance security, like Gypsy Verification Environment, had information-flow analysis for detecting covert channels. Today, we have information flow control, distributed version of it, and hardware versions of non-interference that go to the gates. We're actually past being able to handle that with current tooling if ultra-high-performance is a non-goal.
It's analog and RF side channels that's going to screw them. DOD et al did decades of cat and mouse games under that with their TEMPEST activities. Open research just getting started. Just waiting for The Flood. :)
https://www.usenix.org/system/files/conference/usenixsecurit...
http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf
It's analog and RF side channels that's going to screw them. DOD et al did decades of cat and mouse games under that with their TEMPEST activities. Open research just getting started. Just waiting for The Flood. :)