Tailscale の ACL を Prolog で検証する

2025-01-26 #tech

#Tailscale の ACL

Tailscale には ACL の機能があり、各ホストがどのように通信できるかを制限することができます。例えば次のように書くと hostA から hostB・hostC へは 22 番ポートで通信ができる一方、 hostB からは hostC にしか通信ができない、といった制限をかけられます^[1]：

{
  acls: [
    // hostA は hostB, hostC の 22 番ポートへ接続できる。
    {
      action: "accept",
      src: ["hostA"],
      dst: ["hostB:22", "hostC:22"],
    },
    // hostB は hostC の 22 番ポートへ接続できる。
    {
      action: "accept",
      src: ["hostB"],
      dst: ["hostC:22"], // hostA へはアクセスできない。
    },
  ],
}

この設定をテストするために、Tailscale ACL には tests というフィールドが用意されています。例えば上の設定に対して以下のように書いておくと、ACL の内容を保存するたびに「hostB から hostC:22 へはアクセスできるが hostA:22 へはアクセスできない」ということを確認するテストが行われることになります：

{
  tests: [
    {
      src: "hostB",
      accept: ["hostC:22"], // hostC:22 へはアクセスできる。
      deny: ["hostA:22"], // hostA:22 へはアクセスできない。
    },
  ],
}

さて Tailscale には Tailscale SSH という機能があり、これを使うと SSH 用の鍵対の管理を Tailscale に任せることができ便利です。この Tailscale SSH の接続についても ACL で管理できます。例えば以下のように書くと、各メンバは自分自身が持っているマシンに SSH することができ、さらに管理者は tag:server が付与されたマシン^[2]に追加で SSH することができるという意味になります：

{
  ssh: [
    // メンバは自分が持つマシンに SSH できる。
    {
      action: "check",
      src: ["autogroup:member"],
      dst: ["autogroup:self"],
      users: ["autogroup:nonroot"],
    },
    // 管理者は tag:server がついたマシンに SSH できる。
    {
      action: "check",
      src: ["autogroup:admin"],
      dst: ["tag:server"],
      users: ["autogroup:nonroot"],
    },
  ],
}

#`sshTests` の漏れ

acls に対する tests と同様に、ssh の内容も sshTests というフィールドを使うことでテストすることができます。しかしこのテストの仕組みには漏れがあり、 SSH できないマシン間でも SSH できると判定してしまうことがあります。例えば上の例で hostA と hostB が同じメンバによって所有されている場合、以下のようなテストを書くと通ってほしいのですが、残念ながら通りません：

{
  sshTests: [
    {
      // hostB から hostA へは acls フィールドの設定により接続できないため
      // SSH 不可能であることをテストしたいが、SSH 可能だと判定されてエラーになる。
      src: "hostB",
      dst: ["hostA"],
      accept: [],
      check: [],
      deny: ["user1"],
    },
  ],
}

Tailscale SSH の公式ドキュメントによると、あるマシン A から別のマシン B に Tailscale SSH で接続するためには、ACL の設定が以下の条件を両方とも満たす必要があります：

マシン A からマシン B へ、22 番ポートでの接続が acls フィールドによって許可されていること。
マシン A からマシン B への SSH 接続が ssh フィールドによって許可されていること。

sshTests では後者の ssh フィールドの許可のみを確認し、前者の acls フィールドの確認を行わないため、上記のような誤判定が起こるのだと考えられます。

#Prolog で Tailscale ACL の仕組みを表現する

こういう何かの条件が重なっているかどうかを判定するのに便利なのが Prolog です^[3]。ということで Prolog を使って Tailscale の ACL を検証して、本当は SSH ができないことを検証してみます。なお当方 Prolog はほとんど初めて使ったので使い方が合っているかどうかは眉にツバをつけて見てください。

Prolog の環境は nix-shell -p swi-prolog したら入った SWI-Prolog 9.2.7 です。

ざっと書くと以下の感じです。% から始まる行はコメントです。眠いので説明を端折っていますが、その分コメントをたくさんつけたので許してください。

% user1 が hostA, hostB を持っている。
user_has_host(user1, host_a).
user_has_host(user1, host_b).

% tag:server が hostC についている。
tagged_host(server, host_c).

% autogroup:member には user1 が含まれる。
autogroup_member(user1).

