5 ms·

You are right, but reproducible builds are still very useful, not for high-assurance though.

by zzzcpan 10y ago

nickpsecurity 10y ago
They're barely useful for low assurance. Just read the Csmith paper testing compilers to see the scope of the problem. They solution to what they're really worried about will require (a) a correct compiler, (b) it written in cleanly-separated passes that are human-inspectable (aka probably not C language), (c) implemented with correctness checks to catch logical errors, (d) implemented in safe language to stop or just catch language-level errors, (e) stored in build system hackers can't undetectably sabotaged, (f) trusted distribution to users, and (g) compiled initially with toolchain people trust with optional, second representation for that toolchain. Following Wirth's Oberon and VLISP Scheme, the easiest route is to leverage one of those in a layered process. Scheme, esp PreScheme, is easiest but I know imperative programmers hate LISP's no matter how simple. So, I include a simple, imperative option. So, here's the LISP example. You build initial interpreter or AOT compiler with basic elements, macro's, and assembly code. Easy to verify by eye or testing. You piece-by-piece build other features on top of it in isolated chunks using original representation until you get a real language. You rewrite each chunk in real-language and integrate them. That's first, real compiler that was compiled with the one you built piece by piece starting with a root of trust that was a tiny, static LISP with matching ASM. You can use first, real compiler for everything else. Wirth did something similar out of necessity in P-code and Lilith. In P-code, people needed compilers and standard libraries but couldn't write them. The could write basic system code on their OS's. So, he devised idealized assembly that could be implemented by anyone in almost no code and just with some OS hooks for I/O etc. Then, he modified his Pascal compiler to turn everything into P-code. So, ports & bootstrapping just required implementing one thing. Got ported to 70+ architectures/platforms in 2 years as result. The imperative strategy for anti-subversion is similar. Start with idealized, safe, abstract machine along lines of P-code with ASM implementations. Initial language might be Oberon subset with LISP or similar syntax just for effortless parsing. Initial compiler done in high-level language for human inspection with code side-by-side in subset language for that idealized ASM. It's designed to match high-level language, too. Create initial compiler that way then extend, check, compile, repeat just like Scheme version. The simple, easy code of the initial compilers and high-level language for final compilers means anyone can knock them off in about any language. That will increase diversity across the board as many languages, runtimes, stdlibs, etc are implemented quite differently. Reproducible build techniques can be used on the source code and initial process of compilation if one likes. The real security, though, will be that many people reviewed the bootstrapping code, the ZIP file is hashed/signed, and users can check that source ZIP they acquired and what was reviewed match. Then they just compile and install it.
- zzzcpan 10y ago
  I'm not disagreeing, yes, reproducible builds don't make a lot of sense from a security point of view. But they do from an infrastructural/package management point of view and could make some things easier, more manageable, more reliable.
  - nickpsecurity 10y ago
    Now I'll agree with that! Thanks for the links to it, too, as I lost my bookmarks on the topic during a recent crash.
- dwheeler 10y ago
  Excellent, it's easy! Why haven't you completed this yet? :-) So, a few thoughts. The CSmith paper "Finding and Understanding Bugs in C Compilers" is a fun paper: https://www.cs.utah.edu/~chenyang/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~chenyang/papers/pldi11-preprint.pdf - however, let's delve further. They found defects in every compiler they tried, proprietary and OSS. They even found defects in CompCert - because they were defects in CompCert’s unverified front-end code. What's more, they focused on "atypical combinations of C language features" - which are important, but to far fewer users. Yes, it'd be awesome to have compilers that are perfect have absolutely no defects. Let's work on that. But it will be many, many years before they are widespread. Besides, while no-defects would be awesome, many people are more interested in a different and simpler requirement - they want to detect subversion of binaries (where the binary and source do not correspond). Yes, provably perfect compilers could do that, but you don't need to wait for them; reproducible builds and DDC can provide that now, and you don't have to wait for anything. So let's talk about VLISP. VLISP spawned an amazing number of papers, and was interesting work. Where's the code? MITRE never released it to my knowledge. To me, programs I can't run are in the "who cares?" category, and stuff people can't reproduce & investigate isn't really science anyway. Besides, VLISP only generated code for computers people generally don't use anymore. (You'll notice that I posted the scripts demonstrating DDC so that others can reproduce their execution.) Sure, p-code was awesome in its time, I used it. But when newer hardware (the IBM PC) came along, it got superceded. More importantly for our story, it got superseded before there was time to develop any complex proofs. This is a more general problem: As long as formal proofs demand a massive amount of time, their results will become useless due to obsolescence. We must improve the tooling and models so that the proofs and layers can be done in a much faster and cost-effective way. Proving obsolete stuff is not very helpful. I think the ProVal approach (using Why3) is especially promising, but fundamentally, we need to make it not a massive research effort to write a high-assurance compiler. Oh, and a little out-of-scope: As someone who's written Scheme & Common Lisp for decades, the problem with Lisp isn't its imperative nature; lots of people like Elm and Haskell, which are also functional languages. The problem with Lisps is their hideous syntax; Lisps don't even support infix by default, something every grade schooler learns. One solution is here: http://readable.sourceforge.net/ http://readable.sourceforge.net/ Anyway, what you've outlined is basically a program to build up from small safe components into larger trustworthy components. It's a sound strategy, and one that has been repeatedly advocated for decades by many people. But we also need to admit that it's going to take a long time, because our tooling is only just becoming good enough, and even then only in certain cases. There are serious limitations you're glossing over. Don't ignore shorter-term smaller wins; they're valuable.

