Skip to main content
Glama

TACIT: 型で追跡されるエージェントの能力

論文: 追跡される能力でエージェントを保護する (ACM) · arXiv:2603.00991 · 🏆 CAIS 26 最優秀論文賞

TACIT(型で追跡されるエージェントの能力)は、AIエージェントのためのセーフティハーネスです。 ツールを直接呼び出す代わりに、エージェントはcapture checkingを備えたScala 3でコードを記述します。これは、能力を静的に追跡し、エージェントコードがアクセス権を偽造できず、予算を超えた効果を実行できず、純粋なサブ計算から情報を漏洩できないことを強制する型システムです。 MCPインターフェースを提供するため、MCP互換のすべてのエージェントで簡単に使用できます。

TACITフレームワーク概要

このフレームワークには3つの主要コンポーネントがあります:

  • Scala 3コンパイラ。 エージェントが提出したコードは、セーフモードでcapture checkingを有効にして検証および型チェックされ、能力安全な言語サブセットを強制します。

  • Scala REPL。 ローカルのREPLインスタンスがコンパイルされたコードを実行し、インタラクション間の状態を管理します。ステートレスな一回限りの実行とステートフルなセッションの両方をサポートします。

  • 能力安全性ライブラリ。 エージェントコードが現実世界(ファイルシステム、プロセス実行、ネットワーク、サブエージェント)とやり取りするための唯一のゲートウェイとして機能する型付きAPI。ライブラリは拡張可能です。MCPサーバー自体を変更せずに、ライブラリコードのみを変更して新しい能力を追加できます。

クイックスタート

TACITは、stdioを介してJSON-RPCで通信する標準のMCPサーバーを提供します。Claude Code、OpenCode、GitHub Copilotなど、MCP互換のすべてのエージェントで動作します。

JDK 17+が必要です。

TACITのインストール

以下のインストール方法のいずれかを選択してください。tacit CLIラッパーが推奨オプションです。

オプション1: tacitのインストール(推奨)

tacitは、TACITをローカルで管理するための小さなラッパーコマンドです。tacit setupを一度実行してコマンドをインストールし最新リリースを取得し、tacit updateでJARを更新し、tacit self updateでラッパー自体を更新し、tacit serveでMCPサーバーを起動します。

# 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

これにより、tacitコマンドが~/.local/binにインストールされ、~/.local/binがPATHに含まれていることを確認し、最新リリースが~/.cache/tacit/にダウンロードされます。

一般的なコマンド:

# 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

デフォルトでは、tacitは以下を使用します:

アセット

デフォルトパス

MCPサーバー

~/.cache/tacit/TACIT.jar

ライブラリ

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

オプション2: ビルド済みリリースJARを直接ダウンロード

ラッパーを使用したくない場合は、リリースダウンロードスクリプトを使用してください。

# 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

オプション:

# 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

デフォルトでは、以下がダウンロードされます:

JAR

デフォルトパス

MCPサーバー

./TACIT.jar

ライブラリ

./TACIT-library.jar

ラッパーとスクリプトの両方が、リリースメタデータに公開されているSHA-256ダイジェストに対してダウンロードされたJARを検証し、ダイジェストが欠落しているか一致しないJARのインストールを拒否します。ダウンロードは一時ディレクトリに保存され、検証後にのみ所定の場所に移動されるため、ダウンロードに失敗しても以前にインストールされたJARが置き換えられることはありません。

現在のソースツリーからビルドするには、以下のオプション3を参照してください。

オプション3: ソースからビルド

JDK 17+とsbt 1.12+が必要です。

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

./build.sh

オプション:

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

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

これにより、2つのJARがビルドおよびコピーされます:

JAR

パス

MCPサーバー

./TACIT.jar (または ./dist/TACIT.jar)

ライブラリ

./TACIT-library.jar (または ./dist/TACIT-library.jar)

上記のいずれかのオプションでTACITをインストールしたら、エージェントがMCPサーバーを起動するように設定します。

