diff --git a/src/SUMMARY.md b/src/SUMMARY.md index c0e155f..997cf3b 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -86,7 +86,7 @@ # Specifications and Theory -- [Protocol specification](./protocol.md) +- [Overview](./theory/index.md) - [Syndicated Actor Model]() - [Actors, Entities, Assertions and Messages]() @@ -96,4 +96,6 @@ - [Attenuation of authority for security]() - [Attenuation of authority for privacy]() +- [Protocol specification](./protocol.md) + - [System layer analysis]() diff --git a/src/glossary.md b/src/glossary.md index c0d942d..7e3bd7e 100644 --- a/src/glossary.md +++ b/src/glossary.md @@ -1,27 +1,100 @@ # Glossary +## Action ## Actor ## Assertion ## Attenuation ## Capability + +a.k.a. Cap + +Pointer or handle denoting a live, stateful [entity](#entity) running within an +[actor](#actor). The entity accepts [Preserves](#preserves)-format [messages](#message) and/or +[assertions](#assertion). The capability may be [attenuated](#attenuation) to restrict the +messages and assertions that may be delivered to the denoted entity by way of this particular +handle. + ## Compositional ## Configuration Scripting Language ## Conversational State ## Dataspace ## E +## Embedded References +## Entity +## Event ## Facet +## Initial OID +## Initial Ref ## Macaroon + +[*“Macaroons: Cookies with Contextual Caveats for Decentralized Authorization in the +Cloud.”*](https://research.google/pubs/pub41892/), by Arnar Birgisson, Joe Gibbs Politz, Úlfar +Erlingsson, Ankur Taly, Michael Vrable, and Mark Lentczner. In Proc. Network and Distributed +System Security Symposium (NDSS), 2014. [[PDF]](https://research.google/pubs/pub41892.pdf) + +## Membrane ## Message +## Network + +A network is a group of peers, plus a medium of communication, an addressing model, and an +associated [scope](#scope). + ## Object Capability Model ## Observe +## OID ## Preserves +## Record +a Preserves record +## Reference +a.k.a. Ref +## Relay +## Relay Entity ## S6 ## Schema +## Scope + +A *scope* maps [refs](#reference) to the [entities](#entity) they denote. Scopes exist in +one-to-one relationship to [networks](#network). Because [message bodies](#message) and +[asserted values](#assertion) contain [embedded references](#embedded-references), each message +and assertion transmitted via some network is also inseparable from its scope. + +Most [actors](#actor) will participate in a single scope. However, [relay](#relay) actors +participate in two or more scopes, translating refs back and forth as messages and assertions +traverse the relay. + +**Examples.** + + 1. A process is a scope for in-memory values: in-memory refs contain direct pointers to + entities, which cannot be interpreted outside the context of the process's address space. + The "network" associated with the process's scope is the intra-process graph of object + references. + + 2. A TCP/IP socket (or serial link, or WebSocket, or Unix socket, etc.) is a scope for values + travelling between two connected processes: [refs on the wire](#wire-symbol) denote + entities owned by one or the other of the two participants. The "network" for a socket's + scope is exactly the two connected peers (NB. and is *not* the underlying TCP/IP network, + HTTP network, or Unix kernel that supports the point-to-point link). + + 3. An ethernet segment is a scope for values broadcast among stations: the embedded refs are + (MAC address, [OID](#oid)) pairs. The network is the set of participating peers. + + 4. A running web page is a scope for the JavaScript objects it contains: both local and remote + entities are represented by JavaScript objects. The "network" is the JavaScript heap. + ## Supervision tree ## Supervisor +## Sync Peer Entity +## Synchronization +(`sync` action) ## Syndicated Actor Model Often abbreviated **SAM**. +Source [entities](#entity) running within an [actor](#actor) publish [assertions](#assertion) +and send [messages](#message) to target entities, possibly in other actors. + ## System Layer -## System dataspace +## System Dataspace +## Transport +## Turn +## Wire Symbol diff --git a/src/introduction.md b/src/introduction.md index d20d504..ef259c1 100644 --- a/src/introduction.md +++ b/src/introduction.md @@ -1,11 +1,11 @@ -# Synit: an Alternative System Layer +# Synit: a Reactive Operating System ## Welcome! -Synit is an experiment in applying the [Syndicated Actor -Model](./glossary.md#syndicated-actor-model) to the [System -Layer](./glossary.md#system-layer) of an operating system for personal -computers, including laptops, desktops, and mobile phones. +Synit is an experiment in applying **pervasive reactivity** and **object capabilities** to the +[System Layer](./glossary.md#system-layer) of an operating system for personal computers, +including laptops, desktops, and mobile phones. Its [architecture](./architecture.md) follows +the principles of the [Syndicated Actor Model](./glossary.md#syndicated-actor-model). Synit builds upon the Linux kernel, but replaces many pieces of familiar Linux software, including `systemd`, `NetworkManager`, diff --git a/src/protocol.md b/src/protocol.md index fbd34d1..bc8fe67 100644 --- a/src/protocol.md +++ b/src/protocol.md @@ -1 +1,669 @@ -# Protocol +# Syndicate Protocol + +Actors in the same local [scope](./glossary#scope) communicate directly. To communicate further +afield, scopes may be *connected* using [relay actors](./glossary.md#relay). Relays allow +*indirect* communication: distant entities can be addressed as if they were local. + +Relays exchange *Syndicate Protocol* messages across a [transport](./glossary.md#transport). A +*transport* is the underlying medium connecting one relay to its counterparts on a given +network. For example, a TLS-on-TCP/IP socket may connect a pair of relays to one another, or a +UDP multicast socket may connect an entire group of relays across an ethernet. + +```ditaa protocol-transport + +-------------+ +-------------+ + | | transport | | + | +-----+ +------------------------+ +-----+ | + |. . . |Relay|<-->| TLS/TCP/IP socket |<-->|Relay| . . . | + | +-----+ +------------------------+ +-----+ | + | | | | + +-------------+ +-------------+ +``` + +## Transport requirements + +Transports must + + - be able to carry [Preserves](./glossary.md#preserves) values back and forth, + - be reliable and in-order, + - have a well-defined lifecycle (created → connected → disconnected), and + - assure confidentiality, integrity and replay-resistance. + +This document focuses primarily on point-to-point transports, discussing multicast and +in-memory variations briefly toward the end. + +## Roles and session establishment + +The protocol is completely symmetric, aside from [certain conventions detailed +below](#well-known-oids) about the entities available for use immediately upon connection +establishment. It is *not* a client/server protocol. + +To begin a session on a newly-established point-to-point link, a relay simply starts sending +packets. Each peer starts the session with an empty entity reference map ([see +below](#membranes)) and making no assertions in either the outbound (on behalf of local +entities) or inbound (on behalf of the remote peer) directions. + +## Packet definitions + +```preserves-schema +Packet = Turn / Error / Extension . +``` + +Packets exchanged by relays are [Preserves](./glossary.md#preserves) values defined using +Preserves [schema](./glossary.md#schema). + +A packet may be a *turn*, an *error*, or an *extension*. + +Packets are neither commands nor responses; they are *events*. + +### Extension packets + +```preserves-schema +Extension = < @label any @fields [any ...]> . +``` + +An extension packet must be a Preserves [record](./glossary.md#record), but is otherwise +unconstrained. + +**Handling.** +Peers MUST ignore extensions that they do not understand.[^no-extensions-yet] + +### Error packets + +```preserves-schema +Error = . +``` + +**Handling.** +An error packet describes something that went wrong on the other end of the connection. Error +packets are primarily intended for debugging. + +Receipt of an error packet denotes that the sender has terminated (crashed) and will not +respond further; the connection will usually be closed shortly thereafter. + +Error packets are *optional*: connections may simply be closed without comment. + +### Turn packets + +```preserves-schema +Turn = [TurnEvent ...]. +TurnEvent = [@oid Oid @event Event]. +Event = Assert / Retract / Message / Sync . + +Assert = . +Retract = . +Message = . +Sync = . + +Assertion = any . +Handle = int . +Oid = int . +``` + +A `Turn` is the most important packet variant. It directly reflects the +[SAM](./glossary.md#syndicated-actor-model) notion of a [turn](./glossary.md#turn). + +**Handling.** Each `Turn` carries [events](./glossary.md#event) to be delivered to +[entities](./glossary.md#entity) residing at the receiving end of the transport. + +The `assertion` fields of `Assert` events and the `body` fields of `Message` events may contain +any Preserves value, including embedded entity references. On the wire, these will always be +formatted [as described below](#capabilities-on-the-wire). Upon receipt of a `Turn`, embedded +references are first mapped to internal references. Prior to transmission, internal references +are mapped to their external form. [The mapping procedure to follow is detailed +below.](#membranes) + +After reference rewriting is complete, the sequence of `TurnEvent`s is examined. The +[OID](./glossary.md#oid) in each `TurnEvent` selects an entity known to the recipient. Each +`Event` is either publication of an assertion, retraction of a previously-published assertion, +delivery of a single message, or a [synchronization](./glossary.md#synchronization) event. + +In the case that the receiving party is structured internally using the SAM, it is important to +preserve turn boundaries. Since turn boundaries are a per-[actor](./glossary.md#actor) concept, +but a `Turn` mentions only entities, the receiver must map entities to actors, group +`TurnEvent`s into per-actor queues, and deliver those queues to each actor in a single SAM turn +for each actor. + +The `Handle`s used to refer to published assertions MUST be unique within the scope of the +transport connection. + +## Capabilities on the wire + +Packets sent and received on a point-to-point transport frequently include embedded references. +These references denote *capabilities* for interacting with some entity. + +For example, assertion of a capability-bearing record could appear as the following `Event`: + +```preserves +> +``` + +The `#![0 555]` is [concrete Preserves text syntax](./guide/preserves.md#concrete-syntax) for +an embedded (`#!`) value (`[0 555]`). + +In the Syndicate Protocol, these embedded values MUST conform to the `WireRef` +schema:[^slightly-silly-wireref] + +```preserves-schema +WireRef = @mine [0 @oid Oid] / @yours [1 @oid Oid @attenuation Caveat ...]. +Oid = int . +``` + +The `mine` variant denotes capability references managed by the *sender* of a given packet; the +`yours` variant, the *receiver* of the packet. Accordingly, if a relay receives a packet +mentioning `#![0 555]`, it will later use `#![1 555]` if it needs to send a packet to refer to +that same entity. + +### Attenuation of authority + +A `yours`-variant capability may include a request[^attenuation-is-not-enforceable] to impose +additional conditions on the receiver's use of its own capability, known as an +[attenuation](./glossary.md#attenuation) of the capability's authority. + +An attenuation is a chain of `Caveat`s.[^caveat-terminology-macaroon] A `Caveat` acts as a +function that, given a Preserves value representing an assertion or message body, yields either +a possibly-rewritten value, or no value at all. In the latter case, the value has been +*rejected*. In the former case, the rewritten value is used as input to the next `Caveat` in +the chain, or as the final assertion or message body for delivery to the entity backing the +capability. + +The chain of `Caveats` in an attenuation is written down in *reverse* order: newer `Caveat`s +are appended to the sequence, and each `Caveat`'s output is fed into the input of the next +leftward `Caveat` in the sequence. If no `Caveat`s are present, the capability is unattenuated, +and inputs are passed through to the backing capability unmodified. + +```preserves-schema +Caveat = Rewrite / Alts . + +Rewrite = . +Alts = . +``` + +A `Caveat` can be either a single `Rewrite` or a sequence of alternative possible rewrites, +tried in left-to-right order until one of them accepts the input or there are none left to try. +(A single `Rewrite` *R* is equivalent to ``.) + +A `Rewrite` applies its `Pattern` to the input to the `Caveat`. If it matches, the bindings +captured by the pattern are gathered together and used in instantiation of the `Rewrite`'s +`Template`, yielding the output from the `Caveat`. If the pattern does not match, the `Rewrite` +has rejected the input, and other `alternatives` are tried until none remain, at which point +the whole `Caveat` has rejected the input and processing of the triggering event stops. + +#### Patterns + +A `Pattern` within a rewrite can be any of the following variants: + +```preserves-schema +Pattern = PDiscard / PAtom / PEmbedded / PBind / PAnd / PNot / Lit / PCompound . +``` + +`PDiscard` matches any value: + +```preserves-schema +PDiscard = <_>. +``` + +`PAtom` requires that a matched value be a boolean, a single- or double-precision float, an +integer, a string, a binary blob, or a symbol, respectively: + +```preserves-schema +PAtom = =Boolean / =Float / =Double / =SignedInteger / =String / =ByteString / =Symbol . +``` + +`PEmbedded` requires that a matched value be an embedded capability: + +```preserves-schema +PEmbedded = =Embedded . +``` + +`PBind` first *captures* the matched value, adding it to the bindings vector, and then applies +the nested `pattern`. If the subpattern matches, the `PBind` succeeds; otherwise, it fails: + +```preserves-schema +PBind = . +``` + +`PAnd` is a conjunction of patterns; every pattern in `patterns` must match for the `PAnd` to +match: + +```preserves-schema +PAnd = . +``` + +`PNot` is a pattern negation: if `pattern` matches, the `PNot` fails to match, and *vice +versa*. It is an error for `pattern` to include any `PBind` subpatterns. + +```preserves-schema +PNot = . +``` + +`Lit` is an exact match pattern. If the matched value is exactly equal to `value` (according to +Preserves' own built-in equivalence relation), the match succeeds; otherwise, it fails: + +```preserves-schema +Lit = . +``` + +Finally, `PCompound` patterns match compound data structures. The `rec` variant demands that a +matched value be a record, with label exactly equal to `label` and fields one-for-one matching +the `Pattern`s in `fields`; the `arr` variant demands a sequence, with each element matching +the corresponding element of `items`; and `dict` demands a dictionary having *at least* entries +named by the keys of the `entries` dictionary, each matching the corresponding `Pattern`. + +```preserves-schema +PCompound = + / @rec + / @arr + / @dict . +``` + +#### Bindings + +Bindings resulting from matching are stored as a sequence of values. + +During matching, when a `PBind` pattern is seen, the matcher *first* appends the matched value +to the binding sequence and *then* recurses on the nested subpattern. This makes binding +*indexes* appear in left-to-right order as a `Pattern` is read. + +For example, given the pattern `>, >]>>` and the matched value +`[1 2]`, the resulting captured values will be, in order, `[1 2]`, `1`, and `2`. + +#### Templates + +A `Template` within a rewrite produces a concrete Preserves value when instantiated with a +vector of captured binding values. Template instantiation may fail, yielding no value. + +A given `Template` may be any of the following variants: + +```preserves-schema +Template = TAttenuate / TRef / Lit / TCompound . +``` + +`TAttenuate` first instantiates the sub-`template`. If it yields a value, and if that value is +an embedded reference (i.e. a capability), the `Caveat`s in `attenuation` are appended to the +(possibly-empty) sequence of `Caveat`s already present in the embedded capability. The +resulting possibly-attenuated capability is the final result of instantiation of the +`TAttenuate`. + +```preserves-schema +TAttenuate = . +``` + +`TRef` retrieves the `binding`th (0-based) index into the bindings vector, yielding the +associated captured value as the result of instantiation. It is an error if `binding` is less +than zero, or greater than or equal to the number of bindings in the bindings vector. + +```preserves-schema +TRef = . +``` + +`Lit` (the same definition as used in the grammar for `Pattern` above) instantiates to exactly +its `value` argument: + +```preserves-schema +Lit = . +``` + +Finally, `TCompound` instantiates to compound data. The `rec` variant produces a record with +the given `label` and `fields`; `arr` produces an array; and `dict` a dictionary: + +```preserves-schema +TCompound = + / @rec + / @arr + / @dict . +``` + +#### Validity of Caveats + +The above definitions imply some *validity constraints* on `Caveat`s. + + - All `TRef`s must be bound: the index referred to must relate to the index associated with + some `PBind` in the pattern corresponding to the template. + + - Binding under negation is forbidden: a `pattern` within a `PNot` may not include any `PBind` + constructors. + + - The value produced by instantiation of `template` within a `TAttenuate` must be an embedded + reference (a capability). + +Implementations MUST enforce these constraints (either statically or dynamically). + +#### Pseudocode for attenuation, pattern matching, and template instantiation + +##### Attenuation +```python +def attenuate(attenuation, value): + for caveat in reversed(attenuation): + value = applyCaveat(caveat, value) + if value is None: + return None + return value + +def applyCaveat(caveat, value): + if caveat is 'Alts' variant: + for rewrite in caveat.alternatives: + possibleResult = tryRewrite(rewrite, value); + if possibleResult is not None: + return possibleResult + return None + if caveat is 'Rewrite' variant: + return tryRewrite(caveat, value) + +def tryRewrite(rewrite, value): + bindings = applyPattern(rewrite.pattern, value) + if bindings is None: + return None + else: + return instantiateTemplate(rewrite.template, bindings) +``` + +##### Pattern matching +```python +def match(pattern, value, bindings): + if pattern is 'PDiscard' variant: + return True + if pattern is 'PAtom' variant: + return True if value is of the appropriate atomic class else False + if pattern is 'PEmbedded' variant: + return True if value is a capability else False + if pattern is 'PBind' variant: + append value to bindings + return match(pattern.pattern, value, bindings) + if pattern is 'PAnd' variant: + for p in pattern.patterns: + if not match(p, value, bindings): + return False + return True + if pattern is 'PNot' variant: + return False if match(pattern.pattern, value, bindings) else True + if pattern is 'Lit' variant: + return (pattern.value == value) + if pattern is 'PCompound' variant: + if pattern is 'rec' variant: + if value is not a record: return False + if value.label is not equal to pattern.label: return False + if value.fields.length is not equal to pattern.fields.length: return False + for i in [0 .. pattern.fields.length): + if not match(pattern.fields[i], value.fields[i], bindings): + return False + return True + if pattern is 'arr' variant: + if value is not a sequence: return False + if value.length is not equal to pattern.items.length: return False + for i in [0 .. pattern.items.length): + if not match(pattern.items[i], value[i], bindings): + return False + return True + if pattern is 'dict' variant: + if value is not a dictionary: return False + for k in keys of pattern.entries: + if k not in keys of value: return False + if not match(pattern.entries[k], value[k], bindings): + return False + return True +``` + +##### Template instantiation +```python +def instantiate(template, bindings): + if template is 'TAttenuate' variant: + c = instantiate(template.template, bindings) + if c is not a capability: raise an exception + c′ = c with the caveats in template.attenuation appended to the existing + attenuation in c + return c′ + if template is 'TRef' variant: + if 0 ≤ template.binding < bindings.length: + return bindings[template.binding] + else: + raise an exception + if template is 'Lit' variant: + return template.value + if template is 'TCompound' variant: + if template is 'rec' variant: + return Record(label=template.label, + fields=[instantiate(t, bindings) for t in template.fields]) + if template is 'arr' variant: + return [instantiate(t, bindings) for t in template.items] + if template is 'dict' variant: + result = {} + for k in keys of template.entries: + result[k] = instantiate(template.entries[k], bindings) + return result +``` + +## Membranes + +In order to correctly map between embedded references on the wire and entity references local +to the relay, the relay maintains two stateful objects called *membranes*. A membrane is a +bidirectional mapping between [OID](./glossary.md#oid) and relay-internal entity pointer. + + - The *import membrane* connects OIDs managed by the *remote* peer to local *relay entities* + which proxy access to an "imported" remote entity. + + - The *export membrane* connects OIDs managed by the *local* peer to any local "exported" + entities accessible to the peer. + +```ditaa membranes + | + | + Export Membrane | Import Membrane + | + +-+ | +-+ + Pointer | | ID | ID | | + 0x1234 <-+-+-> "my 7" | "your 7"<-+-+-> 0x9abc + | | | | | + ^ | | ^ | ^ | | ^ + | | | | -+- | | | | + V | | | | | | V + /------\ | | \-------------/ | | /------\ + |Entity| | | | | |Relay |<-- ... + \------/ | | | | |Entity| + 0x1234 | | --------> | | \------/ + =-------------+-+---= packets | | 0x9abc + 0x462e | | <-------- =---+-+-------------= + /------\ | | | | 0xa043 + |Relay | | | | | /------\ +... -->|Entity| | | /-------------\ | | |Entity| + \------/ | | | | | | \------/ + ^ | | | -+- | | | ^ + | | | | | | | | | + V | | V | V | | V + | | | | | + 0x462e <-+-+->"your 3" | "my 3" <-+-+-> 0xa043 + Pointer | | ID | ID | | Pointer + +-+ | +-+ + | + Import Membrane | Export Membrane + | + | +``` + + +```ditaa one-sided-membrane + ---------------------------------------+ + | + Membrane | + ----+---- | + /--\ | | | + |A1|<----+ Pointer | ID +-+-------------transport--- + \--/ | | + +---0x7f1065218700<-+-> 7 + | <---- from remote + /--\ | peer + |A2|<-----0x7f1065229780<-+-> 11 + \--/ | + | ----> to remote + +--0x7f10652fe7c0<-+-> 13 peer + /--\ | | + |A3|<----+ | +-+------------------------- + \--/ | | + | + | + ----------------------------------------+ +``` + + +| Relay |<-\ | ++----------------+ (2) +-------+ | +---------+ | + | ^ \->|Dataspace| | + | | +---------+ | + | V ^ ^ ^ (1) | ++----------------+ TCP/IP +-------+ | | | | +|Remote Syndicate|<----------->| Relay |<----+-/ | | | +|server/dataspace| (3) +-------+ | | | | ++----------------+ | V V V | + | +-------+ +-------+ | + | | Relay | | Relay | | + +----------+-------+-+-------+--+ + ^ ^ + LAN multicast (4) | | UNIX + ... <-------/---------/---------/---------/ | socket + | | | | (5) + v v v v + +-------+ +-------+ +-------+ +-------+ + |. . . | |. . . | |. . . | |. . . | + +-------+ +-------+ +-------+ +-------+ +``` + +In the diagram above, networks (scopes) 1 and 4 are *multicast*, while networks 2, 3 and 5 are +*point-to-point*. Four relays bridge scope 1 to scopes 2 through 5. Within each scope, peers +are able to interact with each other directly. Each point-to-point scope contains exactly two +peers. + +--> + +## Client and server roles + +## Well-known OIDs + +OID 0, initial ref, initial oid + +## Security considerations + +### Secrecy + +### Privacy + +## Specific transport mappings + +TCP/IP + +TLS TCP/IP + +WebSockets + + +## Other kinds of medium + +Multicast/broadcast, in-memory + +## Reference: Complete schema of the protocol + +The following is a consolidated form of the definitions from the text above. + +### Protocol packets + +The authoritative +version of this schema is +[`[syndicate-protocols]/schemas/protocol.prs`](https://git.syndicate-lang.org/syndicate-lang/syndicate-protocols/src/branch/main/schemas/protocol.prs). + +```preserves-schema +version 1 . + +Packet = Turn / Error / Extension . + +Extension = < @label any @fields [any ...]> . + +Error = . + +Assertion = any . +Handle = int . +Event = Assert / Retract / Message / Sync . +Oid = int . +Turn = [TurnEvent ...]. +TurnEvent = [@oid Oid @event Event]. + +Assert = . +Retract = . +Message = . +Sync = . +``` + +### Capabilities, WireRefs, and attenuations + +The authoritative version of this schema is +[`[syndicate-protocols]/schemas/sturdy.prs`](https://git.syndicate-lang.org/syndicate-lang/syndicate-protocols/src/branch/main/schemas/sturdy.prs). + +```preserves-schema +version 1 . + +Attenuation = [Caveat ...]. + +Caveat = Rewrite / Alts . +Rewrite = . +Alts = . + +Oid = int . +WireRef = @mine [0 @oid Oid] / @yours [1 @oid Oid @attenuation Caveat ...]. + +Lit = . + +Pattern = PDiscard / PAtom / PEmbedded / PBind / PAnd / PNot / Lit / PCompound . +PDiscard = <_>. +PAtom = =Boolean / =Float / =Double / =SignedInteger / =String / =ByteString / =Symbol . +PEmbedded = =Embedded . +PBind = . +PAnd = . +PNot = . +PCompound = + / @rec + / @arr + / @dict . + +Template = TAttenuate / TRef / Lit / TCompound . +TAttenuate = . +TRef = . +TCompound = + / @rec + / @arr + / @dict . +``` + +--- + +#### Notes + +[^no-extensions-yet]: This specification does not define any extensions, but future revisions + could, for example, use extensions to perform version-negotiation. Another potential future + use could be to propagate provenance information for tracing/debugging. + +[^slightly-silly-wireref]: The syntax for `WireRef`s is slightly silly, using tuples as + quasi-records with `0` and `1` acting as quasi-labels. It would probably be better to use + real records, like `` and ``. Pros: + less cryptic. Cons: slightly more verbose on the wire. TODO: should we revise the spec in + this regard? + +[^attenuation-is-not-enforceable]: Such conditions can only ever be requests: after all, every + `yours`-capability is already completely accessible to the recipient of the packet. + Similarly, it does not make sense to include an attenuation description on a + `my`-capability. However, in every case, if a party wishes to *enforce* an attenuation on a + `my`- or `yours`-capability, it may record the attenuation against the underlying + capability internally, issuing to its peers a fresh `my`-capability denoting the attenuated + capability. + +[^caveat-terminology-macaroon]: This terminology, "caveat", is lifted from the excellent paper + on [Macaroons](./glossary.md#macaroon), where it is used to describe a more general + mechanism. Future versions of this specification may opt to include some of this + generality. diff --git a/src/theory/index.md b/src/theory/index.md new file mode 100644 index 0000000..1774617 --- /dev/null +++ b/src/theory/index.md @@ -0,0 +1,5 @@ +# Specifications and Theory + +TODO: links + +[Protocol](../protocol.md)