Access Control

Proving authorization properties, role-based guards, and permission hierarchies for smart contracts.

Access control is fundamental to smart contract security. A bug that allows unauthorized access can lead to stolen funds or corrupted state. Sector9 lets you prove access control properties statically, but exported actor methods still need runtime entry guards.

The Access Control Model

Sector9 separates runtime admission from logical proof. You express who can call what using:

Runtime state or parameters for facts that external callers must satisfy
entry_requires to enforce exported-method guards at runtime
requires to expose the same facts as logical verifier preconditions
Ghost state only for proof-only mirrors, summaries, or history
Invariants to maintain role consistency

Ghost state is erased and cannot be the only source of runtime authorization. If a role must be enforced against external callers, keep a runtime representation or a runtime-checkable caller identity and guard it with entry_requires. For the exported-method rule, see entry_requires.

Single Owner Pattern

The simplest access control pattern: one account owns the contract and has exclusive access to sensitive operations.

access-owner-pattern.sr9
// Single owner pattern with ownership transfer
persistent actor {
  var balance : Nat = 0;
  var owner : ?Principal = null;

  // First caller claims ownership
  public shared({caller}) func claimOwnership() : async ()
    modifies owner
    entry_requires owner == null;
    requires owner == null;
    ensures owner == ?caller;
  {
    owner := ?caller;
  };

  // Only owner can deposit
  public shared({caller}) func deposit(amount : Nat) : async ()
    modifies balance
    reads owner
    entry_requires owner == ?caller;
    entry_requires amount > 0;
    requires owner == ?caller;
    requires amount > 0;
    ensures balance == old(balance) + amount;
  {
    balance := balance + amount;
  };

  // Only owner can withdraw
  public shared({caller}) func withdraw(amount : Nat) : async ()
    modifies balance
    reads owner
    entry_requires owner == ?caller;
    entry_requires amount <= balance;
    requires owner == ?caller;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
  {
    balance := balance - amount;
  };

  // Only owner can transfer ownership
  public shared({caller}) func transferOwnership(newOwner : Principal) : async ()
    modifies owner
    entry_requires owner == ?caller;
    requires owner == ?caller;
    ensures owner == ?newOwner;
  {
    owner := ?newOwner;
  };

  // Anyone can check the owner
  public func getOwner() : async ?Principal
    reads owner
    ensures result == owner;
  {
    owner
  };
}

Key elements:

Runtime owner state tracks the owner for exported methods
entry_requires owner == ?caller enforces ownership checks at entry
requires owner == ?caller gives the verifier the same logical fact
transferOwnership allows safe ownership transfer with verification

The verifier proves the methods are safe assuming the entry guard admitted the caller; the runtime projection preserves that guard.

Role-Based Access with Sets

For multiple users with the same role, keep a runtime role representation for admission and use ghost sets only as proof mirrors.

Use runtime role storage for deployed authorization. Ghost sets are useful as proof mirrors, for example to state that the runtime admin list is non-empty or that a runtime update preserves membership facts, but a ghost-only set is not a runtime authorization database.

Key elements:

Runtime role state is required for exported-method admission
entry_requires checks the runtime role fact
Ghost Set values can summarize or mirror the runtime role state in proofs
Invariants can relate the runtime representation to the ghost model
Role changes update runtime state and, when used, the ghost mirror

Permission Levels with Maps

For hierarchical permissions (none < read < write < admin), keep the permission table in runtime state and mirror it with a ghost map when the proof needs set/map-style facts.

For production code, keep the permission table in a runtime collection or other runtime state. A ghost Map<Nat, Nat> can mirror that table for proof facts, but it cannot be the only source of truth for an exported entry_requires check.

Key elements:

Runtime permission state admits or rejects external calls
Ghost maps express proof summaries such as "admin level implies write level"
Pure helpers make logical preconditions readable
Invariants connect runtime permission storage to the ghost model

Multi-Role Systems

Complex systems often have multiple distinct roles. Keep each exported action tied to a runtime guard, and use separate ghost sets or maps when they make the proof simpler.

This pattern separates concerns:

Admins control system configuration (freeze/unfreeze)
Operators perform day-to-day operations (transfers)
Auditors have read-only access for oversight

Each role should have its own runtime entry guard and matching logical precondition. Ghost role sets can help prove role consistency, but exported methods must not rely on ghost-only state for authorization.

Access Control and Async

Access control becomes subtle with async operations. Consider this pattern:

public shared({caller}) func sensitiveOperation() : async ()
  modifies data
  reads admins
  entry_requires isRuntimeAdmin(caller);
  requires Set.contains(caller, admins);
{
  // Check passes here - caller is admin
  let result = try { await externalCall() } catch (_) { 0 };

  // After await: caller still refers to the same account,
  // but admins set may have changed!
  // The invariant guarantees what's preserved across await
  data := result;
}