エージェントの設定

エージェントの設定にTACITをMCPサーバーとして追加します。tacit CLIをインストールした場合は、tacit serveを使用するだけです。TACITを手動でインストールした場合は、明示的なjava -jar ... --library-jar ...形式を使用してください。

プロジェクトの.mcp.json(グローバルな場合は~/.claude.json)に追加します。

tacitを使用する場合:

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

手動のJARパスを使用する場合:

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

opencode.jsonに追加します。

tacitを使用する場合:

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

手動のJARパスを使用する場合:

{
  "$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"
      ]
    }
  }
}

.vscode/mcp.jsonに追加します。

tacitを使用する場合:

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

手動のJARパスを使用する場合:

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

これで、エージェントはTACITのツールを使用してサンドボックス化されたScalaコードを実行できます。

推奨: 組み込みツールの無効化

TACITの能力ベースの安全性を最大限に活用するには、エージェントの組み込みファイル、シェル、ネットワークツールを無効にして、すべての操作がサンドボックス化されたREPLを経由するようにします。

--disallowedToolsを指定して起動し、組み込みツールをブロックします:

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

または、プロジェクトの.claude/settings.jsonに追加します:

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

opencode.jsonで組み込みツールの権限を"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": { "..." : "..." }
  }
}

VS Codeのsettings.jsonで、Copilotが利用できるツールを制限します:

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

Related MCP server: repo-seatbelt

設定

サーバーはCLIフラグまたはJSON設定ファイルで設定できます。エージェントのMCP引数でフラグを直接渡すか、--configを使用してJSONファイルを指定します。

設定はサーバー設定(トランスポート、記録、セッション)とライブラリ設定(サンドボックス動作、能力)に分かれています。JSON設定ファイルでは、ライブラリ設定はlibraryConfigキーの下にあり、処理のためにライブラリに直接渡されます。

CLIフラグ

サーバーフラグ:

フラグ

説明

--library-jar <path>

必須。 ライブラリJAR(TACIT-library.jar)へのパス

-r/--record <dir>

すべての実行をディスクに記録

-q/--quiet

起動バナーとリクエスト/レスポンスのログを抑制

--no-session

セッション関連ツールを無効化

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

すべての実行でREPLのScala 3のlanguage.experimental.safeを有効/無効にする(デフォルト: オン。セーフモードを参照)

--exec-timeout-ms <ms>

単一のREPL評価のウォールクロックタイムアウト(デフォルト: なし。実行タイムアウトを参照)

-c/--config <path>

JSON設定ファイル(--configの後のフラグはファイルの値を上書き)

ライブラリフラグ(一部のlibraryConfigフィールドの省略形):

フラグ

説明

-s/--strict

execを介した安全でないコマンドの組み込み拒否リスト(ファイル操作、シェル、インタープリタ、ネットワークツール、コマンドランナーなど)をブロック。マッチングは大文字と小文字を区別しません。簡単な実験に便利。実際のデプロイメントでは--command-permissionsを推奨。

--command-permissions <patterns>

実行可能なコマンドのカンマ区切りグロブパターン(例: echo,py*,ls)。ワイルドカードとして解釈されるのは*のみ。設定すると、--strictは無視されます。

--network-permissions <patterns>

到達可能なホストのカンマ区切りグロブパターン(例: *.example.com,api.github.com)。ワイルドカードとして解釈されるのは*のみ。

--allowed-roots <paths>

requestFileSystemルートのカンマ区切り外部境界(例: /home/me/project,/tmp)。要求されたルートはこれらのいずれか内のパスに解決される必要があります。未設定の場合はサーバーの作業ディレクトリがデフォルト。

--classified-paths <patterns>

カンマ区切りの分類済みパスパターン(gitignoreスタイル、以下を参照)

--llm-base-url <url>

LLM APIベースURL

--llm-api-key <key>

LLM APIキー

--llm-model <name>

