6 ms·

Once we have reproducible builds, will it be possible to have verifiable builds? As in, can we cryptographically show that source + compiler = binary? Right n

Once we have reproducible builds, will it be possible to have verifiable builds? As in, can we cryptographically show that source + compiler = binary? Right now we can sign source code, we can sign binaries, but we can't shows that source produced binaries. I would feel much happier about installing code if I knew it was from a particular source or author.

detaro 9y ago
What do you mean by "cryptographically show"? With reproducible builds, anyone that has repeated a build can verify that a claimed binary matches, and could sign a statement saying so. But I don't think there are solutions that don't include someone repeating the build, or a clear way of proving that you actually did repeat the build.
zcdziura 9y ago
Just curious: how does one do that? Hash both the binary and source code files, that THAT hash, then sign it? Or am I completely off?
tedunangst 9y ago
No. Or at least this doesn't provide that. I think in theory you could make a crypto compiler that proves the binary is isogonal to the source, but I suspect the verification effort wouldn't be much less than recompiling.
nickpsecurity 9y ago
Yes. The first standard for securing computer systems mandated some protections against this. They were partly made by Paul Karger who invented the compiler subversion Thompson wrote about a decade later. Most just focused on that one thing where Karger et al went on to build systems that were secure from ground up with some surviving NSA pentesting and analysis for 2-5 years. Independently, people started building verified compilers and whole stacks w/ CPU's. They were initially simple with a lot to trust but got better over time. Recently, the two schools have been merging more. Mainstream INFOSEC and IT just ignores it all slowly reinventing it piece by piece with knock offs. It's hard, has performance hit, or is built in something other than C language so don't do it. (shrugs) Here's several examples: VLISP for Scheme48 whose papers are here: https://en.wikipedia.org/wiki/PreScheme https://en.wikipedia.org/wiki/PreScheme C0 compiler + whole stack correctness in Verisoft http://www.verisoft.de/VerisoftRepository.html http://www.verisoft.de/VerisoftRepository.html CompCert Compiler for C http://compcert.inria.fr/ http://compcert.inria.fr/ CakeML Subset of Standard ML https://cakeml.org/ https://cakeml.org/ Rockwell-Collins doing crypto DSL compiled to verified CPU http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf Karger's original paper with the attack from 1970's: https://www.acsac.org/2002/papers/classic-multics.pdf https://www.acsac.org/2002/papers/classic-multics.pdf Myer's landmark work on subversion in high-assurance security from 1980: http://csrc.nist.gov/publications/history/myer80.pdf http://csrc.nist.gov/publications/history/myer80.pdf My framework I developed studying Karger back when I was building secure things: http://pastebin.com/y3PufJ0V http://pastebin.com/y3PufJ0V
- z29LiTp5qUC30n 9y ago
  Well you may want to mention stage0 https://savannah.nongnu.org/projects/stage0/ https://savannah.nongnu.org/projects/stage0/ it starts with just a 280byte hex monitor and builds up to a rather impressive lisp AND forth, while building tools such as a text editor and line macro assembler along the way
  - nickpsecurity 9y ago
    rain1 started a page for people interested in bootstrapping or countering Karger's attack. Several of us are putting as many links as we can find to small, human-understandable tools such as compilers. I added some formally-verified or otherwise justifiable ones (eg 25-core CPU ain't gonna be simple). https://bootstrapping.miraheze.org/wiki/Main_Page https://bootstrapping.miraheze.org/wiki/Main_Page https://web.archive.org/web/20170724144929/https://bootstrapping.miraheze.org/wiki/Main_Page https://web.archive.org/web/20170724144929/https://bootstrap... We're focused on content right now over presentation. So, it will look rough. Hope you all enjoy it or learn something from the projects.

detaro 9y ago

What do you mean by "cryptographically show"? With reproducible builds, anyone that has repeated a build can verify that a claimed binary matches, and could sign a statement saying so. But I don't think there are solutions that don't include someone repeating the build, or a clear way of proving that you actually did repeat the build.

zcdziura 9y ago

Just curious: how does one do that? Hash both the binary and source code files, that THAT hash, then sign it? Or am I completely off?

tedunangst 9y ago

No. Or at least this doesn't provide that. I think in theory you could make a crypto compiler that proves the binary is isogonal to the source, but I suspect the verification effort wouldn't be much less than recompiling.

nickpsecurity 9y ago

Yes. The first standard for securing computer systems mandated some protections against this. They were partly made by Paul Karger who invented the compiler subversion Thompson wrote about a decade later. Most just focused on that one thing where Karger et al went on to build systems that were secure from ground up with some surviving NSA pentesting and analysis for 2-5 years. Independently, people started building verified compilers and whole stacks w/ CPU's. They were initially simple with a lot to trust but got better over time. Recently, the two schools have been merging more. Mainstream INFOSEC and IT just ignores it all slowly reinventing it piece by piece with knock offs. It's hard, has performance hit, or is built in something other than C language so don't do it. (shrugs) Here's several examples: VLISP for Scheme48 whose papers are here: https://en.wikipedia.org/wiki/PreScheme https://en.wikipedia.org/wiki/PreScheme C0 compiler + whole stack correctness in Verisoft http://www.verisoft.de/VerisoftRepository.html http://www.verisoft.de/VerisoftRepository.html CompCert Compiler for C http://compcert.inria.fr/ http://compcert.inria.fr/ CakeML Subset of Standard ML https://cakeml.org/ https://cakeml.org/ Rockwell-Collins doing crypto DSL compiled to verified CPU http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf Karger's original paper with the attack from 1970's: https://www.acsac.org/2002/papers/classic-multics.pdf https://www.acsac.org/2002/papers/classic-multics.pdf Myer's landmark work on subversion in high-assurance security from 1980: http://csrc.nist.gov/publications/history/myer80.pdf http://csrc.nist.gov/publications/history/myer80.pdf My framework I developed studying Karger back when I was building secure things: http://pastebin.com/y3PufJ0V http://pastebin.com/y3PufJ0V

z29LiTp5qUC30n 9y ago
Well you may want to mention stage0 https://savannah.nongnu.org/projects/stage0/ https://savannah.nongnu.org/projects/stage0/ it starts with just a 280byte hex monitor and builds up to a rather impressive lisp AND forth, while building tools such as a text editor and line macro assembler along the way
- nickpsecurity 9y ago
  rain1 started a page for people interested in bootstrapping or countering Karger's attack. Several of us are putting as many links as we can find to small, human-understandable tools such as compilers. I added some formally-verified or otherwise justifiable ones (eg 25-core CPU ain't gonna be simple). https://bootstrapping.miraheze.org/wiki/Main_Page https://bootstrapping.miraheze.org/wiki/Main_Page https://web.archive.org/web/20170724144929/https://bootstrapping.miraheze.org/wiki/Main_Page https://web.archive.org/web/20170724144929/https://bootstrap... We're focused on content right now over presentation. So, it will look rough. Hope you all enjoy it or learn something from the projects.