The U.S. government invented INFOSEC and funded most tech (security or otherwise) that you depend on. So what. It's the specific tech or actions that matter rather than who funds them. At worst, you increase scrutiny or consider subversion issues. Of course, high assurance is specifically designed to counter that. So, people worried about subversion should be using this stuff more than anyone.
Btw, here's two things Galois did with their contracts that mainstream security folks are mostly ignoring instead of building on or applying:
At least some of them have stars in the three digits. I'm impressed an open-source crowd giving it that much attention. Maybe cuz it's on GitHub. The rest might need to go on there, too, for better odds of adoption. Using Google and Save As... are apparently major obstacles of adoption these days. Idk as I'm still trying to figure it out.
I myself have already previously starred Cryptol (I'm acquainted with a few ex-Galois people) but was unaware as to its wider adoption. Certainly I get reasonably frequent notifications on its issues list from Github.
Cool stuff. I think their Xen and Ivory work will probably have highest odds of benefiting people. All kinds of people doing stuff like Arduino and Raspberry Pi that it could be applied to. Either immediately or with a port.
Cryptol is a nice tool, but it can't eliminate most important crypto bugs (for example, the sorts of bugs found in OpenSSL). It's useful for proving things about bit-mixy crypto code like AES, SHA, etc, but that code rarely has bugs (due to known-answer tests).
3. The code is run through visual inspections, static analysis tools like ASTREE or SPARK, tests, covert channel analysis, and so on. Modified if problems are found.
4. An optimizing version of a certified compiler like CompCert produces the object code.
5. It's distributed with public key cryptography and/or Merkle Signatures if people don't trust that. There's modern versions with efficient or unlimited signing.
6. Optionally, a subversion-resistant process builds the fist compiler and checkers in stages.
Btw, here's two things Galois did with their contracts that mainstream security folks are mostly ignoring instead of building on or applying:
http://www.cryptol.net/
http://ivorylang.org/
And a repo with the rest that uses the magical power of open source to counter people's fears and improve the world:
https://github.com/galoisinc
At least some of them have stars in the three digits. I'm impressed an open-source crowd giving it that much attention. Maybe cuz it's on GitHub. The rest might need to go on there, too, for better odds of adoption. Using Google and Save As... are apparently major obstacles of adoption these days. Idk as I'm still trying to figure it out.