You are right, but reproducible builds are still very useful, not for high-assurance though.

by zzzcpan 10y ago

You are right, but reproducible builds are still very useful, not for high-assurance though.

They're barely useful for low assurance. Just read the Csmith paper testing compilers to see the scope of the problem. They solution to what they're really worried about will require (a) a correct compiler, (b) it written in cleanly-separated passes that are human-inspectable (aka probably not C language), (c) implemented with correctness checks to catch logical errors, (d) implemented in safe language to stop or just catch language-level errors, (e) stored in build system hackers can't undetectably sabotaged, (f) trusted distribution to users, and (g) compiled initially with toolchain people trust with optional, second representation for that toolchain. Following Wirth's Oberon and VLISP Scheme, the easiest route is to leverage one of those in a layered process. Scheme, esp PreScheme, is easiest but I know imperative programmers hate LISP's no matter how simple. So, I include a simple, imperative option. So, here's the LISP example. You build initial interpreter or AOT compiler with basic elements, macro's, and assembly code. Easy to verify by eye or testing. You piece-by-piece build other features on top of it in isolated chunks using original representation until you get a real language. You rewrite each chunk in real-language and integrate them. That's first, real compiler that was compiled with the one you built piece by piece starting with a root of trust that was a tiny, static LISP with matching ASM. You can use first, real compiler for everything else. Wirth did something similar out of necessity in P-code and Lilith. In P-code, people needed compilers and standard libraries but couldn't write them. The could write basic system code on their OS's. So, he devised idealized assembly that could be implemented by anyone in almost no code and just with some OS hooks for I/O etc. Then, he modified his Pascal compiler to turn everything into P-code. So, ports & bootstrapping just required implementing one thing. Got ported to 70+ architectures/platforms in 2 years as result. The imperative strategy for anti-subversion is similar. Start with idealized, safe, abstract machine along lines of P-code with ASM implementations. Initial language might be Oberon subset with LISP or similar syntax just for effortless parsing. Initial compiler done in high-level language for human inspection with code side-by-side in subset language for that idealized ASM. It's designed to match high-level language, too. Create initial compiler that way then extend, check, compile, repeat just like Scheme version. The simple, easy code of the initial compilers and high-level language for final compilers means anyone can knock them off in about any language. That will increase diversity across the board as many languages, runtimes, stdlibs, etc are implemented quite differently. Reproducible build techniques can be used on the source code and initial process of compilation if one likes. The real security, though, will be that many people reviewed the bootstrapping code, the ZIP file is hashed/signed, and users can check that source ZIP they acquired and what was reviewed match. Then they just compile and install it.

zzzcpan 10y ago
I'm not disagreeing, yes, reproducible builds don't make a lot of sense from a security point of view. But they do from an infrastructural/package management point of view and could make some things easier, more manageable, more reliable.
- nickpsecurity 10y ago
  Now I'll agree with that! Thanks for the links to it, too, as I lost my bookmarks on the topic during a recent crash.
dwheeler 10y ago
Excellent, it's easy! Why haven't you completed this yet? :-) So, a few thoughts. The CSmith paper "Finding and Understanding Bugs in C Compilers" is a fun paper: https://www.cs.utah.edu/~chenyang/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~chenyang/papers/pldi11-preprint.pdf - however, let's delve further. They found defects in every compiler they tried, proprietary and OSS. They even found defects in CompCert - because they were defects in CompCert’s unverified front-end code. What's more, they focused on "atypical combinations of C language features" - which are important, but to far fewer users. Yes, it'd be awesome to have compilers that are perfect have absolutely no defects. Let's work on that. But it will be many, many years before they are widespread. Besides, while no-defects would be awesome, many people are more interested in a different and simpler requirement - they want to detect subversion of binaries (where the binary and source do not correspond). Yes, provably perfect compilers could do that, but you don't need to wait for them; reproducible builds and DDC can provide that now, and you don't have to wait for anything. So let's talk about VLISP. VLISP spawned an amazing number of papers, and was interesting work. Where's the code? MITRE never released it to my knowledge. To me, programs I can't run are in the "who cares?" category, and stuff people can't reproduce & investigate isn't really science anyway. Besides, VLISP only generated code for computers people generally don't use anymore. (You'll notice that I posted the scripts demonstrating DDC so that others can reproduce their execution.) Sure, p-code was awesome in its time, I used it. But when newer hardware (the IBM PC) came along, it got superceded. More importantly for our story, it got superseded before there was time to develop any complex proofs. This is a more general problem: As long as formal proofs demand a massive amount of time, their results will become useless due to obsolescence. We must improve the tooling and models so that the proofs and layers can be done in a much faster and cost-effective way. Proving obsolete stuff is not very helpful. I think the ProVal approach (using Why3) is especially promising, but fundamentally, we need to make it not a massive research effort to write a high-assurance compiler. Oh, and a little out-of-scope: As someone who's written Scheme & Common Lisp for decades, the problem with Lisp isn't its imperative nature; lots of people like Elm and Haskell, which are also functional languages. The problem with Lisps is their hideous syntax; Lisps don't even support infix by default, something every grade schooler learns. One solution is here: http://readable.sourceforge.net/ http://readable.sourceforge.net/ Anyway, what you've outlined is basically a program to build up from small safe components into larger trustworthy components. It's a sound strategy, and one that has been repeatedly advocated for decades by many people. But we also need to admit that it's going to take a long time, because our tooling is only just becoming good enough, and even then only in certain cases. There are serious limitations you're glossing over. Don't ignore shorter-term smaller wins; they're valuable.