From mboxrd@z Thu Jan 1 00:00:00 1970 From: Mark H Weaver Subject: Trustworthiness of build farms (was Re: CDN performance) Date: Thu, 20 Dec 2018 19:23:47 -0500 Message-ID: <87fturwwup.fsf_-_@netris.org> References: <20181203154335.10366-1-ludo@gnu.org> <87tvju6145.fsf@gnu.org> <87ftv7l6gy.fsf@gmail.com> <871s6qzo6m.fsf_-_@gnu.org> <87y38tx365.fsf@gmail.com> <878t0thfp9.fsf@roquette.mug.biscuolo.net> <874lbfd0sd.fsf@netris.org> <87imzpd70s.fsf@roquette.mug.biscuolo.net> Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:57226) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ga8ci-0002nP-Cz for guix-devel@gnu.org; Thu, 20 Dec 2018 19:25:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ga8cb-00073V-Kd for guix-devel@gnu.org; Thu, 20 Dec 2018 19:25:02 -0500 Received: from world.peace.net ([64.112.178.59]:41902) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1ga8cb-00072D-En for guix-devel@gnu.org; Thu, 20 Dec 2018 19:24:57 -0500 In-Reply-To: <87imzpd70s.fsf@roquette.mug.biscuolo.net> (Giovanni Biscuolo's message of "Wed, 19 Dec 2018 13:40:19 +0100") List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: "Guix-devel" To: Giovanni Biscuolo Cc: guix-devel@gnu.org, 33600@debbugs.gnu.org Hi Giovanni, Giovanni Biscuolo writes: > Mark H Weaver writes: > >> Giovanni Biscuolo writes: >>> with a solid infrastructure of "scientifically" trustable build farms, >>> there are no reasons not to trust substitutes servers (this implies >>> working towards 100% reproducibility of GuixSD) >> >> What does "scientifically trustable" mean? > > I'm still not able to elaborate on that (working on it, a sort of > self-research-hack project) but I'm referencing to this message related > to reduced bootstrap tarballs: > > https://lists.gnu.org/archive/html/guix-devel/2018-11/msg00347.html > > and the related reply by Jeremiah (unfortunately cannot find it in > archives, Message-ID: <877eh81tm4.fsf@ITSx01.pdp10.guru>) > > in particular Jeremiah replied this: > >> so, if I don't get it wrong, every skilled engineer will be able to >> build an "almost analogic" (zero bit of software preloaded) computing >> machine ad use stage0/mes [1] as the "metre" [2] to calibrate all other >> computing machines (thanks to reproducible builds)? > > well, I haven't thought of it in those terms but yes I guess that is one > of the properties of the plan. > > > and > >> so, having the scientific proof that binary conforms to source, there >> will be noo need to trust (the untrastable) > > Well, that is what someone else could do with it but not a direct goal > of the work. > > maybe a more correct definition of the above "scientific proof" should be > "mathematical proof" I agree that a mathematical proof is what we should be aiming for, and the only kind of proof that I could trust in, in this scenario. However, it's important to note several caveats: * A mathematical proof showing that the binary conforms to the source requires a proof of correctness of the language implementation, which in turn requires formal semantics for both the source language and the underlying machine code. As far as I know, the current bootstrappable.org effort does not include anything like this. Existing projects that provide this include CakeML and Jitawa. * One must assume that the hardware behaves according to its formal specification. The veracity of this assumption is not something we can currently verify, and even if we could, it would be invalidated if someone gained physical access to the machine and modified it. * The hardware initialization program (e.g. coreboot) and the kernel used to perform the bootstrap must still be trusted, and unless I'm mistaken, the bootstrappable.org effort does not currently address these issues. * The software running on the substitute servers could be compromised by stealing SSH keys from someone with root access. * If the private signing key of the substitute server can be stolen, e.g. by gaining physical access to the machine for a short time, then a man-in-the-middle can deliver to users compromised binaries that appear to come from the substitute server itself. * Not only the substitute server, but also all of its build slaves, must be trusted as well. So, while I certainly agree that it will be a *major* improvement to avoid the need to blindly trust precompiled bootstrap binaries, we should be clear that the current efforts fall far short of a proof, and there still remain several valid reasons not to place one's trust in substitute servers. Does that make sense? Regards, Mark