From 6a0c15df2963e7163d010efc46412d997f658432 Mon Sep 17 00:00:00 2001 From: Daira Hopwood Date: Fri, 4 Jun 2021 20:45:53 +0100 Subject: [PATCH] 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 --- protocol/protocol.tex | 160 ++++++++++++++++++++++-------------------- 1 file changed, 82 insertions(+), 78 deletions(-) diff --git a/protocol/protocol.tex b/protocol/protocol.tex index 8b5382da..fa73497a 100644 --- a/protocol/protocol.tex +++ b/protocol/protocol.tex @@ -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