% autogroup:admin には user1 が含まれる。
autogroup_admin(user1).

% どのマシンも、自分自身への通信はできる。
accept(X, X, _).

% ここから "acls" の中身を Prolog で書く。
%
% // hostA は hostB, hostC の 22 番ポートへ接続できる。
% {
%   action: "accept",
%   src: ["hostA"],
%   dst: ["hostB:22", "hostC:22"],
% },
accept(host_a, host_b, 22).
accept(host_a, host_c, 22).

% // hostB は hostC の 22 番ポートへ接続できる。
% {
%   action: "accept",
%   src: ["hostB"],
%   dst: ["hostC:22"], // hostA へはアクセスできない。
% },
accept(host_b, host_c, 22).

% ここから "ssh" の中身を Prolog で書く。
%
% // メンバは自分が持つマシンに SSH できる。
% {
%   action: "check",
%   src: ["autogroup:member"],
%   dst: ["autogroup:self"],
%   users: ["autogroup:nonroot"],
% },
has_ssh_key(X, Y) :-     % マシン X がマシン Y に SSH できる（鍵を持っている）ための
                         % 一つの条件は
    autogroup_member(Z), % Z が autogroup:member の一員であって、かつ
    user_has_host(Z, X), % Z がマシン X を所有していて、かつ
    user_has_host(Z, Y). % Z がマシン Y を所有していること。

% // 管理者は tag:server がついたマシンに SSH できる。
% {
%   action: "check",
%   src: ["autogroup:admin"],
%   dst: ["tag:server"],
%   users: ["autogroup:nonroot"],
% },
has_ssh_key(X, Y) :-        % マシン X がマシン Y に SSH できる（鍵を持っている）ための
                            % 一つの条件は
    autogroup_admin(Z),     % Z が autogroup:admin の一員であって、かつ
    user_has_host(Z, X),    % Z がマシン X を所有していて、かつ
    tagged_host(server, Y). % tag:server が Y についている。

% Tailscale SSH を行うためには acls フィールドで 22 番ポートの接続が許可されていて、かつ
% ssh フィールドで許可されている必要があることを書く。
ssh(X, Y) :-            % マシン X からマシン Y に SSH するためには
    accept(X, Y, 22),   % 22 番ポートで X -> Y の接続が許可されていて、かつ
    has_ssh_key(X, Y).  % X が Y の SSH 鍵を持っている必要がある。

以上を main.pl というファイルに書いておき、SWI-Prolog を swipl コマンドで立ち上げ、[main]. と打って読み込みます：

$ swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 9.2.7)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- [main].
true.

?-

上のように true. と返ってきたら読み込めています。

対話環境で Tailscale SSH の接続性を確認してみます。まず hostA から hostB への SSH ができることを見てみます^[4]。

?- once(ssh(host_a, host_b)).
true.

?-

true が返ってきたのでよさそうです。では今度は hostB から hostA への SSH ができないことを見てみます。これが Tailscale の sshTests では確認できなかった接続性です：

?- once(ssh(host_b, host_a)).
false.

?-

正しく false になることが確認できました。やったぜ。ついでに hostB から SSH できるマシンを全列挙してみましょう：

?- findall(X, ssh(host_b, X), L).
L = [host_b, host_c].

?-

hostB 自身と hostC であることが（正しく）分かりました。

#まとめ

Prolog が使える場面としてサザエさんの家系図を表現できる例があまりにも有名ですが[要出典]^[5]、こういう使い方もできるんだなぁということで面白かったです。

#注釈

この様にホスト名を acls で使うためには hosts を適切に埋めておく必要がありますが、ここでは省略します。 ↩
Tailscale のタグは他サービスの service account のような役割を果たします。この場合 tag:server がついているマシンはどのメンバにも所有されておらず、言うなれば tag:server によって所有されたマシンとして扱われます。なおタグとマシンは多対多の関係です。 ↩
あまりにも自然な Prolog の導入。 ↩
once をつけると、変数へ割り当たる値のパターンが複数ある場合に、いずれか一つのパターンで true になれば全体を true にしてくれます（多分）。今回は何らかの割当てで ssh(host_a, host_b) が満たされればよいので once をつけています。 ↩
論理憲法も Gigazine に取り上げられたので有名かもしれない。 ↩

Tailscale の ACL を Prolog で検証する