13/66: ccs-2021: Proof-read and tweak.

[Ludovic Courtès]

civodul pushed a commit to branch master
in repository maintenance.

commit 2c6e49abe8d3e7fb2ee172413669a3a4f5c7d19a
Author: Ludovic Courtès <ludo@gnu.org>
AuthorDate: Mon May 3 16:43:16 2021 +0200

    ccs-2021: Proof-read and tweak.
---
 doc/ccs-2021/security.sbib    |  20 ++++-
 doc/ccs-2021/supply-chain.skb | 201 +++++++++++++++++++++++-------------------
 2 files changed, 127 insertions(+), 94 deletions(-)

diff --git a/doc/ccs-2021/security.sbib b/doc/ccs-2021/security.sbib
index 3b9f57b..dbcfb8e 100644
--- a/doc/ccs-2021/security.sbib
+++ b/doc/ccs-2021/security.sbib
@@ -87,7 +87,7 @@
   (url 
"https://guix.gnu.org/en/blog/2020/guix-further-reduces-bootstrap-seed-to-25/";))
 
 (article thompson1984:trusting-trust
-  (author "Thompson, Ken")
+  (author "Ken Thompson")
   (title "Reflections on Trusting Trust")
   (year "1984")
   (issue_date "Aug 1984")
@@ -102,6 +102,18 @@
   (month "August")
   (pages "761--763"))
 
+(inproceedings merkle1980:protocols
+  (author "Ralph C. Merkle")
+  (institution "ELXSi International")
+  (title "Protocols for Public Key Cryptosystems")
+  (booktitle "Proceedings of the IEEE Symposium on Security and
+Privacy")
+  (address "Oakland, CA")
+  (pages "122--134")
+  (month "April")
+  (year "1980")
+  (url "http://www.merkle.com";))
+
 (inproceedings stevens2017:detection
   (author "Stevens, Marc and Shumow, Daniel")
   (title "Speeding up Detection of SHA-1 Collision Attacks Using Unavoidable 
Attack Conditions")
@@ -155,6 +167,12 @@ Thayer")
   (month "November")
   (url "https://tools.ietf.org/html/rfc4880";))
 
+(misc denis2021:minisign-web
+  (author "Frank Denis")
+  (title "Minisign — Simple tool to sign files and verify signatures")
+  (url "https://jedisct1.github.io/minisign";)
+  (year "2021"))
+
 (misc git2021:hash-transition
   (author "Git project")
   (title "Hash Function Transition")
diff --git a/doc/ccs-2021/supply-chain.skb b/doc/ccs-2021/supply-chain.skb
index 4625c3a..a564000 100644
--- a/doc/ccs-2021/supply-chain.skb
+++ b/doc/ccs-2021/supply-chain.skb
@@ -366,11 +366,11 @@ no use when the server hosting the repository is 
compromised, as
 happened to GNU’s Savannah in 2010 ,(ref :bib 'fsf2010:compromise).])
       
       (p [An attacker who gained access to the server hosting the Guix
-repository with can push code, which every user would then pull.  The
+repository can push code, which every user would then pull.  The
 change might even go unnoticed and remain in the repository forever.
 They may also reset the main branch to an earlier revision, leading
 users to install outdated software with known vulnerabilities—a ,(emph
-[downgrade attack]); the attacker may also change the main branch
+[downgrade attack]).  Likewise, the attacker may change the main branch
 reference so it points to a different branch, containing new malicious
 code—a ,(emph [teleport attack]) ,(ref :bib 'torresarias2016:omitting).
 These are the kind of attacks we want to protect against.]))
@@ -378,13 +378,13 @@ These are the kind of attacks we want to protect 
against.]))
    (chapter :title [Authenticating Git Checkouts]
       :ident "authenticating"
       
-      (p [If we take a step back, the problem we are trying to solve is
+      (p [Taking a step back, the problem we are trying to solve is
 not specific to Guix and to software deployment tools: it’s about
 ,(emph [authenticating Git checkouts]).  By that, we mean that when ,(tt [guix 
pull])
 obtains code from Git, it should be able to tell that all the commits it
 fetched were pushed by authorized developers of the project.  We are
 really looking at individual commits, not tags, because users can choose
-to pull arbitrary points in the commit history of Guix and third-party
+to pull at arbitrary points in the commit history of Guix and third-party
 channels.])
       
       (p [Git is an append-only, content-addressed version control
@@ -392,20 +392,24 @@ system.  Revision history in Git is represented by a 
graph of commit
 objects: each commit can have zero or more parent commits.  In the
 common case, there is a single parent commit pointing to the previous
 revision; “merge commits”, which are created by merging the history of
-two development branches, have two parent commits.  “Append-only” means
-that we only ever ,(emph [add]) new commits to the graph.
+two development branches, have two parents.  “Append-only” means that
+one only ever ,(emph [adds]) new commits to the graph.
 “Content-addressed” corresponds to the fact that commits are referred to
-by their cryptographic content hash (SHA-1); the contents of a revision,
-,(it [trees]) in Git parlance, as well as all other kind of data stored
-in a Git repository, are all content-addressed.])
-
-      (p [Git supports ,(emph [signed commits]).  A signed
-commit includes an additional header containing as ASCII-armored OpenPGP
-signature computer over the other headers of the commit.  Checkout
-authentication requires cryptographically signed commits.  By signing a
+by their cryptographic content hash, currently computed with SHA-1 (more
+on that in ,(numref :text [Section] :ident "sha1")); the contents of a
+revision, ,(it [trees]) in Git parlance, as well as other kinds of data
+stored in a Git repository, are all content-addressed.  As an exception,
+metadata such as references to the latest commit of a branch, is ,(emph
+[not]) stored in the content-addressed store ,(ref :bib
+'torresarias2016:omitting).])
+
+      (p [Git supports ,(emph [signed commits]).  A signed commit
+includes an additional header containing as ASCII-armored OpenPGP
+signature computer over the other headers of the commit.  By signing a
 commit, a Guix developer asserts that they are the one who made the
 commit; they may be its author, or they may be the person who applied
-somebody else’s changes after review.  It also requires a notion of
+somebody else’s changes after review.  Checkout authentication requires
+cryptographically signed commits.  It also requires a notion of
 authorization: we don’t simply want commits to have a valid signature,
 we want them to be signed by an authorized key.  The set of authorized
 keys changes over time as people join and leave the project.])
@@ -418,7 +422,7 @@ keys changes over time as people join and leave the 
project.])
      that lists the OpenPGP key fingerprints of authorized committers.])
     (item [A commit is considered authentic if and only if it is signed by one
      of the keys listed in the ,(tt [.guix-authorizations]) file of each of
-     its parents.  This is the ,(emph [authorization invariant]).]))
+     its parents.  We call this the ,(emph [authorization invariant]).]))
      
 The ,(tt [.guix-authorizations]) format is a Lisp-style s-expression (or
 “sexp”), as shown in ,(numref :text [Figure] :ident
@@ -449,19 +453,18 @@ authorizations.])
         :ident "fig-commits"
         (image :file "images/commit-graph.pdf"))
 