The bound caller : Principal is immutable, so it stays valid. Runtime role state can change during the await through interleaving calls, and any ghost mirror must be related back to actor invariants if you want facts to persist. Recheck authorization after the await when the operation depends on the current role table, not only on the original caller.

Combining with Token Patterns

Access control often combines with token systems. For example, only the owner can mint:

var owner : ?Principal = null;
var totalSupply : Nat = 0;
var balance : Nat = 0;

invariant balance == totalSupply;

public shared({caller}) func mint(amount : Nat) : async ()
  modifies balance, totalSupply
  reads owner
  entry_requires owner == ?caller;
  entry_requires amount > 0;
  requires owner == ?caller;
  requires amount > 0;
  ensures balance == old(balance) + amount;
{
  balance += amount;
  totalSupply += amount;
}

The ownership check combines with the conservation invariant from Token Systems.

Caller Identity

In Sector9, caller identity comes from the IC message context. Bind it with shared({caller}); do not accept a user-provided caller argument.

public shared({caller}) func withdraw(amount : Nat) : async ()
  entry_requires owner == ?caller;
  entry_requires amount <= balance;
  requires owner == ?caller;
  requires amount <= balance;
{
  balance -= amount;
}

The bound caller is a Principal. Your preconditions verify that the caller has appropriate permissions before any state changes occur. See caller identity for the language-level binding.

Common Mistakes

Missing Access Checks

// Wrong - no access check
public func unsafeWithdraw(amount : Nat) : async ()
  modifies balance
{
  balance -= amount;  // Anyone can call this!
}

// Correct - caller comes from the shared method context
public shared({caller}) func safeWithdraw(amount : Nat) : async ()
  modifies balance
  reads owner
  entry_requires owner == ?caller;
  requires owner == ?caller;
{
  balance -= amount;
}

Forgetting Ghost Updates

// Wrong - ghost state not updated
public shared({caller}) func addAdmin(newAdmin : Principal) : async ()
  reads admins
  entry_requires isRuntimeAdmin(caller);
  requires Set.contains(caller, admins);
{
  // Forgot to add newAdmin to the set!
}

// Correct - ghost state synchronized
public shared({caller}) func addAdmin(newAdmin : Principal) : async ()
  modifies admins
  entry_requires isRuntimeAdmin(caller);
  requires Set.contains(caller, admins);
{
  ghost { admins := Set.union(admins, Set.singleton(newAdmin)); };
}

Inconsistent Role Checks

// Wrong - different checks for same role
public shared({caller}) func operationA() : async ()
  entry_requires primaryAdmin == ?caller or secondaryAdmin == ?caller;
  requires primaryAdmin == ?caller or secondaryAdmin == ?caller;

public shared({caller}) func operationB() : async ()
  entry_requires isRuntimeAdmin(caller);
  requires Set.contains(caller, admins);  // Ghost mirror check

// Correct - consistent role definition
public shared({caller}) func operationA() : async ()
  entry_requires isRuntimeAdmin(caller);
  requires Set.contains(caller, admins);

public shared({caller}) func operationB() : async ()
  entry_requires isRuntimeAdmin(caller);
  requires Set.contains(caller, admins);

Use a single pure helper or shared predicate shape consistently to avoid divergent access control logic. If entry_requires checks runtime state and requires checks a ghost mirror, maintain an invariant that connects them.

Permission Model vs Access Control

Sector9 has two distinct "permission" concepts:

Access Control (this page): who can call which functions, enforced by runtime state plus entry_requires and reasoned about with requires
Permission Model: Heap access permissions (reads/modifies) for field access

They work together: access control determines authorization (is this caller allowed?), while the permission model determines capability (can this function access this field?).

Summary

Use runtime variables for authorization facts that must be enforced after deployment
Use ghost variables/sets/maps for proof-only mirrors and summaries
Express exported access checks as entry guards plus preconditions: entry_requires owner == ?caller; requires owner == ?caller
Write pure helpers for readable checks, with runtime and proof sides aligned: entry_requires isRuntimeAdmin(caller) plus requires isAdmin(admins, caller)
Use invariants to maintain role consistency: invariant Set.card(admins) > 0
Update ghost state in ghost { } blocks synchronized with role changes
Consider async interference: roles may change during await, but the bound caller stays stable
Keep runtime checks, logical checks, and actor invariants aligned so access rules remain auditable

The Access Control Model​

Single Owner Pattern​

Role-Based Access with Sets​

Permission Levels with Maps​

Multi-Role Systems​

Access Control and Async​

Combining with Token Patterns​

Caller Identity​

Common Mistakes​

Missing Access Checks​

Forgetting Ghost Updates​

Inconsistent Role Checks​

Permission Model vs Access Control​

Summary​

The Access Control Model

Single Owner Pattern

Role-Based Access with Sets

Permission Levels with Maps

Multi-Role Systems

Access Control and Async

Combining with Token Patterns

Caller Identity

Common Mistakes

Missing Access Checks

Forgetting Ghost Updates

Inconsistent Role Checks

Permission Model vs Access Control

Summary