Skip to main content
Glama

TACIT: Tracked Agent Capabilities In Types

Paper: Securing Agents With Tracked Capabilities (ACM) · arXiv:2603.00991 · 🏆 Best Paper Award at CAIS 26

TACIT (Tracked Agent Capabilities In Types) ist ein Sicherheits-Harness für KI-Agenten. Statt Werkzeuge direkt aufzurufen, schreiben Agenten Code in Scala 3 mit capture checking: einem Typsystem, das Capabilities statisch nachverfolgt und durchsetzt, dass Agentencode keine Zugriffsrechte fälschen, keine Effekte über sein Budget hinaus ausführen und keine Informationen aus reinen Unterberechnungen preisgeben kann. Es stellt eine MCP-Schnittstelle bereit, sodass es einfach von allen MCP-kompatiblen Agenten verwendet werden kann.

Übersicht über das TACIT-Framework

Das Framework hat drei Hauptkomponenten:

  • Scala-3-Compiler. Der vom übermittelte Code des Agenten wird validiert und mit aktiviertem Capture-Checking im Safe Mode typprüft. Dadurch wird eine capability-sichere Sprachteilmenge erzwungen.

  • Scala-REPL. Eine lokale REPL-Instanz führt kompilierten Code aus und verwaltet den Zustand über Interaktionen hinweg. Unterstützt werden sowohl zustandslose Einmalausführungen als auch zustandsbehaftete Sitzungen.

  • Capability-Sicherheitsbibliothek. Eine typisierte API, die als einziges Tor für die Interaktion des Agentencodes mit der realen Welt dient: Dateisystem, Prozessausführung, Netzwerk und Unteragenten. Die Bibliothek ist erweiterbar: Neue Capabilities lassen sich hinzufügen, indem nur der Bibliothekscode geändert wird, ohne den MCP-Server selbst zu verändern.

Schnellstart

TACIT bietet einen standardmäßigen MCP-Server, der über JSON-RPC über stdio kommuniziert. Er funktioniert mit jedem MCP-kompatiblen Agenten, einschließlich Claude Code, OpenCode, GitHub Copilot und anderen.

Erforderlich ist JDK 17+.

TACIT installieren

Wählen Sie einen der unten genannten Installationsansätze. Der tacit-CLI-Webdapter ist die empfohlene Option.

Option 1: tacit installieren (Empfohlen)

tacit ist ein kleiner Wrapper-Befehl zur lokalen Verwaltung von TACIT. Verwenden Sie tacit setup einmal, um den Befehl zu installieren und die neueste Version zu laden, tacit update zum Aktualisieren der JARs, tacit self update zum Aktualisieren des Wrappers selbst und tacit serve zum Starten des MCP-Servers.

# Download the wrapper directly (no git clone required)
curl -fsSL https://raw.githubusercontent.com/lampepfl/tacit/refs/heads/main/tacit -o tacit
chmod +x tacit

# Install it and download the latest TACIT release
./tacit setup

Dadurch wird der Befehl tacit in ~/.local/bin installiert, sichergestellt, dass ~/.local/bin auf PATH liegt, und die neueste Version in ~/.cache/tacit/ heruntergeladen.

Häufige Befehle:

# Refresh the cached release if a new version exists
tacit update

# Refresh the tacit wrapper itself
tacit self update

# Start the MCP server
tacit serve

# Remove the wrapper and cached release
tacit self uninstall

Standardmäßig verwendet tacit:

Artefakt

Standardpfad

MCP-Server

~/.cache/tacit/TACIT.jar

Bibliothek

~/.cache/tacit/TACIT-library.jar

Option 2: Vorgefertigte Release-JARs direkt herunterladen

Falls Sie den Wrapper nicht verwenden möchten, nutzen Sie stattdessen das Release-Download-Skript.

# Download the script directly (no git clone required)
curl -fsSL https://raw.githubusercontent.com/lampepfl/tacit/refs/heads/main/download_release.sh -o download_release.sh
chmod +x download_release.sh

./download_release.sh

Optional:

# Or use wget instead of curl
wget -q https://raw.githubusercontent.com/lampepfl/tacit/refs/heads/main/download_release.sh -O download_release.sh
chmod +x download_release.sh

# Download into a custom directory
./download_release.sh ./dist
./download_release.sh --pre-release ./dist

Standardmäßig werden hier heruntergeladen:

JAR

Standardpfad

MCP-Server

./TACIT.jar

Bibliothek

./TACIT-library.jar

Sowohl der Wrapper als auch das Skript verifizieren die heruntergeladenen JARs anhand der SHA-256-Digests aus den Release-Metadaten und verweigern die Installation einer JAR, deren Digest fehlt oder nicht übereinstimmen. Downloads werden in einem temporären Verzeichnis abgelegt und erst nach der Verifizierung an den endgültigen Ort verschoben, sodass ein fehlgeschlagener Download niemals eine zuvor installierte JAR ersetzt.

Zum Build aus dem aktuellen Quellbaum siehe Option 3 unten.

Option 3: Aus dem Quellcode erstellen

Erforderlich sein JDK 17+ und sbt 1.12+.

git clone https://github.com/lampepfl/tacit.git
cd tacit

./build.sh

Optional:

# Build and copy JARs into a custom directory
./build.sh ./dist

# Show full sbt output while building
./build.sh --verbose

Dabei werden zwei JARs erstellt und kopiert:

JAR

Pfad

MCP-Server

./TACIT.jar (oder ./dist/TACIT.jar)

Bibliothek

./TACIT-library.jar (oder ./dist/TACIT-library.jar)

