From 0d63d00e4c62233131ae07d9a4b5fd07ae16560a Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 15 Sep 2020 12:53:58 -0400 Subject: [PATCH 1/6] audit issue #1811 --- shelley/chain-and-ledger/formal-spec/ledger.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shelley/chain-and-ledger/formal-spec/ledger.tex b/shelley/chain-and-ledger/formal-spec/ledger.tex index f374c7332f9..680f6f9da38 100644 --- a/shelley/chain-and-ledger/formal-spec/ledger.tex +++ b/shelley/chain-and-ledger/formal-spec/ledger.tex @@ -143,7 +143,7 @@ \section{Ledger State Transition} \var{pp}\\ \var{acnt} \end{array} - \vdash \var{ls} \trans{ledgers}{\epsilon} \varUpdate{\var{ls'}} + \vdash \var{ls} \trans{ledgers}{\epsilon} \var{ls} } \end{equation} From 49e3bd73d451a677ee1ecb8a592144c7592c66e6 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 15 Sep 2020 12:56:52 -0400 Subject: [PATCH 2/6] audit issue #1820 --- shelley/chain-and-ledger/formal-spec/update.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex index 7508a069576..f91a084c862 100644 --- a/shelley/chain-and-ledger/formal-spec/update.tex +++ b/shelley/chain-and-ledger/formal-spec/update.tex @@ -241,7 +241,7 @@ \subsection{Protocol Parameter Update Proposals} \\ \var{slot} \geq \fun{firstSlot}~((\epoch{slot}) + 1) - 2\cdot\StabilityWindow \\ - \epoch{slot} = e + 1 + (\epoch{slot}) +1 = e } { \begin{array}{c} From e96ef0e0648fa7ad4abba932dcfad531de8faae8 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 15 Sep 2020 13:04:35 -0400 Subject: [PATCH 3/6] audit issue #1808 --- .../executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs index 087e835daa2..6711963cc19 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs @@ -94,7 +94,7 @@ data DelegPredicateFailure era -- This error is now redundant with StakeKeyAlreadyRegisteredDELEG. -- We should remove it and replace its one use with StakeKeyAlreadyRegisteredDELEG. StakeKeyInRewardsDELEG - !(Credential 'Staking era) -- Credential which is already registered + !(Credential 'Staking era) -- DEPRICATED, now redundant with StakeKeyAlreadyRegisteredDELEG | StakeKeyNotRegisteredDELEG !(Credential 'Staking era) -- Credential which is not registered | StakeKeyNonZeroAccountBalanceDELEG @@ -210,10 +210,7 @@ delegationTransition = do TRC (DelegEnv slot ptr acnt, ds, c) <- judgmentContext case c of DCertDeleg (RegKey hk) -> do - -- note that pattern match is used instead of regCred, as in the spec - -- TODO we can remove the failure StakeKeyInRewardsDELEG and replace - -- the use below with StakeKeyAlreadyRegisteredDELEG - eval (hk ∉ dom (_rewards ds)) ?! StakeKeyInRewardsDELEG hk + eval (hk ∉ dom (_rewards ds)) ?! StakeKeyAlreadyRegisteredDELEG hk pure $ ds From d8088999e296e0714045c4e2a4f36addbc558a40 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 15 Sep 2020 15:00:52 -0400 Subject: [PATCH 4/6] audit issue #1776 --- .../src/Shelley/Spec/Ledger/STS/Ocert.hs | 6 ++-- .../chain-and-ledger/formal-spec/chain.tex | 33 +++++++++++++------ 2 files changed, 26 insertions(+), 13 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs index a6d9fd4a41d..c6706791d70 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs @@ -83,8 +83,8 @@ ocertTransition :: ocertTransition = judgmentContext >>= \(TRC (env, cs, BHeader bhb sigma)) -> do let OCert vk_hot n c0@(KESPeriod c0_) tau = bheaderOCert bhb - vkey = bheaderVk bhb - hk = hashKey vkey + vkcold = bheaderVk bhb + hk = hashKey vkcold s = bheaderSlotNo bhb kp@(KESPeriod kp_) <- liftSTS $ kesPeriod s @@ -100,7 +100,7 @@ ocertTransition = -- above `KESBeforeStartOCERT` -- predicate failure in the -- transition. - verifySignedDSIGN vkey (ocertToSignable $ bheaderOCert bhb) tau ?! InvalidSignatureOCERT n c0 + verifySignedDSIGN vkcold (ocertToSignable $ bheaderOCert bhb) tau ?! InvalidSignatureOCERT n c0 verifySignedKES () vk_hot t bhb sigma ?!: InvalidKesSignatureOCERT kp_ c0_ t case currentIssueNo env cs hk of diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index ed43836619c..abc0986cb94 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -158,6 +158,7 @@ \subsection{Block Definitions} \var{prev} & \HashHeader^? & \text{hash of previous block header}\\ \var{vk} & \VKey & \text{block issuer}\\ \var{vrfVk} & \VKey & \text{VRF verification key}\\ + \var{blockno} & \BlockNo & \text{block number}\\ \var{slot} & \Slot & \text{block slot}\\ \eta & \Seed & \text{nonce}\\ \var{prf}_{\eta} & \Proof & \text{nonce proof}\\ @@ -1240,40 +1241,52 @@ \subsection{Verifiable Random Function} \begin{figure} \emph{VRF helper function} + \begin{align*} + & \fun{poolIDfromBHBody} \in \BHBody \to \KeyHash_{pool} \\ + & \fun{poolIDfromBHBody} = \hashKey{} \circ \bvkcold{} \\ + \end{align*} + % + \begin{align*} + & \fun{mkSeed} \in \Seed \to \Slot \to \Seed \to \Seed \\ + & \fun{mkSeed}~\var{ucNonce}~\var{slot}~\eta_0 = + \var{ucNonce}~\mathsf{XOR}~(\slotToSeed{slot}\seedOp\eta_0)\\ + \end{align*} + % \begin{align*} & \fun{vrfChecks} \in \Seed \to \BHBody \to \Bool \\ & \fun{vrfChecks}~\eta_0~\var{bhb} = \\ & \begin{array}{cl} ~~~~ & - \verifyVrf{\Seed}{\var{vrfVk}}{((\eta_0\seedOp ss)\seedOp\Seede)} + \verifyVrf{\Seed}{\var{vrfK}}{(\fun{mkSeed}~\Seede~\var{slot}~\eta_0)} {(\bprfn{bhb},~\bnonce{bhb}}) \\ ~~~~ \land & - \verifyVrf{\unitInterval}{\var{vrfVk}}{((\eta_0\seedOp ss)\seedOp\Seedl)} + \verifyVrf{\unitInterval}{\var{vrfK}}{(\fun{mkSeed}~\Seedl~\var{slot}~\eta_0)} {(\bprfl{bhb},~\bleader{bhb}}) \\ \end{array} \\ & ~~~~\where \\ - & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\ - & ~~~~~~~~~~\var{vrfVk} \leteq \fun{bvkvrf}~\var{bhb} \\ + & ~~~~~~~~~~\var{slot} \leteq \bslot{bhb} \\ + & ~~~~~~~~~~\var{vrfK} \leteq \fun{bvkvrf}~\var{bhb} \\ \end{align*} % \begin{align*} - & \fun{praosVrfChecks} \in \Seed \to \PoolDistr \to \unitInterval \to \BHBody \to \Bool \\ + & \fun{praosVrfChecks} \in \Seed \to \PoolDistr \to \unitIntervalNonNull \to \BHBody \to \Bool \\ & \fun{praosVrfChecks}~\eta_0~\var{pd}~\var{f}~\var{bhb} = \\ & \begin{array}{cl} - ~~~~ & \var{hk}\mapsto (\sigma,~\var{hk_{vrf}})\in\var{pd} \\ + ~~~~ & \var{hk}\mapsto (\sigma,~\var{vrfHK})\in\var{pd} \\ + ~~~~ \land & \var{vrfHK} = \hashKey{vrfK} \\ ~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \\ ~~~~ \land & \fun{checkLeaderVal}~(\fun{bleader}~\var{bhb})~\sigma~\var{f} \\ \end{array} \\ & ~~~~\where \\ - & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\ - & ~~~~~~~~~~\var{hk_{vrf}} \leteq \hashKey{(\fun{bvkvrf}~\var{bhb})} \\ + & ~~~~~~~~~~\var{hk} \leteq \fun{poolIDfromBHBody}~\var{bhb} \\ + & ~~~~~~~~~~\var{vrfK} \leteq \fun{bvkvrf}~\var{bhb} \\ \end{align*} % \begin{align*} & \fun{pbftVrfChecks} \in \KeyHash_{vrf} \to \Seed \to \BHBody \to \Bool \\ - & \fun{pbftVrfChecks}~\var{vrfh}~\eta_0~~\var{bhb} = \\ + & \fun{pbftVrfChecks}~\var{vrfHK}~\eta_0~~\var{bhb} = \\ & \begin{array}{cl} - ~~~~ & \var{vrfh} = \hashKey{(\fun{bvkvrf}~\var{bhb})} \\ + ~~~~ & \var{vrfHK} = \hashKey{(\fun{bvkvrf}~\var{bhb})} \\ ~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \\ \end{array} \\ \end{align*} From 44ef10a36476e11b03333f88d5b2ba3a9bc077b1 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Wed, 16 Sep 2020 08:12:08 -0400 Subject: [PATCH 5/6] Update shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs Co-authored-by: Nicholas Clarke --- .../executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs index 6711963cc19..3c97011650d 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs @@ -94,7 +94,7 @@ data DelegPredicateFailure era -- This error is now redundant with StakeKeyAlreadyRegisteredDELEG. -- We should remove it and replace its one use with StakeKeyAlreadyRegisteredDELEG. StakeKeyInRewardsDELEG - !(Credential 'Staking era) -- DEPRICATED, now redundant with StakeKeyAlreadyRegisteredDELEG + !(Credential 'Staking era) -- DEPRECATED, now redundant with StakeKeyAlreadyRegisteredDELEG | StakeKeyNotRegisteredDELEG !(Credential 'Staking era) -- Credential which is not registered | StakeKeyNonZeroAccountBalanceDELEG From 9865baaa00325233a5b78246dc7aee52a3349477 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Wed, 16 Sep 2020 08:44:21 -0400 Subject: [PATCH 6/6] rename poolIDfromBHBody to issuerIDfromBHBody --- .../executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs | 7 +++++++ .../executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs | 4 ++-- .../executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs | 6 +++--- shelley/chain-and-ledger/formal-spec/chain.tex | 6 +++--- 4 files changed, 15 insertions(+), 8 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs index f5d5c528711..83954f8e9ba 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs @@ -23,6 +23,7 @@ module Shelley.Spec.Ledger.BlockChain lastAppliedHash, BHBody (..), poolIDfromBHBody, + issuerIDfromBHBody, BHeader (BHeader), Block (Block), LaxBlock (..), @@ -489,6 +490,12 @@ instance -- from the body of the block header. poolIDfromBHBody :: Era era => BHBody era -> KeyHash 'BlockIssuer era poolIDfromBHBody = hashKey . bheaderVk +{-# DEPRECATED poolIDfromBHBody "poolIDfromBHBody has been deprecated (the name is misleading), use issuerIDfromBHBody" #-} + +-- | Retrieve the issuer id (the hash of the cold key) from the body of the block header. +-- This corresponds to either a genesis/core node or a stake pool. +issuerIDfromBHBody :: Era era => BHBody era -> KeyHash 'BlockIssuer era +issuerIDfromBHBody = hashKey . bheaderVk -- | Retrieve the new nonce from the block header body. bnonce :: BHBody era -> Nonce diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs index 2330efd9f18..62202ebffdf 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs @@ -44,7 +44,7 @@ import Shelley.Spec.Ledger.BlockChain bbHash, hBbsize, incrBlocks, - poolIDfromBHBody, + issuerIDfromBHBody, ) import Shelley.Spec.Ledger.EpochBoundary (BlocksMade) import Shelley.Spec.Ledger.Keys (DSignable, Hash, coerceKeyRole) @@ -134,7 +134,7 @@ bbodyTransition = -- Note that this may not actually be a stake pool - it could be a genesis key -- delegate. However, this would only entail an overhead of 7 counts, and it's -- easier than differentiating here. - let hkAsStakePool = coerceKeyRole . poolIDfromBHBody $ bhb + let hkAsStakePool = coerceKeyRole . issuerIDfromBHBody $ bhb slot = bheaderSlotNo bhb firstSlotNo <- liftSTS $ do ei <- asks epochInfo diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs index ce74a10993c..bf8c7dd7cd4 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs @@ -48,8 +48,8 @@ import Shelley.Spec.Ledger.BlockChain ( BHBody (..), BHeader (..), checkLeaderValue, + issuerIDfromBHBody, mkSeed, - poolIDfromBHBody, seedEta, seedL, ) @@ -212,7 +212,7 @@ praosVrfChecks eta0 (PoolDistr pd) f bhb = do (throwError $ VRFLeaderValueTooBig (VRF.certifiedOutput $ bheaderL bhb) sigma f) pure () where - hk = coerceKeyRole . poolIDfromBHBody $ bhb + hk = coerceKeyRole . issuerIDfromBHBody $ bhb vrfK = bheaderVrfVk bhb pbftVrfChecks :: @@ -232,7 +232,7 @@ pbftVrfChecks vrfHK eta0 bhb = do vrfChecks eta0 bhb pure () where - hk = poolIDfromBHBody bhb + hk = issuerIDfromBHBody bhb vrfK = bheaderVrfVk bhb overlayTransition :: diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index abc0986cb94..ad4bc9dbbd1 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -1242,8 +1242,8 @@ \subsection{Verifiable Random Function} \begin{figure} \emph{VRF helper function} \begin{align*} - & \fun{poolIDfromBHBody} \in \BHBody \to \KeyHash_{pool} \\ - & \fun{poolIDfromBHBody} = \hashKey{} \circ \bvkcold{} \\ + & \fun{issuerIDfromBHBody} \in \BHBody \to \KeyHash_{pool} \\ + & \fun{issuerIDfromBHBody} = \hashKey{} \circ \bvkcold{} \\ \end{align*} % \begin{align*} @@ -1278,7 +1278,7 @@ \subsection{Verifiable Random Function} ~~~~ \land & \fun{checkLeaderVal}~(\fun{bleader}~\var{bhb})~\sigma~\var{f} \\ \end{array} \\ & ~~~~\where \\ - & ~~~~~~~~~~\var{hk} \leteq \fun{poolIDfromBHBody}~\var{bhb} \\ + & ~~~~~~~~~~\var{hk} \leteq \fun{issuerIDfromBHBody}~\var{bhb} \\ & ~~~~~~~~~~\var{vrfK} \leteq \fun{bvkvrf}~\var{bhb} \\ \end{align*} %