-      (p [Let’s take an example to illustrate the authorization
+      (p [Let us take an example to illustrate the authorization
 invariant.  In ,(numref :text [Figure] :ident "fig-commits"), each box
-is a commit, and each arrow is a parent relationship.])
-
-      (p [This figure shows two lines of development: the orange line may be 
the
-main development branch, while the purple line may correspond to a
-feature branch that was eventually merged in commit ,(it [F]).  ,(it [F]) is a 
merge
-commit, so it has two parents: ,(it [D]) and ,(it [E]).])
+is a commit, and each arrow is a parent relationship.  This figure shows
+two lines of development: the orange line on the left may be the main
+development branch, while the purple line may correspond to a feature
+branch that was eventually merged in commit ,(it [F]).  ,(it [F]) is a
+merge commit, so it has two parents: ,(it [D]) and ,(it [E]).])
 
       (p [Labels next to boxes show who’s in ,(tt [.guix-authorizations]): for 
commit A,
 only Alice is an authorized committer, and for all the other commits,
-both Bob and Alice are authorized committers.  For each commit, we see
-that the authorization invariant holds; for example:
+both Bob and Alice are authorized committers.  For each commit, the
+authorization invariant holds; for example:
 
 ,(itemize
     (item [commit ,(it [B]) was made by Alice, who was the only authorized 
committer
@@ -471,11 +474,12 @@ that the authorization invariant holds; for example:
     (item [commit ,(it [F]) was made by Alice, who was among the authorized
     committers of both parents, commits ,(it [D]) and ,(it [E]).]))
 
-The authorization invariant has the nice property that it’s simple to
-state, and it’s simple to check and enforce.  This is what ,(tt [guix pull])
-implements.  If your current Guix, as returned by ,(tt [guix describe]) is at
-commit ,(it [A]) and you want to pull to commit ,(it [F]), ,(tt [guix pull]) 
traverses all
-these commits and checks the authorization invariant.])
+The authorization invariant has the nice property that it is simple to
+state, and simple to check and enforce.  This is what ,(tt [guix pull])
+implements.  If a user’s current Guix revision (as returned by the ,(tt
+[guix describe]) command) is at commit ,(it [A]) and the user wants to
+pull to commit ,(it [F]), ,(tt [guix pull]) traverses all these commits
+and checks the authorization invariant.])
 
       (p [Once a commit has been authenticated, all the commits in its
 transitive closure are known to be already authenticated.  ,(tt [guix pull])
@@ -491,28 +495,33 @@ commit by Alice that adds Bob’s key to ,(tt 
[.guix-authorizations]).
 Revocation is similar: any authorized committer can remove entries from
 ,(tt [.guix-authorizations]).  Key rotation can be handled similarly: a
 committer can remove their former key and add their new key in a single
-commit, signed by the former key.])
+commit, signed by the former key.  If a developer’s key is compromised,
+for instance because their laptop was stolen, they can notify other
+committers so they immediately remove the key, thereby preventing it
+from being used to push new commits.])
 
       (p [The authorization invariant satisfies the needs of the Guix
-project.  It has one downside: it prevents pull-request-style workflows.
-Indeed, merging the branch of a contributor not listed in ,(tt
+project.  It has one downside: it does not play well with the
+pull-request-style workflow popularized by some source code hosting
+platforms.  Indeed, merging the branch of a contributor not listed in ,(tt
 [.guix-authorizations]) would break the authorization invariant, unless
 the committer who accepts the changes signs them, which involves
 rewriting the commit history of the branch that was submitted.  It is a
 good tradeoff for Guix where the contribution workflow relies on patches
-sent by email to patch tracker, and where commits are signed by the
+sent by email to a patch tracker, and where commits are signed by the
 committer rather than the original author, but it may be less suitable
 for other workflows.]))
    