LLMモデル名

JSON設定ファイル

{
  "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(オプション)。exec許可リスト: execに渡されるすべてのコマンドが一致する必要があるグロブパターン(ワイルドカードは*のみ)のリスト。これはrequestExecPermission(...)で宣言されたスコープごとのセットの上に重ねられます。コマンドは実際に実行されるには両方に含まれている必要があります。設定すると、strictModeは無視されます。実際のデプロイメントでは、このリストを常に明示的に設定する必要があります。

strictMode(オプション、デフォルトtrue)。execを介して安全でないコマンドの組み込み拒否リストをブロックする簡単な実験用デフォルト: ファイル操作コマンド(cat、ls、rm、tar、chmodなど)、シェル、インタープリタ(python、node、perlなど)、ネットワークツール(curl、wget、sshなど)、コマンドランナー(xargs、nohup、envなど)、および類似のもの。マッチングはコマンドのベース名で大文字と小文字を区別しません。試してみたいだけの場合に便利ですが、実際の使用には粗すぎます。commandPermissionsを推奨します。

networkPermissions(オプション)。ネットワーク許可リスト: httpGet/httpPost/httpRequestを介して到達するすべてのホストが一致する必要があるグロブパターン(ワイルドカードは*のみ)のリスト。commandPermissionsと同様に、これはrequestNetwork(...)で宣言されたスコープごとのセットの上に重ねられます。ホストは両方に含まれている必要があります。未設定の場合、スコープごとのrequestNetwork許可リストのみが適用されます。

allowedRoots(オプション)。ファイルシステムの外側の境界: requestFileSystem(root) が操作できる範囲を制限するパスのリスト。要求されたルートは、(シンボリックリンクを含めて) これらのいずれかと等しいか、その配下にネストされたパスに解決される必要があり、そうでなければアクセスは拒否されます。未設定の場合、サーバーのカレントワーキングディレクトリにデフォルト設定されるため、サンドボックスはそのサブツリーに制限されます(フェイルクローズ)。明示的に設定することで、境界を拡大または移動できます。分類パスのマスキングは、許可されたルート内であればどこでも引き続き適用されます。

シンボリックリンクは、包含チェックの前に常に解決されます(壊れたリンクも含む。壊れたリンクを介した書き込みはそのターゲットを作成するため、チェックされるのはターゲットです)。children/walk(したがってfind/grepRecursive)によって見つかったエントリのうち、許可されたルートの外に解決されるもの(例: .venv/bin/pythonやnode_modules/.binリンク)は、追跡されたりエラーとして報告されたりせず、省略されます。

secureOutput(オプション)。分離環境からのすべてのprintln/print/printf呼び出しをミラーリングする追記専用ファイルへのパス。ただし、Classified[_]値はアンラップされます。エージェントのメイン出力にはマスクされた形式(Classified(***))が引き続き表示されるため、このファイルを読める人だけが実際の内容を見ることができます。親ディレクトリは自動的に作成され、まだ存在しないシンクファイルはPOSIXシステム上で所有者のみの権限(rw-------)で作成されます(アトミックに作成されるため、より広い権限で存在することはありません)。既存のファイルには、権限を変更せずに追記されます。未設定の場合、印刷は通常どおり動作し、ディスクには何も書き込まれません。

classifiedWrite(オプション、デフォルトtrue。JSON設定のみ)。falseに設定すると、分類パスへのすべての書き込みが拒否されます: writeClassified(path, content)、access(path).writeClassified(content)、および分類パスへのmkdir()。 classifyは任意の値をラップできるため、これを有効にしておくと、エージェントが分類ファイル(例: .ssh/authorized_keys)を任意の内容で上書きできることに注意してください: Classifiedメカニズムは機密性を保護しますが、完全性は保護しません。分類ファイルをエージェントに対して読み取り専用にする必要があるデプロイメントでは、これをfalseに設定してください。

分類パスパターン

分類パスパターンはgitignoreスタイルの構文に従います。パスがパターンに一致するか、一致するパスの子孫である場合、そのパスは分類されます。

パターン

一致するもの

例

.ssh

.sshという名前の任意のパスコンポーネント

/home/user/.ssh/id_rsa

.env.*

グロブに一致する任意のコンポーネント

/project/.env.local

config/*/keys

ファイルシステムルートからの相対、ワイルドカード付き

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

**/secrets

任意の深さのsecrets

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

/home/user/.ssh

絶対パス(シンボリックリンク解決済み)

/home/user/.ssh/id_rsa

ルール:

  • パターンに/がない場合: 任意のパスコンポーネントに対して一致(ベースネームマッチング)

  • /を含む相対パターン: ファイルシステムルートにアンカーされる。*、**、?、[…]をサポート

  • 絶対パターン: フルパスに対して一致。非グロブプレフィックスはシンボリックリンクを通して解決される

  • 末尾の/ は削除される(ディレクトリのみの区別はない)

デフォルトの分類パターン(classifiedPathsが設定されていない場合): .ssh、.gnupg、.env、.env.*、.netrc、.npmrc、.pypirc、.docker、.kube、.aws、.azure、.gcloud。

ツール

ツール

パラメータ

説明

execute_scala

code

新しいREPLでScalaスニペットを実行(ステートレス)

create_repl_session

-

永続的なREPLセッションを作成、session_idを返す

execute_in_session

session_id, code

既存のセッションでコードを実行(ステートフル)

list_sessions

-

アクティブなセッションIDを一覧表示

delete_repl_session

session_id

セッションを削除

show_interface

-

完全な機能APIリファレンスを表示

セッションは最大100のアクティブセッションに制限されており、create_repl_sessionは上限に達するとエラーを返します。実行出力は10 MiBに制限され(切り捨ては結果にマークされます)、execは呼び出しごとに最大8 MiBのstdoutと8 MiBのstderrをキャプチャします。

例: ステートフルセッション

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")

セキュリティ機能

TACITの型システムは、エージェントがミスアライメント、幻覚、またはプロンプトインジェクション攻撃下にあるかどうかに関係なく成立する3つの安全性保証を提供します:

プロパティ

意味

機能安全性

機能は偽造も忘却もできない。エージェントは明示的に付与された機能を通じてのみリソースにアクセスできる。

機能完全性

機能は安全性に関わるすべての効果を規制する。エージェントは付与された機能を通じてのみ世界と相互作用する。

局所純粋性

特定の計算を副作用なしとして強制できる。これにより、エージェントが分類データを処理する際の情報漏洩を防ぐ。

機能API

ライブラリは3つの機能リクエストメソッドを公開しており、それぞれがブロックにアクセスをスコープします。機能はスコープされたブロックから逃れることはできません。これはキャプチャチェッカーによってコンパイル時に強制されます。

// 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
}

