* Re: Trustworthiness of build farms (was Re: CDN performance)
@ 2018-12-26 2:29 Jeremiah
2018-12-28 7:12 ` Mark H Weaver
0 siblings, 1 reply; 11+ messages in thread
From: Jeremiah @ 2018-12-26 2:29 UTC (permalink / raw)
To: mhw; +Cc: guix-devel
> If you could add an "In-Reply-To:" header to your responses, that would
> be very helpful. It's easy to add it manually if needed: just copy the
> "Message-ID:" header from the original message and replace "Message-ID:"
> with "In-Reply-To:". As is, it's very difficult for me to keep track of
> any conversation with you.
Sorry abou that, was not something I generally even consider as emacs
handles that bit of tracking for me but I will try to add that in the
future.
> I'm not worried about those languages. Very little code is written in
> them anyway, only a small part of the early bootstrap.
Yet also the point where the trusting trust attacks can most effectively
be inserted. Hence more concern and less trust needs to be placed there.
> My concern is the correspondence between the source code and machine code for the
> majority of the operating system and applications.
That seems more like a feature request for GCC and guile than the
bootstrap or the trustworthiness of the build farms.
> It's important to note that even a relatively obscure bug in the
> compiler is enough to create an exploitable bug in the machine code of
> compiled programs that's not present in the source code.
Absolutely and we already have dozens of living examples due to
performance optimizations done by GCC and Clang exploiting undefined
behavior in the C language and in some cases violating the spec for sake
of compatibility.
> Such compiler bugs and the resulting exploits could be systematically searched for by
> well-resourced attackers.
And actively exploiting as they are already doing.
> So, if we want to *truly* solve the problem of exploitable bugs existing
> only in the machine code and not in the corresponding source, it is not
> enough to eliminate the possibility of code deliberately inserted in our
> toolchain that inserts trojan horses in other software.
Very true, we need formally defined languages which do not have
undefined behavior and rigourous tests that prevent optimizations from
violating the spec. In essense a series of acid tests that ensure the
resulting mental model always exactly matches the computing model that
the compilers will be based upon.
> To truly solve that problem, we need bug-free compilers.
Impossible for all but the simplest of languages as the complexity of
implementing a compiler/assembler/interpreter is ln(c)+a but the
complexity of implementing a bug-free compiler/assembler/interpreter is
(e^(c))! - a. Where a is the complexity cost of supporting it's host architecture.
> In practice, this requires provably correct compilers.
Which in practice turn out *NOT* to be bug free nor complete in regards
to the standard specification. Now, don't get me wrong; provably correct
compilers are a correct step in the right direction but the real
solution is to first generate simplified languages that don't have
undefined behavior and human model first behavior.
> Does that make sense?
Absolutely, certainly something possible to do; but extremely human
effort intensive and I don't see anyone willing to throw 2+ years of
human effort at the problem outside of non-free Businesses like
CompCert.
I'd love to see someone do it, I'd even throw in a few dollars into a
pot to fund it but it is so low down on my list of priorities, I'm not
going to be touching it in the next 2 decades...
-Jeremiah
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Trustworthiness of build farms (was Re: CDN performance)
2018-12-26 2:29 Trustworthiness of build farms (was Re: CDN performance) Jeremiah
@ 2018-12-28 7:12 ` Mark H Weaver
0 siblings, 0 replies; 11+ messages in thread
From: Mark H Weaver @ 2018-12-28 7:12 UTC (permalink / raw)
To: Jeremiah; +Cc: guix-devel
Hi Jeremiah,
Jeremiah@pdp10.guru writes:
>> To truly solve that problem, we need bug-free compilers.
> Impossible for all but the simplest of languages as the complexity of
> implementing a compiler/assembler/interpreter is ln(c)+a but the
> complexity of implementing a bug-free compiler/assembler/interpreter
> is (e^(c))! - a. Where a is the complexity cost of supporting it's
> host architecture.
Where are you getting those complexity expressions from? Can you cite
references to back them up? If not, can you explain how you arrived at
them?
What is 'c'?
>> In practice, this requires provably correct compilers.
> Which in practice turn out *NOT* to be bug free nor complete in regards
> to the standard specification.
If you're referring to the bugs found in CompCert, the ones I know about
were actually bugs in the unverified parts of the toolchain. In the
past, its frontend was unverified, and several bugs were found there.
Even today, it produces assembly code, and depends on an unverified
assembler and linker.
Bugs can also exist in the specifications themselves, of course.
However, in the areas covered by the proofs, the results are quite
dramatic. For example, in the paper "Finding and Understanding Bugs in
C Compilers" by Xuejun Yang, Yang Chen, Eric Eide, and John Regehr,
https://web.stanford.edu/class/cs343/resources/finding-bugs-compilers.pdf
the authors state on page 6:
The striking thing about our CompCert results is that the middle-
end bugs we found in all other compilers are absent. As of early
2011, the under-development version of CompCert is the only compiler
we have tested for which Csmith cannot find wrong-code errors. This
is not for lack of trying: we have devoted about six CPU-years to the
task. The apparent unbreakability of CompCert supports a strong
argument that developing compiler optimizations within a proof
framework, where safety checks are explicit and machine-checked, has
tangible benefits for compiler users
> Now, don't get me wrong; provably correct
> compilers are a correct step in the right direction but the real
> solution is to first generate simplified languages that don't have
> undefined behavior and human model first behavior.
I'm not sure what "and human model first behavior" means, but if you
mean that the semantics of languages should strive to match what a human
would naturally expect, avoiding surprising or unintuitive behavior, I
certainly agree. I consider Standard ML, and some subsets of Scheme and
Lisp, to be such languages.
>> Does that make sense?
> Absolutely, certainly something possible to do; but extremely human
> effort intensive and I don't see anyone willing to throw 2+ years of
> human effort at the problem outside of non-free Businesses like
> CompCert.
If I understand correctly, what you don't expect to happen has already
been done. CakeML is free software, and formally proven correct all the
way down to the machine code. Moreover, it implements a language with
an exceptionally clear semantics and no undefined behavior.
Anyway, you've made it fairly clear that you're not interested in this
line of work, and that's fine. I appreciate the work you're doing
nonetheless.
Regards,
Mark
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Trustworthiness of build farms (was Re: CDN performance)
@ 2019-01-20 12:24 Jeremiah
0 siblings, 0 replies; 11+ messages in thread
From: Jeremiah @ 2019-01-20 12:24 UTC (permalink / raw)
To: cmmarusich, g; +Cc: guix-devel
> > Do you know where one can obtain a copy of this report? I did an
> > Internet search but couldn't find anything.
> me too
> Jeremiah: sorry if I insist (last time, promised!) but could you give us
> some more info about that report?
I am sorry for the delay, the Government shutdown really disabled access
for me in regards to the archives in which it was found.
As I am currently unable to link that resource, I'll do my best to
provide the key points:
It was a top secret report for the Department of Defense written in 1958
and declassified by the Clinton Administration.
1) Computers are being used to replace human thinking and as computers
are growing faster and faster in complexity; there is going to be a
point in the future where computers will be required to design
computers. References back to a 1952 paper about lithography (that I
couldn't find) and that it is likely that chips will replace single
piece logic and thus provide the ultimate place for hiding of malicous
functionality.
2) It is possible to infect the software used in the designing of
Computers on elements common to all computers, which will alter the
circuits to provide weaknesses we can exploit and/or functionality to
leverage that the computer designer, builder and owner do not know
about.
3) If done on a large enough machine, there is room to include infectors
for tools such as assmblers, linkers, loaders and compilers on
functionality that can not be removed.
4) It then details how they could backdoor the Strela computer and how
it could be leveraged to compromise future Soviet computers to ensure a
permanent weapon against the Soviet Union.
5) Then it has a huge section of blacked out text
6) Then a section of possible future hooks depending on how software
evolves in the Soviet Union, thus allowing more pervasive hardware
compromises and eliminating the possibility of trustworthy computing
ever becoming possible on Soviet Computers.
7) Another big blacked out section.
8) Then the final section detailed a list of steps required for a
lithography plant to be assembled by an Intelligence Agency to prevent
their own infrastructure from being compromised by a similiar Soviet
attack; with an estimated spinup time of almost a Decade.
Examples included running traces close to the transistors to create a
radio induced functionality such as The intensional leaking of crypto
secrets upon recieving a very specific frequency.
Allowing magic numbers in a set of memory addresses or registers to
cause functionality to be engaged; such as disabling protections or
giving a process priviledges that would normally be restricted for
security reasons.
I'm sorry as I am likely missing alot of the details and attacks.
Once the Shutdown is done, I'll try again to find that paper for you.
-Jeremiah
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Trustworthiness of build farms (was Re: CDN performance)
@ 2019-01-05 20:15 jeremiah
2019-01-06 20:47 ` Chris Marusich
0 siblings, 1 reply; 11+ messages in thread
From: jeremiah @ 2019-01-05 20:15 UTC (permalink / raw)
To: mhw; +Cc: guix-devel
> In other words, it's anecdotal.
True, it definitely was not a formal proof just data based upon real
world development with large teams of programmers and formal
specifications for correct behavior.
> Obviously, the flaw in this argument is that there exist much more
> efficient ways to add numbers than counting beads. A claim of
> complexity doesn't mean anything unless you can prove that it's a lower
> bound.
I don't deny that there are possibly lower bounds for the work, rather
that is the observed values from large teams doing that development are
what I have available to share.
> There's a reason that I followed my call for bug-free compilers with the
> claim: "In practice, this requires provably correct compilers." I wrote
> that because I know that it's the only known practical way to do it for
> non-trivial languages.
Perfection is a road, not a destination.
One requires a "provabily correct compiler" to bootstrap a "provabily
correct compiler". A step completely skipped.
> Interesting. I hadn't heard of those. Can you cite the details?
One the most obvious is the float size definition and rounding behavior
on x86 hardware. The C standard requires rounding towards even, IEEE
only supports rounding towards infinity, negative infinity and zero. The
C standard allows floats to be expanded (to 80bits) but IEEE doesn't as
it can change the stability of some algorithms.
> Right, which shows the problems with depending on unverified components,
> but CompCert is no longer the state of the art in this regard.
It goes deeper than that.
> In contrast, the CakeML compiler not only produces raw machine code,
> moreover the proofs apply to the raw machine code of the CakeML compiler
> itself. As a result, the only trusted specifications are those of the
> source language and of the underlying machine code behavior (for the
> subset of instructions that are actually generated).
So either CakeML must refuse to compile valid code or will generate
invalid binaries or both.
> I agree that IEEE floating point (and more generally inexact arithmetic)
> is a problem, but a great many useful programs can be written without
> using them, including most (if not all) of the programs that are most
> important for us to trust. Operating systems, compilers, editors, and
> communication tools such as chat clients and mail readers, have no need
> for inexact arithmetic. These are the programs I care most about.
Aside from the compilers that janneke and I have written, no other real
world compilers don't depend upon floating point; why do you think
janneke spent so many hours adding floating point to Mescc?
Try to build Linux without floating point support, it can't be done.
To to build emacs or vim without floating point support in your
compiler.
The reason is simple: Math libraries abuse it for performance and
performance is the only metric most people care about.
The Countless sins of our Industry exit because of those cursed words.
> Why do you include garbage collection in this list? I consider garbage
> collection to be a _requirement_ for human model first behavior. Do you
> consider it a hindrance? Also, multiple verified garbage collectors
> already exist, e.g. those used in the runtimes of CakeML and Jitawa.
Find me one Enterprise grade Operating system that isn't a Lisp machine
that includes garbage collection at the native level.
> I think it's too ambitious to target non-programmers, because they do
> not have the required skills to understand the behavior of complex
> programs, regardless of what language is used. They could perhaps
> understand toy programs, but that's not useful for helping them evaluate
> the trustworthiness of the computing tools they actually use, which is
> what I'm interested in.
Fair preference to have
> Anyway, what language(s) would you consider to be superior to ML or a
> subset of Scheme, based on the goal of human model first behavior?
As much as I hate to admit it but C# and Go tend to be far easier for
most people new to programming. Not that I would ever claim they are
superior languages in any technical sense.
> Would you consider your low-level macro languages to be better suited to
> this task?
Oh no, it exists solely to create a floor for bootstrapping ease and
simplify the problem of cross-platform bootstrap verification.
> I might agree that such simple assembly-like languages are more
> straightforward for understanding the behavior of toy programs, where
> one can keep all of the moving parts in one's head. However, I would
> argue that those desirable properties of assembly-like languages do not
> scale to larger programs.
A self-hosting C compiler isn't exactly a toy program and if you read
it's code, you'll quickly discover there is no need to keep very much in
one's head at all.
It's real weakness is it's type system and lack of runtime.
One must remember a language's greatest strength is also it's greatest
weakness as well. Every desired feature must be paid for, usually in
regards to other desired features.
Performance, correctness and ease of development.
Pick one (the Industry picked Performance)
Things that should have been done differently if correctness was the
goal:
Hardware support for typed memory
Hardware support for garbage collection
Hardware support protecting against memory corruption (ECC, rowhammer
resistence circuits and SRAM instead of DRAM)
Barrel processor architectures (No risk from Spectre, Meltdown or
Raiden)
Hardware Capability tagging of processes
Flatten virtualization down to user processes.
Stack space and Heap Space different from each other and Program space.
Atleast a single attempt in the last 60 years from any military on the
planet to deal with the risks written in the Nexus Intruder Report
published in 1958.
I could spend literal weeks ranting and raving about modern hardware
makes correctness impossible for all but the trivial or the so isolated
from the hardware that performance makes it a non-starter for anything
but journal articles which are never read and forgotten within a
generation.
-Jeremiah
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Trustworthiness of build farms (was Re: CDN performance)
@ 2019-01-04 20:57 Jeremiah
2019-01-05 17:16 ` Mark H Weaver
0 siblings, 1 reply; 11+ messages in thread
From: Jeremiah @ 2019-01-04 20:57 UTC (permalink / raw)
To: mhw; +Cc: guix-devel
> Where are you getting those complexity expressions from?
Approximation of developer effort spent on single pass workflows and
bugfree libraries in the State of Michigan Welfware Eligibility System
extracted from it's ClearCase commit history. (Thank god, I finally got
them to convert to git after 3 years of wailing and gnashing of teeth)
> Can you cite references to back them up?
I can site the numbers I used to generate those approximate complexity equations
> If not, can you explain how you arrived at them?
Simple graphing and curve matching of collected data.
> What is 'c'?
Number of 'Features' a program had.
In short I found it is far easier for a developer to add features to a
program but it is really really hard to make sure the existing
functionality is bug free.
> If you're referring to the bugs found in CompCert, the ones I know about
> were actually bugs in the unverified parts of the toolchain.
I was referring to the bugs in the verified parts in regards to C's
undefined behavior.
> In the past, its frontend was unverified, and several bugs were found there.
> Even today, it produces assembly code, and depends on an unverified
> assembler and linker.
Which depending on if the compiler has been formally proven to only
output valid assembly (no 33bit offset loads) then that is less of a
concern.
(Let us just hope the assembler doesn't arbitrarily choose 8bit
immediates for performance reasons when given a 32bit int)
> Bugs can also exist in the specifications themselves, of course.
The most important class of bugs indeed
> I'm not sure what "and human model first behavior" means, but if you
> mean that the semantics of languages should strive to match what a human
> would naturally expect, avoiding surprising or unintuitive behavior, I
> certainly agree.
That is exactly what I mean. The problem is ultimately do be useful
things one has to support things that violate that in very terriable
ways (like support IEEE floating point, disable garbage collection, etc).
> I consider Standard ML, and some subsets of Scheme and
> Lisp, to be such languages
They certainly do have wonderful properties but I wouldn't say they
qualify as matching the human model first behavior requirement (easy to
verify by doing the 50 non-programmers first hand test)
Ask a room full of non-programmers to use scheme to write a standard web
CRUD app using an SQLite3 database backend or do XML parsing or generate
a pdf/excel file. It doesn't look pretty and most just give up on the
offer of free money after a bit.
> If I understand correctly, what you don't expect to happen has already
> been done. CakeML is free software, and formally proven correct all the
> way down to the machine code. Moreover, it implements a language with
> an exceptionally clear semantics and no undefined behavior.
I don't deny that the CakeML team did an excellent job on their formally
verified backend and their type inferencer. Most humans are not
programmers and of the programmers, most of them programming by proof
isn't in the realm of intuitive.
> Anyway, you've made it fairly clear that you're not interested in this
> line of work, and that's fine.
It isn't so much as not interested but rather it is lower on my priorities
> I appreciate the work you're doing > nonetheless.
As I appreciate the work you do as well.
-Jeremiah
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Trustworthiness of build farms (was Re: CDN performance)
2019-01-04 20:57 Jeremiah
@ 2019-01-05 17:16 ` Mark H Weaver
0 siblings, 0 replies; 11+ messages in thread
From: Mark H Weaver @ 2019-01-05 17:16 UTC (permalink / raw)
To: Jeremiah; +Cc: guix-devel
Hi Jeremiah,
Jeremiah@pdp10.guru writes:
>>>> To truly solve that problem, we need bug-free compilers.
>>> Impossible for all but the simplest of languages as the complexity of
>>> implementing a compiler/assembler/interpreter is ln(c)+a but the
>>> complexity of implementing a bug-free compiler/assembler/interpreter
>>> is (e^(c))! - a. Where a is the complexity cost of supporting it's
>>> host architecture.
>>
>> Where are you getting those complexity expressions from?
> Approximation of developer effort spent on single pass workflows and
> bugfree libraries in the State of Michigan Welfware Eligibility System
> extracted from it's ClearCase commit history. (Thank god, I finally got
> them to convert to git after 3 years of wailing and gnashing of teeth)
>
>> Can you cite references to back them up?
> I can site the numbers I used to generate those approximate complexity equations
>
>> If not, can you explain how you arrived at them?
> Simple graphing and curve matching of collected data.
In other words, it's anecdotal. This is analogous to saying:
"I once saw someone adding numbers A and B by counting beads, and
observed that the time required was |A| + |B|. From this I will
conclude that the complexity of adding numbers is |A| + |B|, and
therefore that adding numbers is impossible for all but the smallest
numbers."
Obviously, the flaw in this argument is that there exist much more
efficient ways to add numbers than counting beads. A claim of
complexity doesn't mean anything unless you can prove that it's a lower
bound.
There's a reason that I followed my call for bug-free compilers with the
claim: "In practice, this requires provably correct compilers." I wrote
that because I know that it's the only known practical way to do it for
non-trivial languages.
>> If you're referring to the bugs found in CompCert, the ones I know about
>> were actually bugs in the unverified parts of the toolchain.
> I was referring to the bugs in the verified parts in regards to C's
> undefined behavior.
Interesting. I hadn't heard of those. Can you cite the details?
>> In the past, its frontend was unverified, and several bugs were found there.
>> Even today, it produces assembly code, and depends on an unverified
>> assembler and linker.
> Which depending on if the compiler has been formally proven to only
> output valid assembly (no 33bit offset loads) then that is less of a
> concern.
> (Let us just hope the assembler doesn't arbitrarily choose 8bit
> immediates for performance reasons when given a 32bit int)
Right, which shows the problems with depending on unverified components,
but CompCert is no longer the state of the art in this regard. In
contrast, the CakeML compiler not only produces raw machine code,
moreover the proofs apply to the raw machine code of the CakeML compiler
itself. As a result, the only trusted specifications are those of the
source language and of the underlying machine code behavior (for the
subset of instructions that are actually generated).
>> Bugs can also exist in the specifications themselves, of course.
> The most important class of bugs indeed
>
>> I'm not sure what "and human model first behavior" means, but if you
>> mean that the semantics of languages should strive to match what a human
>> would naturally expect, avoiding surprising or unintuitive behavior, I
>> certainly agree.
> That is exactly what I mean. The problem is ultimately do be useful
> things one has to support things that violate that in very terriable
> ways (like support IEEE floating point,
I agree that IEEE floating point (and more generally inexact arithmetic)
is a problem, but a great many useful programs can be written without
using them, including most (if not all) of the programs that are most
important for us to trust. Operating systems, compilers, editors, and
communication tools such as chat clients and mail readers, have no need
for inexact arithmetic. These are the programs I care most about.
> disable garbage collection, etc).
Why do you include garbage collection in this list? I consider garbage
collection to be a _requirement_ for human model first behavior. Do you
consider it a hindrance? Also, multiple verified garbage collectors
already exist, e.g. those used in the runtimes of CakeML and Jitawa.
>> I consider Standard ML, and some subsets of Scheme and
>> Lisp, to be such languages
> They certainly do have wonderful properties but I wouldn't say they
> qualify as matching the human model first behavior requirement (easy to
> verify by doing the 50 non-programmers first hand test)
I think it's too ambitious to target non-programmers, because they do
not have the required skills to understand the behavior of complex
programs, regardless of what language is used. They could perhaps
understand toy programs, but that's not useful for helping them evaluate
the trustworthiness of the computing tools they actually use, which is
what I'm interested in.
Anyway, what language(s) would you consider to be superior to ML or a
subset of Scheme, based on the goal of human model first behavior?
Would you consider your low-level macro languages to be better suited to
this task?
I might agree that such simple assembly-like languages are more
straightforward for understanding the behavior of toy programs, where
one can keep all of the moving parts in one's head. However, I would
argue that those desirable properties of assembly-like languages do not
scale to larger programs.
Regards,
Mark
^ permalink raw reply [flat|nested] 11+ messages in thread
* RE: Trustworthiness of build farms (was Re: CDN performance)
@ 2018-12-22 17:23 Jeremiah
2018-12-23 16:37 ` Mark H Weaver
0 siblings, 1 reply; 11+ messages in thread
From: Jeremiah @ 2018-12-22 17:23 UTC (permalink / raw)
To: guix-devel
> 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.
A formal proof would be just one piece used in building layers of trust,
each of them indpendent and reinforcing of each other like layers of
kevlar in a bullet proof vest; thus even if some of the layers break,
the bullet doesn't get in to do damage.
> However, it's important to note several caveats:
Of course, we always miss things.
> * 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.
Well hex2's entire language is:
# line comment - ignore all text until lf
; line comment - ignore all text until lf
[0-F, 0-F] - The 2 chars are nibbles combined into a byte (Big Endian)
:label - The absolute address of the label used by pointers
!label{>label} - the 8bit relative address to label
@label{>label} - the 16bit relative address to label
$label - the 16bit absolute address of label
%label{>label} - the 32bit relative address to label
&label - the 32bit absolute address of label
the ?label>label form changes the displacement from current IP to the IP
of the label (aka calculates the length between labels) and outputs the
value in the format inidicated by the leading char (!@%)
With the explicit requirement of specifying the architecture (which
specifies the format and displacement calculation) and the base address
(aka what address does the IP start at)
The M1-macro language is even smaller:
# line comment - ignore all text until lf
; line comment - ignore all text until lf
DEFINE STRING1 STRING2 - Replace all STRING1 with STRING2
!number - the 8bit value of number in hex form
@number - the 16bit value of number in hex form
%number - the 32bit value of number in hex form
{:!@$%&}string - do not change and just output
"RAW STRING" - Convert to Hex (Big Endian)
'HEX' - Do not change and just output
So the specification for correctness is defined by the languages
themselves but you are correct in that someone has not picked up the
task of making a formally verified version of the tools yet.
> * 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.
Actually no, I am expecting arbitrary hardware platforms to cross verify
each other and thus provided one system is uncompromised or trusted, the
rest can be validated.
> * 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.
Stage0 assumes no operating system nor firmware and runs on bare metal
(literally TTL when done). Mescc-tools is just a port of the
specification to Linux to allow developers to leverage it to simplify
the later task of finishing.
> * The software running on the substitute servers could be compromised by
> stealing SSH keys from someone with root access.
Yes that is true but I don't want you to trust the substitute
servers. They exist for the purpose of convience not security
> * 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.
I believe that is a duplicate of the previous point but yes you are
correct that is a risk of having a single point of trust. Which is why
stage0 by design can not have a single point of trust because the
bootstrap steps can be done on arbitrary hardware and rewritten from
scratch with minimal effort. Thus one must need only review the source
code (which focuses on clarity and understandability and any issues with
it is a bug that needs to be reported).
> * Not only the substitute server, but also all of its build slaves, must
> be trusted as well.
Assume all machines could be compromised, then design assuming that any
of them can be compromised at any time but not all of them all of the
time. Then you have the solution to trust.
> So, while I certainly agree that it will be a *major* improvement to
> avoid the need to blindly trust precompiled bootstrap binaries
In terms of size that is true but in number of people who understand the
seed pieces, that unfortunately has reduced and that issue needs to be
addressed.
> we should be clear that the current efforts fall far short of a proof,
Absolutely agree at this port, we only have the specification for which
the proof must be written and someone will need to write a formally
verified version to verify that our roots of truth which are
approximations of the specification limited by the constraints of time
and human effort have not missed a subtle error.
> and there still remain several valid reasons not to place one's trust in
> substitute servers.
Personally I believe in terms of security and trust in absolute senses
of the words, you are beyound a shadow of a doubt correct but the
substitutes have never been about trust or security but convience which
many guix users want. But that doesn't mean that there are not things we
should start doing to make the task of compromising that trust harder.
For example:
Cryptographic port knocking for administration of servers requiring
access to a physically seperate hard token.
Cryptographically signed software white-listing on servers with the
signing keys being on a seperate system that is offline and the binaries
being signed being built from source on machines that have no internal
state and running only software explicitly specified and required for
the build.
Random system spot checks and wipes.
In short anything that makes single point compromises worthless needs to
be actively considered.
> Does that make sense?
Yes and hopefully my perspective makes sense as well.
-Jeremiah
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Trustworthiness of build farms (was Re: CDN performance)
2018-12-22 17:23 Jeremiah
@ 2018-12-23 16:37 ` Mark H Weaver
0 siblings, 0 replies; 11+ messages in thread
From: Mark H Weaver @ 2018-12-23 16:37 UTC (permalink / raw)
To: Jeremiah; +Cc: guix-devel
Hi Jeremiah,
If you could add an "In-Reply-To:" header to your responses, that would
be very helpful. It's easy to add it manually if needed: just copy the
"Message-ID:" header from the original message and replace "Message-ID:"
with "In-Reply-To:". As is, it's very difficult for me to keep track of
any conversation with you.
Jeremiah@pdp10.guru writes:
>> 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.
>
> A formal proof would be just one piece used in building layers of trust,
> each of them indpendent and reinforcing of each other like layers of
> kevlar in a bullet proof vest; thus even if some of the layers break,
> the bullet doesn't get in to do damage.
Agreed.
>> However, it's important to note several caveats:
> Of course, we always miss things.
>
>> * 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.
> Well hex2's entire language is:
[...]
> The M1-macro language is even smaller:
[...]
I'm not worried about those languages. Very little code is written in
them anyway, only a small part of the early bootstrap. My concern is
the correspondence between the source code and machine code for the
majority of the operating system and applications.
It's important to note that even a relatively obscure bug in the
compiler is enough to create an exploitable bug in the machine code of
compiled programs that's not present in the source code. Such compiler
bugs and the resulting exploits could be systematically searched for by
well-resourced attackers.
So, if we want to *truly* solve the problem of exploitable bugs existing
only in the machine code and not in the corresponding source, it is not
enough to eliminate the possibility of code deliberately inserted in our
toolchain that inserts trojan horses in other software.
To truly solve that problem, we need bug-free compilers. In practice,
this requires provably correct compilers.
Does that make sense?
Mark
^ permalink raw reply [flat|nested] 11+ messages in thread
* [PATCH 0/3] Defaulting to ci.guix.info (aka. berlin.guixsd.org)
@ 2018-12-03 15:43 Ludovic Courtès
2018-12-03 16:12 ` Using a CDN or some other mirror? Ludovic Courtès
0 siblings, 1 reply; 11+ messages in thread
From: Ludovic Courtès @ 2018-12-03 15:43 UTC (permalink / raw)
To: guix-patches; +Cc: guix-devel
Hello Guix!
These patches (actually the last one) switch Guix to default to
<https://ci.guix.info> for substitutes, in preparation for the
upcoming 0.16.0 release (hopefully this week!).
Rationale:
• berlin.guixsd.org generally performs better than hydra.gnu.org;
• berlin supports x86, ARMv7, and AArch64 (hydra lacks AArch64);
• berlin has much more storage space than hydra;
• berlin runs Cuirass on GuixSD, so software-wise, it corresponds
to what we want to push; Cuirass still has limitations in some
ways compared to Hydra, but we’re getting there, and
hydra.gnu.org is still up and running so we can still use it,
e.g., to track build progress until Cuirass is as convenient.
For the domain name I initially wanted “ci.guix.gnu.org” but we failed
to set that up. Oh well, I think that’s OK.
This change modifies the manual. Translations will thus be stale;
Julien, do you think it’d be reasonable to push a new pre-release
to the Translation Project? Or should be just live with the
slight inaccuracy?
Thanks,
Ludo’.
Ludovic Courtès (3):
etc: Add "ci.guix.info.pub" public key file.
Remove most references to hydra.gnu.org.
build: Default to https://ci.guix.info for substitutes.
Makefile.am | 5 +-
build-aux/check-available-binaries.scm | 4 +-
.../check-final-inputs-self-contained.scm | 2 +-
config-daemon.ac | 10 +--
doc/contributing.texi | 2 +-
doc/guix.texi | 67 +++++++++----------
etc/substitutes/ci.guix.info.pub | 1 +
gnu/services/base.scm | 4 +-
gnu/system/install.scm | 2 +-
guix/scripts/build.scm | 2 +-
guix/scripts/size.scm | 2 +-
guix/scripts/substitute.scm | 2 +-
guix/self.scm | 3 +
guix/store.scm | 2 +-
14 files changed, 51 insertions(+), 57 deletions(-)
create mode 120000 etc/substitutes/ci.guix.info.pub
--
2.19.2
^ permalink raw reply [flat|nested] 11+ messages in thread
* Using a CDN or some other mirror?
2018-12-03 15:43 [PATCH 0/3] Defaulting to ci.guix.info (aka. berlin.guixsd.org) Ludovic Courtès
@ 2018-12-03 16:12 ` Ludovic Courtès
2018-12-09 3:33 ` Chris Marusich
0 siblings, 1 reply; 11+ messages in thread
From: Ludovic Courtès @ 2018-12-03 16:12 UTC (permalink / raw)
To: 33600; +Cc: guix-devel
Hello,
Ludovic Courtès <ludo@gnu.org> skribis:
> These patches (actually the last one) switch Guix to default to
> <https://ci.guix.info> for substitutes, in preparation for the
> upcoming 0.16.0 release (hopefully this week!).
Right now, ci.guix.info points to berlin.guixsd.org, the front-end of
the build farm hosted at the MDC.
The previous setup was that mirror.hydra.gnu.org mirrors hydra.gnu.org
(the actual build farm front-end) using an nginx proxy:
https://git.savannah.gnu.org/cgit/guix/maintenance.git/tree/hydra/nginx/mirror.conf
This provides a bit of redundancy that we don’t have currently for
berlin.
Thus, I’m thinking about using a similar setup, but hosting the mirror
on some Big Corp CDN or similar. Chris Marusich came up with a setup
along these lines a while back:
https://lists.gnu.org/archive/html/guix-devel/2016-03/msg00312.html
Compared to Chris’s setup, given that ‘guix publish’ now provides
‘Cache-Control’ headers (that was not the case back then, see
<https://lists.gnu.org/archive/html/guix-devel/2016-03/msg00360.html>),
caching in the proxy should Just Work.
I would like us to set up such a mirror for berlin and then have
ci.guix.info point to that. The project should be able to pay the
hosting fees.
Thoughts?
Would someone like to get started? You’ll undoubtedly get all the
appreciation of each one of us and a beverage of your choice next time
we meet! :-)
Thanks,
Ludo’.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Using a CDN or some other mirror?
2018-12-03 16:12 ` Using a CDN or some other mirror? Ludovic Courtès
@ 2018-12-09 3:33 ` Chris Marusich
2018-12-09 15:59 ` CDN performance Ludovic Courtès
0 siblings, 1 reply; 11+ messages in thread
From: Chris Marusich @ 2018-12-09 3:33 UTC (permalink / raw)
To: Ludovic Courtès, Ricardo Wurmus, Hartmut Goebel,
Thompson, David, Meiyo Peng
Cc: guix-devel, 33600
[-- Attachment #1: Type: text/plain, Size: 13416 bytes --]
Hi everyone,
ludo@gnu.org (Ludovic Courtès) writes:
> Ludovic Courtès <ludo@gnu.org> skribis:
>
> [...] I’m thinking about using a similar setup, but hosting the mirror
> on some Big Corp CDN or similar. Chris Marusich came up with a setup
> along these lines a while back:
>
> https://lists.gnu.org/archive/html/guix-devel/2016-03/msg00312.html
>
> Compared to Chris’s setup, given that ‘guix publish’ now provides
> ‘Cache-Control’ headers (that was not the case back then, see
> <https://lists.gnu.org/archive/html/guix-devel/2016-03/msg00360.html>),
> caching in the proxy should Just Work.
>
> I would like us to set up such a mirror for berlin and then have
> ci.guix.info point to that. The project should be able to pay the
> hosting fees.
>
> Thoughts?
Regarding DNS, it would be nice if we could use an official GNU
subdomain. If we can't use a GNU subdomain, we should at least make
sure we have some kind of DNS auto-renewal set up so that nobody can
poach our domain names. And the operators should take appropriate
precautions when sharing any credentials used for managing it all.
Regarding CDNs, I definitely think it's worth a try! Even Debian is
using CloudFront (cloudfront.debian.net). In fact, email correspondence
suggests that as of 2013, Amazon may even have been paying for it!
https://lists.debian.org/debian-cloud/2013/05/msg00071.html
I wonder if Amazon would be willing to pay for our CloudFront
distribution if we asked them nicely?
In any case, before deciding to use Amazon CloudFront for ci.guix.info,
it would be prudent to estimate the cost. CloudFront, like most Amazon
AWS services, is a "pay for what you use" model. The pricing is here:
https://aws.amazon.com/cloudfront/pricing
To accurately estimate the cost, we need to know how many requests we
expect to receive, and how many bytes we expect to transfer out, during
a single month. Do we have information like this for berlin today?
Although I don't doubt that a CDN will perform better than what we have
now, I do think it would be good to measure the performance so that we
know for sure the money spent is actually providing a benefit. It would
be nice to have some data before and after to measure how availability
and performance have changed. Apart from anecdotes, what data do we
have to determine whether performance has improved after introducing a
CDN? For example, the following information could be useful:
* Network load on the origin server(s)
* Clients' latency to (the addresses pointed to by) ci.guix.info
* Clients' throughput while downloading substitutes from ci.guix.info
We don't log or collect client metrics, and that's fine. It could be
useful to add code to Guix to measure things like this when the user
asks to do so, but perhaps it isn't necessary. It may be good enough if
people just volunteer to manually gather some information and share it.
For example, you can define a shell function like this:
--8<---------------cut here---------------start------------->8---
measure_get () {
curl -L \
-o /dev/null \
-w "url_effective: %{url_effective}\\n\
http_code: %{http_code}\\n\
num_connects: %{num_connects}\\n\
num_redirects: %{num_redirects}\\n\
remote_ip: %{remote_ip}\\n\
remote_port: %{remote_port}\\n\
size_download: %{size_download} B\\n\
speed_download: %{speed_download} B/s\\n\
time_appconnect: %{time_appconnect} s\\n\
time_connect: %{time_connect} s\\n\
time_namelookup: %{time_namelookup} s\\n\
time_pretransfer: %{time_pretransfer} s\\n\
time_redirect: %{time_redirect} s\\n\
time_starttransfer: %{time_starttransfer} s\\n\
time_total: %{time_total} s\\n" \
"$1"
}
--8<---------------cut here---------------end--------------->8---
See "man curl" for the meaning of each metric.
You can then use this function to measure a substitute download. Here's
an example in which I download a large substitute (linux-libre) from one
of my machines in Seattle:
--8<---------------cut here---------------start------------->8---
$ measure_get https://berlin.guixsd.org/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19 2>/dev/null
url_effective: https://berlin.guixsd.org/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19
http_code: 200
num_connects: 1
num_redirects: 0
remote_ip: 141.80.181.40
remote_port: 443
size_download: 69899433 B
speed_download: 4945831.000 B/s
time_appconnect: 0.885277 s
time_connect: 0.459667 s
time_namelookup: 0.254210 s
time_pretransfer: 0.885478 s
time_redirect: 0.000000 s
time_starttransfer: 1.273994 s
time_total: 14.133584 s
$
--8<---------------cut here---------------end--------------->8---
Here, it took 0.459667 - 0.254210 = 0.205457 seconds (about 205 ms) to
establish the TCP connection after the DNS lookup. The average
throughput was 1924285 bytes per second (about 40 megabits per second,
where 1 megabit = 10^6 bits). It seems my connection to berlin is
already pretty good!
We can get more information about latency by using a tool like mtr:
--8<---------------cut here---------------start------------->8---
$ sudo mtr -c 10 --report-wide --tcp -P 443 berlin.guixsd.org
Start: 2018-12-08T16:57:40-0800
HOST: localhost.localdomain Loss% Snt Last Avg Best Wrst StDev
[... I've omitted the intermediate hops because they aren't relevant ...]
13.|-- 141.80.181.40 0.0% 10 205.0 201.9 194.9 212.8 5.6
--8<---------------cut here---------------end--------------->8---
My machine's latency to berlin is about 202 ms, which matches what we
calculated above.
For experimentation, I've set up a CloudFront distribution at
berlin-mirror.marusich.info that uses berlin.guixsd.org as its origin
server. Let's repeat these steps to measure the performance of the
distribution from my machine's perspective (before I did this, I made
sure the GET would result in a cache hit by downloading the substitute
once before and verifying that the same remote IP address was used):
--8<---------------cut here---------------start------------->8---
$ measure_get https://berlin-mirror.marusich.info/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19 2>/dev/null
url_effective: https://berlin-mirror.marusich.info/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19
http_code: 200
num_connects: 1
num_redirects: 0
remote_ip: 13.32.254.57
remote_port: 443
size_download: 69899433 B
speed_download: 9821474.000 B/s
time_appconnect: 0.607593 s
time_connect: 0.532417 s
time_namelookup: 0.511086 s
time_pretransfer: 0.608029 s
time_redirect: 0.000000 s
time_starttransfer: 0.663578 s
time_total: 7.117266 s
$ sudo mtr -c 10 --report-wide --tcp -P 443 berlin-mirror.marusich.info
Start: 2018-12-08T17:04:48-0800
HOST: localhost.localdomain Loss% Snt Last Avg Best Wrst StDev
[... I've omitted the intermediate hops because they aren't relevant ...]
14.|-- server-52-84-21-199.sea32.r.cloudfront.net 0.0% 10 19.8 20.3 14.3 28.9 4.9
--8<---------------cut here---------------end--------------->8---
Establishing the TCP connection took about 21 ms (which matches the mtr
output), and the throughput was about 79 megabits per second. (On this
machine, 100 Mbps is the current link speed, according to dmesg output.)
This means that in my case, when using CloudFront the latency is 10x
lower, and the throughput (for a cache hit) is 2x higher, than using
berlin.guixsd.org directly!
It would be interesting to see what the performance is for others.
Ricardo Wurmus <rekado@elephly.net> writes:
> Large ISPs also provide CDN services. I already contacted Deutsche
> Telekom so that we can compare their CDN offer with the Amazon Cloudfont
> setup that Chris has configured.
That's great! There are many CDN services out there. I am unfamiliar
with most of them. It will be good to see how Deutsche Telekom's
offering compares to CloudFront.
FYI, CloudFront has edge locations in the following parts of the world:
https://aws.amazon.com/cloudfront/features/
Hartmut Goebel <hartmut@goebel-consult.de> writes:
> Am 03.12.2018 um 17:12 schrieb Ludovic Courtès:
>> Thus, I’m thinking about using a similar setup, but hosting the mirror
>> on some Big Corp CDN or similar.
>
> Isn't this a contradiction: Building a free infrastructure relaying on
> servers from some Big Corporation? Let allow the privacy concerns
> raising when delivering data via some Big Corporation.
>
> If delivering "packages" works via static data without requiring any
> additional service, we could ask universities to host Guix, too. IMHO
> this is a much preferred solution since this is a decentralized publish
> infrastructure already in place for many GNU/Linux distributions.
I understand your concern about using a third-party service. However,
we wouldn't be using a CDN as a "software substitute", which is one of
the primary risks of using a web service today:
https://www.gnu.org/philosophy/who-does-that-server-really-serve.html
Instead, we would be using a CDN as a performance optimization that is
transparent to a Guix user. You seem unsettled by the idea of
entrusting any part of substitute delivery to a third party, but
concretely what risks do you foresee?
Regarding your suggestion to ask universities to host mirrors (really,
caching proxies), I think it could be a good idea. As Leo mentioned,
the configuration to set up an NGINX caching proxy of Hydra (or berlin)
is freely available in maintenance.git. Do you think we could convince
some universities to host caching proxies that just run an NGINX web
server using those configurations?
If we can accomplish that, it may still be helpful. If there is
interest in going down this path, I can explore some possibilities in
the Seattle area. If the university-owned caching proxies are easily
discoverable (i.e., we list them on the website), then users might
manually set their substitute URL to point to one that's close by.
Going further, if our DNS provider supports something like "geolocation
routing" for DNS queries, we might even be able to create DNS records
for ci.guix.info that point to those universities' caching proxies. In
this way, when a user resolves ci.guix.info, they would get the address
of a university-owned caching proxy close by. This could have the
benefits of requiring less money than a full-fledged CDN like Amazon
CloudFront, and also decentralizing the substitute delivery, while still
remaining transparent to Guix users. However, it would still require us
to rely on a third-party DNS service.
For example, Amazon Route 53 provides this sort of geolocation routing:
https://docs.aws.amazon.com/Route53/latest/DeveloperGuide/routing-policy.html#routing-policy-geo
I wouldn't be surprised if there are other DNS providers out there who
offer something similar. However, I also wouldn't be surprised if the
overall performance of CloudFront turns out to be better.
"Thompson, David" <dthompson2@worcester.edu> writes:
> If AWS CloudFront is the path chosen, it may be worthwhile to follow
> the "infrastructure as code" practice and use CloudFormation to
> provision the CloudFront distribution and any other supporting
> resources. The benefit is that there would be a record of exactly
> *how* the project is using these commercial services and the setup
> could be easily reproduced. The timing is interesting here because I
> just attended the annual AWS conference on behalf of my employer and
> while I was there I felt inspired to write a Guile API for building
> CloudFormation "stacks". You can see a small sample of what it does
> here: https://gist.github.com/davexunit/db4b9d3e67902216fbdbc66cd9c6413e
Nice! That seems useful. I will have to play with it. I created my
distributions manually using the AWS Management Console, since it's
relatively easy to do. I agree it would be better to practice
"infrastructure as code."
On that topic, I've also heard good things about Terraform by HashiCorp,
which is available under the Mozilla Public License 2.0:
https://github.com/hashicorp/terraform
Here is a comparison of Terraform and CloudFormation:
https://www.terraform.io/intro/vs/cloudformation.html
I looked briefly into packaging Terraform for Guix. It's written in Go.
It seems possible, but I haven't invested enough time yet.
As a final option, since the AWS CLI is already packaged in Guix, we
could just drive CloudFormation or CloudFront directly from the CLI.
Meiyo Peng <meiyo.peng@gmail.com> writes:
> I like the idea of IPFS. We should try it. It would be great if it works
> well.
>
> If at some point we need to setup traditional mirrors like other major
> Gnu/Linux distros, I can contact my friends in China to setup mirrors in
> several universities. I was a member of LUG@USTC, which provides the
> largest FLOSS mirror in China.
IPFS would be neat. So would Gnunet. Heck, even a publication
mechanism using good old BitTorrent would be nice. All of these would
require changes to Guix, I suppose.
A CDN would require no changes to Guix, and that's part of why it's so
appealing.
--
Chris
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]
^ permalink raw reply [flat|nested] 11+ messages in thread
* CDN performance
2018-12-09 3:33 ` Chris Marusich
@ 2018-12-09 15:59 ` Ludovic Courtès
2018-12-13 8:05 ` Chris Marusich
0 siblings, 1 reply; 11+ messages in thread
From: Ludovic Courtès @ 2018-12-09 15:59 UTC (permalink / raw)
To: Chris Marusich; +Cc: Hartmut Goebel, guix-devel, 33600
Hello Chris,
Chris Marusich <cmmarusich@gmail.com> skribis:
> Regarding DNS, it would be nice if we could use an official GNU
> subdomain. If we can't use a GNU subdomain, we should at least make
> sure we have some kind of DNS auto-renewal set up so that nobody can
> poach our domain names. And the operators should take appropriate
> precautions when sharing any credentials used for managing it all.
Agreed.
Regarding the GNU sub-domain, as I replied to Meiyo, I’m in favor of it,
all we need is someone to champion setting it up.
> Regarding CDNs, I definitely think it's worth a try! Even Debian is
> using CloudFront (cloudfront.debian.net). In fact, email correspondence
> suggests that as of 2013, Amazon may even have been paying for it!
>
> https://lists.debian.org/debian-cloud/2013/05/msg00071.html
(Note that debian.net is not Debian, and “there’s no cloud, only other
people’s computer” as the FSFE puts it.)
> Although I don't doubt that a CDN will perform better than what we have
> now, I do think it would be good to measure the performance so that we
> know for sure the money spent is actually providing a benefit. It would
> be nice to have some data before and after to measure how availability
> and performance have changed. Apart from anecdotes, what data do we
> have to determine whether performance has improved after introducing a
> CDN? For example, the following information could be useful:
>
> * Network load on the origin server(s)
> * Clients' latency to (the addresses pointed to by) ci.guix.info
> * Clients' throughput while downloading substitutes from ci.guix.info
Note that performance is one aspect; another one is availability (we’ve
seen that with the recent hydra.gnu.org outage!). We know we’ll always
win in terms of availability by having a CDN in front of our servers.
That said, measuring performance is very useful and it’s great that we
can benefit from your expertise here!
> Here, it took 0.459667 - 0.254210 = 0.205457 seconds (about 205 ms) to
> establish the TCP connection after the DNS lookup. The average
> throughput was 1924285 bytes per second (about 40 megabits per second,
> where 1 megabit = 10^6 bits). It seems my connection to berlin is
> already pretty good!
Indeed. The bandwidth problem on berlin is when you’re the first to
download a nar and it’s not been cached by nginx yet. In that case, you
get very low bandwidth (like 10 times less than when the item is cached
by nginx.) I’ve looked into it, went as far as strace’ing nginx, but
couldn’t find the reason of this.
Do you any idea?
> Establishing the TCP connection took about 21 ms (which matches the mtr
> output), and the throughput was about 79 megabits per second. (On this
> machine, 100 Mbps is the current link speed, according to dmesg output.)
> This means that in my case, when using CloudFront the latency is 10x
> lower, and the throughput (for a cache hit) is 2x higher, than using
> berlin.guixsd.org directly!
Impressive.
> It would be interesting to see what the performance is for others.
I’ve tried this from home (in France, with FTTH):
--8<---------------cut here---------------start------------->8---
$ measure_get https://berlin.guixsd.org/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19 2>/dev/null
url_effective: https://berlin.guixsd.org/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19
http_code: 200
num_connects: 1
num_redirects: 0
remote_ip: 141.80.181.40
remote_port: 443
size_download: 69899433 B
speed_download: 1522001.000 B/s
time_appconnect: 0.178892 s
time_connect: 0.049649 s
time_namelookup: 0.000422 s
time_pretransfer: 0.178934 s
time_redirect: 0.000000 s
time_starttransfer: 0.278312 s
time_total: 45.926021 s
$ measure_get https://berlin-mirror.marusich.info/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19 2>/dev/null
url_effective: https://berlin-mirror.marusich.info/nar/gzip/1bq783rbkzv9z9zdhivbvfzhsz2s5yac-linux-libre-4.19
http_code: 200
num_connects: 1
num_redirects: 0
remote_ip: 2600:9000:2116:6e00:c:49d4:5a80:93a1
remote_port: 443
size_download: 69899433 B
speed_download: 20803402.000 B/s
time_appconnect: 0.552008 s
time_connect: 0.482477 s
time_namelookup: 0.467598 s
time_pretransfer: 0.552157 s
time_redirect: 0.000000 s
time_starttransfer: 0.735758 s
time_total: 3.360500 s
--8<---------------cut here---------------end--------------->8---
Wall-clock time is less than a tenth; woow.
Thanks for sharing your insight and scripts!
Ludo’.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: CDN performance
2018-12-09 15:59 ` CDN performance Ludovic Courtès
@ 2018-12-13 8:05 ` Chris Marusich
2018-12-13 10:41 ` Giovanni Biscuolo
0 siblings, 1 reply; 11+ messages in thread
From: Chris Marusich @ 2018-12-13 8:05 UTC (permalink / raw)
To: Ludovic Courtès; +Cc: Hartmut Goebel, guix-devel, 33600
[-- Attachment #1: Type: text/plain, Size: 5731 bytes --]
Ludovic Courtès <ludo@gnu.org> writes:
> Regarding the GNU sub-domain, as I replied to Meiyo, I’m in favor of it,
> all we need is someone to champion setting it up.
I could help with this. Whom should I contact?
>> Regarding CDNs, I definitely think it's worth a try! Even Debian is
>> using CloudFront (cloudfront.debian.net). In fact, email correspondence
>> suggests that as of 2013, Amazon may even have been paying for it!
>>
>> https://lists.debian.org/debian-cloud/2013/05/msg00071.html
>
> (Note that debian.net is not Debian, and “there’s no cloud, only other
> people’s computer” as the FSFE puts it.)
I do try to avoid the term "cloud" whenever possible. It's hard to
avoid when it's in the product name, though! A wise man once said, "A
cloud in the mind is an obstacle to clear thinking." ;-)
You may be right about debian.net. I don't know who owns that domain.
It's confusing, since debian.org is definitely owned by the Debian
project, and the following page says they're using Amazon CloudFront:
https://deb.debian.org/
Maybe Debian still uses Amazon CloudFront, or maybe they don't any more.
In any case, I've found the following email thread, which documents a
thoughtful discussion regarding whether or not Debian should use a CDN.
They discussed many of the same concerns we're discussing here.
https://lists.debian.org/debian-project/2013/10/msg00029.html
A summary, in the middle of the long thread, is here:
https://lists.debian.org/debian-project/2013/10/msg00074.html
Later, part of the thread broke off and continued here:
https://lists.debian.org/debian-project/2014/02/msg00001.html
That's as far as I've read.
Judging by that email thread, one of the reasons why Debian considered
using a CDN was because they felt that the cost, in terms of people
power, of maintaining their own "proto-CDN" infrastructure had grown too
great. I believe it! I think it would be ill-advised for the Guix
project to expend effort and capital on building and maintaining its own
CDN. I think it would be wiser to focus on developing a decentralized
substitute solution (GNUnet, IPFS, etc.).
That said, I still think that today Guix should provide a third-party
CDN option. For many Guix users, a CDN would improve performance and
availability of substitutes. Contracting with a third party to provide
the CDN service would require much less effort and capital than building
and maintaining a CDN from scratch. This would also enable the project
to focus more on building a decentralized substitute solution. And once
that decentralized solution is ready, it will be easy to just "turn off"
the CDN.
I also understand Hartmut's concerns. The risks he points out are
valid. Because of those risks, even if we make a third-party CDN option
available, some people will choose not to use it. For that reason, we
should not require Guix users to use a third-party CDN, just as we do
not require them to use substitutes from our build farm.
However, not everyone shares the same threat model. For example,
although some people choose not to trust substitutes from our build
farm, still others do. The choice is based on one's own individual
situation. Similarly, if we make a third-party CDN option available and
explain the risks of using it, Guix users will be able to make an
educated decision for themselves about whether or not to use it.
>> Here, it took 0.459667 - 0.254210 = 0.205457 seconds (about 205 ms) to
>> establish the TCP connection after the DNS lookup. The average
>> throughput was 1924285 bytes per second (about 40 megabits per second,
>> where 1 megabit = 10^6 bits). It seems my connection to berlin is
>> already pretty good!
>
> Indeed. The bandwidth problem on berlin is when you’re the first to
> download a nar and it’s not been cached by nginx yet. In that case, you
> get very low bandwidth (like 10 times less than when the item is cached
> by nginx.) I’ve looked into it, went as far as strace’ing nginx, but
> couldn’t find the reason of this.
>
> Do you any idea?
I made a typo here. The value "1924285" should have been "4945831",
which is what measure_get printed. However, the intended result (40
Mbps) is still correct.
Actually, I thought 40 megabits per second was pretty great for a
single-threaded file transfer that originated in Europe (I think?) and
terminated in Seattle (via my residential Comcast downlink). I
requested that particular file many times before that final test run, so
it was probably already cached by nginx.
However, I believe you when you say that it's slow the first time you
download the substitute from berlin. What path does the data take from
its origin through berlin? If berlin needs to download the initial file
from another server, perhaps the connection between berlin and that
server is the bottleneck? Maybe we should discuss that in a different
email thread, though.
> I’ve tried this from home (in France, with FTTH):
>
> [...]
>
> speed_download: 20803402.000 B/s
Wow, that's 166 megabits per second! I'm jealous. :-)
> Wall-clock time is less than a tenth; woow.
I expect others will see similar performance improvements, as long as
they are close to the edge locations provided by Amazon CloudFront and
their local ISP downlink is fast enough to see a benefit. Again, the
edge locations are here:
https://aws.amazon.com/cloudfront/features/
Here's a direct link to their current map:
https://d1.awsstatic.com/global-infrastructure/maps/CloudFront%20Network%20Map%2010.12.18.59e838df2f373247d2efaeb548076e084fd8993e.png
--
Chris
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: CDN performance
2018-12-13 8:05 ` Chris Marusich
@ 2018-12-13 10:41 ` Giovanni Biscuolo
2018-12-15 1:40 ` Mark H Weaver
0 siblings, 1 reply; 11+ messages in thread
From: Giovanni Biscuolo @ 2018-12-13 10:41 UTC (permalink / raw)
To: Chris Marusich, Ludovic Courtès; +Cc: guix-devel, 33600
[-- Attachment #1: Type: text/plain, Size: 3388 bytes --]
Hi Chris,
nice to see this discussion, IMHO how GuixSD subsitutes are distributed
is a key issue in our ecosystem and is _all_ about privacy and metadata
*mass* collection
most "normal users" are not concerned about this so they are fine with
super-centralization since it's a convenience... not us :-)
personally I've come to GuixSD because I see this project as a key part
in liberating me from this class of problems
Chris Marusich <cmmarusich@gmail.com> writes:
[...]
> A summary, in the middle of the long thread, is here:
>
> https://lists.debian.org/debian-project/2013/10/msg00074.html
thank you for the reference, I've only read this summary
the key part of it IMHO is
"Q: Do CDNs raise more security/privacy concerns than our mirrors?"
and the related subthread
https://lists.debian.org/debian-project/2013/10/msg00033.html
the quick reply to the above question is: yes, CDNs raise more
secutiry/privacy concerns than "distributed mirrors"
obviuosly "distributed mirrors" _does_ rise some security/privacy
concerns but *centralization*... much more
[...]
> Judging by that email thread, one of the reasons why Debian considered
> using a CDN was because they felt that the cost, in terms of people
> power, of maintaining their own "proto-CDN" infrastructure had grown too
> great.
I'm still new to guixsd but understood enough to se we are much more
well equipped to maintain our distributed network of substitutes caching
servers... **transparently** configured :-)
[...]
> I also understand Hartmut's concerns. The risks he points out are
> valid. Because of those risks, even if we make a third-party CDN option
> available, some people will choose not to use it.
probably I'll be one of those, I'm considering to maintain a caching
substitute server in a "semi-trusted" colocated space and I'd be very
happy to share that server with the community
[...]
> However, not everyone shares the same threat model. For example,
> although some people choose not to trust substitutes from our build
> farm, still others do.
for this very reason IMHO we should work towards a network of **very
trusted** build farms directly managed and controlled by the GuixSD
project sysadmins; if build farms will be able to quickly provide
substitutes, caching mirrors will be _much more_ effective than today
... and a network of "automated guix challenge" servers to spot
not-reproducible software in GuixSD
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)
> The choice is based on one's own individual
> situation. Similarly, if we make a third-party CDN option available and
> explain the risks of using it, Guix users will be able to make an
> educated decision for themselves about whether or not to use it.
that's an option... like a "last resort" in order to be able to use
guixSD :-)
we could also teach people how to setup their own caching servers and
possibly share them with the rest of the local community (possibly with
some coordination effort from the project sysadmins)
for Milan I've plans to setup such caching mirror in Jan 2019
[...]
happy hacking!
Gio
--
Giovanni Biscuolo
Xelera IT Infrastructures
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: CDN performance
2018-12-13 10:41 ` Giovanni Biscuolo
@ 2018-12-15 1:40 ` Mark H Weaver
2018-12-19 12:40 ` Giovanni Biscuolo
0 siblings, 1 reply; 11+ messages in thread
From: Mark H Weaver @ 2018-12-15 1:40 UTC (permalink / raw)
To: Giovanni Biscuolo; +Cc: guix-devel, 33600
Hi Giovanni,
Giovanni Biscuolo <g@xelera.eu> 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?
Mark
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: CDN performance
2018-12-15 1:40 ` Mark H Weaver
@ 2018-12-19 12:40 ` Giovanni Biscuolo
2018-12-21 0:23 ` Trustworthiness of build farms (was Re: CDN performance) Mark H Weaver
0 siblings, 1 reply; 11+ messages in thread
From: Giovanni Biscuolo @ 2018-12-19 12:40 UTC (permalink / raw)
To: Mark H Weaver; +Cc: guix-devel, 33600
[-- Attachment #1: Type: text/plain, Size: 1967 bytes --]
Hi Mark,
sorry for the late reply
Mark H Weaver <mhw@netris.org> writes:
> Giovanni Biscuolo <g@xelera.eu> 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:
--8<---------------cut here---------------start------------->8---
> 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.
--8<---------------cut here---------------end--------------->8---
and
--8<---------------cut here---------------start------------->8---
> 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.
--8<---------------cut here---------------end--------------->8---
maybe a more correct definition of the above "scientific proof" should be
"mathematical proof"
I lack the theoretical basis to be more precise now, sorry :-S
a marketing-like campaign sould be "no more trusting trust"
best regards
Giovanni
--
Giovanni Biscuolo
Xelera IT Infrastructures
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]
^ permalink raw reply [flat|nested] 11+ messages in thread
* Trustworthiness of build farms (was Re: CDN performance)
2018-12-19 12:40 ` Giovanni Biscuolo
@ 2018-12-21 0:23 ` Mark H Weaver
0 siblings, 0 replies; 11+ messages in thread
From: Mark H Weaver @ 2018-12-21 0:23 UTC (permalink / raw)
To: Giovanni Biscuolo; +Cc: guix-devel, 33600
Hi Giovanni,
Giovanni Biscuolo <g@xelera.eu> writes:
> Mark H Weaver <mhw@netris.org> writes:
>
>> Giovanni Biscuolo <g@xelera.eu> 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
^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2019-01-20 12:24 UTC | newest]
Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-12-26 2:29 Trustworthiness of build farms (was Re: CDN performance) Jeremiah
2018-12-28 7:12 ` Mark H Weaver
-- strict thread matches above, loose matches on Subject: below --
2019-01-20 12:24 Jeremiah
2019-01-05 20:15 jeremiah
2019-01-06 20:47 ` Chris Marusich
2019-01-18 10:54 ` Giovanni Biscuolo
2019-01-04 20:57 Jeremiah
2019-01-05 17:16 ` Mark H Weaver
2018-12-22 17:23 Jeremiah
2018-12-23 16:37 ` Mark H Weaver
2018-12-03 15:43 [PATCH 0/3] Defaulting to ci.guix.info (aka. berlin.guixsd.org) Ludovic Courtès
2018-12-03 16:12 ` Using a CDN or some other mirror? Ludovic Courtès
2018-12-09 3:33 ` Chris Marusich
2018-12-09 15:59 ` CDN performance Ludovic Courtès
2018-12-13 8:05 ` Chris Marusich
2018-12-13 10:41 ` Giovanni Biscuolo
2018-12-15 1:40 ` Mark H Weaver
2018-12-19 12:40 ` Giovanni Biscuolo
2018-12-21 0:23 ` Trustworthiness of build farms (was Re: CDN performance) Mark H Weaver
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.