Safe Mode Examples: Static Capabilities vs Runtime Permissions

Runtime permission systems (sandboxes, ACLs, policy engines) check each operation in isolation: "can this agent read this file? yes. can it call print? yes." They have no way to reason about the composition of permitted operations — a sequence of individually-allowed steps can produce an outcome that no single step would have been allowed to achieve (delete a file by moving it somewhere deletable, exfiltrate a secret by printing it to stdout, escape a scope by capturing a reference in a closure).

Composable capabilities tracked by the type system work differently. Instead of checking operations against a policy at runtime, the type system tracks which capabilities flow where at compile time. An operation that would require a capability the code doesn't have simply cannot be expressed — it's not forbidden by a rule that someone had to anticipate, it's structurally absent from the program. This is a difference in expressivity: there are security properties (information flow, purity of transformations, scope confinement) that static capabilities can enforce and runtime permissions fundamentally cannot.

These examples demonstrate this gap concretely. Each one shows an attack that succeeds under runtime permissions and is blocked at compile time by Scala 3's safe mode with capture checking, as implemented by TACIT.

Each example comes in two (or three) variants:

• *-runtime.scala — shows the attack succeeding under a runtime permission system
• *-safe.scala — shows the same attack blocked by the type system at compile time
• *-safe-allowed.scala / *-safe-simplified.scala — shows that legitimate operations still work

Prerequisites

• JDK 17+
• scala-cli

Setup

1. Initialize the TACIT submodule (optional, for reference)

The tacit/ directory is the TACIT framework (the paper's reference implementation) included as a git submodule. It's not required to run the examples but useful for reference.

git submodule update --init

2. Publish the capability library locally

The examples depend on a small capability library in examples/lib/ that models the TACIT API surface. It must be published to your local Ivy repository before the safe-mode examples can resolve it.

cd examples/lib
scala-cli publish local .

This publishes com.example::safemode-capabilities:0.1.0 to ~/.ivy2/local/.

3. Run the examples

From the examples/ directory:

cd examples

# Runtime examples run directly:
scala-cli run 1-two-directories-runtime.scala

# Safe-mode examples are expected to fail compilation:
scala-cli compile 1-two-directories-safe.scala

Or use the test script to run everything at once (publishes the library, runs all examples, and checks that safe-mode files are correctly rejected by the compiler):

cd examples
./run-all-tests.sh

The script classifies each file as run (expect success), compile (expect rejection), or compile (expect known compiler crash) and reports a summary at the end.

Examples

1. Two Directories (Move-then-Delete)

An agent has two filesystem instances: /data (NonDestructive) and /tmp (FullAccess). It circumvents the "no delete" policy by moving a file to /tmp and deleting it there. Each individual operation passes its runtime permission check.

The type system uses CanDestroy[P] evidence — only FullAccess has it. delete() and moveFile() both require CanDestroy on the source filesystem. copyFile() only requires CanWrite on the target, so it remains available.

File	How to test	Expected
1-two-directories-runtime.scala	scala-cli run	Runs. Move-then-delete succeeds, policy violated.
1-two-directories-safe.scala	scala-cli compile	Fails. CanDestroy[NonDestructive] not found on delete() and moveFile().
1-two-directories-safe-allowed.scala	scala-cli run	Runs. copy, rename-within, move-from-FullAccess all work.

2. Classified Data Exfiltration

An agent reads classified data and tries to exfiltrate it through every available channel: stdout (print), network (HTTP POST), and filesystem (file write). Runtime systems allow each operation individually.

readClassified returns Classified[String]. Classified.map requires a pure function (T -> U, not T => U). The capture checker verifies that the lambda captures no capabilities — no IO, no Network, no FileSystem. Any side effect is a compile error.

File	How to test	Expected
2-classified-exfiltration-runtime.scala	scala-cli run	Runs. Secret exfiltrated via print, network, and map side effect.
2-classified-exfiltration-safe.scala	scala-cli compile	Fails. Three errors: IOCapability, net, fs cannot flow into capture set {}.

3. Capability Scope Escape

An agent captures a filesystem capability in a closure and returns it from the scoped block, using it after the scope has ended. Runtime systems must track all references for revocation — notoriously hard to get right.

The capture checker sees that the closure's type is () ->{fs} String (captures fs), but the block's return type requires () -> String (pure). The capability structurally cannot escape its scope.

File	How to test	Expected
3-scope-escape-runtime.scala	scala-cli run	Runs. Revocation catches it this time, but the approach is fragile.
3-scope-escape-safe.scala	scala-cli compile	Fails. capability 'fs' cannot flow into capture set {}.

4. Confused Deputy via Sub-Agent

An agent with restricted filesystem access asks a sub-agent (via chat()) to read files it shouldn't have access to. The runtime sees a permitted chat call but doesn't know it's an authority escalation.

chat(String): String has no FileSystem in its type signature. The sub-agent structurally cannot access any filesystem regardless of what the prompt says.

File	How to test	Expected
4-confused-deputy-runtime.scala	scala-cli run	Runs. Sub-agent returns /etc/passwd contents.
4-confused-deputy-safe-simplified.scala	scala-cli run	Runs safely. Chat returns a mock response, classified data stays wrapped.
4-confused-deputy-safe.scala	scala-cli compile	Compiler crash (known nightly bug, see below).

Compiler Crash Repro

compiler-crash-repro.scala contains a minimal reproducer for a compiler crash in SafeRefs.checkNotRejected (NoDenotation.owner). The trigger is string interpolation (s"...$x...") in safe mode. No dependencies needed.

Capability Library

The library in lib/ models the key ideas from TACIT:

• FileSystem[P] parameterized by permission level (ReadOnly, NonDestructive, FullAccess)
• CanWrite[P] / CanDestroy[P] type-level evidence gating operations
• Classified[T] with purity-enforced map (pure function T -> U only)
• Scoped capability grants via requestFileSystem, requestNetwork
• @implicitNotFound annotations for clear error messages

The library is compiled without import language.experimental.safe but with @assumeSafe annotations (from scala.caps). Safe-mode consumer code can only call APIs that are either in the safe stdlib subset or explicitly marked @assumeSafe by a library author. This is the key architectural pattern: the library is a trusted boundary, agent code is untrusted.