ネットワークメソッドはまた、プレーンなheaders: Map[String, String]とsecretHeaders: Map[String, Classified[String]]を受け取ります。secretHeaders値(例: readClassifiedで読み取られたAuthorizationトークン)は許可リストに登録されたホストに送信されますが、エージェントコードからは決して観測できません。これにより、エージェントは読み取ることのできない秘密を使用して許可されたAPIに認証できます。httpPostClassifiedが全体像を完成させます: Classified[String]ボディをPOSTし、Classified[String]レスポンスを返すため、機密データは情報フロー制御下にありながら外部サービスを往復できます(下記参照)。

Classifiedによる情報フロー制御

プロジェクトディレクトリで作業する典型的なコードエージェントを考えてみましょう。一部のファイルは通常のものです(ソースコード、ビルド設定、README)。その他は機密です: .env内のAPIキー、secrets/内の認証情報、内部ドキュメント。エージェントはクラウドホスト型LLM(サードパーティサービス)によって駆動されています。エージェントに機密データを使用または処理させたい(内部ドキュメントの要約、キーのローテーション、レポートの処理)が、クラウドプロバイダーに漏洩させたくはありません。

TACITはClassified[T]型を通じてこれを解決します。指定された分類パス(gitignoreスタイルのパターンで--classified-pathsで設定、例: .ssh、.env.*、secrets、**/keys)配下のファイルは、その内容がプレーンなStringではなくClassified[String]にラップされて返されます。特に設定されていない場合、一般的な秘密パス(.ssh、.gnupg、.env、.env.*など)はデフォルトで分類されます。型システムは純粋のみのアクセスを強制します: Classified.mapは純粋関数(T -> U)のみを受け付けます。つまり、効果もキャプチャされた機能もありません。データを変換することはできますが、どこにも送信することはできません。分類データを外部に持ち出そうとする試みはコンパイル時に拒否されます:

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
}

