---
policy-version: 2
---
# Overview
This is Aranya's default policy. It provides the rules that underlie
Aranya's role-based access functionality. It also controls access
to AFC through these RBAC mechanisms.
As a reminder, Aranya policy files use the [literate programming][lp]
paradigm, so this document is both a specification and source code. Code
blocks with the `policy` tag are interpreted by the policy compiler as
policy source code. For more information see Aranya's [policy language
documentation][policy-lang].
## Quick Reference
This policy implements a zero-trust RBAC system that controls
which commands devices can publish to Aranya's distributed graph:
- **Devices** are the primary identity, each containing cryptographic
key pairs for identity, signing, and encryption.
- **Teams** provide the organizational boundary, with exactly one
team per graph. Only devices added to the team can access the
commands published to the team's graph.
- **Roles** control command permissions. Currently we expose a set of
"default roles" - `owner` (emergency access), `admin` (system
administration), `operator` (user management), and `member` (basic
usage). This policy has the capability to define custom roles as well.
- **Rank** is an attribute associated with each object that determines whether a higher ranked object can operate on a lower ranked object.
Any object in the system with an Aranya ID can have a rank associated with it in the policy.
Rank checks are only concerned with ranks associated with devices, roles, and labels specifically when determining if an object has permission to perform certain operations.
The team does not need a rank associated with it since all operations implicitly occur within the context of a team.
## Security Properties
- **Confidentiality** is not a property of the Aranya graph or policy itself. Confidentially is currently enforced with PSKs in the QUIC syncer implementation with plans to migrate to mTLS certificates in the future.
- **Integrity** is enforced by cryptographic hashes of commands added to the Aranya graph.
- **Authorization** is determined by whether an object has permission to perform the operation and outranks the target object(s).
- **Non-Repudiation** graph commands are signed by the device that publishes them allowing the command author to be verified.
- **No Self-Administration**: Devices cannot assign roles or labels to
themselves. This is enforced by rank-based authorization since a device
cannot outrank itself (strict `>` comparison).
# Policy
## What This Policy Controls
This policy defines:
- Which commands each device/role is authorized to publish to the graph
- Which objects are allowed to operate on other objects in the system based on their respective ranks
- How those commands transform facts in the local database
- Validation rules that commands must pass before acceptance
This policy does NOT control:
- Network access or transport layer security
- How devices synchronize the graph (handled by Aranya core)
- Query authorization (queries read local derived state)
## Conventions
Commands are generated by all participating peers, so everything in the
`fields` sections of a command should be considered attacker-controlled
data. Commands must validate the data in some way before using it.
### Query APIs
Policy language v2 does not support directly querying the internal fact
database, so the implementation of the query APIs defined in this
document are a little peculiar.
As background, Aranya supports ephemeral "off graph" commands.
These commands generally function the same as regular "on graph"
commands, except that they are not persisted (added to the graph)
after being evaluated.
The query APIs defined in this document use ephemeral commands
that read data from the fact database and emit effects with the
results. Query APIs that need to logically return lists use
`map` in the `action` to publish an ephemeral command per list
item.
Query APIs must still call `check team_exists()` to ensure that
data for closed teams is not returned.
By convention, the actions, commands, and effects used in queries are
prefixed with "query". e.g. `action query_foo()`, `command QueryFoo`,
and `effect QueryFooResult`.
## Imports
```policy
use afc
use crypto
use device
use envelope
use idam
use perspective
```
- [`afc`][afc-ffi]: [AFC][afc] functionality, such as creating
channels.
- [`crypto`][crypto-ffi]: core cryptographic functionality, like
command signing and verification.
- [`device`][device-ffi]: provides information about the current
device.
- [`envelope`][evp-ffi]: provides access to the special
[`Envelope`][envelope] type.
- [`idam`][idam-ffi]: IDAM functionality, such as access to device
keys.
- [`perspective`][perspective-ffi]: provides information about
the current perspective.
## Policy Basics
An [_action_][actions] is a function that is callable from the
application. Actions can perform data transformations and publish
zero or more _commands_ to the graph. Actions generally require
certain RBAC permissions; see the RBAC section for more
information.
An [_effect_][effects] is a special type of struct that sends
data back to the application and can be thought of as the
_output_ of an action.
A [_fact_][facts] is structured data derived from a _command_.
Facts are stored in a _fact database_, which the policy consults
when making enforcement decisions. Since the graph is a CRDT, all
devices eventually have identical fact databases.
A [_command_][commands] is a signed data structure that devices
publish to the graph. Commands are signed with the device's
Signing Key. The policy controls which commands each device is
authorized to publish.
## Command Priorities
Priorities can be defined for commands by specifying the `priority`
attribute in the command's `attributes` block:
```
command CommandFoo {
attributes {
priority: 100
}
}
```
Branches in the graph are deterministically ordered by the braid algorithm. Higher priority commands are generally evaluated before lower priority commands.
CreateTeam is the first command (a.k.a. the init command), so it doesn't need an assigned priority.
CreateTeam is automatically the highest priority based on ancestry.
In general, deletion and revocation commands should be higher priority than create/modify/use commands. E.g.:
TerminateTeam(500) -> DeleteFoo(400) -> RevokeFoo(300) -> CreateFoo(200) -> UseFoo(100)
Commands that must be called first should have a higher priority than commands that depend on them.
For example, a command to create/assign a label to a device should be higher priority than a command that uses the label.
Delete*, Revoke*, Terminate*, Remove*, etc. commands must have a higher priority assigned to them since they occur later in the braid, but must take precedence over other commands that modify the state of the object.
For example, deleting a label should be higher priority than assigning a label to a device because if the label doesn't exist, operations with the label are invalid.
Command priorities will be required to be defined for each command in the policy. Even the zero priority should be defined. That way, the policy can be audited and does not have any default priorities that cannot be audited.
Ephemeral commands do not need to specify a priority since they do not participate in braiding.
While we could assign sequential priorities (0, 1, 2, ...) to commands to achieve the desired prioritization, this doesn't leave any room for adding new priorities in between priorities that were already defined.
Therefore, initial priorities are defined with room between them for new priorities to be added later. E.g.:
100, 200, 300, etc.
Command priority levels:
| 500 | Terminate | TerminateTeam | Highest priority - team termination takes precedence over all operations |
| 400 | Delete/Remove | DeleteRole, DeleteLabel, RemoveDevice | Deletions and removals must take precedence to prevent operating on deleted objects |
| 300 | Revoke | RevokeRole, RevokeLabelFromDevice, RemovePermFromRole | Revocations must take precedence over assignments to prevent use of revoked privileges |
| 200 | Create | CreateRole, SetupDefaultRole, CreateLabel | Creations must complete before dependent use/assign operations |
| 100 | Use/Assign/Modify | AssignRole, ChangeRole, AssignLabelToDevice, AddDevice, AddPermToRole, ChangeRank | Low priority - depends on objects existing first |
| 0 | Init/Ephemeral | CreateTeam, QueryDevicesOnTeam, QueryAfcChannelIsValid, QueryDeviceRole, QueryDeviceKeyBundle, QueryRank, QueryTeamRoles, QueryRoleHasPerm, QueryRolePerms, QueryLabel, QueryLabels, QueryLabelsAssignedToDevice, AfcCreateUniChannel | Init command evaluated first by ancestry; ephemeral commands don't participate in braiding |
### API Stability and Backward Compatibility
Actions and effects are part of a policy's public API.
Facts and commands are *not* part of a policy's public API.
### Fact Schema Constraints
Fact definitions enforce uniqueness constraints through their key
structure:
- **Single-key facts** (e.g., `Fact[a id]`) allow
exactly one fact per key value.
- **Composite-key facts** (e.g., `Fact[a id, b id]`)
allow exactly one fact per key combination.
- **Empty-key facts** (e.g., `TeamStart[]`) allow exactly one
instance, implementing a singleton pattern.
These constraints are enforced at the storage layer - `create`
operations fail if a fact already exists with the same key, and
`delete` operations fail if the fact doesn't exist.
## Base Cryptography
All commands (except for `CreateTeam`) are signed and verified
with the following routes.
```policy
// Signs the payload using the current device's Device Signing
// Key, then packages the data and signature into an `Envelope`.
function seal_command(payload bytes) struct Envelope {
let parent_id = perspective::head_id()
let author_id = device::current_device_id()
let author_sign_pk = check_unwrap query DeviceSignPubKey[device_id: author_id]
let author_sign_key_id = idam::derive_sign_key_id(author_sign_pk.key)
let signed = crypto::sign(author_sign_key_id, payload)
return envelope::new(
parent_id,
author_id,
signed.command_id,
signed.signature,
payload,
)
}
// Opens an envelope using the author's public Device Signing
// Key.
//
// If verification succeeds, it returns the serialized basic
// command data. Otherwise, if verification fails, it raises
// a check error.
function open_envelope(sealed_envelope struct Envelope) bytes {
let author_id = envelope::author_id(sealed_envelope)
let author_sign_pk = check_unwrap query DeviceSignPubKey[device_id: author_id]
let verified_command = crypto::verify(
author_sign_pk.key,
envelope::parent_id(sealed_envelope),
envelope::payload(sealed_envelope),
envelope::command_id(sealed_envelope),
envelope::signature(sealed_envelope),
)
return verified_command
}
```
## Devices and Identity
An identity in Aranya is called a _device_. Each device has
a globally unique ID, called the _device ID_.
A device can have up to one role associated with it which grants the device a set of permissions.
A device can operate on other objects within the system as long as it has the proper permission via its role and outranks the target objects it wishes to operate on.
```policy
// Records the existence of a device.
fact Device[device_id id]=>{}
// Reports whether the invariants for the device are being upheld.
function valid_device_invariants(device_id id) bool {
let device = query Device[device_id: device_id]
if device is None {
// The device does not exist, so there should not be any
// signing keys for it either.
check !exists DeviceIdentPubKey[device_id: device_id]
check !exists DeviceSignPubKey[device_id: device_id]
check !exists DeviceEncPubKey[device_id: device_id]
} else {
// The device DOES exist, so the device keys MUST also exist.
check exists DeviceIdentPubKey[device_id: device_id]
check exists DeviceSignPubKey[device_id: device_id]
check exists DeviceEncPubKey[device_id: device_id]
}
// NB: Since this function uses `check` internally, it
// doesn't need a return type. But policy v2 `function`s
// *must* have a return type, so we return `true` here.
//
// We could use early returns to make this function have
// a meaningful result, but that would obscure which
// invariant was violated. We would only know that
// `valid_device_invariants` failed, not that (for example)
// `check exists DeviceIdentPubKey[...]` failed.
return true
}
```
### Device Keys
A device has three key pairs, called the _device keys_. Each key
pair has a globally unique ID derived from the public half of the
pair.
#### Device Identity Key
The Device Identity Key is a signing key that identifies the
device. Devices use this key to sign administrative actions, like
rotating their other device keys.
A device's ID is derived from the public half of the Device
Identity Key.
```policy
// Records the public half of a device's Identity Key.
fact DeviceIdentPubKey[device_id id]=>{key bytes}
```
#### Device Signing Key
The Device Signing Key is a signing key used to sign commands
that the device publishes to the graph.
```policy
// Records the public half of the device's Signing Key.
fact DeviceSignPubKey[device_id id]=>{key bytes}
```
#### Device Encryption Key
The Device Encryption Key is a KEM key used to securely send
encapsulated secret keys to other devices. It is primarily used to securely transmit encapsulated secret keys for AFC channels.
```policy
// Records the public half of the device's Encryption Key.
fact DeviceEncPubKey[device_id id]=>{key bytes}
```
### Device Functions
```policy
// Returns a device if one exists, or `None` otherwise.
function try_find_device(device_id id) optional struct Device {
// This function is a little too expensive to call every
// time we need to get a device, so this is only checked
// during debugging/developing by debug_assert().
//
// In the future we'll be able to catch these invariant
// violations in a more efficient manner. For example, the
// policy compiler will be able to check for invariants like
// "If fact A exists then so should fact B", internal
// consistency checks (at the storage layer?) will be able
// to check for corrupted records, etc.
//
debug_assert(valid_device_invariants(device_id))
return query Device[device_id: device_id]
}
// Returns a device if it exists, or raises a check error
// otherwise.
function get_device(device_id id) struct Device {
return check_unwrap try_find_device(device_id)
}
// Returns the device corresponding with the author of the
// envelope.
function get_author(evp struct Envelope) struct Device {
return get_device(envelope::author_id(evp))
}
// Collection of public Device Keys for a device.
struct PublicKeyBundle {
ident_key bytes,
sign_key bytes,
enc_key bytes,
}
// Returns the device's public key bundle.
//
// # Caveats
//
// This function does not directly check whether the device
// exists. However, device management preserves the invariants
// between devices and keys so it would be a very significant
// violation if a device's key existed without the device also
// existing. See `valid_device_invariants`.
function get_device_public_key_bundle(device_id id) struct PublicKeyBundle {
// This function is a little too expensive to call every
// time we need to get a device, so only uncomment this when
// debugging/developing.
//
// See the comment in `try_find_device`.
//
debug_assert(valid_device_invariants(device_id))
let ident_key = check_unwrap query DeviceIdentPubKey[device_id: device_id]
let sign_key = check_unwrap query DeviceSignPubKey[device_id: device_id]
let enc_key = check_unwrap query DeviceEncPubKey[device_id: device_id]
return PublicKeyBundle {
ident_key: ident_key.key,
sign_key: sign_key.key,
enc_key: enc_key.key,
}
}
// Returns the device's encoded public Encryption Key.
//
// # Caveats
//
// This function does not directly check whether the device
// exists. However, it would be a very significant invariant
// violation if a device's key existed without the device also
// existing. See `valid_device_invariants`.
function get_enc_pk(device_id id) bytes {
// This function is a little too expensive to call every
// time we need to get a device, so it is only checked during
// debugging/developing.
//
// See the comment in `try_find_device`.
//
debug_assert(valid_device_invariants(device_id))
let device_enc_pk = check_unwrap query DeviceEncPubKey[device_id: device_id]
return device_enc_pk.key
}
// Returns the device's encryption key ID.
function get_enc_key_id(device_id id) id {
let device_enc_pk = check_unwrap query DeviceEncPubKey[device_id: device_id]
return idam::derive_enc_key_id(device_enc_pk.key)
}
```
### Device Generations
Each device has a _generation_, which is monotonically
incremented each time the device is removed from the team.
```policy
// Tracks the current logical generation for a device.
//
// Each time a device is removed from the team, its generation is
// bumped so that stale per-device state (for example, direct
// label assignments) becomes invalid.
//
// This fact persists across device removals so a re-added device
// starts with the latest generation number.
//
// # Foreign Keys
//
// - `device_id` refers to the `Device` fact
fact DeviceGeneration[device_id id]=>{generation int}
// Returns the device's current generation counter.
// # Caveats
//
// - It does NOT check whether the device exists.
//
// # Errors
//
// Raises a check error if the generation fact does not exist.
function get_device_gen(device_id id) int {
let f = check_unwrap query DeviceGeneration[device_id: device_id]
return f.generation
}
```
### Device Queries
Device queries retrieve information about devices on the team.
See [Query APIs](#query-apis) for more information about the query
APIs.
#### `query_devices_on_team`
Returns all devices on the team.
```policy
// Emits `QueryDevicesOnTeamResult` for each device on the team.
ephemeral action query_devices_on_team() {
// Publishing `QueryDevicesOnTeam` emits
// `QueryDevicesOnTeamResult`.
map Device[device_id: ?] as f {
publish QueryDevicesOnTeam {
device_id: f.device_id
}
}
}
// Emitted when a device is queried by `query_devices_on_team`.
effect QueryDevicesOnTeamResult {
// The ID of a device on the team.
device_id id,
}
// A trampoline that forwards `device_id` to the effect.
ephemeral command QueryDevicesOnTeam {
fields {
device_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
finish {
emit QueryDevicesOnTeamResult {
device_id: this.device_id,
}
}
}
}
```
#### `query_valid_afc_channel`
Returns whether an AFC channel is valid.
```policy
// Emits `QueryAfcChannelIsValid` indicating whether the specified AFC channel is valid.
ephemeral action query_afc_channel_is_valid(sender_id id, receiver_id id, label_id id) {
// Publishing `QueryAfcChannelIsValid` emits
// `QueryAfcChannelIsValidResult`.
publish QueryAfcChannelIsValid {
sender_id: sender_id,
receiver_id: receiver_id,
label_id: label_id,
}
}
// Emitted when an AFC channel is queried by `query_afc_channel_is_valid`.
effect QueryAfcChannelIsValidResult {
// The ID of the sender device.
sender_id id,
// The ID of the receiver device.
receiver_id id,
// The ID of the label.
label_id id,
// Whether the AFC channel is valid.
is_valid bool,
}
// Returns a `QueryAfcChannelIsValidResult` effect indicating whether the AFC channel is valid.
ephemeral command QueryAfcChannelIsValid {
fields {
// The ID of the sender device.
sender_id id,
// The ID of the receiver device.
receiver_id id,
// The ID of the label.
label_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
// Check that both devices have permission to create the AFC channel.
let is_valid = afc_uni_channel_is_valid(this.sender_id, this.receiver_id, this.label_id)
finish {
// TODO: substruct selection from `this`
emit QueryAfcChannelIsValidResult {
sender_id: this.sender_id,
receiver_id: this.receiver_id,
label_id: this.label_id,
is_valid: is_valid
}
}
}
}
```
#### `query_device_role`
Returns the role assigned to a device.
```policy
// Emits `QueryDeviceRoleResult` if a role is assigned to the
// device.
// If the device does not have a role assigned to it, then no effect is emitted.
ephemeral action query_device_role(device_id id) {
publish QueryDeviceRole {
device_id: device_id,
}
}
// Emitted when a device's role is queried by
// `query_device_role`. This is the same structure as the
// `Role` fact.
effect QueryDeviceRoleResult {
// The role's ID.
role_id id,
// The role's name.
name string,
// The ID of the device that created the role.
author_id id,
// Is this a default role?
default bool,
}
ephemeral command QueryDeviceRole {
fields {
device_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let device = get_device(this.device_id)
let assigned_role = try_get_assigned_role(device.device_id)
if assigned_role is None {
finish {}
} else {
let role = unwrap assigned_role
let eff = role as QueryDeviceRoleResult
finish {
emit eff
}
}
}
}
```
### `query_device_public_key_bundle`
Returns a device's `PublicKeyBundle`.
```policy
// Emits `QueryDeviceKeyBundleResult` with the device's key
// bundle.
ephemeral action query_device_public_key_bundle(device_id id) {
publish QueryDeviceKeyBundle {
device_id: device_id,
}
}
// Emitted when a device's public key bundle is queried by
// `query_device_public_key_bundle`.
effect QueryDeviceKeyBundleResult {
// NB: We don't include the device ID here since the caller
// must already know it as it was provided to the action.
device_keys struct PublicKeyBundle,
}
ephemeral command QueryDeviceKeyBundle {
fields {
// The device whose key bundle is being queried.
device_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
// NB: A device's keys exist iff `fact Device` exists, so
// we don't need to use `get_device` or anything
// like that.
let device_keys = get_device_public_key_bundle(this.device_id)
finish {
emit QueryDeviceKeyBundleResult {
device_keys: device_keys,
}
}
}
}
```
## Object Rank
### Overview
Any object with an Aranya ID can have a rank associated with it in the Aranya policy.
Devices, roles, and labels are assigned a rank at the time of creation.
Afterwards, their rank can be modified with the `ChangeRank` command.
The team object does not need a rank associated with it since all operations are implicitly performed in the context of a team.
The highest rank is i64::MAX while the lowest rank is 0.
Objects with higher rank are allowed to operate on objects with a lower rank.
The ranking system is used to ensure that all objects and operations abide by an application-defined hierarchy. The hierarchy can be audited by ensuring that numerical rank values fall into the expected hierarchical levels.
Lower ranked objects are guaranteed to not have permission to operate on higher ranked objects.
For example, a command author with rank 10 would be allowed to assign a label of rank 5 to a device of rank 4 because both of the objects it is operating on are lower rank than the author of the command.
It is recommended to never grant a role of lower rank a permission that a device of higher rank does not have (see [Privilege Escalation Attempt Scenario 2](#Privilege-Escalation-Attempt-Scenario-2)). If this scenario were to occur, the device of higher rank could onboard a pawn device to the team and assign the higher privilege but lower rank role to the pawn device in order to escalate its own privileges.
### Default Hierarchy
When a team is created, the default ranks are:
| Creator Device | `DEFAULT_OWNER_DEVICE_RANK` (1,000,000) |
| Owner Role | `DEFAULT_OWNER_ROLE_RANK` (999,999) |
| Admin Role | `DEFAULT_ADMIN_ROLE_RANK` (800) |
| Operator Role | `DEFAULT_OPERATOR_ROLE_RANK` (700) |
| Member Role | `DEFAULT_MEMBER_ROLE_RANK` (600) |
Note: The owner device intentionally outranks its own role. This is a special case because the owner is a superuser and needs to be able to modify the owner role's permissions. For all other roles, `role_rank > device_rank` is enforced during role assignment.
### Rank Examples
#### Example 1: Simple Role Assignment (3 objects)
**Scenario:** Admin device assigns Member role to a new device.
```
Admin Device (rank 800) → assigns → Member Role (rank 600) to New Device (rank 500)
```
**Checks:**
1. Admin outranks Member Role: 800 > 600 ✓
2. Admin outranks New Device: 800 > 500 ✓
3. Member Role rank >= New Device rank: 600 >= 500 ✓
**Result:** Allowed
#### Example 2: Label Assignment (3 objects)
**Scenario:** Operator assigns a label to a device.
```
Operator Device (rank 700) → assigns → Label (rank 400) → to → Target Device (rank 300)
```
**Checks:**
1. Operator outranks Label: 700 > 400 ✓
2. Operator outranks Target Device: 700 > 300 ✓
**Result:** Allowed
#### Example 3: Failed Operation - Equal Rank
**Scenario:** Device tries to modify another device of equal rank.
```
Device A (rank 500) → tries to assign label to → Device B (rank 500)
```
**Checks:**
1. Device A outranks Device B: 500 > 500 ✗
**Result:** Denied (strict `>` comparison required)
#### Example 4: Self-Administration Prevention
**Scenario:** Device tries to upgrade its own rank.
```
Device (rank 500) → tries to change own rank to → 600
```
**Checks:**
1. Device rank >= new rank: 500 >= 600 ✗
**Result:** Denied (prevents self-promotion)
#### Example 5: Privilege Escalation Prevention (3+ objects)
**Scenario:** Malicious device tries to escalate privileges via a pawn device.
```
Malicious Device (rank 500)
→ onboards Pawn Device (rank 400)
→ tries to assign High-Privilege Role (rank 600) to Pawn
```
**Checks:**
1. Malicious outranks Pawn: 500 > 400 ✓
2. Malicious outranks High-Privilege Role: 500 > 600 ✗
**Result:** Denied (device cannot assign roles that outrank it)
#### Example 6: Role-Device Rank Constraint
**Scenario:** Admin tries to assign a low-rank role to a high-rank device.
```
Admin (rank 800) → assigns → Low Role (rank 300) → to → Device (rank 500)
```
**Checks:**
1. Admin outranks Low Role: 800 > 300 ✓
2. Admin outranks Device: 800 > 500 ✓
3. Low Role rank >= Device rank: 300 >= 500 ✗
**Result:** Denied (role must be >= device rank to prevent device from modifying its own role)
### Rank Fact
Each object in Aranya's RBAC system has at most one rank associated with its Aranya ID.
```policy
// An object rank.
fact Rank[object_id id]=>{rank int}
```
### Rank Comparison
Utility method for checking object ranks before allowing operations to be performed.
```policy
// Returns whether the command author object has permission to perform an operation on the target object.
// The command author's role must have permission to perform the operation.
// The command author must have a higher rank than the object it is operating on.
function author_has_perm_one_target(author_id id, perm enum Perm, target_id id) bool {
check device_has_perm(author_id, perm)
let author_rank = get_object_rank(author_id)
if !author_can_operate_on_target(author_rank, target_id) {
return false
}
return true
}
// Returns whether the command author object has permission to perform an operation on a set of two target objects.
// The command author's role must have permission to perform the operation.
// The command author must have a higher rank than all the objects it is operating on.
function author_has_perm_two_targets(author_id id, perm enum Perm, target_id1 id, target_id2 id) bool {
check device_has_perm(author_id, perm)
let author_rank = get_object_rank(author_id)
if !author_can_operate_on_target(author_rank, target_id1) {
return false
}
if !author_can_operate_on_target(author_rank, target_id2) {
return false
}
return true
}
// Returns whether the command author outranks the target object.
//
// Note: Uses strict greater-than (>) comparison. A device cannot operate on
// objects of equal rank, enforcing a strict hierarchy where devices can only
// modify objects below them in the rank hierarchy.
function author_can_operate_on_target(author_rank int, target_id id) bool {
let object_rank = get_object_rank(target_id)
if author_rank > object_rank {
return true
}
return false
}
```
### Rank Getters/Setters
Utility methods for getting/setting rank values on objects.
```policy
// Get the rank of an object.
function get_object_rank(object_id id) int {
let rank = check_unwrap query Rank[object_id: object_id]
return rank.rank
}
// Set the rank of an object.
//
// Assumptions:
// - Object rank must not exist yet.
// - Author must have rank >= rank it is setting.
finish function set_object_rank(object_id id, rank int) {
// Create new rank fact.
create Rank[object_id: object_id]=>{rank: rank}
}
// Returns whether a role's rank is >= a device's rank.
//
// This check prevents a device from being assigned a role it could
// potentially modify, which would allow it to escalate its own permissions.
//
// Note: Uses greater-than-or-equal (>=) comparison, unlike `author_can_operate_on_target`
// which uses strict greater-than (>). This allows a device to be assigned a role of equal
// rank, which is safe because the device still cannot modify that role (since modification
// requires strictly outranking the target).
//
// The owner device is exempt from this check because its role is assigned
// directly during team creation (see CreateTeam), bypassing AssignRole.
function role_rank_gte_device_rank(role_id id, device_id id) bool {
let role_rank = get_object_rank(role_id)
let device_rank = get_object_rank(device_id)
return role_rank >= device_rank
}
// Returns whether an object exists.
function object_exists(object_id id) bool {
let device_exists = exists Device[device_id: object_id]
let role_exists = exists Role[role_id: object_id]
let label_exists = exists Label[label_id: object_id]
return device_exists || role_exists || label_exists
}
```
### ChangeRank Command
Command for changing the rank of a device or label.
If the target object is a device with an assigned role, the new rank must not
exceed the role's rank. This maintains the invariant that `role_rank >= device_rank`
which was established at role assignment time. To promote a device above its
current role's rank, first change the device's role to one with a higher rank.
The owner device is the sole exception: its rank intentionally exceeds its role's
rank so it can modify the owner role's permissions (see [Default Hierarchy](#default-hierarchy)).
#### Role Ranks Are Immutable
Role ranks cannot be changed after creation. This design decision maintains the
invariant that `role_rank >= device_rank` for all devices assigned to the role
without requiring complex checks that would need to iterate over all assigned
devices.
If a different rank is needed for a role, create a new role with the desired
rank and permissions, migrate devices to it, then delete the old role.
```policy
// Default maximum rank for the team creator device.
let MAX_RANK = 1000000
// TODO: aranya-core#589 use const expression once supported by the
// policy language. E.g.:
// let DEFAULT_OWNER_DEVICE_RANK = MAX_RANK
let DEFAULT_OWNER_DEVICE_RANK = 1000000
// TODO: aranya-core#589 use const expression once supported by the
// policy language. E.g.:
// let DEFAULT_OWNER_ROLE_RANK = saturating_sub(MAX_RANK, 1)
// Note: The owner device intentionally outranks its own role. This is
// a special case because the owner is a superuser and needs to be able
// to modify the owner role's permissions. For all other roles,
// role_rank > device_rank is enforced during role assignment.
let DEFAULT_OWNER_ROLE_RANK = 999999
let DEFAULT_ADMIN_ROLE_RANK = 800
let DEFAULT_OPERATOR_ROLE_RANK = 700
let DEFAULT_MEMBER_ROLE_RANK = 600
// Change the rank of an object.
//
// Assumptions:
// - The object must already have a rank.
// - The command author must have rank > the old rank.
// - The command author must have rank >= the new rank.
// - The command author must know the current rank before setting the new rank (to prevent an accidental race condition).
finish function change_object_rank(object_id id, old_rank int, new_rank int) {
update Rank[object_id: object_id]=>{rank: old_rank} to {rank: new_rank}
}
action change_rank(object_id id, old_rank int, new_rank int) {
publish ChangeRank {
object_id: object_id,
old_rank: old_rank,
new_rank: new_rank,
}
}
effect RankChanged {
// The ID of the object rank was set on.
object_id id,
// The old rank associated with the object.
old_rank int,
// The new rank associated with the object.
new_rank int,
}
command ChangeRank {
attributes {
priority: 100
}
fields {
// The ID of the object to set the rank on.
object_id id,
// The old rank associated with the object.
old_rank int,
// The new rank to associate with the object.
new_rank int,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Check that the object exists before changing its rank.
check object_exists(this.object_id)
// Changing the rank of a role is not supported. Role ranks are fixed
// at creation time to maintain the invariant that role_rank > device_rank
// for all devices assigned to the role.
let is_role = query Role[role_id: this.object_id]
check is_role is None
// The author must have permission to change the rank.
if author.device_id == this.object_id {
// An object can always downgrade its own rank.
check device_has_perm(author.device_id, Perm::ChangeRank)
} else {
check author_has_perm_one_target(author.device_id, Perm::ChangeRank, this.object_id)
}
// Check that author's rank is >= than the rank being set.
// If the author is the current device, this prevents a device from upgrading its own rank.
let author_rank = get_object_rank(author.device_id)
check author_rank >= this.new_rank
// If the target is a device with an assigned role, the new rank
// must not exceed the role's rank. This maintains the invariant
// that role_rank >= device_rank after assignment.
let assigned_role = query AssignedRole[device_id: this.object_id]
if assigned_role is Some {
let role_rank = get_object_rank((unwrap assigned_role).role_id)
check this.new_rank <= role_rank
}
// Check that old_rank matches the object's current rank.
// Implicitly checks that the rank exists before modifying it.
check this.old_rank == get_object_rank(this.object_id)
finish {
change_object_rank(this.object_id, this.old_rank, this.new_rank)
emit RankChanged {
object_id: this.object_id,
old_rank: this.old_rank,
new_rank: this.new_rank,
}
}
}
}
```
### Rank Queries
##### `query_rank`
Returns the rank of an object.
```policy
// Emits `QueryRankResult` with the rank of the object.
// If the object does not have a rank, then no effect is emitted.
ephemeral action query_rank(object_id id) {
publish QueryRank {
object_id: object_id,
}
}
effect QueryRankResult {
// The object's unique ID.
object_id id,
// The rank of the object.
rank int,
}
ephemeral command QueryRank {
fields {
object_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let maybe_rank = query Rank[object_id: this.object_id]
if maybe_rank is None {
finish {}
} else {
let rank = unwrap maybe_rank
finish {
emit QueryRankResult {
object_id: this.object_id,
rank: rank.rank,
}
}
}
}
}
```
### Device Generation Queries
##### `query_device_generation`
Returns the generation counter for a device. This query is intended
for testing only and should not be exposed via any public APIs.
```policy
// Emits `QueryDeviceGenerationResult` with the generation counter
// for the device. If the device does not have a generation counter,
// then no effect is emitted.
ephemeral action query_device_generation(device_id id) {
publish QueryDeviceGeneration {
device_id: device_id,
}
}
effect QueryDeviceGenerationResult {
// The device's unique ID.
device_id id,
// The device's generation counter.
generation int,
}
ephemeral command QueryDeviceGeneration {
fields {
device_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let maybe_gen = query DeviceGeneration[device_id: this.device_id]
if maybe_gen is None {
finish {}
} else {
let gen = unwrap maybe_gen
finish {
emit QueryDeviceGenerationResult {
device_id: this.device_id,
generation: gen.generation,
}
}
}
}
}
```
## Roles and Permissions
### Overview
Aranya uses [Role-Based Access Control][rbac] (RBAC) for system
authorization. Devices are only authorized to access certain
resources if they have been assigned the requisite role with the requisite permissions. Aranya
primarily uses RBAC to restrict which commands devices are
authorized to publish, but custom policy can use roles for many
other purposes.
Conceptually, a role is a `(role_id, name, author_id)` tuple
where
- `role_id` is a globally unique ID for the role,
cryptographically derived from the command that created the
role.
- `name` is a human-readable name for the role. E.g., `admin` or
`operator`.
- `author_id` is the globally unique ID of the device that
created the role.
- `rank` is the rank associated with the role (stored in the `Rank` fact).
```policy
// An RBAC role.
fact Role[role_id id]=>{name string, author_id id, default bool}
```
Generating a role's ID from its originating command prevents
devices from accidentally creating the same role on diverging
branches, which could cause a fail-open security bug.
```policy
// Returns the globally unique ID for a role created by the
// command in `evp`.
//
// NB: This function is deterministic and injective for the
// current policy. Calling it multiple times for the same
// envelope will always return the same ID.
function derive_role_id(evp struct Envelope) id {
// The role ID is the ID of the command that created it.
// TODO: Or we could use H(cmd_id, ...).
return envelope::command_id(evp)
}
```
> **Note**: Upon team creation, the only role that exists is the
> `owner` role. Therefore, the `owner` role is managed by itself.
> It's [roles all the way down][all-the-way-down]. The owner device's
> rank intentionally exceeds its role's rank so it can modify the
> owner role's permissions. This is the sole exception to the
> `role_rank >= device_rank` invariant enforced for all other role
> assignments.
### Privilege Escalation Mitigations
Since the default owner role has all permissions available to it, it is recommended to only use this role for initial team setup. The owner role should delegate permissions to other roles that can be used for ongoing device, role, and label management. This approach reduces the exposure of the superuser account to potential compromise which could result in an attacker gaining complete control of the team.
To mitigate against privilege escalation attempts, it is recommended to create roles with non-overlapping permissions as much as possible. It is especially important to segment permissions for device management, role creation, role permission management, labels, etc. across different roles.
If a single role has too many permissions, it can attempt to use those permissions to escalate its own permissions, escalate permissions of other devices on the team, or onboard malicious devices it maintains control of to be used as a stronghold for future downgrade resistance (see [Privilege Escalation Attempt Scenario 1](#Privilege-Escalation-Attempt-Scenario-1)).
#### Privilege Escalation Attempt Scenario 1
The following scenario describes a possible privilege escalation attempt as well as operational mitigations to prevent the attack vector from occurring.
1. Malicious device onboards a new pawn device it maintains control of (`AddDevice` perm).
2. Malicious device creates a new role (`CreateRole` perm).
3. Malicious device assigns a permission to that role it does not have (`ChangeRolePerms` perm).
4. Malicious device assigns role with escalated permissions to the pawn device (`AssignRole` perm).
5. Malicious device now has escalated permissions via the pawn device it controls.
It is recommended to segment the `AddDevice`, `CreateRole`, `ChangeRolePerms`, and `AssignRole` permissions across different roles to prevent a single device from controlling device onboarding, role permissions management, and role assignment. A similar approach is recommended to mitigate against privilege escalation for label management.
> **Warning**: The `ChangeRolePerms` and `AssignRole` permissions should **never** be assigned to the same role unless it is a superuser role like Owner. A device with both permissions can add any permission to a role it manages and then assign that role to a device it controls, effectively escalating its own privileges. This is a critical security consideration when designing your role hierarchy.
Note that it is important to segment permissions across different roles with the same rank. If the roles have different ranks, one role will outrank the other role and could leverage its privilege over the other role to assign that role to a pawn device it controls in order to escalate permissions.
#### Privilege Escalation Attempt Scenario 2
The following scenario describes a possible privilege escalation attempt by assigning a higher privilege role to a device that is controlled by a malicious device.
1. Malicious device of rank 10 onboards a new pawn device it maintains control of with rank 5 (`AddDevice` perm).
2. Malicious device assigns existing role of rank 4 with permissions it does not have to pawn device (`AssignRole` perm).
3. Malicious device now has escalated permissions via the pawn device it controls.
The ranking system should be leveraged to guard against these types of privilege escalation attempts. The higher privilege role of rank 4 should not have been given a rank lower than a device of rank 10 that is not supposed to have those permissions granted to it.
To mitigate against this privilege escalation attempt, the higher privilege role could have been given a rank higher than the lower privilege device (e.g. a rank of 15). Then the malicious device of rank 10 would not have the ability to assign that role to another device since the rank check in the policy would prevent the role assignment operation from succeeding.
It is recommended to combine a secure ranking system alongside segmented `AddDevice` and `AssignRole` permissions across different roles to safely guard against this scenario.
### Role Scope
The _scope_ of a role is the aggregate set of resources that the
role authorizes devices to access. Resources themselves define
the role(s) that are required to access the resource. Devices with sufficient permissions can change
a role's scope; how this works depends on the resource.
### Role Permissions
Each role has a set of zero or more permissions that it grants to
devices who have been assigned the role. Permissions are assigned only
to roles, and cannot be assigned directly to devices.
Permissions are statically defined in the policy file itself and
cannot be created or deleted at runtime.
The following table shows which objects each permission can be granted to as well as which objects can be modified by an object with the permission:
| CreateTeam | ✅ (implicit) | ❌ | ✅ | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ |
| TerminateTeam | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ |
| SetupDefaultRole | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ | ✅ | ❌ | ❌ |
| AddDevice | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ |
| RemoveDevice | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ |
| ChangeRank | ❌ | ✅ | ❌ | ❌ | ❌ | ✅ | ✅ | ✅ | ❌ |
| CreateRole | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ | ✅ | ❌ | ❌ |
| DeleteRole | ❌ | ✅ | ❌ | ❌ | ✅ | ❌ | ✅ | ❌ | ❌ |
| AssignRole | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ | ✅ | ✅ | ❌ |
| RevokeRole | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ | ✅ | ✅ | ❌ |
| ChangeRolePerms | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ | ✅ | ❌ | ❌ |
| CreateLabel | ❌ | ✅ | ❌ | ❌ | ✅ | ✅ | ❌ | ❌ | ❌ |
| DeleteLabel | ❌ | ✅ | ❌ | ❌ | ✅ | ✅ | ❌ | ❌ | ❌ |
| AssignLabel | ❌ | ✅ | ❌ | ❌ | ❌ | ✅ | ❌ | ✅ | ❌ |
| RevokeLabel | ❌ | ✅ | ❌ | ❌ | ❌ | ✅ | ❌ | ✅ | ❌ |
| CanUseAfc | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ✅ |
| CreateAfcUniChannel | ❌ | ✅ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ✅ |
```policy
// NB: Update `enum Permission` in client and client-capi on changes.
enum Perm {
// # Team management
//
// The role can add a device to the team.
AddDevice,
// The role can remove a device from the team.
RemoveDevice,
// The role can terminate the team. This causes all team
// commands to fail until a new team is created.
TerminateTeam,
// # Rank
//
// The role can change the rank of an object.
ChangeRank,
// # Roles
//
// The role can create a role.
CreateRole,
// The role can delete a role.
DeleteRole,
// The role can assign a role to other devices.
// WARNING: Do not combine with `ChangeRolePerms` on the same role
// (see [Privilege Escalation Mitigations](#privilege-escalation-mitigations)).
AssignRole,
// The role can revoke a role from other devices.
RevokeRole,
// The role can change permissions of other roles.
// WARNING: Do not combine with `AssignRole` on the same role
// (see [Privilege Escalation Mitigations](#privilege-escalation-mitigations)).
ChangeRolePerms,
// The role can set up default roles. This can only be done
// once, so this permission can only effectively be used by
// the `owner` role.
SetupDefaultRole,
// # Labels
//
// The role can create a label.
CreateLabel,
// The role can delete a label.
DeleteLabel,
// The role can assign a label to a device.
AssignLabel,
// The role can revoke a label from a device.
RevokeLabel,
// # AFC
//
// The role can use AFC. This controls the ability to
// create or receive a unidirectional AFC channels.
CanUseAfc,
// The role can create a unidirectional AFC channel.
CreateAfcUniChannel,
}
// Records a permission granted by the role.
//
// # Caveats
//
// We do not yet support prefix deletion, so this fact is NOT
// deleted when a role is deleted. Use `role_has_perm` to
// verify whether a role grants a permission and use
// `device_has_perm` to verify whether a device has
// a permission.
fact RoleHasPerm[role_id id, perm enum Perm]=>{}
// A wrapper for `create RoleHasPerm`.
finish function assign_perm_to_role(role_id id, perm enum Perm) {
create RoleHasPerm[
role_id: role_id,
perm: perm,
]=>{}
}
// Reports whether the role has the specified permission.
//
// # Errors
//
// It raises a check failure if the role does not exist.
function role_has_perm(role_id id, perm enum Perm) bool {
check exists Role[role_id: role_id]
return exists RoleHasPerm[
role_id: role_id,
perm: perm,
]
}
// Reports whether the device has the specified permission.
//
// # Caveats
//
// This function does NOT check whether the device exists.
function device_has_perm(device_id id, perm enum Perm) bool {
let role = check_unwrap query AssignedRole[device_id: device_id]
return role_has_perm(role.role_id, perm)
}
// Adds a permission to the role.
//
// # Security Warning
//
// The `ChangeRolePerms` permission should not be combined with `AssignRole`
// on the same role. A device with both permissions can escalate privileges
// by adding permissions to a role and assigning it to a device it controls.
// See [Privilege Escalation Mitigations](#privilege-escalation-mitigations) for details.
//
// # Assumptions
//
// 1. The author has the `ChangeRolePerms` permission.
// 2. The target role does not already have the permission.
action add_perm_to_role(role_id id, perm enum Perm) {
publish AddPermToRole {
role_id: role_id,
perm: perm,
}
}
// Emitted when a permission is added to a role.
effect PermAddedToRole {
// The role that was updated.
role_id id,
// The permission that was added to the role.
perm enum Perm,
// The device that added the permission to the role.
author_id id,
}
command AddPermToRole {
attributes {
priority: 100
}
fields {
// The ID of the role to which the permission is being
// added.
role_id id,
// The permission being added.
perm enum Perm,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The author must have permission to change role perms.
check author_has_perm_one_target(author.device_id, Perm::ChangeRolePerms, this.role_id)
// The role must not already have the permission.
check !role_has_perm(this.role_id, this.perm)
finish {
create RoleHasPerm[role_id: this.role_id, perm: this.perm]=>{}
emit PermAddedToRole {
role_id: this.role_id,
perm: this.perm,
author_id: author.device_id,
}
}
}
}
// Removes the permission from the role.
//
// Assumptions:
// 1. The author has the `ChangeRolePerms` permission.
// 2. The target role has the permission that is being removed.
action remove_perm_from_role(role_id id, perm enum Perm) {
publish RemovePermFromRole {
role_id: role_id,
perm: perm,
}
}
// Emitted when a permission is removed from a role.
effect PermRemovedFromRole {
// The role from which the permission was removed.
role_id id,
// The permission that was removed from the role.
perm enum Perm,
// The device that removed the permission from the role.
author_id id,
}
command RemovePermFromRole {
attributes {
priority: 300
}
fields {
// The ID of the role from which the permission is being
// removed.
role_id id,
// The permission being removed.
perm enum Perm,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The author must have permission to change role perms.
check author_has_perm_one_target(author.device_id, Perm::ChangeRolePerms, this.role_id)
// The author does not need to hold the permission being removed.
// The rank hierarchy already prevents abuse: a device can only
// modify permissions on roles it outranks, and role_rank > device_rank
// is enforced for role assignments. This means a device cannot
// remove permissions from a role assigned to a higher-ranked device.
// It is an error to remove a permission not assigned to
// the role.
check role_has_perm(this.role_id, this.perm)
// At this point we believe the following to be true:
//
// - the team is active
// - `author` is authorized to remove permissions from
// the role
// - `this.role_id` refers to a role that exists
// - `this.perm` is a valid permission string
// - `this.role_id` currently has the permission `this.perm`
finish {
delete RoleHasPerm[role_id: this.role_id, perm: this.perm]
emit PermRemovedFromRole {
role_id: this.role_id,
perm: this.perm,
author_id: author.device_id,
}
}
}
}
```
### Role Creation
Upon creation, a team only has one role: the `owner` role,
assigned to the team creator. Afterward, the owner can create
additional roles as needed.
Devices are notified about new roles via the `RoleCreated`
effect.
```policy
// The input to `create_role_facts` since the policy language
// has neither named args nor good IDE support.
struct RoleInfo {
// The ID of the role.
role_id id,
// The name of the role.
name string,
// The ID of the device that created the role.
author_id id,
// The rank of the role object.
rank int,
// Is this a default role?
default bool,
}
// Creates the following facts for a role
//
// - Role
finish function create_role_facts(role struct RoleInfo) {
create Role[role_id: role.role_id]=>{
name: role.name,
author_id: role.author_id,
default: role.default,
}
set_object_rank(role.role_id, role.rank)
}
// Emitted when a role is created.
effect RoleCreated {
// ID of the role.
role_id id,
// Name of the role.
name string,
// ID of device that created the role.
author_id id,
// The rank of the role object.
rank int,
// Is this a "default" role?
default bool,
}
```
#### Custom Roles
```policy
// Creates a role with an initial rank.
//
// This action does not (and cannot usefully) check for name
// overlap. Do not assume that role names are unique.
//
// The `role_id` is guaranteed to be unique since it is taken from the unique ID of the role creation command.
//
// # Required Permissions
//
// - `CreateRole`
action create_role(role_name string, rank int) {
publish CreateRole {
role_name: role_name,
rank: rank,
}
}
command CreateRole {
attributes {
priority: 200
}
fields {
role_name string,
rank int,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The author must have the permission to create a role
check device_has_perm(author.device_id, Perm::CreateRole)
// The author's rank must be greater than the rank of the role it is creating.
check get_object_rank(author.device_id) >= this.rank
let role_id = derive_role_id(envelope)
let role_info = RoleInfo {
role_id: role_id,
name: this.role_name,
author_id: author.device_id,
rank: this.rank,
default: false,
}
let role_created = role_info as RoleCreated
finish {
create_role_facts(role_info)
emit role_created
}
}
}
```
#### Default Roles
The `setup_default_roles` action creates exactly three default
roles with fixed names.
- `admin`
- Can create and delete labels
- Typically manages the `operator` role
- `operator`
- Can assign and revoke labels
- Typically manages the `member` role
- `member`
- Can create and delete AFC channels (for labels they have been
granted permission to use)
**Important**: The owner role (created during team creation) is a
superuser with all permissions. Its device rank intentionally exceeds
its role rank so it can manage its own role's permissions (see
[Default Hierarchy](#default-hierarchy)). The owner role should be
used sparingly. After setting up default roles, the owner credentials
should be stored securely (e.g., in an HSM) and only used for
emergency "break glass" scenarios.
To guard against accidental replays, each default role records a
`DefaultRoleSeeded` fact the first time it is created. Subsequent
attempts to seed the same default role will fail the policy checks
before any storage writes occur.
Default role permissions:
| Owner | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Admin | ✅ | ✅ | ❌ | ✅ | ✅ | ✅ | ❌ | ❌ | ✅ | ❌ | ✅ | ✅ | ❌ | ❌ | ❌ | ❌ |
| Operator | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ✅ | ✅ | ❌ | ❌ | ❌ | ❌ | ✅ | ✅ | ❌ | ❌ |
| Member | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ❌ | ✅ | ✅ |
```policy
fact DefaultRoleSeeded[name enum DefaultRoleName]=>{role_id id}
enum DefaultRoleName {
Admin,
Operator,
Member,
}
function default_role_name_to_str(name enum DefaultRoleName) string {
match name {
DefaultRoleName::Admin => { return "admin" }
DefaultRoleName::Operator => { return "operator" }
DefaultRoleName::Member => { return "member" }
}
}
// Setup default roles on a team.
action setup_default_roles() {
publish SetupDefaultRole {
name: DefaultRoleName::Admin,
}
publish SetupDefaultRole {
name: DefaultRoleName::Operator,
}
publish SetupDefaultRole {
name: DefaultRoleName::Member,
}
}
command SetupDefaultRole {
attributes {
priority: 200
}
fields {
// The name of the default role.
name enum DefaultRoleName,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Author must have permission to setup the default roles.
check device_has_perm(author.device_id, Perm::SetupDefaultRole)
check !exists DefaultRoleSeeded[name: this.name]
let name = default_role_name_to_str(this.name)
let role_id = derive_role_id(envelope)
let admin_role_rank = DEFAULT_ADMIN_ROLE_RANK
let operator_role_rank = DEFAULT_OPERATOR_ROLE_RANK
let member_role_rank = DEFAULT_MEMBER_ROLE_RANK
match this.name {
DefaultRoleName::Admin => {
finish {
create_role_facts(RoleInfo {
role_id: role_id,
name: name,
author_id: author.device_id,
rank: admin_role_rank,
default: true,
})
assign_perm_to_role(role_id, Perm::ChangeRank)
assign_perm_to_role(role_id, Perm::AddDevice)
assign_perm_to_role(role_id, Perm::RemoveDevice)
assign_perm_to_role(role_id, Perm::CreateLabel)
assign_perm_to_role(role_id, Perm::DeleteLabel)
assign_perm_to_role(role_id, Perm::CreateRole)
assign_perm_to_role(role_id, Perm::DeleteRole)
assign_perm_to_role(role_id, Perm::ChangeRolePerms)
emit RoleCreated {
role_id: role_id,
name: name,
author_id: author.device_id,
rank: admin_role_rank,
default: true,
}
create DefaultRoleSeeded[
name: this.name,
]=>{role_id: role_id}
}
}
DefaultRoleName::Operator => {
finish {
create_role_facts(RoleInfo {
role_id: role_id,
name: name,
author_id: author.device_id,
rank: operator_role_rank,
default: true,
})
assign_perm_to_role(role_id, Perm::AssignLabel)
assign_perm_to_role(role_id, Perm::RevokeLabel)
assign_perm_to_role(role_id, Perm::AssignRole)
assign_perm_to_role(role_id, Perm::RevokeRole)
emit RoleCreated {
role_id: role_id,
name: name,
author_id: author.device_id,
rank: operator_role_rank,
default: true,
}
create DefaultRoleSeeded[
name: this.name,
]=>{role_id: role_id}
}
}
DefaultRoleName::Member => {
finish {
create_role_facts(RoleInfo {
role_id: role_id,
name: name,
author_id: author.device_id,
rank: member_role_rank,
default: true,
})
assign_perm_to_role(role_id, Perm::CanUseAfc)
assign_perm_to_role(role_id, Perm::CreateAfcUniChannel)
emit RoleCreated {
role_id: role_id,
name: name,
author_id: author.device_id,
rank: member_role_rank,
default: true,
}
create DefaultRoleSeeded[
name: this.name,
]=>{role_id: role_id}
}
}
}
}
}
```
### Role Deletion
```policy
// Deletes a role
//
// The role being deleted must not be assigned to any devices.
//
// # Required Permissions
//
// - `DeleteRole`
action delete_role(role_id id) {
publish DeleteRole {
role_id: role_id
}
}
effect RoleDeleted {
name string,
role_id id,
}
command DeleteRole {
attributes {
priority: 400,
}
fields {
role_id id
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The author must have the permission to delete the role
check author_has_perm_one_target(author.device_id, Perm::DeleteRole, this.role_id)
// The role must exist
check exists Role[role_id: this.role_id]
// The role must not be assigned to any devices
check !exists RoleAssignmentIndex[
role_id: this.role_id,
device_id: ?,
]
// we already checked that this exists
let role = check_unwrap query Role[role_id: this.role_id]
finish {
delete Role[role_id: this.role_id]
delete Rank[object_id: this.role_id]
emit RoleDeleted {
name: role.name,
role_id: this.role_id,
}
}
}
}
```
### Role Assignment
A device can be assigned zero or one roles.
```policy
// Records that a device has been assigned a role.
//
// # Foreign Keys
//
// - `device_id` refers to the `Device` fact
// - `role_id` refers to the `Role` fact
//
// # Caveats
//
// This fact is NOT deleted when a role is deleted. Use one of
// the following functions to retrieve the role assigned to
// a device:
// - `try_get_assigned_role`
// - `get_assigned_role`
// - `get_assigned_role_id`
fact AssignedRole[device_id id]=>{role_id id}
// Secondary index over role assignments to support efficient
// queries keyed by `role_id`.
//
// # Invariants
//
// If `RoleAssignmentIndex[role_id: r, device_id: d]` exists,
// then `AssignedRole[device_id: d]=>{role_id: r}` also exists.
//
// # Foreign Keys
//
// - `role_id` refers to the `Role` fact
// - `device_id` refers to the `Device` fact
fact RoleAssignmentIndex[role_id id, device_id id]=>{}
// Records a new role assignment while keeping the index in sync.
finish function create_role_assignment(device_id id, role_id id) {
create AssignedRole[device_id: device_id]=>{role_id: role_id}
create RoleAssignmentIndex[role_id: role_id, device_id: device_id]=>{}
}
// Deletes an existing role assignment and its index entry.
finish function delete_role_assignment(device_id id, role_id id) {
delete AssignedRole[device_id: device_id]
delete RoleAssignmentIndex[role_id: role_id, device_id: device_id]
}
// Updates a device's role assignment and corresponding index entry.
finish function update_role_assignment(
device_id id,
old_role_id id,
new_role_id id,
) {
update AssignedRole[device_id: device_id]=>{role_id: old_role_id} to {
role_id: new_role_id,
}
delete RoleAssignmentIndex[
role_id: old_role_id,
device_id: device_id,
]
create RoleAssignmentIndex[
role_id: new_role_id,
device_id: device_id,
]=>{}
}
// Returns the role assigned to the device if it exists.
//
// # Caveats
//
// - It does NOT check whether the device exists.
function try_get_assigned_role(device_id id) optional struct Role {
let assigned_role = query AssignedRole[device_id: device_id]
if assigned_role is None {
return None
}
return query Role[role_id: (unwrap assigned_role).role_id]
}
// Returns the role assigned to the device.
//
// # Errors
//
// This function raises a check error if the device has not been
// assigned a role or if the assigned role does not exist.
//
// # Caveats
//
// - It does NOT check whether the device exists.
function get_assigned_role(device_id id) struct Role {
// NB: We could implement this with `try_get_assigned_role`,
// but the generated check errors would be much less
// informative, so we manually implement it instead.
let assigned_role = check_unwrap query AssignedRole[device_id: device_id]
// Verify that the assigned role exists.
//
// There are two reasons the role might not exist:
//
// 1. The role was deleted and the `AssignedRole` fact was
// not also deleted (which is currently acceptable since
// we do not support prefix deletion).
// 2. We have an internal consistency error.
//
// Option (1) is the most likely and we can't really check
// for (2) here.
let role = check_unwrap query Role[role_id: assigned_role.role_id]
return role
}
// Reports whether the provided role represents the default owner role.
function is_owner(role struct Role) bool {
return role.default && role.name == "owner"
}
// Returns the ID of the role assigned to the device.
//
// # Errors
//
// This function raises a check error if the device has not been
// assigned a role.
//
// # Caveats
//
// - It does NOT check whether the device exists.
function get_assigned_role_id(device_id id) id {
return get_assigned_role(device_id).role_id
}
// Returns the ID of the role assigned to the device if it exists.
//
// # Caveats
//
// - It does NOT check whether the device exists.
function try_get_assigned_role_id(device_id id) optional id {
let role = try_get_assigned_role(device_id)
if role is None {
return None
}
return Some((unwrap role).role_id)
}
// Assigns the specified role to the device.
//
// It is an error if the device has already been assigned a role.
// If you want to assign a different role to a device that already
// has a role, use `change_role()` instead.
//
// # Security Warning
//
// The `AssignRole` permission should not be combined with `ChangeRolePerms`
// on the same role. A device with both permissions can escalate privileges
// by adding permissions to a role and assigning it to a device it controls.
// See [Privilege Escalation Mitigations](#privilege-escalation-mitigations) for details.
//
// # Required Permissions
//
// - `AssignRole`
action assign_role(device_id id, role_id id) {
publish AssignRole {
device_id: device_id,
role_id: role_id,
}
}
// Emitted when a device is assigned a role.
effect RoleAssigned {
// The ID of the device that was assigned a role.
device_id id,
// The ID of the role that was assigned.
role_id id,
// The ID of the device that assigned the role.
author_id id,
}
command AssignRole {
attributes {
priority: 100
}
fields {
// The ID of the device being assigned the role.
device_id id,
// The ID of the role being assigned to the device.
role_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The author must have permission to assign the role to the target device.
check author_has_perm_two_targets(author.device_id, Perm::AssignRole, this.role_id, this.device_id)
// The role's rank must be >= the device's rank.
check role_rank_gte_device_rank(this.role_id, this.device_id)
// Ensure the target role exists.
check exists Role[role_id: this.role_id]
// The target device must exist.
check exists Device[device_id: this.device_id]
// Device must not already have a role assigned.
// If the device already has a role assigned, use `ChangeRole` instead.
check !exists AssignedRole[device_id: this.device_id]
// Ensure the role index is also clear before creating a new assignment.
check !exists RoleAssignmentIndex[
role_id: this.role_id,
device_id: this.device_id,
]
// At this point we believe the following to be true:
//
// - the team is active
// - `this.device_id` refers to a device that exists
// - `this.role_id` refers to a role that exists
// - `author` has the `AssignRole` permission
// - `author` outranks the target role and device
// - the role's rank >= the device's rank
// - the device does not already hold `this.role_id`
finish {
create_role_assignment(this.device_id, this.role_id)
emit RoleAssigned {
device_id: this.device_id,
role_id: this.role_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
```
### Role Changing
```policy
// Changes a device's role.
//
// # Security Warning
//
// The `AssignRole` permission should not be combined with `ChangeRolePerms`
// on the same role. A device with both permissions can escalate privileges
// by adding permissions to a role and assigning it to a device it controls.
// See [Privilege Escalation Mitigations](#privilege-escalation-mitigations) for details.
//
// # Required Permissions
//
// - `RevokeRole` for the old role
// - `AssignRole` for the new role
action change_role(
device_id id,
old_role_id id,
new_role_id id,
) {
publish ChangeRole {
device_id: device_id,
old_role_id: old_role_id,
new_role_id: new_role_id,
}
}
// Emitted when a device's role is changed.
effect RoleChanged {
// The ID of the device whose role is being changed.
device_id id,
// The ID of the device's old role.
old_role_id id,
// The ID of the device's new role.
new_role_id id,
// The ID of the device that changed the device's role.
author_id id,
}
command ChangeRole {
attributes {
priority: 100
}
fields {
// The ID of the device being assigned the role.
device_id id,
// The ID of the device's old role.
old_role_id id,
// The new role being assigned to the device.
new_role_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Attempting to change to the same role should fail since a state change is expected.
check this.old_role_id != this.new_role_id
check exists Role[role_id: this.new_role_id]
// The author must have permission to revoke the old role from the device.
check author_has_perm_two_targets(author.device_id, Perm::RevokeRole, this.device_id, this.old_role_id)
// The author must have permission to assign the new role to the device.
check author_has_perm_two_targets(author.device_id, Perm::AssignRole, this.device_id, this.new_role_id)
// The new role's rank must be >= the device's rank.
check role_rank_gte_device_rank(this.new_role_id, this.device_id)
// The target device must exist.
check exists Device[device_id: this.device_id]
let current_assignment = check_unwrap query AssignedRole[device_id: this.device_id]
check current_assignment.role_id == this.old_role_id
// Ensure the role index reflects the existing assignment before updating it.
check exists RoleAssignmentIndex[
role_id: this.old_role_id,
device_id: this.device_id,
]
let old_role = check_unwrap query Role[role_id: this.old_role_id]
if is_owner(old_role) {
check at_least 2 RoleAssignmentIndex[
role_id: this.old_role_id,
device_id: ?,
]=>{}
}
// At this point we believe the following invariants to
// be true:
//
// - `this.old_role_id` and `this.new_role_id` are
// different
// - `this.old_role_id` refers to a role that exists
// - `author` has the `RevokeRole` permission
// - `this.new_role_id` refers to a role that exists
// - `author` has the `AssignRole` permission
// - `author` outranks `old_role`, `new_role`, and the target device
// - the new role's rank >= the device's rank
finish {
update_role_assignment(
this.device_id,
this.old_role_id,
this.new_role_id,
)
emit RoleChanged {
device_id: this.device_id,
new_role_id: this.new_role_id,
old_role_id: this.old_role_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
```
### Role Revocation
```policy
// Revokes the specified role from the device.
//
// # Required Permissions
//
// - `RevokeRole`
action revoke_role(device_id id, role_id id) {
publish RevokeRole {
device_id: device_id,
role_id: role_id,
}
}
// Emitted when a device has its role revoked.
effect RoleRevoked {
// The ID of the device that had its role revoked.
device_id id,
// The ID of the role that was revoked.
role_id id,
// The ID of the device that revoked the role.
author_id id,
}
command RevokeRole {
attributes {
priority: 300
}
fields {
// The ID of the device having its role revoked.
device_id id,
// The ID of the role being revoked.
role_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The author must have permission to revoke the role from the device.
check author_has_perm_two_targets(author.device_id, Perm::RevokeRole, this.device_id, this.role_id)
let role = check_unwrap query Role[role_id: this.role_id]
// The target device must exist.
check exists Device[device_id: this.device_id]
let assignment = check_unwrap query AssignedRole[device_id: this.device_id]
check assignment.role_id == this.role_id
// Ensure the assignment index entry exists so we can remove it.
check exists RoleAssignmentIndex[
role_id: this.role_id,
device_id: this.device_id,
]
if is_owner(role) {
check at_least 2 RoleAssignmentIndex[
role_id: this.role_id,
device_id: ?,
]=>{}
}
// At this point we believe the following to be true:
//
// - the team is active
// - `this.device_id` refers to a device that exists
// - `this.role_id` refers to a role that exists
// - `author` has the `RevokeRole` permission
// - `author` outranks the target role and device
// - the owner role retains at least one assignment after this change
finish {
delete_role_assignment(this.device_id, this.role_id)
emit RoleRevoked {
device_id: this.device_id,
role_id: this.role_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
```
### Role Queries
#### `query_team_roles`
```policy
// Emits `QueryTeamRolesResult` for each role on the team.
ephemeral action query_team_roles() {
map Role[role_id: ?] as f {
publish QueryTeamRoles {
role_id: f.role_id,
name: f.name,
author_id: f.author_id,
default: f.default,
}
}
}
// Emitted when a role is queried by `query_team_roles`.
effect QueryTeamRolesResult {
// The ID of the role.
role_id id,
// The name of the role.
name string,
// The ID of the device that created the role.
author_id id,
// Is this a default role?
default bool,
}
// A trampoline command to forward data to `QueryTeamRolesResult`.
ephemeral command QueryTeamRoles {
fields {
role_id id,
name string,
author_id id,
default bool,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let eff = this as QueryTeamRolesResult
finish {
emit eff
}
}
}
```
## Teams
### Team Creation
Teams are the primary organizational unit in Aranya. Each graph
is associated with exactly one team.
```policy
// A singleton fact that indicates that `CreateTeam` has been
// published.
//
// At first glance this fact is seemingly redundant, since the ID
// of the `CreateTeam` command is the "graph ID," meaning without
// a `CreateTeam` command the graph cannot exist.
//
// However, this fact is required to ensure that we reject all
// subsequent `CreateTeam` commands.
fact TeamStart[]=>{team_id id}
// Reports whether the team exists.
//
// This should always be the first thing that is checked before
// executing a command on a team.
function team_exists() bool {
// Check to see if team is active.
return exists TeamStart[]=>{team_id: ?}
}
// Returns the current team ID.
//
// # Errors
//
// This function raises a check error if the team does not exist.
function team_id() id {
let f = check_unwrap query TeamStart[]=>{team_id: ?}
return f.team_id
}
```
The initial command in the graph is the `CreateTeam` command,
which creates the `TeamStart` fact.
```policy
// Creates a Team.
action create_team(owner_keys struct PublicKeyBundle, nonce bytes) {
publish CreateTeam {
owner_keys: owner_keys,
nonce: nonce,
}
}
// Emitted when a team is created.
effect TeamCreated {
// The ID of the team.
team_id id,
// The ID of the device that owns the team.
owner_id id,
}
command CreateTeam {
attributes {
init: true
}
fields {
// The initial owner's public Device Keys.
owner_keys struct PublicKeyBundle,
// Random nonce to enforce this team's uniqueness.
nonce bytes,
}
// As the first command in the graph, the `CreateTeam`
// command is sealed and opened differently than other
// commands.
seal {
let parent_id = perspective::head_id()
let author_id = device::current_device_id()
let payload = serialize(this)
let author_sign_key_id = idam::derive_sign_key_id(this.owner_keys.sign_key)
let signed = crypto::sign(author_sign_key_id, payload)
return envelope::new(
parent_id,
author_id,
signed.command_id,
signed.signature,
payload,
)
}
open {
let payload = envelope::payload(envelope)
let author_sign_key = deserialize(payload).owner_keys.sign_key
let verified_command = crypto::verify(
author_sign_key,
envelope::parent_id(envelope),
payload,
envelope::command_id(envelope),
envelope::signature(envelope),
)
return deserialize(verified_command)
}
policy {
// NB: This is the only place in the policy file where we
// invert this condition.
check !team_exists()
// TODO: check that `this.nonce` length is like
// 32 bytes or something? It *should* be cryptographically
// secure, but we don't really have a way to check that
// yet. And I'm not sure we want to have policy generate
// the nonce for CreateTeam.
let author_id = envelope::author_id(envelope)
let owner_device_id = idam::derive_device_id(this.owner_keys.ident_key)
// The ID of a team is the ID of the command that created
// it.
let team_id = envelope::command_id(envelope)
// The author must have signed the command with the same
// device keys.
check author_id == owner_device_id
// The ID of the 'owner' role.
let owner_role_id = derive_role_id(envelope)
let owner_rank = DEFAULT_OWNER_DEVICE_RANK
let owner_role_rank = DEFAULT_OWNER_ROLE_RANK
finish {
create TeamStart[]=>{team_id: team_id}
create DeviceGeneration[device_id: owner_device_id]=>{generation: 0}
add_new_device(owner_device_id, this.owner_keys, owner_rank)
create_role_facts(RoleInfo {
role_id: owner_role_id,
name: "owner",
author_id: author_id,
rank: owner_role_rank,
default: true,
})
// Assign all of the administrative permissions to
// the owner role.
assign_perm_to_role(owner_role_id, Perm::TerminateTeam)
assign_perm_to_role(owner_role_id, Perm::AddDevice)
assign_perm_to_role(owner_role_id, Perm::RemoveDevice)
assign_perm_to_role(owner_role_id, Perm::ChangeRank)
assign_perm_to_role(owner_role_id, Perm::CreateLabel)
assign_perm_to_role(owner_role_id, Perm::DeleteLabel)
assign_perm_to_role(owner_role_id, Perm::AssignLabel)
assign_perm_to_role(owner_role_id, Perm::RevokeLabel)
assign_perm_to_role(owner_role_id, Perm::CreateRole)
assign_perm_to_role(owner_role_id, Perm::DeleteRole)
assign_perm_to_role(owner_role_id, Perm::AssignRole)
assign_perm_to_role(owner_role_id, Perm::RevokeRole)
assign_perm_to_role(owner_role_id, Perm::ChangeRolePerms)
assign_perm_to_role(owner_role_id, Perm::SetupDefaultRole)
assign_perm_to_role(owner_role_id, Perm::CanUseAfc)
assign_perm_to_role(owner_role_id, Perm::CreateAfcUniChannel)
// Assign the owner role directly, bypassing the normal
// AssignRole command. This is the sole place where
// device_rank > role_rank is allowed, giving the owner
// device the ability to modify its own role.
create_role_assignment(author_id, owner_role_id)
// We don't have to emit the effects in a particular
// order, but try to make it intuitive.
emit TeamCreated {
team_id: team_id,
owner_id: author_id,
}
emit DeviceAdded {
device_id: owner_device_id,
device_keys: this.owner_keys,
rank: owner_rank,
}
emit RoleCreated {
role_id: owner_role_id,
name: "owner",
author_id: author_id,
default: true,
rank: owner_role_rank,
}
emit RoleAssigned {
device_id: author_id,
role_id: owner_role_id,
author_id: author_id,
}
}
}
}
// Adds the device to the team.
finish function add_new_device(
device_id id,
kb struct PublicKeyBundle,
rank int,
) {
create Device[device_id: device_id]=>{}
create DeviceIdentPubKey[device_id: device_id]=>{
key: kb.ident_key,
}
create DeviceSignPubKey[device_id: device_id]=>{
key: kb.sign_key,
}
create DeviceEncPubKey[device_id: device_id]=>{
key: kb.enc_key,
}
set_object_rank(device_id, rank)
}
// Deletes the core device facts for `device_id`.
finish function delete_device_core(device_id id) {
delete Device[device_id: device_id]
delete DeviceIdentPubKey[device_id: device_id]
delete DeviceSignPubKey[device_id: device_id]
delete DeviceEncPubKey[device_id: device_id]
delete Rank[object_id: device_id]
}
```
### Team Termination
Teams can also be terminated with the `TerminateTeam` command.
```policy
// Terminates a Team.
//
// # Required Permissions
//
// - `TerminateTeam`
action terminate_team(team_id id) {
publish TerminateTeam {
team_id: team_id,
}
}
effect TeamTerminated {
// The ID of the team that was terminated.
team_id id,
// The ID of the device that terminated the team.
owner_id id,
}
// This effect is emitted when a command could cause certain AFC channels to be invalidated.
// When the effect is handled, the user should run the `query_afc_channel_is_valid()` query to determine which of its AFC channels are still valid.
effect CheckValidAfcChannels{}
command TerminateTeam {
attributes {
priority: 500
}
fields {
// The ID of the team being terminated.
team_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Author must have permission to terminate the team.
check device_has_perm(author.device_id, Perm::TerminateTeam)
let current_team_id = team_id()
check this.team_id == current_team_id
// At this point we believe the following to be true:
//
// - the team is active
// - `author` has the `TerminateTeam` permission
// - the requested team matches the currently executing team
finish {
delete TeamStart[]
emit TeamTerminated {
team_id: current_team_id,
owner_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
```
### Adding Devices
```policy
// Adds a device to the team with an initial rank.
//
// # Required Permissions
//
// - `AddDevice`
// - `AssignRole` (if assigned an initial role)
action add_device(device_keys struct PublicKeyBundle, initial_role_id optional id, rank int) {
publish AddDevice {
device_keys: device_keys,
rank: rank,
}
if initial_role_id is Some {
let role_id = unwrap initial_role_id
let device_id = idam::derive_device_id(device_keys.ident_key)
publish AssignRole {
device_id: device_id,
role_id: role_id,
}
}
}
// Emitted when a device is added to the team.
effect DeviceAdded {
// Uniquely identifies the device.
device_id id,
// The device's set of public Device Keys.
device_keys struct PublicKeyBundle,
// The rank of the device object.
rank int,
}
command AddDevice {
attributes {
priority: 100
}
fields {
// The new device's public Device Keys.
device_keys struct PublicKeyBundle,
// Device rank.
rank int,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Author must have permission to add a device to the team.
check device_has_perm(author.device_id, Perm::AddDevice)
// The author's rank must be greater than the rank of the device it is adding to the team.
check get_object_rank(author.device_id) >= this.rank
let device_id = idam::derive_device_id(this.device_keys.ident_key)
check !exists Device[device_id: device_id]
check !exists DeviceIdentPubKey[device_id: device_id]
check !exists DeviceSignPubKey[device_id: device_id]
check !exists DeviceEncPubKey[device_id: device_id]
let existing_gen = query DeviceGeneration[device_id: device_id]
// At this point we believe the following to be true:
//
// - the team is active
// - `author` has the `AddDevice` permission
// - the key material is not already present on the team
//
// Depending on whether the device has been seen before,
// we either seed a new generation counter or reuse the
// existing one.
if existing_gen is None {
finish {
create DeviceGeneration[device_id: device_id]=>{generation: 0}
add_new_device(
device_id,
this.device_keys,
this.rank,
)
emit DeviceAdded {
device_id: device_id,
device_keys: this.device_keys,
rank: this.rank,
}
}
} else {
finish {
add_new_device(
device_id,
this.device_keys,
this.rank,
)
emit DeviceAdded {
device_id: device_id,
device_keys: this.device_keys,
rank: this.rank,
}
}
}
}
}
```
### Removing Devices
Removing the final owner would leave the team without a break-glass
principal, so any attempt to remove the last owner is rejected even if
initiated by another device.
```policy
// Removes a device from the team.
//
// # Required Permissions
//
// - `RemoveDevice`
action remove_device(device_id id) {
publish RemoveDevice {
device_id: device_id,
}
}
// Emitted when a device is removed from the team.
effect DeviceRemoved {
// The ID of the device that was removed from the team.
device_id id,
// The ID of the device that removed `device_id`.
author_id id,
}
command RemoveDevice {
attributes {
priority: 400
}
fields {
// The ID of the device being removed from the team.
device_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// The target device must exist.
check exists Device[device_id: this.device_id]
// Author must have permission to remove a device from the team.
// Devices should always be allowed to remove themselves even without RemoveDevice permission.
if author.device_id != this.device_id {
check author_has_perm_one_target(author.device_id, Perm::RemoveDevice, this.device_id)
}
// Clean up optional per-device facts that may or may not
// exist.
let assigned_role = query AssignedRole[device_id: this.device_id]
let device_gen = check_unwrap query DeviceGeneration[device_id: this.device_id]
let next_gen = check_unwrap add(device_gen.generation, 1)
if assigned_role is Some {
let role_id = (unwrap assigned_role).role_id
// Invariant check.
check exists RoleAssignmentIndex[
role_id: role_id,
device_id: this.device_id,
]
// The assigned role must exist.
let role = check_unwrap query Role[role_id: role_id]
// Ensure that a team always has at least one owner.
if is_owner(role) {
check at_least 2 RoleAssignmentIndex[
role_id: role_id,
device_id: ?,
]=>{}
}
finish {
update DeviceGeneration[device_id: this.device_id]=>{generation: device_gen.generation} to {
generation: next_gen
}
delete_role_assignment(this.device_id, role_id)
delete_device_core(this.device_id)
emit DeviceRemoved {
device_id: this.device_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
} else {
// TODO: Consider adding an index on
// `device_id` so we can sanity-check that no stray
// role assignments remain.
finish {
update DeviceGeneration[device_id: this.device_id]=>{generation: device_gen.generation} to {
generation: next_gen
}
delete_device_core(this.device_id)
emit DeviceRemoved {
device_id: this.device_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
}
```
## AFC
### Labels
Labels provide topic segmentation for AFC. Devices can only participate
in a channel if they have been granted permission to use the channel's
label. Devices can be granted permission to use an arbitrary number of
labels.
```policy
// Records a label.
fact Label[label_id id]=>{name string, author_id id}
```
- `label_id` is a globally unique ID for the label,
cryptographically derived from the command that created the
label (see `derive_label_id`).
- `name` is a non-unique, human-readable name for the label.
E.g., `telemetry`.
- `author_id` is the globally unique ID of the device that
created the label.
Generating a label's ID from its originating command prevents
devices from accidentally creating the same label on diverging
branches, which could cause a fail-open security bug.
```policy
// Returns the globally unique ID for a label created by the
// command in `evp`.
//
// NB: This function is deterministic and injective for the
// current policy. Calling it multiple times for the same
// envelope will always return the same ID.
function derive_label_id(evp struct Envelope) id {
// The label ID is the ID of the command that created it.
// TODO: Or we could use H(cmd_id, ...).
return envelope::command_id(evp)
}
```
#### Label Creation
```policy
// Creates a label with an initial rank.
//
// - `name` is a short description of the label, like
// "TELEMETRY".
//
// This action does not (and cannot usefully) check for name
// overlap. Do not assume that label names are unique.
//
// The `label_id` is guaranteed to be unique since it is taken from the unique ID of the label creation command.
//
// # Required Permissions
//
// - `CreateLabel`
action create_label(name string, rank int) {
publish CreateLabel {
label_name: name,
rank: rank,
}
}
// Emitted when the `CreateLabel` command is successfully
// processed.
effect LabelCreated {
// Uniquely identifies the label.
label_id id,
// The label name.
label_name string,
// The rank of the label.
rank int,
// The ID of the device that created the label.
label_author_id id,
}
command CreateLabel {
attributes {
priority: 200
}
fields {
// The label name.
label_name string,
// The initial rank of the label.
rank int,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Author must have permission to create a label.
check device_has_perm(author.device_id, Perm::CreateLabel)
// The author's rank must be greater than the rank of the label it is creating.
check get_object_rank(author.device_id) >= this.rank
// A label's ID is the ID of the command that created it.
let label_id = derive_label_id(envelope)
// At this point we believe the following to be true:
//
// - the team is active
// - `author` has the `CreateLabel` permission
finish {
create Label[label_id: label_id]=>{
name: this.label_name,
author_id: author.device_id,
}
set_object_rank(label_id, this.rank)
emit LabelCreated {
label_id: label_id,
label_name: this.label_name,
rank: this.rank,
label_author_id: author.device_id,
}
}
}
}
```
#### Label Deletion
Deleting a label revokes access from all devices who have been
granted permission to use it.
```policy
// Deletes a label.
//
// # Required Permissions
//
// - `DeleteLabel`
action delete_label(label_id id) {
// TODO: Should we add a `reason` field?
publish DeleteLabel {
label_id: label_id,
}
}
// Emitted when the `DeleteLabel` command is successfully
// processed.
effect LabelDeleted {
// The label name.
label_name string,
// The label author's device ID.
label_author_id id,
// Uniquely identifies the label.
label_id id,
// The ID of the device that deleted the label.
author_id id,
}
command DeleteLabel {
attributes {
priority: 400
}
fields {
// The unique ID of the label being deleted.
label_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Author must have permission to delete a label and outrank the label.
check author_has_perm_one_target(author.device_id, Perm::DeleteLabel, this.label_id)
// We can't query the label after it's been deleted, so
// make sure we pull all of its info out of the fact
// database.
let label = check_unwrap query Label[label_id: this.label_id]
// At this point we believe the following to be true:
//
// - the team is active
// - `author` has the `DeleteLabel` permission
// - `author` outranks `this.label_id`
// - `this.label_id` refers to a label that exists
finish {
// TODO: We can't delete these yet because the
// storage layer does not yet support prefix deletion.
// See https://github.com/aranya-project/aranya-core/issues/229
//
// delete LabelAssignedToDevice[label_id: label.label_id, device_id: ?]
delete Label[label_id: label.label_id]
delete Rank[object_id: label.label_id]
emit LabelDeleted {
label_name: label.name,
label_author_id: label.author_id,
label_id: label.label_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
```
#### Label Assignment
Labels can be assigned to zero or more devices. The labels assigned to a
device are permitted to have different `ChanOp`s. When determining
whether a device is allowed to use a label, the more permissive `ChanOp`
is used.
##### Label Assignment to Devices
```policy
// Records that a device was granted permission to use a label
// for certain channel operations.
//
// # Foreign Keys
//
// - `label_id` refers to the `Label` fact.
// - `device_id` refers to the `Device` fact.
//
// # Caveats
//
// TODO: https://github.com/aranya-project/aranya-core/issues/229
// We do not yet support prefix deletion, so this fact is NOT
// deleted when the label is deleted.
fact LabelAssignedToDevice[label_id id, device_id id]=>{op enum ChanOp, device_gen int}
// Grants the device permission to use the label.
//
// - It is an error if the author does not have the role required
// to assign this label.
// - It is an error if `device_id` refers to the author (devices
// are never allowed to assign labels to themselves).
// - It is an error if the device does not exist.
// - It is an error if the label does not exist.
// - It is an error if the device has already been granted
// permission to use this label for its current generation.
// - It is an error if the device is not permitted to use AFC.
// - It is an error if the device's generation has changed since
// the action was authored (stale membership epoch).
//
// # Required Permissions
//
// - `AssignLabel`
//
// Additionally, the target device must have `CanUseAfc` permissions
action assign_label_to_device(device_id id, label_id id, op enum ChanOp) {
// Bind the command to this membership epoch.
let gen = get_device_gen(device_id)
publish AssignLabelToDevice {
device_id: device_id,
label_id: label_id,
op: op,
device_gen: gen,
}
}
// Emitted when the `AssignLabelToDevice` command is successfully
// processed.
effect AssignedLabelToDevice {
// The ID of the device that was assigned the label.
device id,
// The ID of the label that was assigned.
label_id id,
// The ID of the device that assigned the label.
author_id id,
}
command AssignLabelToDevice {
attributes {
priority: 100
}
fields {
// The target device.
device_id id,
// The label being assigned to the target device.
label_id id,
// The channel operations the device is allowed to use
// the label for.
op enum ChanOp,
// Device generation at authoring time; rejects stale epochs.
device_gen int,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Author must have permission to assign a label and outrank the target device and label.
check author_has_perm_two_targets(author.device_id, Perm::AssignLabel, this.device_id, this.label_id)
// Make sure we uphold `AssignedLabelToDevice`'s foreign
// keys.
check exists Device[device_id: this.device_id]
check exists Label[label_id: this.label_id]
// The target device must be able to use AFC.
check device_has_perm(this.device_id, Perm::CanUseAfc)
// Reject if the device's membership epoch changed (e.g. reordered remove/re-add).
let current_gen = get_device_gen(this.device_id)
check this.device_gen == current_gen
let existing_assignment = query LabelAssignedToDevice[
label_id: this.label_id,
device_id: this.device_id,
]
if existing_assignment is Some {
// Only allow reuse when the stored assignment is
// from an older device generation.
let assignment = unwrap existing_assignment
check assignment.device_gen < current_gen
// At this point we believe the following to be true:
//
// - `author` has the `AssignLabel` permission
// - `author` outranks `this.label_id`
// - `author` outranks `this.device_id`
// - `this.device_id` refers to a device that exists
// - `this.label_id` refers to a label that exists
// - the command's generation matches the device's current generation
// - the existing assignment is stale because the device has
// been re-provisioned
finish {
update LabelAssignedToDevice[
label_id: this.label_id,
device_id: this.device_id,
]=>{
op: assignment.op,
device_gen: assignment.device_gen,
} to {
op: this.op,
device_gen: current_gen,
}
emit AssignedLabelToDevice {
device: this.device_id,
label_id: this.label_id,
author_id: author.device_id,
}
}
} else {
// At this point we believe the following to be true:
//
// - `author` has the `AssignLabel` permission
// - `author` outranks `this.label_id`
// - `author` outranks `this.device_id`
// - `this.device_id` refers to a device that exists
// - `this.label_id` refers to a label that exists
// - the command's generation matches the device's current generation
finish {
create LabelAssignedToDevice[
label_id: this.label_id,
device_id: this.device_id,
]=>{
op: this.op,
device_gen: this.device_gen,
}
emit AssignedLabelToDevice {
device: this.device_id,
label_id: this.label_id,
author_id: author.device_id,
}
}
}
}
}
```
#### Label Revocation
```policy
// Revokes permission to use a label from a device.
//
// - It is an error if the device does not exist.
// - It is an error if the label does not exist.
// - It is an error if the device has not been granted permission
// to use this label.
//
// # Required Permissions
//
// - `RevokeLabel`
action revoke_label_from_device(device_id id, label_id id) {
publish RevokeLabelFromDevice {
device_id: device_id,
label_id: label_id,
}
}
// Emitted when the `RevokeLabelFromDevice` command is
// successfully processed.
effect LabelRevokedFromDevice {
// The ID of the device the label was removed from.
device_id id,
// The ID of the label that was revoked.
label_id id,
// The name of the label that was revoked.
label_name string,
// The ID of the author of the label.
label_author_id id,
// The ID of the device that revoked the label.
author_id id,
}
command RevokeLabelFromDevice {
attributes {
priority: 300
}
fields {
// The target device.
device_id id,
// The label being revoked from the target device.
label_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let author = get_author(envelope)
// Implicitly checks that the device exists.
let target = get_device(this.device_id)
// The author device must have permission to revoke the label and outrank the target device and label.
check author_has_perm_two_targets(author.device_id, Perm::RevokeLabel, this.device_id, this.label_id)
// We need to get label info before deleting
let label = check_unwrap query Label[label_id: this.label_id]
let assignment = check_unwrap query LabelAssignedToDevice[
label_id: this.label_id,
device_id: this.device_id,
]
// Reject revocations of stale label assignments. When a
// device is removed and re-added its generation counter is
// incremented, which implicitly invalidates all prior label
// assignments. Revoking one of those stale assignments
// would delete the fact row and prevent a future (valid)
// assign from reusing it via the `device_gen < current_gen`
// update path.
check label_assignment_matches_gen(this.device_id, assignment.device_gen)
// At this point we believe the following to be true:
//
// - the team is active
// - `author` has the `RevokeLabel` permission
// - `author` outranks `this.device_id`
// - `author` outranks `this.label_id`
// - `this.label_id` refers to a label that exists
// - the label assignment matches the device's current generation
finish {
delete LabelAssignedToDevice[
label_id: this.label_id,
device_id: this.device_id,
]
emit LabelRevokedFromDevice {
device_id: target.device_id,
label_id: this.label_id,
label_name: label.name,
label_author_id: label.author_id,
author_id: author.device_id,
}
emit CheckValidAfcChannels {}
}
}
}
```
#### Label Lookup
```policy
// Returns the channel operation for a particular label, or `None`
// if the device does not have permission to use the label.
//
// # Caveats
//
// - It does NOT check whether the device exists.
function get_allowed_chan_op_for_label(device_id id, label_id id) optional enum ChanOp {
// Now see if the device was directly granted permission
// to use the label.
let assigned_to_dev = query LabelAssignedToDevice[
label_id: label_id,
device_id: device_id,
]
let device_op = device_assignment_op(device_id, assigned_to_dev)
return device_op
}
// Returns the channel operation for a device-specific label
// assignment if it matches the device's current generation.
function device_assignment_op(
device_id id,
assignment optional struct LabelAssignedToDevice,
) optional enum ChanOp {
if assignment is None {
return None
}
let assigned = unwrap assignment
if label_assignment_matches_gen(
device_id,
assigned.device_gen,
) {
return Some(assigned.op)
}
return None
}
// Reports whether a device's direct label assignment generation
// matches the device's current generation counter.
function label_assignment_matches_gen(
device_id id,
assignment_gen int,
) bool {
let maybe_gen = query DeviceGeneration[device_id: device_id]
if maybe_gen is None {
return false
}
return (unwrap maybe_gen).generation == assignment_gen
}
```
#### Permission Queries
Permission queries for determining what permissions are assigned to roles and devices.
##### `query_role_has_perm`
Returns whether a role has a specific permission.
If the role does not have the permission, no effect is emitted.
```policy
// Emits `QueryRoleHasPermResult` if the role has the permission.
// If the role does not have the permission, no effect is emitted.
ephemeral action query_role_has_perm(role_id id, perm enum Perm) {
publish QueryRoleHasPerm {
role_id: role_id,
perm: perm,
}
}
effect QueryRoleHasPermResult {
// The role's unique ID.
role_id id,
// The permission the role has.
perm enum Perm,
}
ephemeral command QueryRoleHasPerm {
fields {
role_id id,
perm enum Perm,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
// Check that the role exists.
check exists Role[role_id: this.role_id]
let has_perm = exists RoleHasPerm[role_id: this.role_id, perm: this.perm]
if has_perm {
finish {
emit QueryRoleHasPermResult {
role_id: this.role_id,
perm: this.perm,
}
}
} else {
finish {}
}
}
}
```
##### `query_role_perms`
Returns an effect for each permission the role has.
If the role does not have any permissions, no effects are emitted.
```policy
// Emits `QueryRolePermsResult` for each permission assigned to the role.
// If the role does not have any permissions, no effects are emitted.
ephemeral action query_role_perms(role_id id) {
map RoleHasPerm[role_id: role_id, perm: ?] as f {
publish QueryRolePerms {
role_id: f.role_id,
perm: f.perm,
}
}
}
effect QueryRolePermsResult {
// The role's unique ID.
role_id id,
// The permission assigned to the role.
perm enum Perm,
}
ephemeral command QueryRolePerms {
fields {
role_id id,
perm enum Perm,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
// Check that the role exists.
check exists Role[role_id: this.role_id]
finish {
emit QueryRolePermsResult {
role_id: this.role_id,
perm: this.perm,
}
}
}
}
```
#### Label Queries
Label queries retrieve information about labels on the team.
See [Query APIs](#query-apis) for more information about the query
APIs.
##### `query_label`
Returns a specific label if it exists.
```policy
// Emits `QueryLabelResult` for the label if it exists.
// If the label does not exist then no effect is emitted.
ephemeral action query_label(label_id id) {
publish QueryLabel {
label_id: label_id,
}
}
effect QueryLabelResult {
// The label's unique ID.
label_id id,
// The label name.
label_name string,
// The ID of the device that created the label.
label_author_id id,
}
ephemeral command QueryLabel {
fields {
label_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let maybe_label = query Label[label_id: this.label_id]
if maybe_label is None {
finish {}
} else {
let label = unwrap maybe_label
finish {
emit QueryLabelResult {
label_id: label.label_id,
label_name: label.name,
label_author_id: label.author_id,
}
}
}
}
}
```
##### `query_labels`
Returns a list of all labels that exist in the team.
```policy
// Emits one `QueryLabelsResult` for each label in the team.
// If the team does not have any labels then no effects are
// emitted.
ephemeral action query_labels() {
map Label[label_id: ?] as f {
publish QueryLabels {
label_id: f.label_id,
label_name: f.name,
label_author_id: f.author_id,
}
}
}
effect QueryLabelsResult {
// The label's unique ID.
label_id id,
// The label name.
label_name string,
// The ID of the device that created the label.
label_author_id id,
}
// Trampoline to forward info to `QueryLabelsResult`.
ephemeral command QueryLabels {
fields {
label_id id,
label_name string,
label_author_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
finish {
emit QueryLabelsResult {
label_id: this.label_id,
label_name: this.label_name,
label_author_id: this.label_author_id,
}
}
}
}
```
##### `query_labels_assigned_to_device`
```policy
// Emits `QueryLabelsAssignedToDeviceResult` for all labels the
// device has been granted permission to use.
ephemeral action query_labels_assigned_to_device(device_id id) {
// TODO: make this query more efficient when policy supports
// it. The key order is optimized for `delete`.
map LabelAssignedToDevice[label_id: ?, device_id: ?] as f {
if f.device_id == device_id {
if label_assignment_matches_gen(f.device_id, f.device_gen) {
let label = check_unwrap query Label[label_id: f.label_id]
publish QueryLabelsAssignedToDevice {
device_id: f.device_id,
label_id: f.label_id,
label_name: label.name,
label_author_id: label.author_id,
}
}
}
}
}
effect QueryLabelsAssignedToDeviceResult {
// The device's unique ID.
device_id id,
// The label's unique ID.
label_id id,
// The label name.
label_name string,
// The ID of the device that created the label.
label_author_id id,
}
ephemeral command QueryLabelsAssignedToDevice {
fields {
device_id id,
label_id id,
label_name string,
label_author_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
// Check that the device exists.
check exists Device[device_id: this.device_id]
finish {
emit QueryLabelsAssignedToDeviceResult {
device_id: this.device_id,
label_id: this.label_id,
label_name: this.label_name,
label_author_id: this.label_author_id,
}
}
}
}
```
#### Label Directionality
AFC channels are always unidirectional, with a channel creator who is
permitted to send data and the other peer who receives data. A label's
`ChanOp` controls whether a device can operate as the channel creator
(`SendOnly`), channel receiver (`RecvOnly`), or both (`SendRecv`).
```policy
// Valid channel operations for a label assignment.
enum ChanOp {
// The device can only receive data in channels with this
// label.
RecvOnly,
// The device can only send data in channels with this
// label.
SendOnly,
// The device can send and receive data in channels with this
// label.
SendRecv,
}
```
### AFC
#### AFC Unidirectional Channel Creation
Creates a unidirectional AFC channel. This is an ephemeral command,
which means that it can only be emitted within an ephemeral session and
is not added to the graph of commands. Furthermore, it does not persist
any changes to the factDB.
The `create_afc_uni_channel` action creates the `ChannelKey`,
encapsulates it for the peer, and sends the encapsulation through the
`AfcCreateUniChannel` command. When processing the command, the
corresponding recipient will decapsulate their key and store it in the
shared memory DB.
```policy
ephemeral action create_afc_uni_channel(receiver_id id, label_id id) {
let parent_cmd_id = perspective::head_id()
let author_id = device::current_device_id()
let author_enc_key_id = get_enc_key_id(author_id)
let peer_enc_pk = get_enc_pk(receiver_id)
let ch = afc::create_uni_channel(
parent_cmd_id,
author_enc_key_id,
peer_enc_pk,
author_id,
receiver_id,
label_id,
)
publish AfcCreateUniChannel {
receiver_id: receiver_id,
label_id: label_id,
peer_encap: ch.peer_encap,
channel_key_id: ch.key_id,
}
}
// Emitted when the author of a unidirectional AFC channel
// successfully processes the `AfcCreateUniChannel` command.
effect AfcUniChannelCreated {
// The unique ID of the previous command.
parent_cmd_id id,
// The device ID of the participant that can receive data.
receiver_id id,
// The channel author's encryption key ID.
author_enc_key_id id,
// The channel peer's encoded public encryption key.
peer_enc_pk bytes,
// The channel label.
label_id id,
// The channel key ID.
channel_key_id id,
// The channel peer's encapsulated KEM shared secret.
encap bytes,
}
// Emitted when the peer of a unidirectional AFC channel
// successfully processes the `AfcCreateUniChannel` command.
effect AfcUniChannelReceived {
// The unique ID of the previous command.
parent_cmd_id id,
// The device ID of the participant that can send data.
sender_id id,
// The channel author's encryption key ID.
author_enc_pk bytes,
// The channel peer's encryption key ID.
peer_enc_key_id id,
// The channel label.
label_id id,
// The channel peer's encapsulated KEM shared secret.
encap bytes,
}
ephemeral command AfcCreateUniChannel {
fields {
// The device ID of the participant that can receive
// data.
receiver_id id,
// The label applied to the channel.
label_id id,
// The channel peer's encapsulated KEM shared secret.
peer_encap bytes,
// The ID of the AFC channel key.
channel_key_id id,
}
seal { return seal_command(serialize(this)) }
open { return deserialize(open_envelope(envelope)) }
policy {
check team_exists()
let sender = get_author(envelope)
let sender_id = sender.device_id
let receiver_id = this.receiver_id
let receiver = check_unwrap try_find_device(receiver_id)
// Check that both devices have permission to create the AFC channel.
check afc_uni_channel_is_valid(sender_id, receiver_id, this.label_id)
let parent_cmd_id = envelope::parent_id(envelope)
let current_device_id = device::current_device_id()
if current_device_id == sender_id {
// We authored this command.
let peer_enc_pk = get_enc_pk(receiver_id)
let sender_enc_key_id = get_enc_key_id(sender_id)
finish {
emit AfcUniChannelCreated {
parent_cmd_id: parent_cmd_id,
receiver_id: receiver_id,
author_enc_key_id: sender_enc_key_id,
peer_enc_pk: peer_enc_pk,
label_id: this.label_id,
channel_key_id: this.channel_key_id,
encap: this.peer_encap,
}
}
} else if current_device_id == receiver_id {
// We're the intended recipient of this command.
let author_enc_pk = get_enc_pk(sender_id)
let receiver_enc_key_id = get_enc_key_id(receiver_id)
finish {
emit AfcUniChannelReceived {
parent_cmd_id: parent_cmd_id,
sender_id: sender_id,
author_enc_pk: author_enc_pk,
peer_enc_key_id: receiver_enc_key_id,
label_id: this.label_id,
encap: this.peer_encap,
}
}
} else {
// This is an off-graph session command, so only the
// communicating peers should process this command.
check false
}
}
}
// Reports whether an AFC channel is valid according to the policy.
// The following criteria must be met for an AFC channel to be valid:
// - The label must exist
// - The label must be assigned to the sender with write permissions: `SendOnly` or `SendRecv`
// - The label must be assigned to the receiver with read permissions: `RecvOnly` or `SendRecv`
// - The sender must have `CreateAfcUniChannel` permission assigned to its respective role.
// - Sender and receiver devices must:
// - Be members of the team
// - Not have matching device IDs
// - Have `CanUseAfc` permission assigned to their respective roles
function afc_uni_channel_is_valid(sender_id id, receiver_id id, label_id id) bool {
// The label must exist.
let label = query Label[label_id: label_id]
if label is None {
return false
}
// Devices cannot create channels with themselves.
//
// This should have been caught by the AFC FFI
if sender_id == receiver_id {
return false
}
// Devices must be members of the team
let sender = try_find_device(sender_id)
if sender is None {
return false
}
let receiver = try_find_device(receiver_id)
if receiver is None {
return false
}
// The writer must have permissions to write (send) data.
let writer_op = get_allowed_chan_op_for_label(sender_id, label_id)
if writer_op is None {
return false
}
match unwrap writer_op {
ChanOp::RecvOnly => { return false }
ChanOp::SendOnly => {}
ChanOp::SendRecv => {}
}
// The reader must have permission to read (receive) data.
let reader_op = get_allowed_chan_op_for_label(receiver_id, label_id)
if reader_op is None {
return false
}
match unwrap reader_op {
ChanOp::RecvOnly => {}
ChanOp::SendOnly => { return false }
ChanOp::SendRecv => {}
}
// Sender must have `CreateAfcUniChannel`, `CanUseAfc` permissions
if !device_has_perm(sender_id, Perm::CreateAfcUniChannel) {
return false
}
if !device_has_perm(sender_id, Perm::CanUseAfc) {
return false
}
// Receiver must have `CanUseAfc` permission
if !device_has_perm(receiver_id, Perm::CanUseAfc) {
return false
}
return true
}
```
[//]: # (links)
[actions]: https://aranya-project.github.io/policy-book/reference/top-level/actions.html
[afc]: https://aranya-project.github.io/afc/
[afc-ffi]: https://crates.io/crates/aranya-afc-util
[all-the-way-down]: https://en.wikipedia.org/wiki/Turtles_all_the_way_down
[commands]: https://aranya-project.github.io/policy-book/reference/top-level/commands.html
[crypto-ffi]: https://crates.io/crates/aranya-crypto-ffi
[device-ffi]: https://crates.io/crates/aranya-device-ffi
[effects]: https://aranya-project.github.io/policy-book/reference/top-level/effects.html
[envelope]: https://aranya-project.github.io/policy-book/reference/top-level/commands.html#envelope-type
[evp-ffi]: https://crates.io/crates/aranya-envelope-ffi
[facts]: https://aranya-project.github.io/policy-book/reference/top-level/facts.html
[idam-ffi]: https://crates.io/crates/aranya-idam-ffi
[lp]: https://en.wikipedia.org/wiki/Literate_programming
[perspective-ffi]: https://crates.io/crates/aranya-perspective-ffi
[policy-lang]: https://aranya-project.github.io/policy-book/reference/introduction.html
[rbac]: https://csrc.nist.gov/glossary/term/rbac