Wenn TACIT über eine der Optionen oben installiert ist, konfigurieren Sie Ihren Agenten so, dass er den MCP-Server startet.

Konfigurieren Ihres Agenten

Fügen Sie TACIT als MCP-Server in der Konfiguration Ihres Agenten hinzu. Haben Sie die CLI tacit installiert, verwenden Sie einfach tacit serve. Bei manueller TACIT-Installation verwenden Sie stattdessen die explizite Form java -jar ... --library-jar ....

Fügen Sie in die .mcp.json Ihres Projekts ein (oder global in ~/.claude.json).

Mit tacit:

{
  "mcpServers": {
    "tacit": {
      "command": "tacit",
      "args": ["serve"]
    }
  }
}

Mit manuellen JAR-Pfaden:

{
  "mcpServers": {
    "tacit": {
      "command": "java",
      "args": [
        "-jar", "/path/to/TACIT.jar",
        "--library-jar", "/path/to/TACIT-library.jar"
      ]
    }
  }
}

Fügen Sie in Ihre opencode.json-Datei ein.

Mit tacit:

{
  "$schema": "https://opencode.ai/config.json",
  "mcp": {
    "tacit": {
      "type": "local",
      "enabled": true,
      "command": ["tacit", "serve"]
    }
  }
}

Mit manuellen zu Pfaden:

{
  "$schema": "https://opencode.ai/config.json",
  "mcp": {
    "tacit": {
      "type": "local",
      "enabled": true,
      "command": [
        "java",
        "-jar", "/path/to/TACIT.jar",
        "--library-jar", "/path/to/TACIT-library.jar"
      ]
    }
  }
}

Fügen Sie in Ihre .vscode/mcp.json-Datei ein.

Mit tacit:

{
  "servers": {
    "tacit": {
      "command": "tacit",
      "args": ["serve"]
    }
  }
}

Mit manuellen JAR-Pfaden:

{
  "servers": {
    "tacit": {
      "command": "java",
      "args": [
        "-jar", "/path/to/TACIT.jar",
        "--library-jar", "/path/to/TACIT-library.jar"
      ]
    }
  }
}

Der Agent kann nun die Werkzeuge von TACIT nutzen, um Sandbox-Scala-Code auszuführen.

Empfohlen: Integrierte Werkzeuge deaktivieren

Um die voll "capability-basierte" Sicherheit von TACIT zu nutzen, deaktivieren Sie die "integrierte Datei-, Shell- und Netzwerk-Werkzeuge" des Agenten, damit alle Operationen über das Sandbox-vergleichbare REPL laufen.

Starten Sie mit --disallowedTools, um integrierte Werkzeuge zu blockieren:

claude --disallowedTools "Bash,Read,Write,Edit,WebFetch"

Oder fügen Sie es in die Datei .claude/settings.json Ihres Projekts ein:

{
  "permissions": {
    "disallowedTools": ["Bash", "Read", "Write", "Edit", "WebFetch"]
  }
}

Setzen Sie in opencode.json die Berechtigungen für integrierte Werkzeuge auf "deny":

{
  "$schema": "https://opencode.ai/config.json",
  "permission": {
    "*": "ask",
    "bash": "deny",
    "read": "deny",
    "edit": "deny",
    "glob": "deny",
    "grep": "deny",
    "list": "deny",
    "tacit*": "allow"
  },
  "mcp": {
    "tacit": { "..." : "..." }
  }
}

Beschränken Sie in Ihrer VS-Code-settings.json die für Copilot verfügbaren Werkzeuge:

{
  "github.copilot.chat.agent.tools": {
    "terminal": false,
    "fs_read": false,
    "fs_write": false
  }
}

Related MCP server: edict-lang

Konfiguration

Der Server kann über CLI-Flags oder eine JSON-Konfigurationsdatei konfiguriert werden. Übergeben Sie Flags direkt in den MCP-Argumenten Ihres Agenten oder verwenden Sie --config, um auf eine JSON-Datei zu verweisen.

Die Konfiguration wird in Serverkonfiguration (Transport, Aufzeichnung, Sitzungen) und Bibliothekskonfiguration (Sandbox-Verhalten, Capabilities) unterteilt. In JSON-Konfigurationsdatei liegen die Bibliothekseinstellungen unter dem Schlüssel libraryConfig und werden direkt an die Bibliothek zur Verarbeitung übergeben.

CLI-Flags

Server-Flags:

Flag

Beschreibung

--library-jar <path>

Erforderlich. Pfad zur JAR-Bibliothek (TACIT-library.jar)

-r/--record <dir>

Protokolliert jede Ausführung auf der Festplatte

-q / --quiet

Unterdrückt Startbanner und Anfrage-/Antwortprotokollierung

--no-session

Deaktiviert sitzungsbezogene Werkzeuge

--safe-mode / --no-safe-mode

Aktiviert/deaktiviert language.experimental.safe von Scala 3 in der REPL für jede Ausführung (Standard: an; siehe Sicherheitsmodus)

--exec-timeout-ms <ms>

Wall-Clock-Timeout für eine einzelne REPL-Auswertung (Standard: keine; siehe Ausführungs-Timeout)

-c / --config <path>

JSON-Konfigurationsdatei (Flags nach --config überschreiben Dateiwerte)

Bibliothek-Flags (Kurzform für einige libraryConfig-Felder):

Flag

Beschreibung

-s / --strict

Blockiert über exec eine integrierte Denylist unsicherer Befehle (Dateioperationen, Shells, Interpreter, Netzwerk-Tools, Befehlsstarter usw.). Der Abgleich ist fallweise unempfindlich. Praktisch für schnelle Experimente; für echten Produktionsbetrieb bevorzugen Sie --command-permissions.