-   (chapter :title [Bootstrapping] :ident "bootstrapping"
+   (chapter :title [Establishing Trust] :ident "bootstrapping"
       
       (p [You may have noticed that something is missing from the
-explanation above: what do we do about commit ,(it [A]) in the example
-above?  In other words, which commit do we pick as the first one where
-we can start verifying the authorization invariant?])
+explanation above: what do we do about commit ,(it [A]) in ,(numref
+:text [Figure] :ident "fig-commits")?  In other words, which commit
+do we pick as the first one where we can start verifying the
+authorization invariant?])
 
       (figure
-        :legend [The introductory commit in a graph.]
+        :legend [The introductory commit in a commit graph.]
         :ident "fig-commit-graph-intro"
         (image :file "images/commit-graph-intro.pdf"))
 
@@ -521,20 +530,22 @@ Previously, one would identify a channel simply by its 
URL.  Now, when
 introducing a channel to users, one needs to provide an additional piece
 of information: the first commit where the authorization invariant
 holds, and the fingerprint of the OpenPGP key used to sign that commit
-(it’s not strictly necessary but provides an additional check).])
+(the fingerprint is not strictly necessary from a security perspective
+but it provides an additional check).])
 
       (p [Consider the commit graph on ,(numref :text [Figure] :ident
 "fig-commit-graph-intro").  On this figure, ,(it [B]) is the introduction 
commit.  Its
-ancestors, such as ,(it [A]) are considered authentic.  To authenticate, ,(it 
[C]),
+ancestors, such as ,(it [A]), are considered authentic.  To authenticate, ,(it 
[C]),
 ,(it [D]), ,(it [E]), and ,(it [F]), we check the authorization invariant.])
 
       (p [As always when it comes to establishing trust, distributing
 channel introductions is very sensitive.  The introduction of the
-official ,(tt [guix]) channel is built into Guix.  Users obtain it when they
-install Guix the first time; hopefully they verify the signature on the
-Guix tarball or ISO image, as noted in the installation instructions,
-which reduces chances of getting the “wrong” Guix, but it is still very
-much trust-on-first-use (TOFU).])
+official ,(tt [guix]) channel is built into Guix.  Users obtain it when
+they install Guix the first time.  Installation instructions instruct
+users to verify the provided OpenPGP detached signature on the tarball
+or ISO installation image they download.  This reduces chances of
+getting the “wrong” Guix, following a trust-on-first-use (TOFU)
+approach.])
 
       (figure
         :legend [Specification of a channel along with its ,(emph 
[introduction]).]
@@ -562,29 +573,32 @@ to advertise the channel's introduction.  Users then have 
to provide the
 channel’s introduction in their ,(tt [channels.scm]) file, as shown in
 ,(numref :text [Figure] :ident "fig-channel-spec").])
 
-      (p [The ,(tt [guix describe]) command now prints the introduction if
+      (p [The ,(tt [guix describe]) command prints the introduction if
 there’s one.  That way, one can share their channel configuration,
 including introductions, without having to be an expert.])
 
-      (p [Channel introductions also solve another problem: forks.
-Respecting the authorization invariant “forever” would effectively
-prevent “unauthorized” forks—forks made by someone who’s not in
-,(tt [.guix-authorizations]).  Someone publishing a fork simply needs to emit
-a new introduction for their fork, pointing to a different starting
-commit.])
-
-      (p [Last, channel introductions give a ,(emph [point of reference]): if 
an
-attacker manipulates branch heads on Savannah to have them point to
-unrelated commits (such as commits on an orphan branch that do not share
-any history with the “official” branches), authentication will
-necessarily fail as it stumbles upon the first unauthorized commit made
-by the attacker.  In the figure above, the red branch with commits ,(it [G])
-and ,(it [H]) cannot be authenticated because it starts from ,(it [A]), which 
lacks
-,(tt [.guix-authorizations]) and thus fails the authorization invariant.])
-
-      (p [That’s all for authentication!  I’m glad you read this far.
-At this point you can take a break or continue with the next section on
-how ,(tt [guix pull]) prevents downgrade attacks.]))
+      (p [Channel introductions also solve another problem: ,(it
+[forks]).  Forks are an integral part of free software, which gives
+everyone the right to distribute modified copies of the software; one
+might choose to distribute a fork of Guix or a fork of a channel with
+different features or different packages.  Respecting the authorization
+invariant “forever” would effectively prevent “unauthorized” forks—forks
+made by someone who is not in ,(tt [.guix-authorizations]).  To address
+this, someone publishing a fork advertises a new introduction for their
+fork, pointing to a different starting commit.])
+
+      (p [Last, channel introductions give a ,(emph [point of
+reference]).  Assume an attacker attempts a ,(emph [teleport attack]) by
+modifying branch references on the server hosting the official
+repository ,(ref :bib 'torresarias2016:omitting).  They could change
+branch references so they point to unrelated commits, such as commits on
+an “orphan” branch that do not share any history with the “official”
+branches, but in that case, authentication will fail as it stumbles upon
+the first unauthorized commit made by the attacker.  In ,(numref :text
+[Figure] :ident "fig-commit-graph-intro"), the red branch with commits
+,(it [G]) and ,(it [H]) cannot be authenticated because it starts from
+,(it [A]), which lacks ,(tt [.guix-authorizations]) and thus fails the
+authorization invariant.]))
    
    (chapter :title [Downgrade Attacks] :ident "downgrade"
       
@@ -592,9 +606,9 @@ how ,(tt [guix pull]) prevents downgrade attacks.]))
 ,(emph [downgrade]) or ,(emph [roll-back]) attacks.  The attack consists in 
tricking
 users into installing older, known-vulnerable software packages, which
 in turn may offer new ways to break into their system.  This is not
-strictly related to the authentication issue we’ve been discussing,
-except that it’s another important issue in this area that we took the
-opportunity to address.])
+strictly related to the authentication issue discussed above, but it is
+an important issue that is more easily addressed with this model in
+place.])
 
       (p [Guix saves provenance info for itself: the ,(tt [guix
 describe]) command prints that information, essentially the Git commits
@@ -678,7 +692,7 @@ Rollback detection prevents just that, rollbacks, but there 
is no
 mechanism in place to tell whether a given mirror is stale.  To mitigate
 that, channel authors can specify, in the repository, the channel’s
 ,(emph [primary URL]).  This piece of information lives in the
-`.guix-channel` file, in the repository, so it’s authenticated.  ,(tt
+,(tt [.guix-channel]) file, in the channel’s repository, so it’s 
authenticated.  ,(tt
 [guix pull]) uses it to print a warning when the user pulls from a
 mirror:]
 
@@ -694,9 +708,8 @@ Building from this channel:
 …
 ]))
 
