1. 9

  2. 4

    Nice write-up. Mr. Bushnell misses the point in that quote so much it’s like he was replying to a different comment. Clearly, the benefit is defense in depth where we don’t assume one measure will work in all circumstances. You posted evidence that it in fact didn’t work a few times. So, an obfuscation layer is added as a way to make attackers do more work. Many are lazy enough that such techniques can keep riff raff out reducing burden on administrators who clean up machines if nothing else.

    Your article claims they have a good track record so far on vulnerabilities. If I was them, I’d hire some high-assurance security folks to start throwing everything they can at the concurrency model, FFI, compiler, and especially any native code left. Much like Microsoft is doing at Microsoft Research with things like VCC, TLA+, and CoqASM. Google instead seems to mostly hire young people out of colleges who have never been exposed to such methods. High-assurance security & history is still taught at many colleges based on what course material I accidentally discover looking up HA tech. Maybe not at those Google recruits from or just not practical applications where students ignore it in favor of something else. Something like Go would benefit as it’s simple enough for both medium- and high-assurance methods to handle.

    For instance, they could immediately counter the Karger compiler-compiler attack by hand-translating the Go compiler source to first IL of CompCert. Probably find some errors in compiler itself just running a Go port of Csmith through both of those compilers where differences on Go’s side (versus CompCert’s) would probably be bugs. Separation logic a la VCC or SPARK Ada could model sequential, pointer-manipulating components like garbage collector to prove safety. TLA+ models along lines of C-to-TLA+ to analyze concurrency properties, filesystem use, and so on. Many opportunities to make Go even safer or even faster (unsafe, optimized algorithm formally verified).

    1. 3

      I’ve actually been toying with the idea of using cgo and Ada SPARK compiled into shared libraries so that you can have portions of your code with formal verification. I haven’t had much time to put into it, but I think it is a hack that might tickle the fancy of those of us who like HA systems.

      1. 2

        That’s a great idea. Exactly the kind of thing I have in mind using one language’s tooling to benefit code in another.

    2. 2

      Suggest go, practices.

      web and programming aren’t specifically related as those other tags, and security is correct.