TITLE: Computer Programs Aren't Pure Abstractions. They Live in the World. AUTHOR: Eugene Wallingford DATE: February 21, 2018 3:38 PM DESC: ----- BODY: Guile Scheme guru Andy Wingo recently wrote a post about langsec, the idea that we can bake system security into our programs by using languages that support proof of correctness. Compilers can then be tools for enforcing security. Wingo is a big fan of the langsec approach but, in light of the Spectre and Meltdown vulnerabilities, is pessimistic that it really matter anymore. If bad actors can exploit the hardware that executes our programs, then proving that the code is secure doesn't do much good. I've read a few blog posts and tweets that say Wingo is too pessimistic, that efforts to make our languages produce more secure code will still pay off. I think my favorite such remark, though, is a comment on Wingo's post itself, by Thomas Dullien:
I think this is too dark a post, but it shows a useful shock: Computer Science likes to live in proximity to pure mathematics, but it lives between EE and mathematics. And neglecting the EE side is dangerous - which not only Spectre showed, but which should have been obvious at the latest when Rowhammer hit.
There's actual physics happening, and we need to be aware of it.
It's easy for academics, and even programmers who work atop an endless stack of frameworks, to start thinking of programs as pure abstractions. But computer programs, unlike mathematical proofs, come into contact with real, live hardware. It's good to be reminded sometimes that computer science isn't math; it lives somewhere between math and engineering. That is good in so many ways, but it also has its downsides. We should keep that in mind. -----