Hacker News Reader

Comment by morecoffee | Hacker News Reader

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.

View on HN

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.

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

C0 compiler + whole stack correctness in Verisoft http://www.verisoft.de/VerisoftRepository.html

CompCert Compiler for C http://compcert.inria.fr/

CakeML Subset of Standard ML https://cakeml.org/

Rockwell-Collins doing crypto DSL compiled to verified CPU 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

Myer's landmark work on subversion in high-assurance security from 1980: 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

Well you may want to mention 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

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://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.

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.

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?

Reply on news.ycombinator.com