diff --git a/papers/README.md b/papers/README.md index b0071ac7b..57dbc9db3 100644 --- a/papers/README.md +++ b/papers/README.md @@ -5,7 +5,6 @@ This directory contains the repository-owned Rings whitepaper copy. - `rings.pdf`: compiled Rings whitepaper. - `rings.tex`: LaTeX source for the Rings whitepaper. - `cites.bib`: bibliography used by `rings.tex`. -- `imgs/rings/path.png`: image asset referenced by `rings.tex`. Build with: diff --git a/papers/cites.bib b/papers/cites.bib index cf83b9b6b..bd0bb086d 100644 --- a/papers/cites.bib +++ b/papers/cites.bib @@ -124,7 +124,7 @@ @misc{Libp2p author = {{Protocol Labs}}, title = {{libp2p}: A Modular Network Stack}, year = {2026}, - note = {\url{https://libp2p.io/}} + note = {\url{https://libp2p.io/}, accessed 2026-07-07} } @inproceedings{TorNetwork, @@ -162,3 +162,140 @@ @misc{webassembly year = {2019}, note = {\url{https://www.w3.org/TR/2019/REC-wasm-core-1-20191205/}} } + +@inproceedings{SFS, + author = {David Mazi{\`e}res and Michael Kaminsky and M. Frans Kaashoek and Emmett Witchel}, + title = {Separating Key Management from File System Security}, + booktitle = {Proceedings of the 17th ACM Symposium on Operating Systems Principles}, + pages = {124--139}, + year = {1999}, + doi = {10.1145/319151.319160} +} + +@misc{DIDCore, + author = {{W3C Decentralized Identifier Working Group}}, + title = {Decentralized Identifiers ({DIDs}) v1.0: Core Architecture, Data Model, and Representations}, + howpublished = {W3C Recommendation}, + year = {2022}, + note = {\url{https://www.w3.org/TR/2022/REC-did-core-20220719/}} +} + +@inproceedings{Pastry, + author = {Antony Rowstron and Peter Druschel}, + title = {Pastry: Scalable, Decentralized Object Location, and Routing for Large-Scale Peer-to-Peer Systems}, + booktitle = {Middleware 2001}, + series = {Lecture Notes in Computer Science}, + volume = {2218}, + pages = {329--350}, + year = {2001}, + doi = {10.1007/3-540-45518-3_18} +} + +@article{Tapestry, + author = {Ben Y. Zhao and Ling Huang and Jeremy Stribling and Sean C. Rhea and Anthony D. Joseph and John Kubiatowicz}, + title = {Tapestry: A Resilient Global-Scale Overlay for Service Deployment}, + journal = {IEEE Journal on Selected Areas in Communications}, + volume = {22}, + number = {1}, + pages = {41--53}, + year = {2004} +} + +@inproceedings{CAN, + author = {Sylvia Ratnasamy and Paul Francis and Mark Handley and Richard Karp and Scott Shenker}, + title = {A Scalable Content-Addressable Network}, + booktitle = {Proceedings of ACM SIGCOMM}, + pages = {161--172}, + year = {2001}, + doi = {10.1145/383059.383072} +} + +@inproceedings{SitMorrisDHTSecurity, + author = {Emil Sit and Robert Morris}, + title = {Security Considerations for Peer-to-Peer Distributed Hash Tables}, + booktitle = {Peer-to-Peer Systems}, + series = {Lecture Notes in Computer Science}, + volume = {2429}, + pages = {261--269}, + year = {2002}, + doi = {10.1007/3-540-45748-8_25} +} + +@inproceedings{SecureRoutingOverlays, + author = {Miguel Castro and Peter Druschel and Ayalvadi Ganesh and Antony Rowstron and Dan S. Wallach}, + title = {Secure Routing for Structured Peer-to-Peer Overlay Networks}, + booktitle = {5th USENIX Symposium on Operating Systems Design and Implementation}, + year = {2002}, + doi = {10.1145/844128.844156} +} + +@inproceedings{SybilDouceur, + author = {John R. Douceur}, + title = {The Sybil Attack}, + booktitle = {Peer-to-Peer Systems}, + series = {Lecture Notes in Computer Science}, + volume = {2429}, + pages = {251--260}, + year = {2002}, + doi = {10.1007/3-540-45748-8_24} +} + +@inproceedings{EclipseOverlay, + author = {Atul Singh and Tsuen-Wan J. Ngan and Peter Druschel and Dan S. Wallach}, + title = {Eclipse Attacks on Overlay Networks: Threats and Defenses}, + booktitle = {25th IEEE International Conference on Computer Communications}, + pages = {1--12}, + year = {2006} +} + +@misc{WebRTCMeasurement, + author = {Kosuke Nakagawa and Manabu Tsukada and Keiichi Shima and Hiroshi Esaki}, + title = {{WebRTC}-based Measurement Tool for Peer-to-Peer Applications and Preliminary Findings with Real Users}, + howpublished = {arXiv:2112.02163}, + year = {2021}, + note = {\url{https://arxiv.org/abs/2112.02163}} +} + +@article{LampsonProtection, + author = {Butler W. Lampson}, + title = {Protection}, + journal = {ACM SIGOPS Operating Systems Review}, + volume = {8}, + number = {1}, + pages = {18--24}, + year = {1974}, + doi = {10.1145/775265.775268} +} + +@article{AbadiAccessControl, + author = {Mart{\'i}n Abadi and Michael Burrows and Butler Lampson and Gordon Plotkin}, + title = {A Calculus for Access Control in Distributed Systems}, + journal = {ACM Transactions on Programming Languages and Systems}, + volume = {15}, + number = {4}, + pages = {706--734}, + year = {1993}, + doi = {10.1145/155183.155225} +} + +@article{MoggiMonads, + author = {Eugenio Moggi}, + title = {Notions of Computation and Monads}, + journal = {Information and Computation}, + volume = {93}, + number = {1}, + pages = {55--92}, + year = {1991}, + doi = {10.1016/0890-5401(91)90052-4} +} + +@inproceedings{PlotkinPretnarEffects, + author = {Gordon Plotkin and Matija Pretnar}, + title = {Handlers of Algebraic Effects}, + booktitle = {Programming Languages and Systems}, + series = {Lecture Notes in Computer Science}, + volume = {5502}, + pages = {80--94}, + year = {2009}, + doi = {10.1007/978-3-642-00590-9_7} +} diff --git a/papers/imgs/rings/path.png b/papers/imgs/rings/path.png deleted file mode 100644 index 42adfbb34..000000000 Binary files a/papers/imgs/rings/path.png and /dev/null differ diff --git a/papers/rings.pdf b/papers/rings.pdf index ebba74dc6..80b44f502 100644 Binary files a/papers/rings.pdf and b/papers/rings.pdf differ diff --git a/papers/rings.tex b/papers/rings.tex index 069bad3b0..a43c7de08 100644 --- a/papers/rings.tex +++ b/papers/rings.tex @@ -11,7 +11,6 @@ \usepackage{epsfig} \usepackage{epstopdf} \usepackage{url} -\usepackage{enumitem} \usepackage{array} \usepackage[utf8]{inputenc} \usepackage[english]{babel} @@ -23,9 +22,16 @@ \newtheorem{constraint}{Constraint} \newtheorem{assumption}{Assumption} \newtheorem{proposition}{Proposition} +\newtheorem{theorem}{Theorem} +\newtheorem{lemma}{Lemma} \newtheorem{invariant}{Invariant} \newtheorem{obligation}{Obligation} +\newcommand{\RingsObj}{\mathsf{Model}_{Rings}} +\newcommand{\SetOverR}{\mathbf{Set}/R} +\newcommand{\NS}{\mathsf{NS}} +\newcommand{\NonClaim}{\mathsf{NonClaim}_{Rings}} + \usetikzlibrary{shapes,arrows,positioning,patterns,through} \tikzset{ @@ -48,8 +54,8 @@ } \author{Ryan~J.~Kung% -\thanks{Ryan J. Kung can be reached at ryankung@ieee.org. Manuscript created February 8, 2023; last updated July 4, 2026.}} -\title{\huge Rings: An Algebraic Structured Peer-to-Peer Network\\ +\thanks{Ryan J. Kung can be reached at ryankung@ieee.org. Manuscript created February 8, 2023; last updated July 8, 2026.}} +\title{Rings: An Algebraic Structured Peer-to-Peer Network\\ for Decentralized Identity and Resource Ownership} \date{} \IEEEaftertitletext{% @@ -58,19 +64,19 @@ \parbox{0.90\textwidth}{% \centering\bfseries Abstract\\[0.5\baselineskip]% \normalfont -Rings is an implemented algebraic structured peer-to-peer network for -decentralized identity, resource ownership, transport, storage, and application -protocols. The project starts from a concrete failure mode in contemporary -Internet systems: application servers, DNS names, relay services, and platform -accounts often become the authority that identities and data must trust. Rings -instead treats identities and resources as algebraic objects over a structured -CorrectChord overlay, with browser and native runtimes connected through -WebRTC/WebAssembly adapters and cryptographic protocols kept on carriers -separate from the routing identifier space. -The core object is -\[ - \mathcal{Rings}= - (R,\mathcal{R}_N,\mathbf{Set}/R,\Omega_N, +This paper presents Rings, an implemented structured peer-to-peer network, and +specifies its authority boundary as a carrier-separated algebra. The motivating +failure mode is authority collapse: +\[ + \mathsf{root}(id,data,route) + \in\{\mathsf{server},\mathsf{dns},\mathsf{relay},\mathsf{platform}\}. +\] +Given an overlay, namespaces, protocol effects, and cryptographic sessions, +the problem is to construct a total owner map while preventing non-placement +carriers from changing ownership: +\[ + \RingsObj= + (R,\mathcal{R}_N,\SetOverR,\Omega_N, \mathsf{T}^{\mathcal{E}}_A,\Pi,\mathbb{G},\mathcal{X}) \] with @@ -78,15 +84,43 @@ \begin{array}{rcl} R&=&\mathbb{Z}/2^{160}\mathbb{Z},\\ \mathcal{R}_N&=&\text{Correct-Chord overlay object},\\ + v_0&\in&\{1,\ldots,256\},\\ + \Theta&\subseteq&N,\qquad + \operatorname{StoreOwner}^{v_0}_{\Theta}:R\to\Theta,\\ \Omega_N(X,H)&=&(X,\operatorname{owner}_N\circ H),\\ \tau_\nu&:&S_\nu\times I_\nu \to\mathsf{T}^{\mathcal{E}_\nu}_{A_\nu}(S_\nu\times O_\nu). \end{array} \] \[ - \{D,V,M,H,Q,W\}\subset\operatorname{Obj}(\mathbf{Set}/R), - \qquad - \mathsf{CryptoCarrier}\cap R=\varnothing. +\begin{array}{rcl} +\mathsf{Claim}_{core} +&=& +\mathsf{WellDef}(\Omega_N) +\land\mathsf{CarrierSep} +\land\mathsf{NonInterfere}\\ +&&{}\land\mathsf{MorphismPreserve} +\land\mathsf{EffectTyped},\\ +\mathsf{Claim}_{ledger} +&=&\mathsf{EvidenceScoped}_{\Gamma}\land\mathsf{LedgerDisc}_{Rings}. +\end{array} +\] +This paper gives a bounded algebraic account of the implemented system and a +ledger for which claims the paper admits: +\[ +\begin{array}{rcl} +\mathsf{Formalized}_{paper} +&=&\mathsf{Core}_{Rings},\\ +\mathsf{Admitted}_{paper} +&\subseteq&\mathsf{Spec}\uplus\mathsf{Artifact}_{R},\\ +\mathsf{Eval}_{reported} +&\subset&\mathsf{ReportedOnly},\\ +\mathsf{OnionImpl}_{R}&=&\mathsf{OnionReg}\cup\mathsf{OnionCircuit},\\ +\mathsf{OnionImpl}_{R}&\subseteq&\mathsf{Artifact}_{R},\\ +\mathsf{OnionImpl}_{R}&\not\Rightarrow&\mathsf{Anon},\\ +\mathsf{OnionImpl}_{R}&\not\Rightarrow&\mathsf{WANPerf},\\ +\mathsf{PerfClaim}_{R}&\in&\mathsf{Obligation}. +\end{array} \] }% \hfill\mbox{}% @@ -98,90 +132,273 @@ \section{Introduction} -Centralized application platforms simplify deployment, but they also concentrate -identity, naming, storage, and traffic control at service operators. Cloud and -platform centralization therefore becomes a privacy, availability, and autonomy -risk for users who need direct communication and durable control over their -data~\cite{Kshetri2013,Zissis2012,KshetriMurugesan2013}. The Rings project is motivated by -this observation: a sovereign network should let a participant own an identity, -establish a session, route to another identity or resource, and run application -protocols without turning a single application server into the root of -authority. - -Rings is implemented as a network, but this paper is organized around the -algebraic structure that makes the implementation coherent. It states the -ideal carrier, ownership, transition, and safety laws that the implementation -realizes and continues to refine. The older intuition was that Decentralized -Identifiers (DIDs) directly form a finite ring suitable for all routing and -cryptographic operations. The refined model is more precise: Chord identifiers -form an additive circular carrier for placement, interval order, replica -selection, and finger targets; threshold schemes, signatures, encryption, and -zero-knowledge protocols use their own fields or groups. - -The resulting design has three practical consequences. First, DIDs and virtual -DIDs (VIDs) share the same 160-bit placement surface, so identities, mailboxes, -service descriptors, chunks, subrings, and application rendezvous points can be -routed by one owner function. Second, Rings builds on Chord and CorrectChord -rather than replacing the overlay literature: successor lists, predecessor -relations, join, rectify, and stabilize are the maintenance substrate on which -Rings semantics are layered~\cite{Chord,ZaveChordCorrect}. Third, state -transitions return typed effects instead of directly performing network IO, -which allows the overlay to be reasoned about as a pure state machine and then -interpreted by browser or native runtimes. +Centralized platforms are efficient deployment mechanisms but poor authority +carriers: identity, naming, storage, and traffic control collapse to service +operators~\cite{Kshetri2013,Zissis2012,KshetriMurugesan2013}. This paper +studies Rings through the following algebraic question: +\[ +\begin{array}{rcl} +\mathsf{Own}(d)&=&k_d,\\ +\mathsf{Place}_\nu(x)&=&\operatorname{owner}_N(H_\nu(x)),\\ +\mathsf{Run}(\mathcal{P}_\nu)&=& + \tau_\nu:S_\nu\times I_\nu\to + \mathsf{T}^{\mathcal{E}_\nu}_{A_\nu}(S_\nu\times O_\nu),\\ +\mathsf{RootOfAuthority}&\neq&\mathsf{ApplicationServer},\\ +\mathsf{CryptoCarrier}\cap R&=&\varnothing . +\end{array} +\] + +Chord and CorrectChord supply the routing substrate; DID-style proofs supply +self-certifying identity; WebRTC and WebAssembly supply runtime interpretation; +CRDTs supply one merge algebra. None alone gives a typed law for owner, +carrier, and evidence scope: +\[ +\begin{array}{rl} +\mathsf{Chord}/\mathsf{CorrectChord} + &\Rightarrow + \mathsf{ringLookup}\not\Rightarrow\mathsf{resourceAuthority},\\ +\mathsf{DID} + &\Rightarrow + \mathsf{keyBoundName}\not\Rightarrow\mathsf{overlayOwner},\\ +\mathsf{WebRTC} + &\Rightarrow + \mathsf{browserTransport}\not\Rightarrow\mathsf{protocolLaw},\\ +\mathsf{CRDT} + &\Rightarrow + \mathsf{mergeLaw}\not\Rightarrow\mathsf{placementLaw}. +\end{array} +\] +The contribution is a composition theorem plus a ledger discipline. The Chord +identifier space is the additive cyclic group for placement and interval order; +signatures, threshold schemes, encryption, and zero-knowledge protocols remain +in their own fields or groups: +\[ +\begin{array}{rcl} +R&=&\mathbb{Z}/2^{160}\mathbb{Z},\\ +\mathsf{CC}&\in&\{\mathbb{F}_q,\mathbb{G},\mathbb{Z}_q\},\\ +R\cap\mathsf{CC}&=&\varnothing. +\end{array} +\] +\[ +\begin{array}{rcl} +C_1&=&\Omega_N:\SetOverR\to\mathbf{Set}/N,\\ +C_2&=&\mathsf{CarrierSep}\Rightarrow\mathsf{NonInterfere},\\ +C_3&=&\mathsf{Admit}_{R}(c,k)\Rightarrow\mathsf{Support}_{R}(c,k),\\ +C_4&=&\mathsf{ReportedOnly}\not\Rightarrow\mathsf{PerfClaim}_{R}. +\end{array} +\] +These four claims define the paper's scientific unit. \section{Problem Statement and Design Goals} -Rings addresses a narrow but recurring gap between existing decentralized -systems. Kademlia-derived systems provide scalable lookup, but the XOR metric -does not by itself give Rings the circular ownership law needed for successor -lists, replicated ownership, and interval-based placement. Relay networks and -mixnets improve metadata resistance, but they are not structured P2P ownership -systems. Blockchains provide global ordering, but embedding consensus in every -message or storage operation would turn Rings into a ledger rather than an -algebraic structured peer-to-peer substrate. - -The problem is therefore to specify a network object -\[ - \mathcal{Rings} -\] -that simultaneously supports: -\begin{enumerate}[leftmargin=*,noitemsep,topsep=0pt] -\item self-certifying identity and delegated sessions; -\item structured lookup and resource ownership; -\item browser-native and native transport surfaces; -\item application protocols with typed side effects; -\item cryptographic protocols over correct carriers; -\item bounded algebraic and operational obligations for routing and state repair. -\end{enumerate} - -This paper makes the following contributions. It presents Rings as an -algebraic structured peer-to-peer network, not merely as an overlay lookup -routine. It models the Rings identifier space as the additive cyclic group -\(R=\mathbb{Z}/2^{160}\mathbb{Z}\), not as a general finite field. It lifts -resource placement into \(\mathbf{Set}/R\), so each protocol object carries an -explicit map into the overlay. It uses CorrectChord as the maintenance law -before introducing Rings-specific replication, storage, mailbox, relay, and -ranking semantics. It gives a writer effect monad for DHT transitions and a -TLA-style state relation for model checking and trace replay. These algebraic -and operational artifacts are the core of the paper; the surrounding text -explains why those artifacts exist and how they relate to prior systems. +Existing decentralized systems solve orthogonal subproblems. The missing +object is the commuting authority layer between identity, placement, execution, +and evidence: +\[ +\begin{array}{rl} +\mathcal{N}_R=&\{(X_\nu,H_\nu)\}_\nu,\\ +\mathcal{P}_R=&\{\mathcal{P}_\nu\}_\nu,\\ +\mathsf{Input}=&(\Pi,\mathcal{R}_N,\mathcal{N}_R, + \mathcal{P}_R,\mathcal{X}),\\ +\mathsf{Need}=& + \left\{\begin{array}{l} + \mathsf{Owner}:X_\nu\to N,\\ + \mathsf{Run}:\mathcal{P}_\nu\to\mathsf{Effects}, + \end{array}\right.\\ +\mathsf{Forbidden}=& + \left\{\begin{array}{l} + \mathsf{CryptoCarrier}=R,\\ + \mathsf{Evidence}_{\Gamma}=\mathsf{UniversalClaim}. + \end{array}\right. +\end{array} +\] + +\begin{obligation}[Design target] +\[ +\begin{array}{rcl} +G_{id}&=&\mathsf{SelfCertID}\land\mathsf{DelegatedSession},\\ +G_{own}&=&\mathsf{StructuredOwner},\\ +G_{io}&=&\mathsf{BrowserNativeTransport},\\ +G_{eff}&=&\mathsf{TypedProtocolEffect},\\ +G_{cr}&=&\mathsf{CarrierCorrectCrypto},\\ +G_{rep}&=&\mathsf{BoundedRepairEvidence},\\ +G_{bd}&=&\mathsf{ExplicitClaimBoundary},\\ +G_*&=& +G_{id}\land G_{own}\land G_{io}\land G_{eff}\\ +&&{}\land G_{cr}\land G_{rep}\land G_{bd}. +\end{array} +\] +\end{obligation} + +\begin{definition}[Methodology and claim ledger] +\[ +\begin{array}{rcl} +\mathsf{Method} +&=& +\mathsf{Mot} +\to\mathsf{Spec} +\to\mathsf{Algebra} +\to\mathsf{ImplMap}\\ +&&{}\to\mathsf{Evidence}_{\Gamma} +\to\mathsf{Obligation},\\[3pt] +\Gamma&=&(|N|,\mathsf{topology},\mathsf{scheduler},\mathsf{fault}),\\[3pt] +\mathsf{ClaimKind} +&=& +\mathsf{Spec}\cup\mathsf{Impl} +\cup\mathsf{Evidence}_{\Gamma}\cup\mathsf{Obligation},\\ +\mathsf{Ev}_{\Gamma}&=&\mathsf{Evidence}_{\Gamma},\\ +\mathsf{Anchor}&=&\mathsf{Label}\cup\mathsf{Path}\cup\mathsf{ArtifactId},\\ +\mathsf{Scope}&=&\mathsf{Finite}\cup\mathsf{AllModel}\cup\mathsf{Open},\\ +\mathsf{Ledger}_{R} +&\subseteq& +\mathsf{Prop}_{R}\times\mathsf{ClaimKind}\times\mathsf{Anchor}\times\mathsf{Scope},\\ +\mathsf{row}_{R}(c,k,a,\sigma) +&\Leftrightarrow& +(c,k,a,\sigma)\in\mathsf{Ledger}_{R},\\ +\mathsf{Prop}_{R}&=&\{c:\exists k,a,\sigma.\mathsf{row}_{R}(c,k,a,\sigma)\},\\ +\mathsf{Support}_{R} +&:&\mathsf{Prop}_{R}\times\mathsf{ClaimKind}\to\{\top,\bot\},\\ +\mathsf{Support}_{R}(c,k) +&\Leftrightarrow& +\exists a,\sigma.\mathsf{row}_{R}(c,k,a,\sigma),\\ +\mathsf{Admit}(c) +&\Leftrightarrow& +\exists k\in\mathsf{ClaimKind}.\ \mathsf{Admit}_{R}(c,k). +\end{array} +\] +\end{definition} + +\begin{definition}[Global symbols and non-claims] +\[ +\begin{array}{rcl} +\NS&=&\{D,V,M,H,U,Q,W\},\qquad VID=V,\\ +\mathsf{Time}&=&\mathbb{T},\quad +\mathsf{Ctx}=B^*,\quad \mathsf{Cap}\subseteq A^*,\\ +\mathsf{Domain}&=&\mathsf{WitnessDomain},\quad +\mathsf{Order}=\{<,=,>,\bot\},\\ +\mathsf{Prov}&=&(\mathsf{src},\mathsf{rev},\mathsf{cmd}, + \mathsf{seed},\mathsf{host}),\\ +\mathsf{Limit}&=&\NonClaim\cup\mathsf{Obligation}. +\end{array} +\] +\[ +\begin{aligned} +\NonClaim +&=\{\mathsf{Novel}(\mathsf{DHT}), +\mathsf{Novel}(\mathsf{DID})\}\\ +&\quad{}\cup +\{\mathsf{Novel}(\mathsf{WebRTC})\}\\ +&\quad{}\cup +\{\mathsf{Novel}(\mathsf{CRDT}), +\mathsf{Novel}(\mathsf{Crypto})\}\\ +&\quad{}\cup +\{\mathsf{ByzLive},\mathsf{Consensus},\mathsf{WANPerf}\}\\ +&\quad{}\cup +\{\mathsf{Anon},\mathsf{Unlinkability},\mathsf{OnionPerf}\}\\ +&\quad{}\cup +\{\mathsf{FullVNodeRouting},\mathsf{VNodePerf}\}. +\end{aligned} +\] +\end{definition} + +\begin{table}[htbp] +\centering +\scriptsize +\setlength{\tabcolsep}{2.5pt} +\begin{tabular}{p{1.7cm}|p{1.55cm}|p{3.6cm}} +\hline +Claim family & Ledger class & Anchor and scope \\ \hline +\(\Omega_N,\mathsf{PMor}\) & \(\mathsf{Spec}\) & Definitions and Theorem~\ref{thm:carrier-separated-ownership} \\ +Chord state & \(\mathsf{Spec}\cup\mathsf{Ev}_{\Gamma}\) & Algorithms~\ref{alg:join}--\ref{alg:stabilize}; finite checks \\ +DID/session & \(\mathsf{Impl}\) & signed session and context predicates \\ +Storage VNs & \(\mathsf{Impl}\cup\mathsf{Ev}_{\Gamma}\) & affine keys, virtual owners, storage tests \\ +E2E frames & \(\mathsf{Impl}\cup\mathsf{Ev}_{\Gamma}\) & signed frame and receiver policy \\ +Onion circuits & \(\mathsf{Impl}\cup\mathsf{Ev}_{\Gamma}\) & exit registry, route builder, layered AEAD tests \\ +Chunking & \(\mathsf{Impl}\cup\mathsf{Ev}_{\Gamma}\) & Algorithm~\ref{alg:e2e_chunking}; bounded reassembly \\ +Deferred APIs & \(\mathsf{Spec}\cup\mathsf{Obligation}\) & mailbox, hidden descriptor, secret sharing \\ +Wit/rank/sec. & \(\mathsf{Spec}\cup\mathsf{Obligation}\) & policy predicates, no global security theorem \\ +Benchmark rows & \(\notin\mathsf{ClaimKind}\) & baseline/runtime coordinates, not admitted eval \\ +\hline +\end{tabular} +\caption{Claim-ledger instantiation. Rows inside \(\mathsf{ClaimKind}\) may be +admitted only through an explicit ledger row \((c,k,a,\sigma)\); +\(\mathsf{ReportedOnly}\) rows are coordinates, not claim evidence.} +\label{claim-ledger-table} +\end{table} + +\[ +\begin{array}{rcl} +\ell_{own}&=&(\mathsf{OwnerLaw},\mathsf{Spec}, + \mathrm{Thm}\,\ref{thm:carrier-separated-ownership},\mathsf{AllModel}),\\ +\ell_{mor}&=&(\mathsf{MorphLaw},\mathsf{Spec}, + \mathrm{Thm}\,\ref{thm:carrier-separated-ownership},\mathsf{AllModel}),\\ +\ell_{eff}&=&(\mathsf{EffectLaw},\mathsf{Spec}, + \mathrm{Lem}\,\ref{lem:effect-confinement},\mathsf{AllModel}),\\ +\ell_{car}&=&(\mathsf{CarrierLaw},\mathsf{Spec}, + \mathrm{Lem}\,\ref{lem:carrier-noninterference},\mathsf{AllModel}),\\ +\mathsf{Ledger}_{core}&=&\{\ell_{own},\ell_{mor},\ell_{eff},\ell_{car}\},\\ +\mathsf{Ledger}_{R}&\supseteq&\mathsf{Ledger}_{core}. +\end{array} +\] + +\begin{definition}[Contribution boundary] +\[ +\begin{aligned} +\mathsf{Reuse}_{Rings} +&=\{\mathsf{Chord},\mathsf{CorrectChord},\mathsf{DID}, + \mathsf{WebRTC},\\ +&\quad{}\mathsf{CRDT},\mathsf{OnionRouting}\},\\ +\mathsf{New}_{Rings} +&=(\Omega_N,\mathsf{PMor},\mathsf{CarrierSep}, + \mathsf{LedgerDisc}_{Rings}). +\end{aligned} +\] +\[ +\begin{aligned} +\mathsf{Contribution}_{paper} +&=(\mathsf{Reuse}_{Rings},\mathsf{New}_{Rings}),\\ +\mathsf{TheoremTarget}_{paper} +&=\mathsf{Core}_{Rings},\\ +\mathsf{LedgerTarget}_{paper} +&=\mathsf{LedgerDisc}_{Rings}. +\end{aligned} +\] +The formal theorem is Theorem~\ref{thm:carrier-separated-ownership}; +\(\mathsf{LedgerDisc}_{Rings}\) is an admission discipline, not a semantic +entailment from \(\mathsf{Reuse}_{Rings}\) and not a performance theorem. +\end{definition} \section{Algebraic System Model} -\begin{assumption}[System scope] +\begin{assumption}[System and adversary scope] \[ \begin{array}{rcl} -\mathsf{fault}&=&\mathsf{fail\mbox{-}stop},\\ -\mathsf{auth}(m,\sigma,k)&=&V(k,\sigma,m),\\ -\mathsf{net}&=&\mathsf{async},\\ -\mathsf{io}&=&I_X:A_X^*\to\mathsf{IO},\\ +\kappa&\in&\mathbb{N},\\ +\mathsf{fault}_{overlay}&=&\mathsf{fail\mbox{-}stop},\\ +\mathsf{Adv}_{net}&=& + \left\{\begin{array}{l} + \mathsf{delay},\mathsf{drop},\mathsf{dup},\\ + \mathsf{reorder},\mathsf{replay} + \end{array}\right\},\\ +\mathsf{Adv}_{id}&=& + \left\{\begin{array}{l} + \mathsf{manyDID},\mathsf{stolenSession},\\ + \mathsf{staleProof} + \end{array}\right\},\\ +\Pr[\mathsf{Forge}_{\Pi}(A,\kappa)]&\leq&\epsilon_{\Pi}(\kappa),\\ +\Pr[\mathsf{Preimage}_{H}(A,\kappa)]&\leq&\epsilon_{H}(\kappa),\\ +\epsilon_{\Pi},\epsilon_H&\in&\mathsf{negl},\\ \mathsf{consensus}&\notin&\mathsf{Overlay},\\ \mathsf{order}&=&\mathsf{SidecarWitness},\\ \mathsf{crypto\_ops}&\cap&\mathsf{route\_ops}=\varnothing. \end{array} \] -The fail-stop clause scopes overlay maintenance; identity, ranking, and -application protocols still carry adversarial predicates at their own layer. +Thus CorrectChord is the safety root only for crash-scoped overlay maintenance. +Cryptographic claims are computational assumptions; compromised keys and +Byzantine routing are adversarial cases. Eclipse resistance, Sybil resistance, +anonymity, and denial-of-service resistance must be discharged by admission, +session typing, ranking, relay, quota, and measurement predicates at their own +layers. \end{assumption} \begin{definition}[Identifier carrier] @@ -191,7 +408,8 @@ \section{Algebraic System Model} R&=&\mathbb{Z}/M\mathbb{Z},\\ \delta_a(x)&=&(x-a)\bmod M,\\ (a,b]_R&=&\{x\in R:0<\delta_a(x)\leq\delta_a(b)\},\\ -\mathsf{RouteOps}_R&=&\{0,+,-,\delta_a,(\_,\_]_R\},\\ +(a,b)_R&=&\{x\in R:0<\delta_a(x)<\delta_a(b)\},\\ +\mathsf{RouteOps}_R&=&\{0,+,-,\delta_a,(\_,\_]_R,(\_,\_)_R\},\\ \mathsf{Mult}_R&\notin&\mathsf{RouteOps}_R. \end{array} \] @@ -200,61 +418,114 @@ \section{Algebraic System Model} \begin{definition}[Live topology] \[ \begin{array}{rcl} - N&\subset&R,\quad N\neq\varnothing,\\[2pt] + N&\subset&R,\quad 1\le |N|<\infty,\\[2pt] \operatorname{owner}_N(k) - &=&\arg\min_{u\in N}\delta_k(u),\\[6pt] + &=&\arg\min_{u\in N}\delta_k(u),\\[4pt] + \operatorname{cw}_N(n) + &=&\operatorname{sort}_{\delta_n}(N\setminus\{n\})\cdot\langle n\rangle,\\[4pt] + \operatorname{succ}_N(n) + &=&\operatorname{head}(\operatorname{cw}_N(n)),\\[4pt] \operatorname{pred}_N(n) - &=&\arg\min_{p\in N\setminus\{n\}}\delta_p(n),\\[6pt] - \operatorname{Succ}^q_N(n) &=& - \operatorname{take}_q - \bigl(\operatorname{sort}_{\delta_n}(N\setminus\{n\})\bigr),\\[6pt] - \delta_a|_N&=&\mathsf{injective}. + \begin{cases} + \bot,& |N|=1,\\ + \arg\min_{p\in N\setminus\{n\}}\delta_p(n),& |N|>1, + \end{cases}\\[8pt] + \operatorname{Succ}^q_N(n) + &=&\operatorname{take}_{\min(q,|N|)}(\operatorname{cw}_N(n)). \end{array} \] +The list \(\operatorname{cw}_N(n)\) contains strictly clockwise live nodes and +uses \(n\) only as the wrap-around sentinel. Hence a singleton ring has +\(\operatorname{Succ}^q_N(n)=\langle n\rangle\) and +\(\operatorname{pred}_N(n)=\bot\). \end{definition} \begin{assumption}[Correct-Chord stable base] \[ \begin{array}{rcl} -r&=&|\operatorname{Succ}^r_N(n)|,\\ -\mathsf{Steady}(N)&\Rightarrow&|N|\geq r+1,\\ -|N|0},\\ +\mathsf{Steady}(N,r)&\Rightarrow&|N|\geq r+1,\\ +\mathsf{Init}(N,r)&\Leftrightarrow&1\le |N|\le r,\\ +|\operatorname{Succ}^r_N(n)|&=&\min(r,|N|),\\ \mathsf{Maintain}&=& \{\mathsf{join},\mathsf{rectify}\}\\ &&\cup\{\mathsf{stabilize}\}_{CorrectChord}. \end{array} \] -This is the CorrectChord stable base of Zave~\cite{ZaveChordCorrect}. +CorrectChord claims in this paper are stable-ring claims under +\(\mathsf{Steady}(N,r)\); singleton and small-ring behavior is an explicit +initialization edge case, not evidence for \(r\) distinct live successors. \end{assumption} -\begin{definition}[Affine replica set] +\begin{definition}[Affine replica set and storage VNODE ownership] +Write \(S^v_{\Theta}=\operatorname{StoreOwner}^{v}_{\Theta}\) and +\(Q^{\rho,v}_{\Theta}=\operatorname{RepOwner}^{\rho,v}_{\Theta}\), where +\(\Theta\subseteq N\) is the storage-owner view used for one owner decision. \[ \begin{array}{rcl} -\rho&\in&\mathbb{N}_{>0},\\ -\operatorname{rot}^{\rho}_i(k) - &=&k+\left\lfloor M\cdot i/\rho\right\rfloor,\\[4pt] -\operatorname{Rep}^{\rho}_N(k) +1\le\rho&\le&M,\\ +v_0&\in&\{1,\ldots,256\},\\ +\Theta_n(t)&=&\{n\}\cup\operatorname{Succ}_n(t)\\ +&&{}\cup\operatorname{Pred}_n(t)\cup\operatorname{Finger}_n(t),\\ +\operatorname{repkey}^{\rho}_i(k) + &=&(k+\left\lfloor M\cdot i/\rho\right\rfloor)\bmod M,\quad 0\le i<\rho,\\[4pt] +\operatorname{RepKey}^{\rho}(k) + &=& + \langle \operatorname{repkey}^{\rho}_i(k):0\leq i<\rho\rangle,\\[4pt] +z^v_{n,i}&=&H(\mathtt{rings{:}vnode},net,n,i),\\ +\operatorname{vnode}^{v}_{net}(n,i) +&=&z^v_{n,i},\\ +V^v_{\Theta}&=& +\{(n,z^v_{n,i}):n\in\Theta,0\le i0),\\ +r_i&=&\operatorname{repkey}^{\rho}_i(k),\\ +q_i &=& - \{\operatorname{owner}_N(\operatorname{rot}^{\rho}_i(k)): - 0\leq i<\rho\}. + S^{v}_{\Theta}(r_i),\\ +Q^{\rho,v}_{\Theta}(k) + &=& + \langle q_i:0\leq i<\rho\rangle. +\end{array} +\] +\[ +\begin{array}{rcl} +P_k&=&\operatorname{set}(\operatorname{RepKey}^{\rho}(k)),\\ +O^\Theta_k&=&\operatorname{set}(Q^{\rho,v_0}_{\Theta}(k)),\\ +|P_k|&=&\rho,\\ +1\le |O^\Theta_k|&\leq&\min(\rho,|\Theta|),\\ +\mathsf{collapse}_{\Theta,\rho,v_0}(k) +&\Leftrightarrow&|O^\Theta_k|<\min(\rho,|\Theta|). \end{array} \] -Storage redundancy uses affine rotations of the entry key. Successor lists -remain the CorrectChord safety root for topology maintenance, not the storage -replica set. +Replica keys specify intended placement cardinality; storage VNODE ownership +maps each placement key to a physical owner through derived virtual positions. +The paper's default storage mode has \(v_0>0\); \(v=0\) is the legacy off-switch. +The implementation instantiates \(\Theta\) as \(\Theta_n(t)\), an authenticated +local topology view; \(\Theta=N\) is an offline global-coordinate model. +Virtual positions are not signing identities and do not own transport sessions. +CorrectChord successor lists remain the topology safety root. \end{definition} -\begin{definition}[Rings overlay object] +\begin{definition}[Rings overlay model] \[ - \mathcal{R}_N= - (R,N,\operatorname{owner}_N,\operatorname{pred}_N, - \operatorname{Succ}^r_N,\operatorname{Rep}^{\rho}_N,F,E), +\begin{array}{rcl} + \mathcal{R}_N&=& + (R,N,\operatorname{owner}_N,\operatorname{pred}_N,\\ + &&\operatorname{Succ}^r_N,\operatorname{StoreOwner}^{v_0}_{\Theta},\\ + &&\operatorname{RepOwner}^{\rho,v_0}_{\Theta},F,E). +\end{array} \] \[ \begin{array}{rcl} F&\subseteq&N\times\mathbb{N}\times N,\\ -E&=&\prod_{v\in VID}E_v,\\ +E&=&\prod_{\nu\in\NS}E_\nu,\\ \mathsf{SafetyRoot}(\mathcal{R}_N)&=& (\operatorname{pred}_N,\operatorname{Succ}^r_N),\\ \mathsf{PerfWitness}(\mathcal{R}_N)&=&F. @@ -283,39 +554,69 @@ \section{Algebraic System Model} \end{proof} \begin{constraint}[Carrier separation] +\label{constraint:carrier-separation} +Write \(P_o=\mathsf{PlacementOps}\), \(C_o=\mathsf{CryptoOps}\), and +\(R_o=\mathsf{RunOps}\). \[ \begin{array}{rcl} \mathsf{PlacementOps}&=& - \{0,+,-,\delta_a,(a,b]_R\}\\ -&&\cup\{\operatorname{owner}_N,\operatorname{Rep}^r_N\},\\ + \{0,+,-,\delta_a,(a,b]_R,(a,b)_R\}\\ +&&\cup\{\operatorname{owner}_N\}\\ +&&\cup\{\operatorname{RepKey}^{\rho}\}\\ +&&\cup\{\mathsf{vnode},\mathsf{StoreOwner},\mathsf{RepOwner}\},\\ \mathsf{CryptoOps}&=& \{\times,^{-1},\cdot_{scalar},\mathsf{interp}\}\\ &&\cup\{\mathsf{pair},\mathsf{subgroup}\},\\ -\mathsf{PlacementOps}&\cap&\mathsf{CryptoOps}=\varnothing,\\ -\mathsf{CryptoCarrier}&\in&\{\mathbb{F}_q,\mathbb{G},\mathbb{Z}_q\}. +\mathsf{TransportOps}&=& + \{\mathsf{offer},\mathsf{answer},\mathsf{send},\mathsf{recv}\},\\ +\mathsf{EffectOps}&=& + \{\mathsf{emit},\mathsf{defer},\mathsf{store}\}\\ +&&\cup\{\mathsf{load},\mathsf{schedule}\},\\ +\mathsf{RunOps}&=&\mathsf{TransportOps}\cup\mathsf{EffectOps},\\ +\mathsf{Ops}&=& +\mathsf{PlacementOps}\uplus\mathsf{CryptoOps}\\ +&&{}\uplus\mathsf{RunOps},\\ +P_o\cap C_o&=&\varnothing,\\ +P_o\cap R_o&=&\varnothing,\\ +\mathsf{CryptoCarrier}&\in&\{\mathbb{F}_q,\mathbb{G},\mathbb{Z}_q\},\\ +\pi_R&:&\mathsf{Ops}\to\operatorname{End}(R),\\ +a\in P_o +&\Rightarrow& +\pi_R(a)\in\operatorname{End}(R),\\ +a\in C_o\cup R_o +&\Rightarrow& +\left\{\begin{array}{l} +\pi_R(a)=\operatorname{id}_R,\\ +a\notin P_o. +\end{array}\right. \end{array} \] \end{constraint} +Thus a concrete operation can affect placement only through a member of +\(\mathsf{PlacementOps}\). Transport, effect, and cryptographic operations may +alter runtime state, payloads, or cryptographic carriers, but their induced +endomorphism on \(R\) is the identity. \begin{table}[htbp] \centering -\small -\begin{tabular}{p{2.0cm}|p{4.8cm}} +\footnotesize +\begin{tabular}{p{1.65cm}|p{5.15cm}} \hline Object & Carrier or law \\ \hline Chord IDs & additive cyclic group $R$ \\ DID proof & signature verifier and transcript law \\ VID placement & $H_\nu:X_\nu\to R$ then owner map \\ Storage merge & join semilattice or explicit finalizer \\ -E2E encryption & finite field or curve group \\ +E2E encryption & group operation plus byte-to-point adapter \\ Sequencing & partial order over witness domains \\ Effects & writer monad over action lists \\ \hline \end{tabular} -\normalsize \caption{Carrier boundaries in the Rings model} \label{carrier-table} \end{table} +Table~\ref{carrier-table} is the carrier-level summary used by the separation +constraint; it is not an additional security or performance claim. \section{Architecture As Interfaces} @@ -329,52 +630,53 @@ \section{Architecture As Interfaces} T & (C,A_T,\mathsf{offer},\mathsf{answer},\mathsf{send},\mathsf{recv})\\ O & \mathcal{R}_N\\ X & (S_X,A_X,\mathsf{cap},I_X)\\ -P & \{\mathcal{P}_\nu\}_{\nu\in Namespace}\\ +P & \{\mathcal{P}_\nu\}_{\nu\in\NS}\\ L & \mathsf{App}\circ P \end{array} \] \end{definition} -\begin{figure}[htbp] -\centering -\begin{tikzpicture}[every node/.style={draw,minimum width=5.1cm,minimum height=.55cm,align=center,font=\bfseries}] -\node (1) at (4.5,0) {Identity Layer}; -\node (2) at (4.5,0.7) {Transport Layer}; -\node (3) at (4.5,1.4) {Overlay Layer}; -\node (4) at (4.5,2.1) {Extension Runtime Layer}; -\node (5) at (4.5,2.8) {Protocol Layer}; -\node (6) at (4.5,3.5) {Application Layer}; -\end{tikzpicture} -\caption{Layers of Rings Network} -\label{layers} -\end{figure} +The interface tuple \(\mathcal{A}\) separates identity, transport, overlay, +extension runtime, protocol, and application layers. Only the overlay owns +\(\mathcal{R}_N\); the other layers discharge typed obligations through +\(I,T,X,P\). \begin{definition}[Identity proof] \[ - \Pi=(K,\Sigma,V,D,\mathsf{enc},\mathsf{ttl}) + \Pi=(K,\Sigma,V,\operatorname{did},\mathsf{enc},\mathsf{ttl}) \] \[ \begin{array}{rcl} V&:&K\times\Sigma\times B^*\to\{\top,\bot\},\\ -D&:&K\to R,\\ +\operatorname{did}&:&K\to X_D,\\ \mathsf{enc}&:&\Sigma\to B^*,\\ -\mathsf{ttl}&:&\Sigma\to Time. +\mathsf{ttl}&:&\Sigma\to \mathsf{Time}. \end{array} \] \end{definition} -\begin{invariant}[Session authority] +\begin{invariant}[Typed session authority] \[ - d\in X_D,\qquad s\in K. + sid=(d,s,e,ctx,cap),\qquad d\in X_D,\quad s\in K,\quad now=latex'] - \node (A) {Node 1}; - \node (B) [right of=A] {Node 2}; - \draw[->] (A |-, -1) -- node[above] {Offer} (B |-, -1); - \draw[->] (B |-, -2) -- node[above] {Answer} (A|-, -2 ); - \draw[->] (A |-, -3) -- node[above] {Accept Offer} (B |-, -3); - \draw[->] (A |-, -4) -- node[above] {Send ICE Candidate} (B |-, -4); - \draw[->] (B |-, -5) -- node[above] {Send ICE Candidate} (A |-, -5); - \draw[->,dashed] (B) -- (A); - \draw[pattern=north east lines, pattern color=red] (A.south west) -- (A.south east) -- (A.north east) -- (A.north west) -- cycle; - \draw[pattern=north east lines, pattern color=blue] (B.south west) -- (B.south east) -- (B.north east) -- (B.north west) -- cycle; - \draw[red, thick] (A.south) -- ++(0,-5.2cm); - \draw[blue, thick] (B.south) -- ++(0,-5.2cm); -\end{tikzpicture} -\caption{Standard SDP/ICE exchange} -\label{webrtc-standard-sdp} -\end{figure} - -\begin{figure}[htbp] -\begin{tikzpicture}[node distance=5cm,auto,>=latex'] - \node (A) {Node 1}; - \node (B) [right of=A] {Node 2}; - \draw[->] (A |-, -1) -- node[above] {Offer And ICE} (B |-, -1); - \draw[->] (B |-, -2) -- node[above] {Answer and ICE} (A|-, -2 ); - \draw[->,dashed] (B) -- (A); - \draw[pattern=north east lines, pattern color=red] (A.south west) -- (A.south east) -- (A.north east) -- (A.north west) -- cycle; - \draw[pattern=north east lines, pattern color=blue] (B.south west) -- (B.south east) -- (B.north east) -- (B.north west) -- cycle; - \draw[red, thick] (A.south) -- ++(0,-2.2cm); - \draw[blue, thick] (B.south) -- ++(0,-2.2cm); -\end{tikzpicture} -\caption{Rings single round-trip SDP/ICE exchange} -\label{webrtc-rings-sdp} -\end{figure} +WebRTC signaling is a runtime adapter rather than a new overlay primitive. +The Rings transport layer may batch offer, answer, and ICE material into fewer +protocol actions, but correctness remains delegated to the WebRTC/ICE state +machines; evaluation therefore reports connection setup separately from overlay +lookup. \begin{definition}[Runtime interpreter] \[ @@ -440,27 +713,8 @@ \section{Architecture As Interfaces} \] \end{definition} -\begin{figure}[htbp] - \begin{tikzpicture}[node distance=3cm,auto,>=latex'] - \node (A) {Browser}; - \node (B) [right of=A] {Wasm Module}; - \node (C) [right of=B] {Js Runtime}; - \draw (A) -- (A |-, -5.5); - \draw (B) -- (B |-, -5.5); - \draw (C) -- (C |-, -5.5); - \draw[->] (A |-, -1) -- node[midway, above] {Download Module} (B |-, -1); - \draw[->] (B |-, -2) -- node[midway, above] {Decode Binary} (C |-, -2); - \draw[->] (C|-, -3) -- node[midway, above] {Compile} (B|-, -3); - \draw[->] (B|-,-4) -- node[midway, above] {Execute} (C|-, -4); - \draw[->] (C|-,-5) -- node[midway, above] {Call} (B|-,-5); - \draw[pattern=north east lines, pattern color=gray] (A.south west) -- (A.south east) -- (A.north east) -- (A.north west) -- cycle; - \draw[pattern=north east lines, pattern color=gray] (B.south west) -- (B.south east) -- (B.north east) -- (B.north west) -- cycle; - \draw[pattern=north east lines, pattern color=gray] (C.south west) -- (C.south east) -- (C.north east) -- (C.north west) -- cycle; - \draw[->,dashed] (B) -- (C); -\end{tikzpicture} -\caption{Wasm module execution boundary} -\label{wasm-boundary} -\end{figure} +WebAssembly is modeled only through \(I_X\) and \(\mathsf{cap}\): it interprets +effect lists under runtime capabilities and does not change the overlay object. \begin{obligation}[Runtime confinement] \[ @@ -477,9 +731,9 @@ \section{Category and Effects} \begin{definition}[Namespace object] \[ \begin{array}{rcl} -\nu&\in&\{D,V,M,H,U,Q,W\},\\ +\nu&\in&\NS,\\ H_\nu&:&X_\nu\to R,\\ -(X_\nu,H_\nu)&\in&\mathbf{Set}/R. +(X_\nu,H_\nu)&\in&\SetOverR. \end{array} \] \end{definition} @@ -487,7 +741,7 @@ \section{Category and Effects} \begin{definition}[Placement functor] \[ \begin{array}{rcl} - \Omega_N&:&\mathbf{Set}/R\to\mathbf{Set}/N,\\ + \Omega_N&:&\SetOverR\to\mathbf{Set}/N,\\ (X,H)&\mapsto&(X,\operatorname{owner}_N\circ H). \end{array} \] @@ -566,38 +820,227 @@ \section{Category and Effects} \end{definition} \begin{definition}[Protocol morphism] +\label{def:protocol-morphism} \[ \Sigma:\mathcal{P}_\nu\to\mathcal{P}_\mu = - (\sigma_X,\sigma_S,\sigma_I,\sigma_O,\sigma_{\mathcal{E}},\sigma_A^*) + (\sigma_X,\sigma_S,\sigma_I,\sigma_O, + \sigma_{\mathcal{E}},\sigma_A,\sigma_A^*) \] \[ \begin{array}{rcl} +\sigma_X&:&X_\nu\to X_\mu,\qquad +\sigma_S:S_\nu\to S_\mu,\\ +\sigma_I&:&I_\nu\to I_\mu,\qquad +\sigma_O:O_\nu\to O_\mu,\\ +\sigma_{\mathcal{E}}&:&\mathcal{E}_\nu\to\mathcal{E}_\mu,\qquad +\sigma_A:A_\nu\to A_\mu,\\ \sigma_A^*&:&A_\nu^*\to A_\mu^*,\\ +\sigma_A^*(\epsilon)&=&\epsilon,\\ +\sigma_A^*(a\cdot\alpha)&=&\sigma_A(a)\cdot\sigma_A^*(\alpha),\\ \sigma_A^*(\alpha\cdot\beta)&=&\sigma_A^*(\alpha)\cdot\sigma_A^*(\beta),\\ -H_\mu\circ\sigma_X&=&H_\nu,\\[4pt] - \mathsf{T}_{\sigma_A}^{\sigma_{\mathcal{E}}} - (\sigma_S\times\sigma_O) - \circ\tau_\nu - &=& - \tau_\mu\circ(\sigma_S\times\sigma_I). +H_\mu\circ\sigma_X&=&H_\nu . +\end{array} +\] +\[ +\begin{array}{rcl} +\mathsf{T}_{\sigma_A}^{\sigma_{\mathcal{E}}}(e) +&=&\sigma_{\mathcal{E}}(e),\\ +\mathsf{T}_{\sigma_A}^{\sigma_{\mathcal{E}}}(s,o,\alpha) +&=&(\sigma_S(s),\sigma_O(o),\sigma_A^*(\alpha)),\\[3pt] +\mathsf{T}_{\sigma_A}^{\sigma_{\mathcal{E}}}\circ\tau_\nu +&=& +\tau_\mu\circ(\sigma_S\times\sigma_I). \end{array} \] +The predicate \(\mathsf{PMor}_{\nu\mu}(\Sigma)\) is the conjunction of these +typing and preservation equations. \end{definition} -\begin{figure}[htpb] - \begin{center} -\begin{tikzpicture} -\node[rectangle, draw] (actor) {Actor}; -\node[rectangle, draw, below of=actor] (mailbox) {Mailbox}; -\node[rectangle, draw, below of=mailbox] (message) {Message}; -\draw[->] (actor) -- (mailbox); -\draw[->] (mailbox) -- (message); -\end{tikzpicture} -\end{center} -\caption{Actor Model} -\label{actor-model} -\end{figure} +\begin{lemma}[Owner totality] +\label{lem:owner-totality} +If \(1\le |N|<\infty\) and \(H_\nu:X_\nu\to R\), then +\[ + P_\nu^N=\operatorname{owner}_N\circ H_\nu:X_\nu\to N +\] +is total. +\end{lemma} +\begin{proof} +\[ + \forall k\in R.\quad + \operatorname{owner}_N(k)=\arg\min_{u\in N}\delta_k(u)\in N . +\] +Finite nonempty \(N\) gives existence; \(\delta_k:R\to\mathbb{N}\) gives a +total order key. +\end{proof} + +\begin{lemma}[Morphism preservation] +\label{lem:morphism-preservation} +\[ +\mathsf{PMor}_{\nu\mu}(\Sigma_{\nu\mu}) +\Rightarrow +P_\mu^N\circ\sigma_X=P_\nu^N . +\] +\end{lemma} +\begin{proof} +\[ +P_\mu^N\circ\sigma_X += +\operatorname{owner}_N\circ H_\mu\circ\sigma_X += +\operatorname{owner}_N\circ H_\nu += +P_\nu^N .\qedhere +\] +\end{proof} + +\begin{lemma}[Effect confinement] +\label{lem:effect-confinement} +\[ +\forall\nu\in\NS.\forall s,i.\quad +\tau_\nu(s,i)\in +\mathsf{T}^{\mathcal{E}_\nu}_{A_\nu}(S_\nu\times O_\nu). +\] +Moreover, if \(\mathsf{emit}(\tau_\nu(s,i))\subseteq\mathsf{cap}\), then +\[ + I_X(\pi_A(\tau_\nu(s,i)))\in\mathsf{IO} + \quad\land\quad + a\notin\mathsf{cap}\Rightarrow I_X(a)=\mathsf{Reject}(a). +\] +\end{lemma} +\begin{proof} +The first formula is the type of \(\tau_\nu\). The second is exactly the runtime +confinement obligation for the interpreter \(I_X\). +\end{proof} + +\begin{lemma}[Carrier non-interference] +\label{lem:carrier-noninterference} +\[ +\begin{array}{rcl} +a&\in&\mathsf{CryptoOps}\cup\mathsf{RunOps}\\ +&\Rightarrow& +\forall(X,H)\in\SetOverR.\\ +&&\left\{\begin{array}{l} +\Omega_N(X,\pi_R(a)\circ H)=\Omega_N(X,H),\\ +\Omega_N(X,H)=(X,\operatorname{owner}_N\circ H). +\end{array}\right. +\end{array} +\] +\end{lemma} +\begin{proof} +By Constraint~\ref{constraint:carrier-separation}, such \(a\) has +\(\pi_R(a)=\operatorname{id}_R\). Hence +\(\operatorname{owner}_N\circ\pi_R(a)\circ H +=\operatorname{owner}_N\circ H\). +\end{proof} + +\begin{definition}[Correct base predicate] +\label{def:correct-base} +\[ +\begin{array}{rcl} +\mathsf{CorrectBase}(N,S) +&\Rightarrow& +\left\{\begin{array}{l} +1\le |N|<\infty,\\ +\forall k\in R.\operatorname{owner}_N(k)\in N,\\ +\mathsf{CorrectChord}(N,S). +\end{array}\right. +\end{array} +\] +The theorem below uses only the displayed total-owner consequence. The stronger +steady-state lookup obligation is stated in the Chord section as +\(\operatorname{Inv}_{ring}(N,S)\land\mathsf{FingerInv}(N,S)\). +\end{definition} + +\begin{theorem}[Carrier-separated ownership theorem] +\label{thm:carrier-separated-ownership} +Assume \(\mathsf{CorrectBase}(N,S)\), carrier separation, and protocol morphisms satisfying +Definition~\ref{def:protocol-morphism}. Then +\[ +\begin{array}{rcl} +\mathsf{OwnerLaw}&\equiv&\forall\nu,x.\\ +&&P_\nu^N(x)=\operatorname{owner}_N(H_\nu(x))\in N,\\ +\mathsf{MorphLaw}&\equiv&\forall\nu,\mu,\Sigma.\\ +&&\mathsf{PMor}_{\nu\mu}(\Sigma) +\Rightarrow P_\mu^N\circ\sigma_X=P_\nu^N,\\ +\mathsf{EffectLaw}&\equiv&\forall\nu,s,i.\\ +&&\tau_\nu(s,i)\in +\mathsf{T}^{\mathcal{E}_\nu}_{A_\nu}(S_\nu\times O_\nu),\\ +\mathsf{CarrierLaw}&\equiv&\forall a\in\mathsf{CryptoOps}\cup\mathsf{RunOps}.\\ +&&\forall(X,H)\in\SetOverR.\\ +&&\Omega_N(X,\pi_R(a)\circ H)=\Omega_N(X,H),\\ +\mathsf{Core}_{Rings}&\equiv&\mathsf{OwnerLaw}\land\mathsf{MorphLaw}\\ +&&{}\land\mathsf{EffectLaw}\land\mathsf{CarrierLaw}. +\end{array} +\] +\end{theorem} +\begin{proof} +OwnerLaw follows from Definition~\ref{def:correct-base} and +Lemma~\ref{lem:owner-totality}; MorphLaw is +Lemma~\ref{lem:morphism-preservation}; EffectLaw is +Lemma~\ref{lem:effect-confinement}; CarrierLaw is +Lemma~\ref{lem:carrier-noninterference}. +\end{proof} + +\begin{constraint}[Claim ledger discipline] +\label{constraint:claim-ledger} +\begingroup\small +\[ +\begin{array}{rl} +\mathsf{Admit}_{R}(c,k)\Leftrightarrow& +k\in\mathsf{ClaimKind}\land +\exists a,\sigma.\mathsf{row}_{R}(c,k,a,\sigma),\\ +\mathsf{Admit}_{R}(c,\mathsf{Ev}_{\Gamma})\Rightarrow& +\mathsf{finite}(\Gamma)\land\mathsf{declared}(\Gamma),\\ +\mathsf{row}_{R}(c,\mathsf{Spec},a,\sigma)\Rightarrow& +c\in\left\{\begin{array}{l} +\mathsf{OwnerLaw},\mathsf{MorphLaw},\\ +\mathsf{EffectLaw},\mathsf{CarrierLaw} +\end{array}\right.\\ +&{}\land a\in\mathsf{Anchor},\\ +\mathsf{row}_{R}(c,\mathsf{Impl},a,\sigma)\Rightarrow& +a\in\mathsf{Manifest}_{R},\\ +\mathsf{row}_{R}(c,\mathsf{Ev}_{\Gamma},a,\sigma)\Rightarrow& +\mathsf{Witness}_{R}(c,\Gamma)\land a\in\mathsf{Manifest}_{R},\\ +\mathsf{row}_{R}(c,\mathsf{Obligation},a,\sigma)\Rightarrow& +c\in\mathsf{Obligation}\land\sigma=\mathsf{Open},\\ +\multicolumn{2}{l}{\mathsf{ReportedOnly}\notin\mathsf{ClaimKind},}\\ +\mathsf{Reject}_{R}(c)\Leftrightarrow&c\in\NonClaim,\\ +\mathsf{Reject}_{R}(c)\Rightarrow& +\neg\exists k.\;\mathsf{Admit}_{R}(c,k),\\ +\mathsf{LedgerDisc}_{Rings} +=&\mathsf{Admit}_{R}\land\mathsf{Reject}_{R}. +\end{array} +\] +\endgroup +Thus non-claims are excluded by the admission judgment; they are not proved +unreachable by Theorem~\ref{thm:carrier-separated-ownership}. +\end{constraint} + +\begin{proposition}[Claim-ledger admissibility] +\[ +\begin{array}{rl} +\mathsf{Admit}_{R}(c,k)\Rightarrow& +\exists a,\sigma.\mathsf{row}_{R}(c,k,a,\sigma),\\ +\mathsf{row}_{R}(c,k,a,\sigma)\Rightarrow& +\mathsf{Support}_{R}(c,k),\\ +c\in\NonClaim\Rightarrow&\neg\mathsf{Admit}(c),\\ +\mathsf{ReportedOnly}\notin\mathsf{ClaimKind}\Rightarrow& +\neg\mathsf{Admit}_{R}(c,\mathsf{ReportedOnly}),\\ +\mathsf{Admit}_{R}(c,\mathsf{Ev}_{\Gamma}) +\Rightarrow& +\left\{\begin{array}{l} +\mathsf{finite}(\Gamma),\\ +\mathsf{declared}(\Gamma). +\end{array}\right. +\end{array} +\] +\end{proposition} +\begin{proof} +The first and third lines are Constraint~\ref{constraint:claim-ledger}. The +second line unfolds the definition of \(\mathsf{Support}_{R}\). The fourth line +follows because admission quantifies only over \(\mathsf{ClaimKind}\). +\end{proof} \section{Chord Overlay} @@ -612,78 +1055,79 @@ \section{Chord Overlay} \] This section fixes Chord as the base protocol and CorrectChord as the maintenance law~\cite{Chord,ZaveChordCorrect}. -\begin{figure}[h] - \begin{center} - \begin{tikzpicture}[node distance=5cm,auto,>=latex'] - \xdef\N{16} - \xdef\S{3} - \xdef\deltadegree{360/\N} - \draw[thick] (0,0) circle (\S); - \foreach \i in {0,...,15} { - \foreach \j in {1,...,4}{ - \pgfmathsetmacro{\result}{mod(\i+2^\j,\N)} - \draw (-\i*\deltadegree+90:\S) -- (-1*\result*\deltadegree+90:\S); - } - } - \foreach \i in {0,...,15} - \node (\i) [circle,fill=white,draw=black,thick] at (-\i*\deltadegree+90:\S) {\i}; - \end{tikzpicture} - \end{center} - \caption{Chord algorithm, lookup protocol} - \label{dht} -\end{figure} - -\begin{definition}[Local node state] -\[ - S_n=(p_n,L_n,F_n,E_n) -\] +\begin{definition}[Local node state and Chord auxiliaries] \[ \begin{array}{rcl} -p_n&\in&N\cup\{\bot\},\\ -L_n&\in&N^{\leq r},\\ -F_n&:&\mathbb{N}\rightharpoonup N,\\ -E_n&\subseteq&E,\\ - p_n=\operatorname{pred}_N(n), -&& - L_n=\operatorname{Succ}^r_N(n). +S_n&=&(p_n,L_n,F_n,E_n),\\ +n&\in&N\subset R,\\ +p_n&\in&N\cup\{\bot\},\quad L_n\in N^{\le r},\\ +F_n&:&\{0,\ldots,159\}\rightharpoonup N. \end{array} \] -\end{definition} - -\begin{definition}[Finger target] +The algorithms are written over identifiers \(n\in N\); an implementation node +record \(\hat n\) is projected by \(\operatorname{id}(\hat n)=n\). \[ \begin{array}{rcl} - \operatorname{target}_i(n)&=&n+2^i,\\ - \operatorname{finger}_i(n)&=& - \operatorname{owner}_N(\operatorname{target}_i(n)),\\ - F_n(i)&\in&\{\bot,\operatorname{finger}_i(n)\}. +\mathsf{head}(\langle\rangle)&=&\bot,\\ +\mathsf{Normalize}_r(n,X) +&=&\operatorname{take}_{\min(r,|N|)}(U_n(X)),\\ +U_n(X)&=&\operatorname{uniq}(\operatorname{filter}_N(X)\cdot\operatorname{cw}_N(n)),\\ +\operatorname{target}_i(n)&=&n+2^i \bmod M,\\ +\operatorname{finger}_i(n)&=&\operatorname{owner}_N(\operatorname{target}_i(n)),\\ +\mathsf{FingerInv}(N,S)&\Leftrightarrow& +\forall n\in N.\forall i<160.\\ +&&{}\left\{\begin{array}{l} +F_n(i)\downarrow,\\ +F_n(i)=\operatorname{finger}_i(n). +\end{array}\right.,\\ +\mathsf{RouteSet}_S(n)&=& + \operatorname{rng}(F_n)\cup\operatorname{set}(L_n),\\ +\mathsf{Cand}_S(n,k)&=& +\mathsf{RouteSet}_S(n)\cap(n,k)_R,\\ +\mathsf{ClosestPreceding}_S(n,k) +&=&\max_{\delta_n}\mathsf{Cand}_S(n,k). \end{array} \] +Here \(\mathsf{ClosestPreceding}_S(n,k)=\bot\) when the displayed set is empty. \end{definition} \begin{algorithm} -\caption{DHT Join Transitions} +\caption{DHT Join and Rectify Transitions} \label{alg:join} \begin{algorithmic}[1] \Function{BeginJoin}{$n, known$} -\State $pred[n]\gets none$ -\State $a\gets FindSuccessor(n.did)$ -\State \Return $Remote(known, a)$ +\State $pred[n]\gets \bot$ +\If{$known=\bot$} + \State $succ[n]\gets \langle n\rangle$ + \State \Return $Done$ +\EndIf +\State \Return $Remote(known, FindSuccessor(n))$ \EndFunction \Function{InstallSuccessor}{$n, s$} -\State $succ[n]\gets take(r, [s])$ -\State \Return $Remote(s, QuerySuccList(s))$ +\If{$s=\bot$} + \State \Return $Repair(DiscoverSuccessor(n))$ +\EndIf +\State $succ[n]\gets \mathsf{Normalize}_r(n,\langle s\rangle)$ +\State \Return $Remote(s, QuerySuccList)$ \EndFunction \Function{InstallSuccList}{$n, s, list$} -\State $succ[n]\gets take(r, s :: list)$ -\If{$head(succ[n]) \neq none$} +\State $succ[n]\gets \mathsf{Normalize}_r(n,\langle s\rangle\cdot list)$ \State $h\gets head(succ[n])$ -\State $notify\gets Notify(h, n.did)$ -\State $sync\gets SyncStorage(h)$ -\State \Return $Multi(notify, sync)$ +\If{$h=\bot$} + \State \Return $Repair(DiscoverSuccessor(n))$ +\ElsIf{$h=n$} + \State \Return $Done$ \Else -\State \Return $Noop$ + \State $a\gets Remote(h, Notify(n))$ + \State $b\gets Remote(h, SyncStorage(n))$ + \State \Return $Multi(a,b)$ +\EndIf +\EndFunction +\Function{HandleNotify}{$n, q$} +\If{$q\neq n \land (pred[n]=\bot \lor q\in(pred[n],n)_R)$} + \State $pred[n]\gets q$ \EndIf +\State \Return $Noop$ \EndFunction \end{algorithmic} \end{algorithm} @@ -692,21 +1136,23 @@ \section{Chord Overlay} \caption{DHT Lookup Algorithm} \label{alg:lookup} \begin{algorithmic}[1] -\Function{Lookup}{$key, node$} - \State $s\gets head(succ[node])$ - \If{$s = none$} - \State \Return $Repair(QuerySuccList(node))$ - \EndIf - \If{$key \in (node.did, s]$} - \State \Return $Local(s)$ - \EndIf - \State $next\gets closest\_preceding\_node(node, key)$ - \If{$next = none$} - \State \Return $Repair(QuerySuccList(s))$ - \Else - \State $a\gets FindSuccessor(key)$ - \State \Return $Remote(next, a)$ - \EndIf +\Function{FindSuccessor}{$key, n$} +\If{$key=n$} + \State \Return $Found(n)$ +\EndIf +\State $s\gets head(succ[n])$ +\If{$s=\bot$} + \State \Return $Repair(QuerySuccList(n))$ +\ElsIf{$s=n$} + \State \Return $Found(n)$ +\ElsIf{$key\in(n,s]_R$} + \State \Return $Found(s)$ +\EndIf +\State $next\gets \mathsf{ClosestPreceding}_S(n,key)$ +\If{$next=\bot$ or $next=n$} + \State $next\gets s$ +\EndIf +\State \Return $Remote(next, FindSuccessor(key))$ \EndFunction \end{algorithmic} \end{algorithm} @@ -728,31 +1174,51 @@ \section{Chord Overlay} \node (\i) [circle,fill=white,draw=black,thick] at (-\i*\deltadegree+90:\S) {\i}; \end{tikzpicture} \end{center} - \caption{Chord algorithm, lookup protocol} + \caption{Chord finger targets from node 1 in a 16-node ring} \label{lookup-figure} \end{figure} +Figure~\ref{lookup-figure} illustrates finger targets only; lookup correctness is +the interval invariant below. \begin{algorithm}[h] \caption{DHT Stabilization} \label{alg:stabilize} \begin{algorithmic}[1] +\Function{BeginStabilize}{$n$} +\State $s\gets head(succ[n])$ +\If{$s=\bot$} + \State \Return $Repair(DiscoverSuccessor(n))$ +\ElsIf{$s=n$} + \State \Return $Noop$ +\Else + \State \Return $Remote(s, QueryTopology)$ +\EndIf +\EndFunction \Procedure{Stabilize}{$n, topo$} \State $actions\gets []$ -\State $c\gets topo.pred$ \State $s\gets head(succ[n])$ -\If {$c \neq none$ and $c \in (n.did, s)$} -\State $succ[n]\gets insert(succ[n], c)$ -\State $actions\gets actions :: FindSuccessor(c)$ +\If{$s=\bot$} + \State \Return $Repair(DiscoverSuccessor(n))$ +\ElsIf{$s=n$} + \State \Return $Noop$ \EndIf -\State $succ[n]\gets take(r, merge(succ[n], topo.succ))$ -\If{$head(succ[n]) \neq none$} +\State $c\gets topo.pred$ +\If{$c\neq\bot$ and $c\neq n$ and $c\in(n,s)_R$} + \State $succ[n]\gets \mathsf{Normalize}_r(n,\langle c\rangle\cdot succ[n])$ +\EndIf +\State $succ[n]\gets \mathsf{Normalize}_r(n,succ[n]\cdot topo.succ)$ \State $h\gets head(succ[n])$ -\State $actions\gets actions :: Notify(h, n.did)$ +\If{$h\neq\bot$ and $h\neq n$} + \State $a\gets Remote(h, Notify(n))$ + \State $b\gets Remote(h, QuerySuccList)$ + \State $actions\gets actions\cdot[a,b]$ \EndIf \State \Return $Multi(actions)$ \EndProcedure \end{algorithmic} \end{algorithm} +Algorithm~\ref{alg:biasdid} fixes the notation for the biased circular order +used by placement comparisons. \begin{invariant}[Ring fixpoint] \[ @@ -760,27 +1226,40 @@ \section{Chord Overlay} \operatorname{Inv}_{ring}(N,S) \equiv \forall n\in N.\;& p_n=\operatorname{pred}_N(n)\\ - &\land L_n=\operatorname{Succ}^r_N(n). + &\land L_n=\operatorname{Succ}^r_N(n)\\ + &\land \mathsf{head}(L_n)=\operatorname{succ}_N(n). \end{aligned} \] \end{invariant} \begin{invariant}[Lookup owner preservation] \[ +\mathsf{Eval}_S(n,k)\Downarrow o +\] +be the fair closure of Algorithm~\ref{alg:lookup}, where +\(Remote(m,FindSuccessor(k))\) resumes the same lookup at node \(m\). Then +\[ \begin{aligned} -&\mathsf{Steady}(N)\land\operatorname{Inv}_{ring}(N,S)\\ +&(\mathsf{Steady}(N,r)\lor |N|=1) +\land\operatorname{Inv}_{ring}(N,S)\\ &\Rightarrow - \operatorname{Lookup}(S,k)\Downarrow - \operatorname{owner}_N(k). +\forall n\in N.\forall k\in R.\; +\mathsf{Eval}_S(n,k)\Downarrow \operatorname{owner}_N(k). \end{aligned} \] -\[ - \Downarrow - = - \mathsf{Reach}_{A_D}(\ref{alg:lookup},\ref{alg:stabilize}). -\] \end{invariant} +\begin{proof}[Proof obligation] +If Algorithm~\ref{alg:lookup} returns \(Found(s)\) by the interval test, then +\(s=head(L_n)=\operatorname{succ}_N(n)\) and no live node lies in \((n,s)_R\); +therefore \(\operatorname{owner}_N(k)=s\). If it forwards, the chosen target is +either the closest preceding finger/list entry or the first successor; in both +cases it lies in \((n,k)_R\), so \(\delta_{next}(k)<\delta_n(k)\). Finiteness of +\(N\) gives termination. The branches \(key=n\) and \(s=n\) discharge +the singleton and exact-owner edge cases. Repair branches are outside the +steady-ring premise. +\end{proof} + \section{DID and Resource Algebra} \begin{definition}[DID namespace] @@ -791,9 +1270,10 @@ \section{DID and Resource Algebra} \] \[ \begin{array}{rcl} -D(k)&=&H_D(k),\\ -\operatorname{owner}_N(D(k))&\in&N,\\ -\operatorname{Session}&\subseteq&X_D\times K\times Time. +D_K(k)&=&H_D(\operatorname{did}(k)),\\ +\operatorname{owner}_N(D_K(k))&\in&N,\\ +\operatorname{Session}&\subseteq&X_D\times K\times + \mathsf{Time}\times\mathsf{Ctx}\times\mathsf{Cap}. \end{array} \] \end{definition} @@ -859,15 +1339,53 @@ \section{DID and Resource Algebra} \begin{invariant}[Placement] \[ - \operatorname{Inv}_{place}\equiv - \forall \nu,x.\; - \operatorname{replicas}(H_\nu(x)) - \subseteq - \operatorname{Rep}^{\rho}_N(H_\nu(x)). +\begin{array}{rcl} +P_{\nu,x}&=&\operatorname{set}(\operatorname{RepKey}^{\rho}(H_\nu(x))),\\ +K^{impl}_{\nu,x}&\subseteq&R,\\ +\operatorname{Inv}_{place} +&\equiv& +\forall \nu,x.\;K^{impl}_{\nu,x}\subseteq P_{\nu,x}. +\end{array} \] \end{invariant} +\begin{obligation}[Replica realization] +\[ +\begin{array}{rcl} +\Theta&\in&\{\Theta_n(t),N\},\\ +O^\Theta_{\nu,x}&=& +\operatorname{set}(Q^{\rho,v_0}_{\Theta}(H_\nu(x))),\\ +L^\Theta_{\nu,x}&=&|O^\Theta_{\nu,x}|,\\ +\mathsf{FR}^{\Theta}_{\nu,x} +&\Leftrightarrow&L^\Theta_{\nu,x}=\min(\rho,|\Theta|),\\ +\mathsf{Col}^{\Theta}_{\nu,x} +&\Leftrightarrow&L^\Theta_{\nu,x}<\min(\rho,|\Theta|),\\ +\mathsf{LC}^{\Theta}_{\nu,x}&\Leftrightarrow& +\mathsf{Admit}_{R}(\mathsf{FR}^{\Theta}_{\nu,x}, +\mathsf{Evidence}_{\Gamma}),\\ +\mathsf{LC}^{\Theta}_{\nu,x}&\Rightarrow& + \operatorname{Inv}_{place}\land\mathsf{FR}^{\Theta}_{\nu,x},\\ +G_R^\Theta&=& + \{(\nu,x):\mathsf{Col}^{\Theta}_{\nu,x}\},\\ +G_R^\Theta\neq\varnothing&\Rightarrow& +\mathsf{FullReplica}_{R}\in\mathsf{Obligation}. +\end{array} +\] +Here \(\mathsf{FR}\), \(\mathsf{Col}\), and \(\mathsf{LC}\) abbreviate full +redundancy, collapse, and live claim; \(G_R^\Theta\) is the replica gap set and +\(\mathsf{FullReplica}_{R}\) is the full-replica-realization obligation. When +\(|\Theta|<\rho\), fewer than \(\rho\) distinct owners is not collapse; +collapse means fewer owners than the selected view can realize. For runtime +claims, \(\Theta=\Theta_n(t)\); reported coordinates may use \(\Theta=N\). +For the paper default \(v_0>0\), \(O^\Theta_{\nu,x}\) is the image of the +storage VNODE owner map. This is a placement claim, not a full routing-VNODE +or load-balance theorem. +\end{obligation} + \begin{definition}[Mailbox] +\[ + \mathsf{Class}(\mathsf{Mailbox})\subseteq\{\mathsf{Spec},\mathsf{Obligation}\}. +\] \[ \begin{array}{rcl} mbox(d,e)&=&H_M(\mathtt{rings.mailbox}\Vert d\Vert e),\\ @@ -877,11 +1395,14 @@ \section{DID and Resource Algebra} \end{definition} \begin{definition}[Hidden service descriptor] +\[ + \mathsf{Class}(\mathsf{HiddenDesc})\subseteq\{\mathsf{Spec},\mathsf{Obligation}\}. +\] \[ \begin{array}{rcl} h&=&(\nu,\rho,Intro,Relay,\\ -&&Cap,K,exp,rank),\\ -VID(h)&=&H_H(h),\\ +&&\mathsf{Cap},K,exp,rank),\\ +\operatorname{vid}(h)&=&H_H(h),\\ \mathsf{Lookup}(h)&=&P^N_H(h),\\ \mathsf{Valid}(h,\sigma)&=&\operatorname{Auth}_H(h,\sigma). \end{array} @@ -889,6 +1410,9 @@ \section{DID and Resource Algebra} \end{definition} \begin{definition}[Subring] +\[ + \mathsf{Class}(\mathsf{Subring})=\{\mathsf{Impl}\}. +\] \[ \mathcal{S}_u=(u,N_u,\operatorname{owner}_{N_u}, \operatorname{Succ}^{r_u}_{N_u},E_u) @@ -919,37 +1443,158 @@ \section{Cryptographic Carriers and Traffic} \caption{ElGamal Encryption and Decryption} \label{alg:elgamal} \begin{algorithmic}[1] -\State \textbf{Input:} Message $m$, private key $x \in \mathbb{Z}_q$, public key $h = g^x$, generator $g$ -\State \textbf{Output:} Encrypted message $(c_1, c_2)$ +\State \textbf{Input:} Encoded group element $m_G\in\mathbb{G}$, private key $x \in \mathbb{Z}_q$, public key $h = g^x$, generator $g$ +\State \textbf{Output:} Group ciphertext $(c_1, c_2)$ \Procedure{Encryption}{} \State Choose a random integer $k \in \mathbb{Z}_q$ \State Compute $c_1 = g^k$ -\State Compute $c_2 = m\cdot h^k$ +\State Compute $c_2 = m_G\cdot h^k$ \State \Return $(c_1, c_2)$ \EndProcedure \Procedure{Decryption}{} -\State Compute $m = c_2\cdot(c_1)^{-x}$ -\State \Return $m$ +\State Compute $m_G = c_2\cdot(c_1)^{-x}$ +\State \Return $m_G$ \EndProcedure \end{algorithmic} \end{algorithm} +Algorithm~\ref{alg:elgamal} is the group-level carrier operation. Byte +payloads must first be encoded into curve points and split into bounded frames. +The direct ElGamal body is malleable when detached from its signed transport +envelope. The Rings frame layer therefore binds message signatures, DID +ownership of the public key, stream identifiers, sequence numbers, and +final-frame checks into the security boundary rather than treating them as +optional metadata. + +\begin{definition}[Onion exit registry and circuit] +\label{def:onion-circuit} +\[ + \mathsf{Class}(\mathsf{OnionImpl}_{R}) + \subseteq\{\mathsf{Impl},\mathsf{Evidence}_{\Gamma}\}. +\] +\begingroup\small +\[ +\begin{array}{rcl} +\mathsf{Topic}_{onion}&=&\mathtt{onion\_exits},\\ +e&=&(d,k_d,s,nt,net,svc,tr,\pi,\\ +&&{}t_0,t_h,t_x,\sigma),\\ +p&=&(svc,tr,\chi),\\ +\operatorname{svc}(p)&=&svc,\quad +\operatorname{tr}(p)=tr,\quad +\operatorname{target}(p)=\chi,\\ +\operatorname{ExitOK}(e,t)&\Leftrightarrow& +V(k_d,\sigma,e\setminus\sigma)=\top\\ +&&{}\land\operatorname{did}(k_d)=d +\land tseq,\\ +\mathsf{Dup}_{\Delta}(f)&\Leftrightarrow& + seq(f)\in seen_{seq}\\ +&&{}\lor \operatorname{fid}(f)\in seen_{fid}\\ +&&{}\lor pending(seq(f))=f,\\ +\mathsf{Conflict}_{\Delta}(f)&\Leftrightarrow& + seq(f)\in\operatorname{dom}(pending)\\ +&&{}\land pending(seq(f))\neq f,\\ +\mathsf{New}_{\Delta}(f)&\Leftrightarrow& + seq(f)\notin seen_{seq}\cup\operatorname{dom}(pending)\\ +&&{}\land \operatorname{fid}(f)\notin seen_{fid}\\ +&&{}\land\neg closed\\ +&&{}\land seq(f)-next\leq w\\ +&&{}\land(final=\bot\lor seq(f)\leq final)\\ +&&{}\land(last(f)\Rightarrow\mathsf{NoFuture}_{\Delta}(seq(f))),\\ +\operatorname{Accept}_{\Delta}(f)&\Leftrightarrow& + \operatorname{FrameValid}(f)\\ +&&{}\land\mathsf{New}_{\Delta}(f),\\ +\operatorname{Reject}_{\Delta}(f)&\Leftarrow& + \operatorname{FrameValid}(f)\\ +&&{}\land\mathsf{Conflict}_{\Delta}(f),\\ +\operatorname{DropDup}_{\Delta}(f)&\Leftrightarrow& + \operatorname{FrameValid}(f)\\ +&&{}\land\mathsf{Dup}_{\Delta}(f)\\ +&&{}\land\mathsf{emit}=\epsilon. +\end{array} +\] +Here \(w\) is receiver policy, not a signed wire field. A byte-identical +duplicate may be valid and dropped; a same-sequence different pending frame is +rejected as equivocation. +\end{definition} + \begin{definition}[Secret sharing placement] +\[ + \mathsf{Class}(\mathsf{SecretSharing}) + \subseteq\{\mathsf{Spec},\mathsf{Obligation}\}. +\] \[ \begin{array}{rcl} P&\in&\mathbb{F}_q[X],\\ @@ -993,6 +1638,8 @@ \section{Cryptographic Carriers and Traffic} \EndProcedure \end{algorithmic} \end{algorithm} +Algorithm~\ref{alg:e2e_chunking} gives the bounded split/reassembly shape; it +does not claim MSRP interruption or interleaving semantics. \begin{invariant}[Chunk reassembly] \[ @@ -1009,6 +1656,10 @@ \section{Cryptographic Carriers and Traffic} \section{Ordering, Ranking, and Security} \begin{definition}[Sidecar witness] +\[ + \mathsf{Class}(\mathsf{SidecarWitness}) + \subseteq\{\mathsf{Spec},\mathsf{Obligation}\}. +\] \[ w=(domain,root,height,time,finality). \] @@ -1033,11 +1684,14 @@ \section{Ordering, Ranking, and Security} \end{aligned} \] \[ - \chi:Domain_a\times Domain_b\to Order. + \chi:\mathsf{Domain}\times\mathsf{Domain}\to\mathsf{Order}. \] \end{definition} \begin{definition}[Ranking event] +\[ + \mathsf{Class}(\mathsf{Ranking})\subseteq\{\mathsf{Spec},\mathsf{Obligation}\}. +\] \[ \begin{aligned} q=(&subject,rater,behavior,\\ @@ -1069,63 +1723,194 @@ \section{Ordering, Ranking, and Security} \begin{table}[htbp] \centering -\small -\setlength{\tabcolsep}{2pt} -\begin{tabular}{p{1.1cm}|p{2.1cm}|p{2.35cm}} +\scriptsize +\setlength{\tabcolsep}{1.5pt} +\begin{tabular}{@{}>{\raggedright\arraybackslash}p{1.05cm} +>{\raggedright\arraybackslash}p{2.35cm} +>{\raggedright\arraybackslash}p{2.95cm}@{}} \hline -Attack & Predicate & Rings control \\ \hline -Sybil & many DIDs, one actor & admission cost, ranking, challenge \\ -Replay & stale valid $\sigma$ & nonce, TTL, session epoch \\ -MITM & wrong key for DID & DID proof, signed envelope, E2E \\ -DoS & unbounded resource use & quotas, ranking, chunk bounds \\ +Attack & Predicate & Boundary claimed here \\ \hline +Sybil & one actor controls many DIDs & not solved by overlay; admission, ranking, quota \\ +Eclipse & biased neighbor or successor view & not claimed under Byzantine routing; requires secure-routing policy \\ +Replay & stale valid signature or frame & typed session, expiry, nonce/sequence set \\ +MITM & wrong key for DID or session & DID proof, signed envelope, context binding \\ +DoS & unbounded storage, relay, or chunks & quotas, TTL, chunk bounds, backpressure \\ +Privacy & route or relay observation & relay policy only; no anonymity theorem \\ \hline \end{tabular} -\normalsize -\caption{Security predicates and controls} +\caption{Threat predicates and claim boundaries} \label{security-table} \end{table} +Table~\ref{security-table} fixes the negative boundary: listed attacks are not +discharged by the overlay theorem. -\begin{obligation}[Replay rejection] +\begin{definition}[Security and policy boundary] \[ \begin{array}{rcl} -\operatorname{accept}(s,\eta,t) -&\Rightarrow& - \eta\notin Seen_s\land t