--command-permissions <Pässe>

Mit Komma getrennte Glob-Muster für ausführbare Befehle (z. B. echo,py*,ls). Nur * wird als Wildcard interpretiert. Wenn gesetzt, wird --strict ignoriert.

--network-permissions <patterns>

Mit Komma getrennte Glob-Muster erreichbarer Hosts (z. B. *.example.com,api.github.com). Nur *` wird als Wildcard interpretiert.

--allowed-roots <paths>

Mit Komma getrennte äußere Begrenzung für requestFileSystem-Wurzeln (z. B. /home/me/project,/tmp). Eine angeforderte Wurzel muss innerhalb einer dieser Begrenzung aufgelöst werden. Standardwert: Arbeitsverzeichnis des Servers, falls nichts angegeben.

--classified-paths <patterns>

Mit Komma getrennte klassifizierte Pfadmuster (gitignore-Stil, siehe unten)

--llm-base-url <url>

Basis-URL der LLM-API

--llm-api-key <key>

LLM-API-Schlüssel

--llm-model <name>

Name des LLM-Modells

JSON-Konfigurationsdatei

{
  "recordPath": "/tmp/recordings",
  "quiet": true,
  "sessionEnabled": true,
  "safeMode": true,
  "executionTimeoutMs": 60000,
  "libraryJarPath": "/path/to/TACIT-library.jar",
  "libraryConfig": {
    "commandPermissions": ["sbt", "scala", "javac", "java", "make"],
    "networkPermissions": ["*.scala-lang.org", "github.com", "docs.oracle.com"],
    "allowedRoots": ["/home/user/project", "/tmp"],
    "classifiedPaths": [".ssh", ".env", ".env.*", "secrets"],
    "secureOutput": "/tmp/secure.log",
    "classifiedWrite": false,
    "llm": {
      "baseUrl": "https://api.example.com",
      "apiKey": "sk-...",
      "model": "gpt-..."
    }
  }
}

commandPermissions (optional). Die Exec-Allowlist: eine Liste von Glob-Mustern (nur * ist ein Platzhalter), die jeder an exec übergebene Befehl erfüllen muss. Diese ergänzt die pro Scope deklarierte Menge aus requestExecPermission(...), ein Befehl muss in beiden enthalten sein, um tatsächlich ausgeführt zu werden. Wenn gesetzt, wird strictMode ignoriert. In echten Bereitstellung sollten Sie diese Liste immer explizit konfigurieren.

strictMode (optional, Standard true). Eine Standard-Einstellung für schnelle Experimente, die über exec eine integrierte Denylist unsichere Befehle blockiert: Dateioperationen (cat, ls, rm, tar, chmod, ...), Shells, Interpreter (python, node, perl, ...), Netzwerk-Tools (curl, wget, ssh, ...), Kommandostartered (xargs, nohup, env, ...) und Vergleichbares. Dabei wird die Groß-/Kleinschreibung beim Befehlsnamen ignoriert. Praktisch zum Ausprobieren, aber zu grob für echte Nutzung; bevorzugen Sie commandPermissions.

networkPermissions (optional). Die Netzwerk-Allowlist: eine Liste von Glob-Mustern (nur * ist ein Platzhalter), die jeder Host erfüllen muss, der über httpGet/httpPost/httpRequest erreicht wird. Wie commandPermissions liegt sie zusätzlich auf der pro Scope deklarierten Menge aus requestNetwork(...); ein Host muss in beiden enthalten sein. Wenn nicht gesetzt, gilt nur die pro Scope vorhandene requestNetwork-Allowlist.

allowedRoots (optional). Die äußere Grenze des Dateisystems: eine Liste von Pfaden, die einschränken, wo requestFileSystem(root) operieren darf. Ein angeforderter Root muss (einschließlich Symlinks) zu einem Pfad auflösen, der gleich oder unter einem dieser Pfade liegt, andernfalls wird der Zugriff verweigert. Wenn nicht gesetzt, wird standardmäßig das aktuelle Arbeitsverzeichnis des Servers verwendet, sodass die Sandbox auf diesen Teilbaum beschränkt ist (Fail-Closed). Setzen Sie es explizit, um die Grenze zu erweitern oder zu verschieben. Die Maskierung klassifizierter Pfade gilt weiterhin innerhalb jedes gewährten Roots.

Symlinks werden immer vor der Containment-Prüfung aufgelöst, einschließlich toter Symlinks (ein Schreiben durch einen toten Link erzeugt dessen Ziel, also wird das Ziel geprüft). Einträge, die von children/walk (und daher von find/grepRecursive) gefunden werden und außerhalb des gewährten Roots auflösen, wie z. B. ein .venv/bin/python- oder node_modules/.bin-Link, werden weggelassen, anstatt verfolgt oder als Fehler gemeldet zu werden.

secureOutput (optional). Pfad zu einer Append-only-Datei, die jeden println/print/printf-Aufruf aus der Isolation spiegelt, jedoch mit entpackten Classified[_]-Werten. Die Hauptausgabe des Agents zeigt weiterhin die maskierte Form (Classified(***)), sodass nur derjenige, der diese Datei lesen kann, den echten Inhalt sieht. Übergeordnete Verzeichnisse werden automatisch erstellt, und eine noch nicht vorhandene Senkendatei wird auf POSIX-Systemen mit Nur-Eigentümer-Berechtigungen (rw-------) erstellt (atomar, sodass sie nie mit weiteren Berechtigungen existiert). Eine vorhandene Datei wird mit unveränderten Berechtigungen angehängt. Wenn nicht gesetzt, verhält sich das Drucken normal und es wird nichts auf die Festplatte geschrieben.

classifiedWrite (optional, Standard true; nur JSON-Konfiguration). Wenn auf false gesetzt, werden alle Schreibvorgänge auf klassifizierte Pfade verweigert: writeClassified(path, content), access(path).writeClassified(content) und mkdir() auf einem klassifizierten Pfad. Beachten Sie, dass ein Agent, da classify jeden Wert umhüllen kann, bei aktivierter Option klassifizierte Dateien (z. B. .ssh/authorized_keys) mit beliebigem Inhalt überschreiben kann: Der Classified-Mechanismus schützt die Vertraulichkeit, nicht die Integrität. Setzen Sie dies in Bereitstellungen auf false, in denen klassifizierte Dateien für den Agenten schreibgeschützt sein müssen.

Klassifizierte Pfadmuster

Klassifizierte Pfadmuster folgen der gitignore-ähnlichen Syntax. Ein Pfad ist klassifiziert, wenn er einem Muster entspricht oder ein Nachkomme eines Treffers ist.

Muster

Entspricht

Beispiel

.ssh

Jede Pfadkomponente namens .ssh

/home/user/.ssh/id_rsa

.env.*

Jede Komponente, die dem Glob entspricht

/project/.env.local

config/*/keys

Relativ zum Dateisystem-Root, mit Wildcard

<root>/config/prod/keys/secret.pem

**/secrets

secrets in beliebiger Tiefe

<root>/a/b/secrets/key.txt

/home/user/.ssh

Absoluter Pfad (Symlinks aufgelöst)

/home/user/.ssh/id_rsa

Regeln:

  • Kein / im Muster: Entspricht jeder Pfadkomponente (Basename-Abgleich)

  • Relatives Muster mit /: Am Dateisystem-Root verankert; unterstützt *, **, ?, […]

  • Absolutes Muster: Gegen den vollständigen Pfad abgeglichen; Nicht-Glob-Präfix wird durch Symlinks aufgelöst

  • Nachgestelltes / wird entfernt (keine Verzeichnis-nur-Unterscheidung)

Standardmäßige klassifizierte Muster (wenn classifiedPaths nicht konfiguriert ist): .ssh, .gnupg, .env, .env.*, .netrc, .npmrc, .pypirc, .docker, .kube, .aws, .azure, .gcloud.

Werkzeuge

Werkzeug

Parameter

Beschreibung

execute_scala

code

Führt ein Scala-Snippet in einer frischen REPL aus (zustandslos)

create_repl_session

-

Erstellt eine persistente REPL-Sitzung, gibt session_id zurück

execute_in_session

session_id, code

Führt Code in einer bestehenden Sitzung aus (zustandsbehaftet)

list_sessions

-

Listet aktive Sitzungs-IDs auf

delete_repl_session

session_id

Löscht eine Sitzung

show_interface

-

Zeigt die vollständige Capability-API-Referenz

Sitzungen sind auf 100 aktive Sitzungen begrenzt; create_repl_session gibt bei Erreichen der Grenze einen Fehler zurück. Die Ausgabe ist auf 10 MiB begrenzt (Kürzung wird im Ergebnis markiert), und exec erfasst höchstens 8 MiB stdout und 8 MiB stderr pro Aufruf.

Beispiel: Zustandsbehaftete Sitzung

1. create_repl_session          → session_id: "abc-123"
2. execute_in_session(code: "val x = 42")   → x: Int = 42
3. execute_in_session(code: "x * 2")        → val res0: Int = 84
4. delete_repl_session(session_id: "abc-123")

Sicherheitsfunktionen

Das Typsystem von TACIT bietet drei Sicherheitsgarantien, die unabhängig davon gelten, ob der Agent fehlausgerichtet ist, halluziniert oder unter Prompt-Injection-Angriff steht:

Eigenschaft

Bedeutung

Capability-Sicherheit

Capabilities können weder gefälscht noch vergessen werden. Der Agent kann nur auf Ressourcen zugreifen, die ihm explizit gewährt wurden.

Capability-Vollständigkeit

Capabilities regulieren alle sicherheitsrelevanten Effekte. Der Agent interagiert nur über seine gewährten Capabilities mit der Welt.

Lokale Reinheit

Bestimmte Berechnungen können als nebenwirkungsfrei erzwungen werden. Dies verhindert Informationslecks, wenn Agents klassifizierte Daten verarbeiten.

Capability-API

Die Bibliothek stellt drei Capability-Anfragemethoden bereit, die jeweils den Zugriff auf einen Block begrenzen. Capabilities können ihren begrenzten Block nicht verlassen. Dies wird zur Kompilierzeit durch den Capture-Checker durchgesetzt.

// File system: scoped to a root directory
requestFileSystem("/tmp/work") {
  val f = access("data.txt")
  f.write("hello")
  val lines = f.readLines()
  grep("data.txt", "hello")
  find(".", "*.txt")
}

// Process execution: scoped to an allowlist of commands
requestExecPermission(Set("ls", "cat")) {
  val result = exec("ls", List("-la"))
  println(result.stdout)
}

// Network: scoped to an allowlist of hosts
requestNetwork(Set("api.example.com")) {
  val body = httpGet("https://api.example.com/data")
  httpPost("https://api.example.com/submit", """{"key":"value"}""")
  // Arbitrary verbs with a status code:
  val resp = httpRequest("DELETE", "https://api.example.com/item/42")  // resp.status, resp.body
}

Die Netzwerkmethoden akzeptieren auch einfache headers: Map[String, String] und secretHeaders: Map[String, Classified[String]]. Ein secretHeaders-Wert (z. B. ein Authorization-Token, das über readClassified gelesen wird) wird an den Whitelist-Host gesendet, ist aber für den Agent-Code niemals beobachtbar, sodass sich ein Agent mit einem Geheimnis, das er nicht lesen kann, bei einer erlaubten API authentifizieren kann. httpPostClassified vervollständigt das Bild: Es sendet einen Classified[String]-Body per POST und gibt eine Classified[String]-Antwort zurück, sodass sensible Daten durch einen externen Dienst zirkulieren können, während sie unter Informationsflusskontrolle bleiben (siehe unten).

Informationsflusskontrolle über Classified

Betrachten wir einen typischen Code-Agenten, der in einem Projektverzeichnis arbeitet. Einige Dateien sind gewöhnlich (Quellcode, Build-Konfigurationen, READMEs). Andere sind sensibel: API-Schlüssel in .env, Anmeldedaten in secrets/, interne Dokumente. Der Agent wird von einem cloud-gehosteten LLM (einem Drittanbieterdienst) betrieben. Wir möchten, dass der Agent die sensiblen Daten verwendet oder verarbeitet (interne Dokumente zusammenfasst, Schlüssel rotiert, Berichte verarbeitet), sie aber niemals an den Cloud-Anbieter weitergibt.

TACIT löst dies über den Typ Classified[T]. Dateien unter festgelegten klassifizierten Pfaden (konfiguriert über --classified-paths mit gitignore-ähnlichen Mustern, z. B. .ssh, .env.*, secrets, **/keys) geben ihren Inhalt in Classified[String] zurück, statt in einfachem String. Wenn nicht anders konfiguriert, sind gängige Geheimpfade (.ssh, .gnupg, .env, .env.* usw.) standardmäßig klassifiziert. Das Typsystem erzwingt nur-reinen Zugriff: Classified.map akzeptiert nur reine Funktionen (T -> U), d. h. keine Effekte und keine erfassten Capabilities. Sie können die Daten transformieren, aber nicht irgendwohin senden. Jeder Versuch, klassifizierte Daten zu exfiltrieren, wird zur Kompilierzeit abgelehnt:

requestFileSystem("/project") {
  val secret = readClassified("secrets/api-key.txt")

  // Compile error: map captures the file capability, not a pure function
  secret.map: s =>
    access("exfil.txt").write(s) // error: capturing f is not allowed
    s

  // Compile error: print out the classified content to the cloud LLM
  secret.map: s =>
    println(s) // error: capturing IOCapability is not allowed
    s
}

Wie kann der Agent also nützliche Arbeit mit klassifizierten Daten leisten? Durch ein Dual-LLM-Design: Ein separates vertrauenswürdiges lokales LLM verarbeitet klassifizierte Inhalte. Das Framework bietet eine chat-Überladung, die Classified[String] akzeptiert und Classified[String] zurückgibt. Das vertrauenswürdige LLM sieht den Inhalt, aber das Ergebnis bleibt umhüllt und kann niemals zum nicht vertrauenswürdigen Cloud-Modell zurückfließen.

Klassifizierter Datenfluss

requestFileSystem("/project") {
  // OK: read classified content
  val doc = readClassified("secrets/contract-v2.txt")

  // OK: pure transformation
  val upper = doc.map(_.trim)

  // OK: send to trusted local LLM, result stays Classified
  val summary = chat(doc.map(s => s"Summarize the following document:\n$s"))
  // summary: Classified[String], content is still protected

  // OK: write back to a classified file
  writeClassified("secrets/summary.txt", summary)
}

Neben dem vertrauenswürdigen LLM und klassifizierten Dateien kann ein Classified-Wert auch an einen Whitelist-Netzwerkhost fließen, ohne deklassiert zu werden, entweder als geheimer Anfrage-Header (z. B. zur Authentifizierung bei einer erlaubten API) oder als klassifizierter POST-Body, dessen Antwort umhüllt bleibt:

requestNetwork(Set("api.example.com")) {
  requestFileSystem("/project") {
    val key = readClassified("secrets/api.key")

    // OK: the token reaches the allowlisted host as a header, but is never
    // observable to agent code (the value cannot be printed or inspected).
    val me = httpGet("https://api.example.com/me",
                     secretHeaders = Map("Authorization" -> key.map("Bearer " + _)))

    // OK: secret body in, Classified response out.
    val payload = readClassified("secrets/report.json")
    val reply = httpPostClassified("https://api.example.com/process", payload)
    // reply: Classified[String]
  }
}

Sicherer Modus

Vom Agenten generierter Code wird unter Scala 3s sicherem Modus (import language.experimental.safe) kompiliert, der eine capability-sichere Sprachteilmenge durchsetzt:

  1. Keine ungeprüften Typumwandlungen oder Pattern-Matches

  2. Keine Funktionen aus dem Modul caps.unsafe

  3. Keine @unchecked-Annotationen

  4. Keine Laufzeitreflexion

  5. Kompilierung mit aktivierter Capture-Prüfung und expliziten Nullwerten, die alle Mutationseffekte verfolgt

  6. Globale Objekte und Funktionen nur zugänglich, wenn sie sicher implementiert sind

Diese Einschränkungen verhindern, dass Agents Capabilities durch unsichere Umwandlungen, Reflexion oder Typsystemlücken „vergessen". Code, der die Kompilierung nicht besteht, wird niemals ausgeführt.

Der sichere Modus ist eine experimentelle Funktion, die noch aktiv entwickelt wird. Standardmäßig verwendet TACIT einen statischen Code-Validator, der nach verbotenen Mustern sucht, um die Teilmenge des sicheren Modus durchzusetzen. Das Flag --safe-mode (oder "safeMode": true in der JSON-Konfiguration) importiert zusätzlich language.experimental.safe in jede REPL-Ausführung und entscheidet sich für die Compiler-interne Durchsetzung von Scala 3.

Ausführungs-Timeout

--exec-timeout-ms <ms> (oder "executionTimeoutMs" in der JSON-Konfiguration) begrenzt die Wanduhrzeit einer einzelnen REPL-Auswertung. Der Wert muss positiv sein; Null oder negative Werte werden beim Start abgelehnt. Bei einem Timeout erhält der Client einen sofortigen Fehler, anstatt zu hängen, und bei zustandsbehafteten Sitzungen behält die Sitzung ihren vorherigen Zustand, sodass die abgebrochene Anweisung keine beobachtbare Wirkung hat.

Der Watchdog führt jede Auswertung auf einem Worker-Thread aus und ist Best-Effort: Interrupt-empfindliche Arbeit (blockierende E/A, Schlaf, die meisten Bibliotheksaufrufe) wird zuverlässig begrenzt, aber eine reine CPU-Schleife, die nie auf Interrupts prüft, läuft im Hintergrund weiter und hält weiterhin die Ausgabesperre der REPL. Harte Präemption würde eine Prozess-Isolation erfordern; dieser Regler ist ein Robustheits-Schutz, keine Sandbox-Grenze. Wenn nicht gesetzt (Standard), laufen Auswertungen ohne Timeout.

LLM-Integration

Ein sekundäres LLM ist über die chat-Methode verfügbar, ohne dass ein Capability-Bereich erforderlich ist. Die Sicherheit kommt vom Classified-Typsystem: chat(String): String für reguläre Daten, chat(Classified[String]): Classified[String] für sensible Daten.

// Regular chat
val answer = chat("What is 2 + 2?")

// Classified chat: input and output stay wrapped
requestFileSystem("/secrets") {
  val secret = readClassified("/secrets/key.txt")
  val result = chat(secret.map(s => s"Summarize: $s"))
  // result is Classified[String], cannot be printed or leaked
}

Konfiguration über CLI-Flags (--llm-base-url, --llm-api-key, --llm-model) oder eine JSON-Konfigurationsdatei (--config). Jede OpenAI-kompatible API wird unterstützt.

Experimentelle Ergebnisse

Wir evaluieren TACIT hinsichtlich Sicherheit und Ausdruckskraft (siehe Paper, Abschnitt 4 für Details).

Sicherheit (RQ1). Im klassifizierten Modus (Geheimnisse in Classified[String] umhüllt) erreichen sowohl Claude Sonnet 4.6 als auch MiniMax M2.5 100 % Sicherheit über alle 131 Versuche. Jede Injection und bösartige Aufgabe wird vom Typsystem blockiert. Die Nützlichkeit bleibt hoch (99,2 % für Sonnet, 90,0 % für MiniMax).

Ausdruckskraft (RQ2). Bei τ2-bench und SWE-bench Lite erreichen Agents, die TACITs capability-sichere Umgebung verwenden, gleiche oder leicht bessere Ergebnisse als Standard-Tool-Calling-Baselines über alle getesteten Modelle (gpt-oss-120b, MiniMax M2.5, DeepSeek V3.2), was zeigt, dass das Schreiben typsicheren Scalas die agentische Leistung nicht verschlechtert.

Erweitern der Bibliothek: Hinzufügen einer eigenen API

Die Bibliothek (library/) definiert die Capability-API, die Benutzercode innerhalb der REPL aufrufen kann. Um benutzerdefinierte Berechtigungen und feingranulare Zugriffskontrolle zu implementieren, können Sie neue Capabilities hinzufügen (z. B. Datenbankzugriff, Nachrichtenwarteschlangen, Serververwaltung), indem Sie die Bibliothek ändern und nur das Bibliotheks-JAR neu erstellen.

Bibliotheksstruktur

library/
├── Interface.scala          # Public API trait (what user code sees)
├── impl/
│   ├── InterfaceImpl.scala  # Wires everything together (exports Ops objects)
│   ├── BaseFileSystem.scala    # Shared path validation and gitignore-style classified-path matching
│   ├── FileOps.scala           # grep, grepRecursive, find
│   ├── ProcessOps.scala        # exec, execOutput
│   ├── WebOps.scala            # httpGet, httpPost, httpRequest, httpPostClassified
│   ├── LlmOps.scala            # chat
│   ├── RealFileSystem.scala    # FileSystem on real disk
│   ├── VirtualFileSystem.scala # In-memory FileSystem (for testing)
│   ├── ClassifiedImpl.scala    # Classified[T] wrapper implementation
│   ├── ProcessPermissionImpl.scala # Concrete ProcessPermission
│   ├── NetworkImpl.scala       # Concrete Network
│   ├── GlobMatcher.scala       # Shared `*`-glob to regex utility
│   ├── LibraryConfig.scala     # Library configuration with JSON parsing
│   └── LlmConfig.scala        # LLM configuration case class
└── test/                    # Library-level tests

Schritt-für-Schritt: Hinzufügen einer neuen API

Hier ist ein Beispiel für das Hinzufügen einer hypothetischen requestDatabase-Fähigkeit.

1. Typen und Fähigkeit in Interface.scala definieren

// Add a result type
case class QueryResult(columns: List[String], rows: List[List[String]])

// Add a capability class. Note the `private[library]` constructor: capability
// classes must not be constructible or extendable by agent code.
class DatabasePermission private[library] (val connectionString: String) extends caps.SharedCapability

// Add methods to the Interface trait
trait Interface:
  // ... existing methods ...

  def requestDatabase[T](connectionString: String)(op: DatabasePermission^ ?=> T)(using IOCapability): T

  def query(sql: String)(using DatabasePermission): QueryResult

Wichtige Punkte:

  • Die Fähigkeitsklasse muss caps.SharedCapability erweitern. Dadurch wird Scalas 3-Capture-Checker in die Lage versetzt, zu verhindern, dass die Fähigkeit ihren scoped-Block verlässt.

  • Die request*-Methode nimmt einen Block op entgegen, der die Fähigkeit als Kontextparameter (?=>) erhält. Das ^-Zeichen bedeutet, dass die Fähigkeit vom Capture-Checker verfolgt wird.

  • Operationsmethoden (wie query) nehmen die Fähigkeit als using-Parameter, sodass sie nur innerhalb des entsprechenden request*-Blocks aufgerufen werden können.

2. Die Operationen in impl/ implementieren

Erstellen Sie library/impl/DatabaseOps.scala:

package tacit.library

import language.experimental.captureChecking

object DatabaseOps:
  def query(sql: String)(using perm: DatabasePermission): QueryResult =
    // Your implementation here
    // perm.connectionString has the connection info
    ???

3. In InterfaceImpl einbinden

Exportieren Sie in library/impl/InterfaceImpl.scala Ihre neuen Operationen und implementieren Sie die request*-Methode:

abstract class InterfaceImpl private[library] (...) extends Interface:
  export FileOps.*
  export ProcessOps.*
  export WebOps.*
  export DatabaseOps.*   // ← add this

  // ... existing methods ...

  def requestDatabase[T](connectionString: String)(op: DatabasePermission^ ?=> T)(using IOCapability): T =
    val perm = new DatabasePermission(connectionString)
    op(using perm)

4. Direkten Zugriff im Validator blockieren (Serverseite)

Wenn Ihre neue API eine Java-/Scala-Bibliothek kapselt, die Benutzer nicht direkt aufrufen sollen, fügen Sie verbotene Muster in src/main/scala/executor/CodeValidator.scala hinzu:

ForbiddenPattern("db-jdbc", raw"java\.sql\b".r, "Direct JDBC access is forbidden; use requestDatabase"),
ForbiddenPattern("db-driver", raw"DriverManager".r, "DriverManager is forbidden; use requestDatabase"),

Dadurch wird sichergestellt, dass der Benutzercode über die Fähigkeits-API läuft, statt sie zu umgehen.

5. Abhängigkeiten hinzufügen (falls erforderlich)

Wenn Ihre neue API externe Bibliotheken benötigt, fügen Sie sie dem lib-Projekt in build.sbt hinzu:

lazy val lib = project
  .in(file("library"))
  .settings(
    // ... existing settings ...
    libraryDependencies ++= Seq(
      "com.openai" % "openai-java" % "4.38.0",
      "org.postgresql" % "postgresql" % "42.7.3",  // ← add your dep
    ),
  )

6. Das Library-JAR neu erstellen

sbt "lib/assembly"

Der Server-JAR muss nicht neu erstellt werden, es sei denn, Sie haben CodeValidator (Schritt 4) oder anderen serverseitigen Code geändert. Weisen Sie den Server einfach auf das neue Library-JAR:

java -jar server.jar --library-jar new-library.jar

7. Ihre neue API in der Dev-REPL testen

Für eine schnelle Iteration ohne einen Agenten zu starten, starten Sie die Dev-REPL, eine interaktive Scala-Eingabeaufforderung, die mit der Fähigkeits-API und demselben CodeValidator wie der MCP-Server vorinstalliert ist:

sbt devRepl                                  # default config
sbt "devRepl --strict --config my.json"      # with flags

Dinge, die Sie beachten sollten

  • Fähigkeiten müssen caps.SharedCapability erweitern. Das ist es, was die Capture-Überprüfung funktionieren lässt. Ohne sie kann der Compiler den Gültigkeitsbereich der Fähigkeit nicht verfolgen, und Benutzer könnten sie aus dem request*-Block herausleaken.

  • Fähigkeitsklassen und ihre Implementierungen sind versiegelt. Alle Fähigkeitstypen (FileSystem, Network, ProcessPermission, IOCapability, Classified, FileEntry) und jede Impl-Klasse (RealFileSystem, NetworkImpl, LlmOps, ...) haben private[library]-Konstruktoren, sodass Agentencode sie weder instanziieren noch erweitern kann: Fähigkeiten können nur aus den request*-Scopes stammen. Behalten Sie diese Invariante für jede von Ihnen hinzugefügte Fähigkeit bei: Geben Sie der Klasse einen private[library]-Konstruktor und machen Sie auch konkrete Impls private[library].

  • Auch das Interface selbst ist versiegelt. Der Konstruktor von InterfaceImpl ist private[library], sodass nichts außerhalb der Bibliothek die Policy-JSON wählen kann. Der Server registriert die Bibliothekskonfiguration einmal pro Sandbox (InterfaceImpl.configure, aufgerufen über den Klassenlader der REPL, bevor Code ausgeführt wird), und der Präambel instanziiert das parameterlose SandboxInterface, dessen Policy diese registrierte Konfiguration ist. Agentencode, der SandboxInterface selbst erweitert, erhält nur eine identische, policy-gebundene Schnittstelle, niemals eine breitere.

  • Capture-Checking ist experimentell. Das Projekt verwendet -language:experimental.captureChecking. Das Compiler-Verhalten kann sich zwischen Scala-3-Nightly-Versionen ändern. Wenn Sie unerwartete Fehler erhalten, prüfen Sie, ob das Problem mit dem Capture-Checking zusammenhängt, indem Sie das Flag vorübergehend entfernen.

  • Die Bibliothek verwendet Scala 3 Nightly. Der Build lädt automatisch das neueste Scala-3-Nightly. Das bedeutet, dass Ihr Code mit hochmodernem Scala kompatibel sein muss. Wenn Sie Stabilität benötigen, legen Sie eine bestimmte Version in build.sbt fest (val scala3Version = "3.x.y").

  • Interface.scala wird als Ressource gebündelt. Der Server kopiert Interface.scala beim Build in seine Ressourcen, damit das Tool show_interface es anzeigen kann. Wenn Sie neue APIs hinzufügen, sehen Benutzer sie automatisch über show_interface – keine zusätzliche Arbeit nötig.

  • Verbotene Muster betreffen Benutzercode, nicht Bibliothekscode. Der Validator in CodeValidator.scala prüft nur benutzergesendeten Code. Die Bibliothek selbst kann java.io, java.net, ProcessBuilder usw. in ihrer Implementierung frei verwenden. Aber wenn Ihre neue API eine Java-API kapselt, sollten Sie ein entsprechendes verbotenes Muster hinzufügen.

  • Das Bibliotheks-JAR ist eine Ressource. Der Server kopiert Interface.scala zur Build-Zeit in seine Ressourcen, damit das Tool show_interface es anzeigen kann. Wenn Sie neue APIs hinzufügen, sehen Benutzer sie automatisch über show_interface – keine zusätzliche Arbeit nötig.

  • Verbotene Muster werden auf Benutzercode angewendet, nicht auf Bibliothekscode. Der Validator in CodeValidator.scala prüft nur den vom Benutzer eingereichten Code. Die Bibliothek selbst kann java.io, java.net, ProcessBuilder usw. in ihrer Implementierung frei verwenden. Aber wenn Ihre neue API eine Java-API kapselt, sollten Sie ein entsprechendes verbotenes Muster hinzufügen, damit Benutzer Ihren Fähigkeits-Wrapper nicht umgehen können.

  • Das Bibliotheks-JAR ist ein Fat-JAR. sbt "lib/assembly" erzeugt ein JAR, das alle Abhängigkeiten der Bibliothek enthält (z. B. openai-java). Wenn Sie eine Abhängigkeit hinzufügen, wird sie automatisch eingebunden.

  • Der Server hängt zur Kompilierzeit von Bibliothekstypen ab. Der Server hängt vom Interface-Typ ab, um die REPL auszuführen. Stellen Sie sicher, dass Ihre Änderung mit dem vom Server erwarteten Interface kompatibel ist.

  • Testen Sie Ihre API zuerst auf Bibliotheksebene. Das Verzeichnis library/test/ enthält Tests auf Bibliotheksebene mit MUnit, ausgeführt mit scala-cli test library --server=false (sie sind nicht Teil von sbt test; --server=false umgeht einen ASM-Konflikt zwischen den aktuellen Scala-3-Nightly-Versionen und scala-cli). Testen Sie Ihre neuen Operationen dort, bevor Sie sie über den MCP-Server testen. Siehe LibrarySuite.test.scala für ein Beispiel.

  • Fügen Sie die neuen Fähigkeiten zur Dokumentation hinzu. CAPABILITIES.md listet alle verfügbaren Fähigkeiten auf. Fügen Sie die neue Fähigkeit zur Tabelle hinzu.

sbt clean                      # Clean build artifacts
sbt compile                    # Compile
sbt test                       # Run the server test suites (src/test/scala)
sbt "testOnly *McpServerSuite" # Run a single server suite
scala-cli test library --server=false   # Run the library test suites (library/test)
sbt assembly                   # Build both JARs (server + library)
sbt "lib/assembly"             # Build library JAR only
sbt devRepl                    # Interactive REPL for testing the library

sbt test führt nur die Server-Suites aus. Die library/test/-Suites werden separat mit scala-cli test library --server=false ausgeführt.

# Basic
java -jar target/scala-*/TACIT-assembly-*.jar \
  --library-jar library/target/scala-*/TACIT-library.jar

# With logging
java -jar server.jar --library-jar library.jar --record ./log

# With JSON config
java -jar server.jar --library-jar library.jar --config config.json

Zitierung

@inbook{10.1145/3786335.3813127,
author = {Odersky, Martin and Zhao, Yaoyu and Xu, Yichen and Bra\v{c}evac, Oliver and Pham, Cao Nguyen},
title = {Securing Agents With Tracked Capabilities},
year = {2026},
isbn = {9798400724152},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3786335.3813127},
booktitle = {Proceedings of the ACM Conference on AI and Agentic Systems},
pages = {812–838},
numpages = {27}
}

Lizenz

Apache-2.0

A
license - permissive license
Not graded
quality - not tested
A
maintenance

Maintenance

UpdatingMaintainers
UpdatingResponse time
2wRelease cycle
10Releases (12mo)
Commit activity

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Servers

  • F
    license
    Not graded
    quality
    D
    maintenance
    A unified MCP server providing observability, safety control, and behavior evolution for high-agency AI agents through tracing, replaying, and auditing. It features real-time firewall guardrails and ML-driven anomaly detection to monitor, block, or fork agent actions based on risk.
    7
  • A
    license
    C
    quality
    B
    maintenance
    Agent-first programming language: agents produce JSON AST, the compiler validates, type-checks, effect-checks, verifies contracts via Z3/SMT, and compiles to WASM. 19 MCP tools for the full compile-and-execute loop.
    22
    123
    11
    MIT

View all related MCP servers

Related MCP Connectors

View all MCP Connectors

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/lampepfl/TACIT'

If you have feedback or need assistance with the MCP directory API, please join our Discord server