1. 10
  1. 2

    So, then they started offering a version compiled with CompCert and… oh wait, nevermind. Few writing about this stuff ever promote or use CompCert. ;)

    1. 1

      @nickpsecurity: I did not know that project, very interesting. I did learn quite some things that were useful from the article.

      1. 1

        Here’s you a survey paper (pdf) on secure compilation that gives you a lot of background and current information. They started trying to mathematically prove correctness of compilers. That was typically for one language, though, with interactions between them (eg C w/ assembly, Java w/ C FFI) causing problems. The cutting edge is “fully-abstract, secure compilation” that addresses that. An older technique that’s not as math-heavy was “type-based, certified compilation” (here) at FLINT. They had type systems at every level from high-level source to intermediate language to assembly language that could catch errors or ensure consistency.

        So, there’s you some stuff to think about on that topic. That’s compilers. David A. Wheeler’s page on SCM security addresses securing repo’s, esp for distribution.