-      (p [So far we talked about mechanics in a rather abstract way.  That 
might
-satisfy the graph theorist or the Git geek in you, but if you are up for
-a quick tour of the implementation, the next section is for you!]))
+      (p [Together with downgrade prevention, it makes it more difficult
+to trick users into getting stale revisions.]))
 
    (chapter :title [Implementation]
       :ident "implementation"
@@ -713,14 +726,13 @@ This choice was not motivated by a belief that OpenPGP is 
the “right
 tool for the job”—on the contrary, its complexity, which is a result its
 broad and extensible specification ,(ref :bib
 'callas2007:rfc4880-openpgp), made it a poor candidate in our eyes.
-More focused options, such as minisign,(footnote (ref :url
-"https://jedisct1.github.io/minisign";)), looked more appealing.
-However, we felt that the fact that OpenPGP commit signing is
-well-supported by Git makes a significant practical difference:
-developers can easily be set up to sign commits with GnuPG and commands
-such as ,(tt [git log]) can verify and display signatures; ways to deal
-with OpenPGP keys and signatures, although complex, are also
-well-documented.])
+More focused options such as minisign ,(ref :bib
+'denis2021:minisign-web) looked more appealing.  However, we felt that
+the fact that OpenPGP commit signing is well-supported by Git makes a
+significant practical difference: developers can easily be set up to
+sign commits with GnuPG and commands such as ,(tt [git log]) can verify
+and display signatures; ways to deal with OpenPGP keys and signatures,
+although complex, are also well-documented.])
         
         (p [Key distribution is an important issue.  We did not want
 the whole mechanism to lazily fetch public keys from key servers:
@@ -779,10 +791,12 @@ pull]).  The implementation must be able to perform 
well.])
 consider than, if a commit has been authenticated, then all the commits
 in its transitive closure are automatically considered authentic and do
 not need to be checked.  This optimization stems from the fact that the
-commit graph is a Merkle DAG.  The implementation takes advantage of it
-in two ways: by not skipping commits that are in the transitive closure
-of the currently-used Guix commit, and by maintaining a per-user cache
-of previously-authenticated commits that can also be skipped.])
+commit graph has integrity properties similar to that of a Merkle-style
+directed acyclic graph ,(ref :bib 'merkle1980:protocols).  The
+implementation takes advantage of it in two ways: by skipping commits
+that are in the transitive closure of the currently-used Guix commit,
+and by maintaining a per-user cache of previously-authenticated commits
+that can also be skipped.])
         
         (p [At the implementation level, two key decisions were made:
 verifying signatures in-process, and dismissing unnecessary OpenPGP
@@ -805,7 +819,7 @@ context; what matters is whether the authorization 
invariant holds.]))
       (section :title [Generalization]
         
         (p [As explained in ,(numref :text [Section] :ident
-"rationale"), the general problem being solved—authenticating Git
+"rationale"), the general problem being solved — authenticating Git
 checkouts—is in no way specific to Guix, and the solution we devised may
 in fact be of interest to ,(emph [any]) Git user.  For this reason, and
 also to facilitate the work of Guix channel developers, we introduced a
@@ -862,7 +876,7 @@ to run such hooks at the time.])
 least for advanced users with rather unusual workflows.  As an example,
 we have had reports of users who would pull to development or
 work-in-process branches, using ,(tt [guix pull --branch=,(it
-[devel])]), where ,(it [devel]) is the name of the branch.  When trying
+[devel])]), where ,(tt [devel]) is the name of the branch.  When trying
 to pull back to the main branch, ,(tt [guix pull]) would report an
 error saying that the target commit is “unrelated” to the source
 commit.  Indeed, because the development branch has not been merged into
@@ -971,16 +985,17 @@ was deployed more than a year ago.  Users updating with 
,(tt [guix
 pull]) may have noticed a new progress bar while commits are being
 authenticated.  Apart from that, the change was transparent and our
 experience so far has been positive.  The authentication mechanism is
-built around the Git commit graph; it’s a mechanism to ,(emph
+built around the Git commit graph; it is a mechanism to ,(emph
 [authenticate Git checkouts]) and in that sense it is not tied to Guix
 and its application domain.  To our knowledge, this is the first
-client-side-only Git update authentication in use.])
+client-side-only Git update authentication mechanism in use.])
       
       (p [Guix records the commits of channels used to deploy a set of
 packages or even a complete operating system.  We took advantage of
 that, together with knowledge of the commit graph of these channels, to
 prevent downgrade attacks—both when running ,(tt [guix pull]) and when
-deploying the operating system.])
+deploying the operating system, which is another distinguishing
+feature.])
 
       (p [The security of the software supply chain as managed by Guix
 relies on: auditability (every piece of software is built from source),
@@ -992,9 +1007,9 @@ software supply chain issues at their core.])
 
       (p [The security of free operating systems of course also depends
 on the security of the upstream software packages being distributed.  We
-hope our Git authentication model and/or tool can find its way as part
-of the development workflows upstream.  This would address one of the
-weakest points in today’s practices.])
+hope our Git authentication model and/or tool can find its way in
+upstream development workflows.  This would address one of the
+weakest points in today’s development practices.])
 
       #;(p [To bootstrap trust, we added the notion of ,(it [channel
 introductions]).  These are now visible in the user interface, in