では、エージェントは分類データでどのように有用な作業ができるのでしょうか? デュアルLLM設計を通じて: 別の信頼されたローカルLLMが分類コンテンツを処理します。フレームワークはClassified[String]を受け取りClassified[String]を返すchatオーバーロードを提供します。信頼されたLLMはコンテンツを見ますが、結果はラップされたままであり、信頼されていないクラウドモデルに流れることは決してありません。

分類データフロー

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)
}

信頼されたLLMと分類ファイルに加えて、Classified値は許可リストに登録されたネットワークホストに非分類のまま流出することもできます。秘密のリクエストヘッダーとして(例: 許可されたAPIへの認証)、またはレスポンスがラップされたままの分類POSTボディとして:

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]
  }
}

セーフモード

エージェント生成コードはScala 3のセーフモード(import language.experimental.safe)でコンパイルされ、機能安全な言語サブセットを強制します:

  1. チェックされていない型キャストやパターンマッチは不可

  2. caps.unsafeモジュールの機能は不可

  3. @uncheckedアノテーションは不可

  4. ランタイムリフレクションは不可

  5. キャプチャチェックと明示的ヌルを有効にしてコンパイルし、すべてのミューテーション効果を追跡

  6. グローバルオブジェクトと関数は、安全に実装されている場合にのみアクセス可能

これらの制限により、エージェントが安全でないキャスト、リフレクション、または型システムの穴を通じて機能を「忘れる」ことを防ぎます。コンパイルに合格しないコードは決して実行されません。

セーフモードはまだ活発に開発中の実験的機能です。デフォルトでは、TACITは禁止パターンをチェックする静的コードバリデータを使用してセーフモードサブセットを強制します。--safe-modeフラグ(またはJSON設定の"safeMode": true)は、さらにlanguage.experimental.safeをすべてのREPL実行にインポートし、Scala 3のコンパイラ内強制をオプトインします。

実行タイムアウト

--exec-timeout-ms <ms>(またはJSON設定の"executionTimeoutMs")は、単一のREPL評価のウォールクロック時間を制限します。値は正である必要があります。ゼロまたは負の値は起動時に拒否されます。タイムアウト時、クライアントはハングする代わりにプロンプトエラーを受け取り、ステートフルセッションの場合、セッションは以前の状態を保持するため、放棄されたステートメントは観測可能な効果を持ちません。

ウォッチドッグは各評価をワーカースレッドで実行し、ベストエフォートです: 割り込み応答性のある作業(ブロッキングI/O、スリープ、ほとんどのライブラリ呼び出し)は確実に制限されますが、割り込みをチェックしない純粋なCPUループはバックグラウンドで実行され続け、REPLの出力ロックを保持し続けます。ハードなプリエンプションにはプロセスレベルの分離が必要です。このノブは堅牢性ガードであり、サンドボックス境界ではありません。未設定の場合(デフォルト)、評価はタイムアウトなしで実行されます。

LLM統合

