Move the section on abstraction to the Abstract Protocol section, and split section 5.2 to avoid renumbering.

fixes #512

Signed-off-by: Daira Hopwood <daira@jacaranda.org>
This commit is contained in:
Daira Hopwood 2021-06-04 20:45:53 +01:00
parent f4a0a1284e
commit 6a0c15df29
1 changed files with 82 additions and 78 deletions

View File

@ -3651,7 +3651,76 @@ Other \networks using variants of the \Zcash protocol may exist, but are not des
\intropart
\lsection{Abstract Protocol}{abstractprotocol}
\extralabel{cautionlinkage}{\lsection{Abstract Protocol}{abstractprotocol}}
\vspace{-1ex}
\hfill\begin{minipage}{0.8\linewidth}
\small
\begin{poetry}
\item \emph{`We all know that the only mental tool by means of which a very finite piece of reasoning}
\item \emph{\hphantom{`}can cover a myriad cases is called ``abstraction''; as a result the effective exploitation of}
\item \emph{\hphantom{`}[their] powers of abstraction must be regarded as one of the most vital activities of a}
\item \emph{\hphantom{`}competent programmer. In this connection it might be worth-while to point out that the}
\item \emph{\hphantom{`}purpose of abstracting is \textbf{not} to be vague, but to create a new semantic level in which}
\item \emph{\hphantom{`}one can be absolutely precise.'}
\vspace{0.5ex}
\item \hfill--- Edsger Dijkstra, ``The Humble Programmer'' \cite{EWD-340}\!\!
\end{poetry}
\end{minipage}
\vspace{2ex}
Abstraction is an incredibly important idea in the design of any complex system. Without abstraction,
we would not be able to design anything as ambitious as a computer, or a cryptographic protocol.
Were we to attempt it, the computer would be hopelessly unreliable or the protocol would be insecure,
if they could be completed at all.
The aim of abstraction is primarily to limit how much a human working on a piece of a system has to
keep in mind at one time, in order to apprehend the connections of that piece to the remainder.
The work could be to extend or maintain the system, to understand its security or other properties,
or to explain it to others.
In this specification, we make use wherever possible of abstractions that have been developed by
the cryptography community to model cryptographic primitives: \pseudoRandomFunctions, \commitmentSchemes,
\signatureSchemes, etc.
Each abstract primitive has associated syntax (its interface as used by the rest of the system) and
security properties, as documented in this part. Their instantiations are documented in part
\crossref{concreteprotocol}.
In some cases this syntax or these security requirements have been extended to meet the needs of the
\Zcash protocol. For example, some of the PRFs used in \Zcash need to be \collisionResistant, which
is not part of the usual security requirement for a PRF; some \signatureSchemes need to support
additional functionality and security properties; and so on. Also, security requirements are sometimes
intentionally stronger than what is known to be needed, because the stronger property is simpler
or less error-prone to work with, and/or because it has been studied in the cryptographic literature
in more depth.
We explicitly \emph{do not claim}\!, however, that all of these instantiations satisfying their documented
syntax and security requirements would be sufficient for security or correctness of the overall \Zcash protocol,
or that it is always necessary. The claim is only that it helps to understand the protocol; that is, that
analysis or extension is simplified by making use of the abstraction. In other words,
\emph{a good way to understand} the use of that primitive in the protocol is to model it as an instance
of the given abstraction. And furthermore, if the instantiated primitive does not in fact satisfy the
requirements of the abstraction, then this is an error that should be corrected --whether or not it leads
to a vulnerability-- since that would compromise the facility to understand its use in terms of the abstraction.
In this respect the abstractions play a similar rôle to that of a type system (which we also use): they
add a form of redundancy to the specification that helps to express the intent.
Each property is a claim that may be incorrect (or that may be insufficiently precisely stated to
determine whether it is correct). An example of an incorrect security claim occurs in the \Zerocash protocol:
the instantiation of the \noteCommitment scheme used in \Zerocash failed to be \binding at the intended
security level (see \crossref{internalh}).
Another hazard that we should be aware of is that abstractions can be ``leaky'': an instantiation may impose
conditions on its correct or secure use that are not captured by the abstraction's interface and semantics.
Ideally, the abstraction would be changed to explicitly document these conditions, or the protocol changed to
rely only on the original abstraction.
An abstraction can also be incomplete (not quite the same thing as being leaky): it intentionally --usually
for simplicity-- does not model an aspect of behaviour that is important to security or correctness. An example
would be resistance to side-channel attacks; this specification says little about side-channel defence, among
many other implementation concerns.
\lsubsection{Abstract Cryptographic Schemes}{abstractschemes}
@ -7711,79 +7780,7 @@ status (spent or unspent).
\intropart
\lsection{Concrete Protocol}{concreteprotocol}
\vspace{-1ex}
\lsubsection{Caution}{cautionlinkage}
\vspace{-1ex}
\hfill\begin{minipage}{0.8\linewidth}
\small
\begin{poetry}
\item \emph{`We all know that the only mental tool by means of which a very finite piece of reasoning}
\item \emph{\hphantom{`}can cover a myriad cases is called ``abstraction''; as a result the effective exploitation of}
\item \emph{\hphantom{`}[their] powers of abstraction must be regarded as one of the most vital activities of a}
\item \emph{\hphantom{`}competent programmer. In this connection it might be worth-while to point out that the}
\item \emph{\hphantom{`}purpose of abstracting is \textbf{not} to be vague, but to create a new semantic level in which}
\item \emph{\hphantom{`}one can be absolutely precise.'}
\vspace{0.5ex}
\item \hfill--- Edsger Dijkstra, ``The Humble Programmer'' \cite{EWD-340}\!\!
\end{poetry}
\end{minipage}
\vspace{2ex}
Abstraction is an incredibly important idea in the design of any complex system. Without abstraction,
we would not be able to design anything as ambitious as a computer, or a cryptographic protocol.
Were we to attempt it, the computer would be hopelessly unreliable or the protocol would be insecure,
if they could be completed at all.
The aim of abstraction is primarily to limit how much a human working on a piece of a system has to
keep in mind at one time, in order to apprehend the connections of that piece to the remainder.
The work could be to extend or maintain the system, to understand its security or other properties,
or to explain it to others.
In this specification, we make use wherever possible of abstractions that have been developed by
the cryptography community to model cryptographic primitives: \pseudoRandomFunctions, \commitmentSchemes,
\signatureSchemes, etc.
Each abstract primitive has associated syntax (its interface as used by the rest of the system) and
security properties, as documented in part \crossref{abstractprotocol}. Their instantiations are
documented in this \emph{Concrete Protocol} part.
In some cases this syntax or these security requirements have been extended to meet the needs of the
\Zcash protocol. For example, some of the PRFs used in \Zcash need to be \collisionResistant, which
is not part of the usual security requirement for a PRF; some \signatureSchemes need to support
additional functionality and security properties; and so on. Also, security requirements are sometimes
intentionally stronger than what is known to be needed, because the stronger property is simpler
or less error-prone to work with, and/or because it has been studied in the cryptographic literature
in more depth.
We explicitly \emph{do not claim}\!, however, that all of these instantiations satisfying their documented
syntax and security requirements would be sufficient for security or correctness of the overall \Zcash protocol,
or that it is always necessary. The claim is only that it helps to understand the protocol; that is, that
analysis or extension is simplified by making use of the abstraction. In other words,
\emph{a good way to understand} the use of that primitive in the protocol is to model it as an instance
of the given abstraction. And furthermore, if the instantiated primitive does not in fact satisfy the
requirements of the abstraction, then this is an error that should be corrected --whether or not it leads
to a vulnerability-- since that would compromise the facility to understand its use in terms of the abstraction.
In this respect the abstractions play a similar rôle to that of a type system (which we also use): they
add a form of redundancy to the specification that helps to express the intent.
Each property is a claim that may be incorrect (or that may be insufficiently precisely stated to
determine whether it is correct). An example of an incorrect security claim occurs in the \Zerocash protocol:
the instantiation of the \noteCommitment scheme used in \Zerocash failed to be \binding at the intended
security level (see \crossref{internalh}).
Another hazard that we should be aware of is that abstractions can be ``leaky'': an instantiation may impose
conditions on its correct or secure use that are not captured by the abstraction's interface and semantics.
Ideally, the abstraction would be changed to explicitly document these conditions, or the protocol changed to
rely only on the original abstraction.
An abstraction can also be incomplete (not quite the same thing as being leaky): it intentionally --usually
for simplicity-- does not model an aspect of behaviour that is important to security or correctness. An example
would be resistance to side-channel attacks; this specification says little about side-channel defence, among
many other implementation concerns.
\extralabel{boxnotation}{\lsubsection{Integers, Bit Sequences, and Endianness}{endian}}
\lsubsection{Integers, Bit Sequences, and Endianness}{endian}
All integers in \Zcash-specific encodings are unsigned, have a fixed
bit length, and are encoded in little-endian byte order \emph{unless otherwise
@ -7824,9 +7821,13 @@ and integers:
bit first, and concatenate the resulting groups in the same order as the bytes.
\end{itemize}
In bit layout diagrams, each box of the diagram represents a sequence of bits.
Diagrams are read from left-to-right, with lines read from top-to-bottom;
the breaking of boxes across lines has no significance.
\vspace{-1ex}
\extralabel{boxnotation}{\lsubsection{Bit layout diagrams}{bitlayout}}
We sometimes use bit layout diagrams, in which each box of the diagram represents
a sequence of bits. Diagrams are read from left-to-right, with lines read from
top-to-bottom; the breaking of boxes across lines has no significance.
The bit length $\ell$ is given explicitly in each box, except when it is obvious
(e.g. for a single bit, or for the notation $\zeros{\ell}$ representing the sequence
of $\ell$ zero bits, or for the output of $\LEBStoOSP{\ell}$).
@ -13104,7 +13105,7 @@ field of a \blockHeader as follows:
\end{formulae}
\introlist
Recall from \crossref{endian} that bits in the above diagram are
Recall from \crossref{bitlayout} that the bits in the above diagram are
ordered from most to least significant in each byte.
For example, if the first $3$ elements of $i$ are $[69, 42, 2^{21}]$,
then the corresponding bit array is:
@ -14336,6 +14337,9 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
\historyentry{2021.2.3}{}
\begin{itemize}
\item Move the section on abstraction (previously section 5.1) to \crossref{abstractprotocol}.
Section 5.2 has been split into two (\crossref{endian} and \crossref{bitlayout}) to
avoid renumbering later subsections.
\item Correct an error in the encoding of height-in-coinbase for \blocks at heights
$\barerange{1}{16}$.
\item Clarify, in \crossref{blockchain}, requirements on the range of \blockHeights that