-
Notifications
You must be signed in to change notification settings - Fork 102
Capability theory in Pact
Definition of standard capability sc of domain d, which is the name of the defcap whose parameters are P and defines the predicate/"guard" function g, which can compose/"import" other capabilities CI.
For managed capability mc, it has all the features of c, plus it can decompose P into free or "identifying" variables that further inform its type, and bound or "quantifying" variables that are computed in the manager function m:
"Module admin" describes a privilege escalation that is specified by the module declaration itself, either as keyset-based or governance-based, the latter requiring specification of a defcap to guard module upgrade.
Module admin capability mm has a special type a, is parameterized by the module name n, cannot be managed, allows composition, and specifies either guard function g or keyset k.
In practice, managed capabilities are uniform with standard capabilities with only the presence of m to differentiate them, with the operational suggestion that m should match on PF and compute on PB. Module admin remains its own subtype.
c :: a = (n, g, CI)
If m is populated in c d, the capability is considered "managed".
The defcap special form plays two roles: it resembles a standard defun with a name, arguments and a body, which serves to implement the guard function g, but it also specifies a "capability reference" that uniquely identifies some inhabitant of d parameterized by P.
When a defcap is used for module governance, it specifies g only, as the module name n is inferred.
The defcap construction operates as a constructor of a capability reference c* d:
defcap also defines the lambda function g operating on environment E. In addition to validating whatever is directly required to acquire the capability, it can "compose" or import other capabilities CI. Lastly it is pure in that it cannot update database state.
As such, g has the same shape as Pact's operation enforce-guard :: guard -> E -> Either Error (). We remark that g is therefore "both an enforcement and definintion of a guard".
Capabilities are collected in slots, which are scoped to indicate their operational semantics. The slot s stores the reference c* d, scope o, and any composed capability slots SI.
Managed capabilities are said to be "installed" as they can only be constructed and evaluated once. They are mutated by m when code requests a capability of matching domain d, described later.
Stack capabilities are said to be "acquired" by user code, and are scoped/managed by the call-stack at acquisition time.
A composed capability inherits the scope of the composing/parent capability and its slot inhabits parent CI.
For a given domain d, the manager function takes the parameters of a managed capability PM and those of a requested stack capability PS, which on success returns updated params for the managed capability P'M. The function is a pure function that is not intended to consider the environment, although this is not forbidden operationally.
NB the ideal presentation is PMB -> PSB -> Either Error P'MB, where match has occurred on the free parameters.
Signers/witnesses are associated with capability references as a map W from the witness w to the associated capability references C*w.
The runtime R stores two sets of capability slots, Managed (SM) and Acquired (SA), the map of signer witnesses W, and a collection to track "seen" managed capabilities _C*M.
SA operates as a stack in keeping with the callstack-scope of with-capability.
Operationally, it also accumulates pending capabilities as a stack, to properly handle nested composition, and secure in Pact's terminating design that a failure means the stack being slightly inaccurate during capability acquisition is of no consequence.
Post-validation, the stack is pruned as needed:
- composed are popped and installed into parent SI;
- managed are popped and inserted into SM;
- acquired are left on the stack. After body is executed, the stack is blindly popped.
Managed capabilities are said to be installed by one of two mechanisms: install-capability or automatically when specified in W. Only managed capabilities can be installed, so non-managed capabilities in W are ignored.
Reference c*M d is either specified in the install-capability call or already constructed in W.
Managed capabilities are tracked in runtime C*M with their initially-installed parameterizations to prevent duplicate installs. If this is found, no action is taken.
c*M d is added to C*M for dupe install tracking.
Newly-installed references execute g to validate install. Composed capabilities are added to SI as normal, but are not "manageable" themselves.
A new slot containing c*M d is added to SM.
Managed capability stays in SM for the entire transaction, although it mutates per the manager function. The tracked reference in C*M is never mutated.
The with-capability special form attempts to acquire a stack-scoped or acquired capability, which upon success executes
a contained body form.
The first argument of with-capability applies the defcap as a constructor to create reference cA* d.
If a slot with c*A d is already in SA, control returns to the body form with no action.
SM is scanned for any managed slots for references of the same domain d. For each, the associated manager function m is executed. The first to succeed wins. Order of execution is the natural order of the capability references.
NB: Ideally, it should be tested for an exact match on (d, PF) as only one match should be possible, and that one m function executed.
For the installed capability cM* d, and the requested stack capability to acquire cA* d, the manager function is invoked, which upon success produces c'M* d.
The slot for cM* d is replaced with the c'M* d result from the manager function. Composed capabilities (SI) in cM* d are "copied" into SI in the requested capability slot.
In a situation where a capability slot of matching domain d was found but none succeeded, the acquire operation fails.
If d is managed but nothing was installed for d, acquire fails.
If d is not managed, g is executed to validate acquisition.
If m or g succeeds, a new slot containing c*A d is added to SA, and the body is executed.
Once the body of with-capability terminates, the slot for c*A d is popped off of SA and terminates, along with any composed capabilities in SI.
Import, via compose-capability can only occur in g, so there is always a "parent" capability slot ready to receive the capability in CI.
The first argument of compose-capability applies the defcap as a constructor to create reference cI* d.
The procedure from here on out is identical to a stack/acquired capability, with the exception that on success no body form is executed, and failure causes the parent to fail as well.
Install cI* d parent CI.
Composed capabilities go out of scope/terminate with their parent capability.
require-capability looks for specified reference cR* d in SA, including any composed capabilities. As such it does not modify R so is safe to use anywhere. Also, it does not check SM, which means that acquired capabilities are the only actual "enforcement" mechanism, as possibly managed by caps in SM.
When enforce-keyset is invoked, matching signer witnesses are included if and only if a capability in C*W is "in scope", which is anywhere in SM or SA including all composed capabilities, as well as any "pending" capabilities "coming into scope".
Note that since managed capabilities can only be installed once, those installed by dint of being in W are only validated against specified witnesses in W once. Thus, specifying a managed capability for w ensures that w will only be "used once".
A module admin capability m a is an automatically acquired and managed capability such that acquisition results in automatic install and the capability effectively remains in scope for the rest of the transaction.
Module admin is automatic in the following scenarios:
- Module upgrade.
- Direct access to module tables.
- Invocation of a module guard outside of module code.
Reference c* an is constructed. If a slot is already installed, acquisition is trivially successful (ie, a trivial m function). If not, a new slot for c* an is constructed, and guard is tested.
For keysets, this is simply enforcing the keyset. For governance function g, the function is evaluated.
On success, slot for c* an is installed (added to SM) and acquired (pushed onto SA). The capability reference is also added to "seen" collection C*M.
Currently there is no way to manually acquire module admin. Whether the mechanism is keyset or cap-based governance, while it is possible to replicate governance in a separate capability, it is currently impossible to directly reference module admin in code.
TODO without this, there is no way to bind a signer to module admin, so a key with some other capability won't match this test. It is possible that the syntax for caps in W should admit a special syntax for indicating c* an, namely the bare module name. This could also suffice for other uses needing a module admin reference.
Management of module admin simply allows the capability to come into scope anytime after first acquisition.
Given the extreme power of module admin, it appears alarming that its scope is so lenient. However the rationale is to give module administrators the most power to perform tasks like data migration and threat mitigation, namely by directly accessing database tables outside of module code. Also, module governance is potentially expensive to grant, as in decentralized cases involving tallying votes in the database, so not making this grant sticky can result in prohibitive performance or gas usage by re-acquiring the capability.
Any attempt to allow extra-module code to have a mechanism to acquire module admin manually makes it possible for third-party code to do so as well. Conversely, requiring all administrator code to reside in the module burdens the module author with properly securing those functions with module admin, which as noted above is impossible currently, requiring duplicate methods.
We note that third-party exploits of module admin are very hard to pull off, and indeed can only happen if the admin transaction calls into third-party code which is ready to enact the exploit (which would fail in any normal transaction and draw attention to itself, as there is no way to detect that module admin is acquired).
Finally, this firmly sounds the alarm that putting module-admin credentials in a transaction is a highly sensitive operation which should not call 3rd party code if it can help it, and instead wait for a safe transaction in which to do so.
Pact code is guaranteed to terminate by
- not allowing anonymous lambdas -- all lambdas must be declared in module code
- resolving all references at module load, failing on any cycle
However, there are two cases where a module can execute "dynamic" code that has not been previously resolved at runtime:
-
Keyset predicate evaluation. Custom keyset predicates are stored as a bare string and evaluated in
enforce-keysetas an application of the indicated function. - User guard evaluation. User guards can be read from the database or constructed externally, and are evaluated by-name as the application of the indicated function.
In both cases, they are run in a special context that tests the call stack for a repeated occurrence of the application function name, and fails if found.
Thus Pact enforces termination in all cases.
The guard function g, when evaluated, runs as a "normal" application of d as a function with P for arguments. The invariants for safe execution of this function are:
Generally this is implied by being a "normal" application in a module, thus as standard Pact module code.
The ability to bring a capability into scope, either managed or call-stack, is restricted to in-module code only.
For acquisition, this guarantees that any state-mutating code guarded by with-capability cannot escape the confines of the declaring module. Otherwise, the authority granted by the capability is unknowable.
For installation, this ensures that the scenarios in which a managed capability is installed are only:
- Module code controlled by the author
- Installation via inclusion in W.
#2 is essential as it allows the end-user who might be affected by the capability to control how and if it is installed. Obviously, #2 will fail if for some reason this install cannot be achieved.
As "unscoped" capabilities, the goal here is to prevent a capability from being installed by untrusted code. Having said that, examples of safe usages of #1 are not known at this time, but the in-module restriction means that if one emerges, it's possible, and otherwise module authors can simply avoid it. (It is also useful for testing to install capabilities by acquiring module admin).
Acquire or install of c* d both change the state of R:
- acquire pushes a slot for c* d onto _SA.
- install adds a slot for c* d to SM and adds c* d to "seen" C*M.
If during this operation, a nested acquire or install were to happen:
- A nested install within an outer acquire would violate the scope implied by the outer acquire, as the nested install would persist after the outer acquire goes out of scope.
- A nested install within an outer install has no obvious defects.
- A nested acquire in an outer acquire would allow protected state-mutating activity scoped by the nested acquire to occur, while we were trying to see if we can acquire the outer capability, presumably guarding some other state-mutating activity. Reasoning about state in this scenario is unsatisfying at a minimum and possibly incoherent. It is if nothing else inelegant, although the stack scope would probably be unharmed.
- A nested acquire within an outer install has the same concerns as #2 about executing some state-modifying activity in the body of the install.
Since some issue above applies in either nested install (#1) or acquire (#3, #4), install and acquire are prevented while executing g. This is accomplished by testing for a defcap in the call stack when either install-capability or require-capability are invoked.
Obviously, this is what compose-capability is for, importing some other capability into the scope of the outer capability. compose-capability has the reverse invariant that it can only be invoked within a defcap execution, using the same call-stack-checking mechanism.
require-capability does not affect R, as it simply fails if it does not find the indicated capability in SA. It also does not mutate state.
It is therefore safe in any context, acquire or install, as requiring within g does not produce any unwanted effects. It is more logical to compose instead of require in g, but it is otherwise harmless, and there are perhaps scenarios where testing without acquiring is correct. Plus as we will see, require is useful in user guards, which may be tested in the context of g.
This is a happy conclusion, as requiring capabilities in user guards are useful for certain scenarios, like allowing modules to pay gas for some external user: the external user can indicate some account that is controlled by a user guard that tests for a capability in the foreign module, which has been installed by the external user in W.
As noted above, there are two places where code is dynamically evaluated. While user guards are the more relevant case, anything said about user guards can easily apply to keyset predicates, as they execute in identical contexts:
- The evaluation context is pure, which means the code cannot mutate state.
- As noted above, termination is operationally guaranteed.
As acquire and install cause execution of g, they are unsafe in dynamic code:
-
Unsafe failures due to purity violations. Dynamic code is run in a pure context, whereas g is not thus restricted. The outer context of dynamic execution will cause impure code in g to fail.
-
Unsafe failures if evaluated in g. If g tests a user guard or keyset predicate that attempts to acquire or install, the dynamic code will fail due to the restrictions above on acquire or install in g.
TODO: this is not enforced currently. Dynamic code should be noted as such in the call stack, so that it can be detected and always fail upon embedded acquire or install.
Note that here, "unsafe" refers to a slightly different notion of safety which we will call "semantic safety": an unexpected failure in dynamic code renders the intention of the dynamic code inoperable, in a way that would otherwise be undetectable during module load and potentially testing. In other words, the real safety here is totality, where the cases of the dynamic code failing are feasible to enumerate.
This note is here because "safety" when talking about capabilities often refers to avoiding exploits like privilege escalation. In this context it is more about having total semantics for a user guard or keyset predicate.
For the same reasons that require is safe in g, it is safe in dynamic code:
- Purity is ensured, as require is pure and without any effects on the capability state.
- Termination and "semantic safety" are ensured, as g is never invoked when requiring.
None of the enforcements in this section are currently detected at compile time, as there is no type-level representation of capabilities to guide it; while Pact's compilation could detect immediate violations, it cannot detect violations in linked code, even if it is in the same module. Therefore it is not currently possible to do this.
Instead, runtime guarantees ensure that simple coverage of impacted code will immediately cause failure if these invariants are violated.