セカンダリLLMはchatメソッドを通じて利用可能で、機能スコープは不要です。安全性はClassified型システムからもたらされます: 通常データ用のchat(String): String、機密データ用のchat(Classified[String]): Classified[String]。

// 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
}

CLIフラグ(--llm-base-url、--llm-api-key、--llm-model)またはJSON設定ファイル(--config)で設定します。OpenAI互換のAPIであればどれでもサポートされます。

実験結果

TACITを安全性と表現力について評価します(詳細は論文セクション4を参照)。

安全性(RQ1)。 分類モード(秘密がClassified[String]にラップされている)では、Claude Sonnet 4.6とMiniMax M2.5の両方が全131回の試行で100%のセキュリティを達成しました。すべてのインジェクションと悪意のあるタスクは型システムによってブロックされます。ユーティリティは高いままです(Sonnetで99.2%、MiniMaxで90.0%)。

表現力(RQ2)。 τ2-benchとSWE-bench Liteにおいて、TACITの機能安全ハーネスを使用するエージェントは、テストされたすべてのモデル(gpt-oss-120b、MiniMax M2.5、DeepSeek V3.2)で標準のツール呼び出しベースラインと同等かわずかに上回り、型安全なScalaを書くことがエージェントのパフォーマンスを低下させないことを実証しています。

ライブラリの拡張: 独自APIの追加

ライブラリ(library/)は、ユーザーコードがREPL内で呼び出すことができる機能APIを定義します。カスタム権限ときめ細かいアクセス制御を実装するには、ライブラリを変更してライブラリJARのみを再ビルドすることで、新しい機能(例: データベースアクセス、メッセージキュー、サーバー管理)を追加できます。

ライブラリ構造

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

ステップバイステップ: 新しいAPIの追加

架空の requestDatabase 機能を追加する例を示します。

1. Interface.scala で型と機能を定義する

// 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

重要なポイント:

  • 機能クラスは caps.SharedCapability を継承する必要があります。これにより、Scala 3のキャプチャチェッカーが機能がスコープ付きブロックから逃げ出すのを防ぐことができます。

  • request* メソッドは、機能をコンテキストパラメータ (?=>) として受け取るブロック op を取ります。^ マークは、機能がキャプチャチェッカーによって追跡されることを意味します。

  • 操作メソッド (query など) は機能を using パラメータとして取るため、対応する request* ブロック内でのみ呼び出すことができます。

2. impl/ で操作を実装する

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. InterfaceImpl に組み込む

library/impl/InterfaceImpl.scala で、新しい操作をエクスポートし、request* メソッドを実装します:

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. バリデータで直接アクセスをブロックする(サーバー側)

新しいAPIが、ユーザーが直接呼び出すべきではないJava/Scalaライブラリをラップする場合は、src/main/scala/executor/CodeValidator.scala に禁止パターンを追加します:

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"),

これにより、ユーザーコードが機能APIを迂回するのではなく、機能APIを経由することが保証されます。

5. 依存関係を追加する(必要な場合)

新しいAPIに外部ライブラリが必要な場合は、build.sbt の lib プロジェクトに追加します:

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. ライブラリJARを再ビルドする

sbt "lib/assembly"

CodeValidator(手順4)やその他のサーバー側コードを変更しない限り、サーバーJARを再ビルドする必要はありません。サーバーを新しいライブラリJARに向けるだけです:

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

7. 開発用REPLで新しいAPIを試す

エージェントを起動せずに素早く反復するには、開発用REPLを起動します。これは、機能APIとMCPサーバーが使用するのと同じ CodeValidator がプリロードされた対話型Scalaプロンプトです:

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

注意すべき点

  • 機能は caps.SharedCapability を継承する必要があります。 これがキャプチャチェックを機能させるものです。これがないと、コンパイラは機能のスコープを追跡できず、ユーザーが request* ブロックの外に機能を漏らす可能性があります。

  • 機能クラスとその実装はシールされています。 すべての機能型 (FileSystem、Network、ProcessPermission、IOCapability、Classified、FileEntry) とすべての実装クラス (RealFileSystem、NetworkImpl、LlmOps など) は private[library] コンストラクタを持つため、エージェントコードはそれらをインスタンス化も拡張もできません。機能は request* スコープからのみ取得できます。追加する機能についてもこの不変条件を維持してください: クラスに private[library] コンストラクタを与え、具象実装も private[library] にします。

  • インターフェース自体もシールされています。 InterfaceImpl のコンストラクタは private[library] であるため、ライブラリの外部からポリシーJSONを選択することはできません。サーバーはサンドボックスごとにライブラリ設定を1回登録し(InterfaceImpl.configure、任意のコードが実行される前にREPLのクラスローダーを通じて呼び出される)、プリアンブルはパラメータなしの SandboxInterface をインスタンス化します。そのポリシーは登録された設定です。SandboxInterface 自体を拡張するエージェントコードは、同一のポリシーにバインドされたインターフェースのみを取得し、より広いものを取得することはありません。

  • キャプチャチェックは実験的です。 このプロジェクトは -language:experimental.captureChecking を使用しています。コンパイラの動作はScala 3ナイトリーバージョンによって変わる可能性があります。予期しないエラーが発生した場合は、フラグを一時的に削除してキャプチャチェックが原因かどうかを確認してください。

  • ライブラリはScala 3ナイトリーを使用しています。 ビルドは最新のScala 3ナイトリーを自動的に取得します。つまり、コードは最先端のScalaと互換性がある必要があります。安定性が必要な場合は、build.sbt で特定のバージョンを固定してください(val scala3Version = "3.x.y")。

  • Interface.scala はリソースとしてバンドルされています。 サーバーはビルド時に Interface.scala をリソースにコピーし、show_interface ツールがそれを表示できるようにします。新しいAPIを追加すると、ユーザーは show_interface を通じて自動的にそれらを確認できます。追加の作業は不要です。

  • 禁止パターンはユーザーコードに対して実行され、ライブラリコードには実行されません。 CodeValidator.scala のバリデータはユーザーが送信したコードのみをチェックします。ライブラリ自体は実装で java.io、java.net、ProcessBuilder などを自由に使用できます。ただし、新しいAPIがJava APIをラップする場合は、ユーザーが機能ラッパーを迂回できないように、対応する禁止パターンを追加する必要があります。

  • ライブラリJARはファットJARです。 sbt "lib/assembly" は、ライブラリのすべての依存関係(例: openai-java)を含むJARを生成します。依存関係を追加すると、自動的にバンドルされます。

  • サーバーはコンパイル時にライブラリ型に依存します。 サーバーはREPLを実行するためにインターフェース型に依存します。変更がサーバーの期待するインターフェースと互換性があることを確認してください。

  • まずライブラリレベルでAPIをテストしてください。 library/test/ ディレクトリには、MUnitを使用したライブラリレベルのテストがあり、scala-cli test library --server=false で実行されます(これらは sbt test の一部ではありません。--server=false は、現在のScala 3ナイトリーとscala-cliにバンドルされているBloopサーバーとの間のASMの衝突を回避します)。MCPサーバーを通じた統合テストの前に、そこで新しい操作をテストしてください。例については LibrarySuite.test.scala を参照してください。

開発

要件:

  • JDK 17+

  • sbt 1.12+

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 はサーバースイートのみを実行します。library/test/ スイートは scala-cli test library --server=false で個別に実行されます。

# 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

引用

@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}
}

ライセンス

Apache-2.0

Related MCP Connectors

Related MCP Servers

  • 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
    84 npm
    13
    MIT
  • A
    license
    Not graded
    quality
    B
    maintenance
    Enables AI agents to operate through a local, signed boundary that blocks prompt injection and secret leakage, verifies outputs, preserves cross-session memory, and provides offline-verifiable receipts. It also exposes 900+ MCP tools for discoverable agent actions.
    7
    MIT