Skip to content

feat: add capability prescripts — LoggedCap (audit trail) and DualKey#40

Merged
bordumb merged 1 commit intomainfrom
dev-auditability
Mar 22, 2026
Merged

feat: add capability prescripts — LoggedCap (audit trail) and DualKey#40
bordumb merged 1 commit intomainfrom
dev-auditability

Conversation

@bordumb
Copy link
Copy Markdown
Collaborator

@bordumb bordumb commented Mar 22, 2026

Primarily following from these papers:

Saltzer & Schroeder (1975), specifically two design principles:

LoggedCap implements Design Principle #8: Compromise Recording — "mechanisms that reliably record that a compromise of information has occurred can be used in place of more elaborate mechanisms that completely prevent loss." The paper notes that "many computer systems record the date and time of the most recent use of each file. If this record is tamperproof and reported to the owner, it may help discover unauthorized use." LoggedCap does this — append-only, tamper-resistant (no clear() or remove() methods), records timestamp + permission + outcome for every exercise.

DualKeyCap implements Design Principle #5: Separation of Privilege — "a protection mechanism that requires two keys to unlock it is more robust and flexible than one that allows access to the presenter of only a single key." The paper gives the nuclear launch example: "two different people both give the correct command." ApproverA and ApproverB being !Clone move-only handles enforces that once distributed, no single holder can approve both sides.

Both types also implement the paper's prescript concept (Section II.C.4) — "a rule that must be followed before access to an object is permitted, thereby introducing an opportunity for human judgment." The paper lists five prescript actions: (1) no action, (2) audit trail logging, (3) cooling-off delay, (4) buddy system approval, (5) external authorization signal. LoggedCap is prescript #2, DualKeyCap is prescript #4.

Secondary connections:

  • Dennis & Van Horn (1966): The try_cap() interposition pattern mirrors their supervisor-mediated capability exercise — all capability operations pass through a validation gate before granting access. Cap::new() being pub(crate) is the software analog of their hardware-enforced capability creation.
  • Melicher et al. (2017): The !Has<P> design on both types preserves Wyvern's non-transitive authority property — holding a LoggedCap<FsRead> does not give you the same authority as holding a Cap<FsRead>, because you must go through the fallible try_cap() gate. This is the "caretaker" pattern from the object-capability literature that Melicher formalizes.

@bordumb bordumb self-assigned this Mar 22, 2026
@bordumb bordumb merged commit 29dbc9b into main Mar 22, 2026
6 checks passed
@bordumb bordumb deleted the dev-auditability branch March 22, 2026 16:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant