SSHのホスト鍵設定

ホスト鍵とは

SSHの鍵はデジタル署名用の秘密鍵であり、本人確認に使われる。いわゆるid_rsaは、ユーザー側の本人確認のために使われる。

一方、SSHサーバー側も専用の秘密鍵を所有している。これは /etc/ssh/ssh_host_{dsa,ecdsa,ed25519,rsa}_key のような場所に保管されている。SSH接続の際には、これを使った公開鍵認証も行われる。クライアント側の .ssh/known_hosts と照らし合わせてチェックする。

ホスト鍵がないと何が問題か

もし悪意ある第三者が通信を盗聴・改竄できる場合、偽のサーバーと通信させることができてしまう。すると、適切な暗号を用いて全くの別人と会話しているという本末転倒な状態になる。偽のサーバー上と気付かずにsudoパスワードを入れたら困ったことになるかもしれない。

HashKnownHostsをオフにする

筆者は、ホスト鍵を安全に運用するために、HashKnownHostsオフにするべきだと考えている。

そもそも HashKnownHosts とは、 .ssh/known_hosts においてホスト名をハッシュ化して保存するオプションである。ハッシュ化をしない場合、 known_hosts の各行は以下のようになっている。

example.com ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHayNTYAAAAIbmlzdHAyNTYAAABBBAHOh5LY0tU5hZGZn4iFvUQ9EJSGW7n9KbTXj5WK5AEIQNB5ShhNPwJcXqtc5hxwEmBX2VSdjUFkIT6U2Otur7w=

HashKnownHosts を使うと、「ホスト名またはIPアドレス」「署名方式」「公開鍵」のうち、「ホスト名またはIPアドレス」の部分がハッシュ化され、

|1|tbdGjw+HE9Clw2hC7ezBLOMGFGI=|xOtpgqDyfDlT/PB7cYm442R1+zY= ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHayNTYAAAAIbmlzdHAyNTYAAABBBAHOh5LY0tU5hZGZn4iFvUQ9EJSGW7n9KbTXj5WK5AEIQNB5ShhNPwJcXqtc5hxwEmBX2VSdjUFkIT6U2Otur7w=

のようになる(|1|ソルト|ハッシュ|)。ハッシュ化することで、

  • 特定のホスト名が、この行に該当するかどうかは判定できる。
  • しかし、この行だけ見て、ホスト名を復元することは困難である。

となる。つまり、

  • HashKnownHostsメリット: known_hosts が漏洩しても、接続先ホストの情報が復元できない。
  • HashKnownHostsデメリット: known_hosts の管理が困難になる。どのホストを信任しているかわからないため、偽のホストを信頼してしまう危険性が増える。

と考えられる。接続先ホストの情報は仮に漏れても大きな影響はなさそうだし、むしろ known_hosts が漏洩するような状況では秘密鍵など他の重要な情報も漏れている状況だから、メリットがデメリットに釣り合わないと思う。

known_hosts を管理する

ここでは、ホスト名のハッシュ化を止めた上で、 known_hosts をきちんと管理することを考えたい。前述のとおり、 known_hosts の基本フォーマットは

ホスト名またはIPアドレス 署名方式 公開鍵 (コメント)

である。また、 # で始まる行もコメントである。

「ホスト名またはIPアドレス」の部分の詳細なフォーマットは以下の通り。

  • 基本的には、 gitlab.com とか 52.167.219.168 のようにホスト名またはIPアドレスがそのまま使える。
  • 22番以外のポートのときは、 [example.com]:60022 とか [192.0.2.23]:60022 のように[]づけで表記する。
  • , で複数のホスト名またはIPアドレスを並べることができる。ホスト名とIPアドレスを並べてもよい。 (ハッシュ化していないときのみ)
  • * は0文字以上のワイルドカードとして使える。 (ハッシュ化していないときのみ)
  • ? は1文字のワイルドカードとして使える。 (ハッシュ化していないときのみ)

例えば、GitHubとGitLabのための known_hosts は以下のように書ける。

# GitHub -- marked CheckHostIP no
github.com ssh-rsa AAAAB3NzaC1yc2EAAAABIwAAAQEAq2A7hRGmdnm9tUDbO9IDSwBK6TbQa+PXYPCPy6rbTrTtw7PHkccKrpp0yVhp5HdEIcKr6pLlVDBfOLX9QUsyCOV0wzfjIJNlGEYsdlLJizHhbn2mUjvSAHQqZETYP81eFzLQNnPHt4EVVUh7VfDESU84KezmD5QlWpXLmvU31/yMf+Se8xhHTvKSCZIFImWwoG6mbUoWf9nzpIoaSjB+weqqUUmpaaasXVal72J+UX2B+2RPW3RcT0eOzQgqlJL3RKrTJvdsjE3JEAvGq3lGHSZXy28G3skua2SmVi/w4yCE6gbODqnTWlg7+wC604ydGXA8VJiS5ap43JXiUFFAaQ==

# GitLab
gitlab.com,52.167.219.168 ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHAyNTYAAAAIbmlzdHAyNTYAAABBBFSMqzJeV9rUzU4kWitGjeR4PWSa29SPqJ1fVkhtj3Hw9xjLVXVYrU9QlYWrOLXBpQ6KWjbjTDTdDkoohFzgbEY=
gitlab.com,52.167.219.168 ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQCsj2bNKTBSpIYDEGk9KxsGh3mySTRgMtXL583qmBpzeQ+jqCMRgBqB98u3z++J1sKlXHWfM9dyhSevkMwSbhoR8XIq/U0tCNyokEi/ueaBMCvbcTHhO7FcwzY92WK4Yt0aGROY5qX2UKSeOvuP4D6TPqKF1onrSzH9bx9XUf2lEdWT/ia1NEKjunUqu1xOB/StKDHMoX4/OKyIzuS0q/T1zOATthvasJFoPrAjkohTyaDUz2LN5JoH839hViyEG82yB+MjcFV5MU3N1l1QL3cVUCh93xSaua1N85qivl+siMkPGbO5xR/En4iEY6K2XPASUEMaieWVNTRCtJ4S8H+9
gitlab.com,52.167.219.168 ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIAfuCHKVTjquxvt6CM6tdG4SLp1Btn/nOeHHE5UOzRdf

CheckHostIP をオフにする

ホスト鍵は基本的に、接続しようとしたDNS名と照合される。しかし、 CheckHostIP が有効の場合、IPアドレスに対しても照合が行われる。

普通、DNSの対応付けが変わっていても、接続先のサーバーが想定通りのホスト鍵を返せば信頼してもよいはずなので、 CheckHostIP は予防的な意味合いが強いと思われる。特に、GitHubのようにDNSラウンドロビンを使っている場合は面倒なので、上記のワイルドカードを使うか、そもそも CheckHostIP を外してしまうのがよいと思う。 (GitHubのIPアドレス一覧)

StrictHostKeyChecking の有効化

想定していないホスト鍵が送られてきたとき、SSHは以下のように振る舞う。

  • 別のホスト鍵を既に知っている場合、問答無用で接続拒否になる。オレオレ詐欺で言うところの「母ちゃん俺だよ、携帯番号変えたからさ」というやつである。どうしても接続するならknown_hostsを手動かコマンドでいじる必要がある。
  • 未知のホストの場合
    • StrictHostKeyChecking yes の場合: 接続拒否する。
    • StrictHostKeyChecking no の場合: known_hostsに追加して続行する。
    • StrictHostKeyChecking ask の場合(デフォルト): ユーザーの答えに応じて上のどちらかの処理をする。

.ssh/config に入っているホストにしか接続しないような生活であれば、どれもそれほど変わらないと思う。筆者は StrictHostKeyChecking yes にしておき、新規ホストを追加したとき、そのホストに対して一時的に StrictHostKeyChecking ask を付与している。

EC2への対処

EC2のように、同じIPアドレスのマシンを消したりまた立ち上げたりしていると、既知のホスト鍵との衝突でどうしても接続拒否になってしまう。せっかく known_hosts をちゃんと管理しているので、テキストエディタで消してしまうとよいと思うが、ホスト鍵のチェックを強制的に省略する方法もあるにはある

UpdateHostKeys の有効化

UpdateHostKeys ask とすると、ホスト鍵が更新されたときに、新しいホスト鍵を known_hosts に追加することができる。(以前のホスト鍵で認証したあとで送られてくるので、問題はない。) サーバー側をうまく設定すれば、キーローテーションをすることもできる。

まとめと宣伝

known_hosts はちゃんと管理することもできる。ちなみに known_hostsauthorized_keys を正しくハイライトするVimプラグインを作ったのでぜひ。

再帰的余代数について

最近、再帰的余代数という概念について少し勉強したので、証明をまとめてPDFにした。

github.com

動機など細かいところには触れられていないが、以下のことが証明されている。

  • 再帰的余代数 = 始代数
  • Setでは、再帰的ならば整礎

WSL+Xming環境整備

WSLとXmingを組み合わせていい感じに環境整備できてきたので記録をとる。

WSLとXmingについて

  • WSLはWindows上でLinuxのプロセスを実行する機能である。互換性は完全ではないが、多くのソフトウェアが動くようになっている。ただし、そのままではGUIは動かない。
  • XmingWindows上で動作するXサーバーのうちの一つ (Cygwin/Xの派生) である。XはLinuxで使えるGUIの仕組みで、画面側がXサーバー、アプリ側がXクライアントとなってTCP経由で接続できるという特徴がある。ここではWSL側をクライアントにしてXmingに繋ぐことで、GUIを使えるようにする。

Xming最新版の取得

Xmingの最新版のビルドを入手するには£10.00程度の寄付が必要である。多くの人は2007年(!!!)のバージョンを使っている。そういうわけなので巷の評判は気にせず最新版を入手するといいと思う。 (たとえば、勝手に英語キーボード設定になる問題には今のところ遭遇していない)

同ページの寄付に関するセクションに詳しい説明がある。以下は勝手に翻訳したもの

寄付をすると、ドナーパスワードがメールで送られます。それを使うことで、XmingのWebリリース版と開発スナップショット版を個人利用のために取得することができます。パスワードは、PayPalの支払い履歴に記載されているメールアドレスに対して送られます。そのため、支払いメールアドレスが有効なメールアドレスであることと、私のISPのメールサーバー ([WWW]zen.co.uk 、例えば smarthost01.mail.zen.net.uk) をブロックしていないことを確認しておいてください。寄付以外の方法(コードやパッチなど)で貢献をした場合や、パスワードが送られてこない場合は、私に連絡をしてください。また、PayPalを使えず、代替手段が必要な場合も、私にメール (訳注: ここにメールアドレスが書いてあります) で連絡をしてください。寄付金額として10ポンドを提案していますが、これより低い金額だと手数料の割合が高くなってしまうからです。注意: 上のボタンを経由してPayPalで支払いをする場合、PayPalのアカウントは必要ありませんが、クッキーを有効にする必要があります。

寄付はPayPal経由と書いてあるが、PayPalは日本からの寄付を許可していない(おそらく法的な理由)。その場合は上にあるように作者にメールをするとよい。以下は筆者の送ったメールの例

Subject: Want to donate from Japan

Text:

I want to donate to Xming from Japan, from which I can’t donate money via PayPal due to legal reasons. Could you offer alternatives if any?

Masaki Hara

すると代替手段を教えてもらえる。筆者は、作者からPayPalの支払いリンクを送ってもらう方法(日本から寄付はできないが、支払いはできる)を選んだ。

Subject: Re: Re: Want to donate from Japan

Text:

Thank you! Can I receive a payment link then?

しばらくするとPayPalの支払いリンクを送ってもらえるので、それに対して£10.00支払うと、パスワードが送られてくる。

Xmingのインストール

今回はWSLから呼び出す形での利用のみを想定しているのでPuTTY連携は考えない。そのため以下の2つをインストールする。

Xming-fontsはXming-x64のあとにインストールする。逆順にすると C:\Program Files (x86)\Xming にインストールしようとしてしまう。

ちなみにこのXming-fontsだが、ほぼEmacs用である。GTKやQtなどで作られているGUIアプリはクライアント側(Linux側)のフォントを参照するからである。

Xmingの起動

はじめはXming Launchなどを使って起動してみるとよいが、オプションがわかってしまったあとはショートカットを作るほうが楽だ。

"C:\Program Files\Xming\Xming.exe" :0 -clipboard -multiwindow -xkbmodel jp106 -xkblayout jp -dpi auto -wgl へのショートカットを作成した。

  • :0 は画面の番号で、これに6000を足したTCPポートで通信が行われる。
  • -clipboard によりWindows側のクリップボードと共有する。
  • -multiwindowXmingのモードの一つで、Linux側のウインドウ1個がWindows側のウインドウ1個に対応する。
  • -xkbmodel jp106 -xkblayout jp は日本語キーボード配列を指定している。
  • -dpi autoWindows側のDPIを継承する。筆者のコンピューターはNew Surface Proで、高DPI環境だが、この設定だけでかなりうまく設定される。
  • -wglOpenGLアクセラレーションを有効化する。

WSLの設定 (Ubuntuのインストール)

Bash on Ubuntu on Windowsをインストールしてみよう! - Qiita」に従ってWSLを設定した。WSLの上では他のディストリビューションも動かせるが、ここではUbuntuを仮定する。

Xfce4のインストール

bash.exeを起動して xfce4-sesson, xfce4-goodies, gnome-keyring, fonts-vlgothic, fcitx-skk をインストールした。 (ここで日本語フォントを入れておかないと、Xming-fontの有無に関係なく日本語が化けて困ることになる)

起動スクリプトの作成

以下のような内容のスクリプトを /home/qnighy/Xming.sh に置いた。

#!/bin/bash

# ホームから開始したいので
cd
# パーミッション777のファイルが量産されると困るので
umask 0022
# localhost:0.0の略で、これでXmingに繋がることになる
export DISPLAY=:0.0
# 必ずXming経由でOpenGLを使う
export LIBGL_ALWAYS_INDIRECT=1

# gnome-keyringをスタート (SSH鍵を覚えさせたいので)
eval $(gnome-keyring-daemon --start --components=pkcs11,secrets,ssh)
export GNOME_KEYRING_CONTROL SSH_AUTH_SOCK

# インプットメソッドの設定 (fcitxの場合)
IM=fcitx
export XMODIFIERS="@im=$IM"
export GTK_IM_MODULE=$IM
export QT_IM_MODULE=$IM
export NO_AT_BRIDGE=1
# 全角/半角キーが連打される例のやつを防ぐ
xset -r 49
# fcitxを起動
fcitx

# SHLVLを0に下げてからターミナルを起動
SHLVL=0 xfce4-terminal

bash.exe -l /home/qnighy/xming.sh のように実行するとターミナルが出てくる。やっほい

ショートカットの作成

bash.exeを黙らせたいので、無言で実行するためのユーティリティーを導入する。

The Run utilityからrun-x64.zipをダウンロードして、中にあるrun.exeC:\Windows\System32\にコピーする。 (Xmingの作者が作っている模様)

その後、 C:\Windows\System32\run.exe C:\Windows\System32\bash.exe -l /home/qnighy/xming.sh に対してショートカットを作成する。

アイコンをいい感じにする

Xmingの作るウインドウは、極力Linux側のアイコンを反映するが、上手くいかないことがある。特にxfce4-terminalは上手くいかなかったので、手動で設定する。

まず imagemagick を入れて、以下のようにしてicoファイルを作成する。

convert /usr/share/icons/elementary-xfce/apps/*/xfce-terminal.png xfce-terminal.ico

同じ方法で色々なアイコンをicoに変換できる。

作ったicoWindows側に置く。まずショートカットが不恰好なのでショートカットのアイコンに設定する。

続いてXmingrcをいじる。Xmingrcのデフォルト設定は C:\Program Files\Xming\Xmingrc にあるので、これを C:\Users\qnighy\Xmingrc にコピーする。

# Xming Server Default Resource File
# follow.exe and xhost.bat are in "Tools and clients"
Menu apps {
    "&View the log" viewlog
    "&Tail the log" execd follow
    "&Reload Xmingrc" reload
    &Usage execd "Xming :999 -help"
    "Access Control &Status" execd "xhost.bat"
    "&Command Prompt" execd cmd
    "Host &Finder" finder
    separator
}
RootMenu apps
SilentExit
Debug "Using the default Xmingrc configuration file."

これを弄って以下のようにした。

# Xming Server Default Resource File
# follow.exe and xhost.bat are in "Tools and clients"
Menu apps {
    "&View the log" viewlog
    "&Tail the log" execd follow
    "&Reload Xmingrc" reload
    "&Usage" execd "Xming :999 -help"
    "Access Control &Status" execd "xhost.bat"
    "&Command Prompt" execd cmd
    separator
}
RootMenu apps
SilentExit
Icons {
    # アイコンを上書き
    xfce4-terminal C:\Users\qnighy\xfce-terminal.ico
}

こうするとウインドウクラスかウインドウ名がxfce4-terminalであるようなウインドウには、指定したアイコンを使うようになる (Xmingrcの説明も参照)

ところで、ウインドウクラスを調べるには xprop コマンドを使う。 xprop を実行したあと、調べたいウインドウをクリックすると、以下のように色々な属性が表示される。

$ xprop
_NET_WM_STATE(ATOM) = 
_NET_WM_USER_TIME(CARDINAL) = 3901640
_WINDOWSWM_NATIVE_HWND(INTEGER) = 328280, 0
WM_STATE(WM_STATE):
        window state: Normal
        icon window: 0x0
WM_HINTS(WM_HINTS):
        Client accepts input or input focus: True
        Initial state is Normal State.
        window id # of group leader: 0xe00001
XdndAware(ATOM) = BITMAP
_MOTIF_DRAG_RECEIVER_INFO(_MOTIF_DRAG_RECEIVER_INFO) = 0x6c, 0x0, 0x5, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x10, 0x0, 0x0, 0x0
WM_WINDOW_ROLE(STRING) = "xfce4-terminal-1506224785--565597661"
_NET_WM_SYNC_REQUEST_COUNTER(CARDINAL) = 14680070
_NET_WM_WINDOW_TYPE(ATOM) = _NET_WM_WINDOW_TYPE_NORMAL
_NET_WM_USER_TIME_WINDOW(WINDOW): window id # 0xe00005
WM_CLIENT_LEADER(WINDOW): window id # 0xe00001
_NET_WM_PID(CARDINAL) = 20
WM_LOCALE_NAME(STRING) = "ja_JP.UTF-8"
WM_CLIENT_MACHINE(STRING) = "qnighy-chris"
WM_NORMAL_HINTS(WM_SIZE_HINTS):
        user specified size: 362 by 0
        program specified minimum size: 93 by 116
        program specified resize increment: 19 by 38
        program specified base size: 17 by 40
        window gravity: NorthWest
WM_PROTOCOLS(ATOM): protocols  WM_DELETE_WINDOW, WM_TAKE_FOCUS, _NET_WM_PING, _NET_WM_SYNC_REQUEST
WM_CLASS(STRING) = "xfce4-terminal", "Xfce4-terminal"
WM_ICON_NAME(STRING) = "Terminal - xprop"
_NET_WM_ICON_NAME(UTF8_STRING) = "Terminal - xprop"
WM_NAME(STRING) = "Terminal - xprop"
_NET_WM_NAME(UTF8_STRING) = "Terminal - xprop"

このうち WM_CLASS と書かれているものがウインドウクラスにあたる。はじめから xprop | grep WM_CLASS とやると楽かもしれない。

困っていること

  • dbusがうまく動かない。redditとかに色々書いてあるけど手元ではまだ動いていない。
  • OpenGLで複雑なことをしようとすると厳しい。なぜかGLSLのコンパイルが通らない。
  • 他にも変なシステムコールは通らないので、そういうことをやるときは仮想マシンを立ち上げる。

古いRubyをビルドする

動機

現時点でRubyの最新版は2.4, サポートされているのは2.2までで、2.1以前はメンテナンス対象外である。そのような古いバージョンを動かすのは決してよいことではない。

しかし実のところ、現在でも多くのWindowsマシンで、Ruby1.8.1とRuby1.9.2p0が動作している。具体的には、RPGツクールXP, RPGツクールVXというソフトウェアで作られたゲームはRuby1.8.1の処理系とともに配布されており、RPGツクールVX Aceというソフトウェアで作られたゲームはRuby1.9.2p0の処理系とともに配布されている。既に多くのゲームが世に送り出されているのみならず、これらのいずれのツールも、未だにそれぞれ根強い人気があり、今でも多くの名作が作られている。「ふりーむ」というサイトで「RPGツクール XP」と検索した結果からも、その人気を伺い知ることができる。

そういった事情から筆者はRuby1.8.1とRuby1.9.2p0に強い興味があり、ビルドを試みたところ、いくつかの問題があった。

前提

とりあえず、Ubuntu 16.04 x86_64でのビルドを想定している。アーキテクチャを拡大すれば、より多くの問題が顕在化するかもしれない。

Ruby1.9.2p0の問題

Ruby1.9.2p0を現代の環境でビルドすると、以下の問題があった。

  • 継続・コルーチン処理が最適化で壊れる
  • bisonでコンパイルエラーになる

継続・コルーチン処理が最適化で壊れる

Fiberやcall/ccの処理はスタックのコピーによって実現されているが、コンパイラによってはspレジスタの最適化によりこの処理が壊れてしまい、処理系がサイレントに死ぬことがある。これはr34278をbackportすることで解決できた。

bisonでコンパイルエラーになる

pure-parser周りの仕様変更により新しめのbisonでコンパイルできない。これはr42282をbackportすることで解決できた。

Ruby1.8.1の問題

Ruby1.8.1を現代の環境でビルドすると、以下の問題があった。

  • group_memberの衝突
  • bisonとの組み合わせでGCが壊れる
  • autoconf2.6x系列でビルドできない

group_memberの衝突

file.cで定義されているgroup_memberと、Cライブラリのgroup_memberが衝突する。これはgroup_memberrb_group_memberにリネームすることで解決できた。歴史的にはこの変更はr13240r26682の組み合わせといえる。

bisonとの組み合わせでGCが壊れる

ある程度新しいbisonはLRのセマンティックバリューのスタックをヒープで管理することがあるが、この場合Ruby1.8.1だとヒープ上のセマンティックバリューのマーク漏れが発生する。ノードのnd_fileが汚染された結果、次のGCのタイミングでGCのフリーノードの直前のRVALUEの最後の1バイトが破壊され、その1バイトがノードからのポインタになっていた場合に領域外参照でサイレントに死ぬ。これはr9355, r9405, r9416, r9382, r9639をbackportすることで解決できた。

autoconf2.6x系列でビルドできない

いくつかの複合的な問題からautoconf2.6系列でビルドできない。これはr10189の一部、r10392r11594をbackportして、srcdirの解釈を正しくするよう少し改造を加えることで解決できた。

成果物

現時点での成果物をqnighy/ruby-1.9.2p0qnighy/ruby-1.8.1に置いてある。

Rust-proofを使ってみる

概要: Rust-proofはElectrolysisと同様にRustプログラムから検証条件を抽出するが、LeanではなくSMTソルバであるZ3向けの検証条件を出力する。こちらも開発が放棄されているように見えるが現在もビルド可能である。

準備

テスト用リポジトリを準備する

$ cargo new rustproof-test
$ cd rustproof-test

該当のnightlyバージョンを取得する (Electrolysisと同様、Rust-proofもコンパイラプラグインのため、特定のnightlyバージョンに強く依存している)

$ rustup override set nightly-2016-08-12

Z3をインストール

$ sudo apt install z3

使ってみる

Cargo.toml に以下の依存関係を書く

[dependencies]
rustproof = { git = "https://github.com/Rust-Proof/rustproof.git", rev = "654b004" }

src/lib.rs に以下のように関数を書く。これはEXAMPLESに掲載されているものとほぼ同様だが、5:i32のような型つきリテラル5i32に置き換えてある。

// feature(plugin) を有効化してrustproofをロード
#![feature(plugin)]
#![plugin(rustproof)]

// #[condition] によりコンパイル時にrustproofによるチェックが走る

#[condition(pre="(x:i32 <= i32::MAX - 5i32)", post="return:i32 == (x:i32 + 5i32)")]
pub fn add_five(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

#[condition(pre="(x:i32 <= i32::MAX - 4i32)", post="return:i32 == (x:i32 + 5i32)")]
pub fn add_five_invalid(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

#[condition(pre="true", post="(x:bool==true IMPLIES return:bool==false) && (x:bool==false IMPLIES return:bool==true)")]
pub fn boolean_not(x:bool) -> bool {
    if x == true {
        false
    } else {
        true
    }
}

検証を実行するには単にコンパイラを起動すればよい。

$ cargo build
   Compiling rustproof-test v0.1.0

fn add_five(..) Verification Condition is valid.


fn boolean_not(..)  Verification Condition is valid.


fn add_five_invalid(..) Verification Condition is not valid.

(model 
  (define-fun x () (_ BitVec 32)
    #x7ffffffb)
)

    Finished debug [unoptimized + debuginfo] target(s) in 42.84 secs

まとめ

大変よい試みだが、古すぎるのが残念だと思う。rust-proofが開発された経緯は不明だが、documentsというディレクトリに不穏な資料が残されているので見てみると面白いかもしれない。

Electrolysisを使ってみた

概要: ElectrolysisはRustの検証条件をLEANに出力するプロジェクトである。これを使ってみた。

Electrolysisとは

Electrolysis (electrolysis: 電解) はSebastian Ullrich氏の修士研究で開発されたプロジェクトで、Rustプログラムの正当性や計算量に関する検証条件をLean Theorem Proverの命題として出力する機能を提供する。

なお、GitHubの様子だと、このプロジェクトは修論の日付からほぼ開発がストップしているようだ。Ullrich氏はその後、Electrolysisの成果の一部をLEANに還元するなどの活動をしているようだ。

Electrolysisの実行

以下、Ubuntu 16.04を仮定する。

ElectrolysisはRustのコンパイラプラグインとして実装されているため、Rustの特定のnightlyバージョンに強く依存している。また、libcore自体を検証ターゲットにしているため、Rustコンパイラソースコード自体も取得する必要がある。

$ git clone https://github.com/Kha/electrolysis.git
$ cd electrolysis
$ rustup override add $(cat rust-nightly-version)
$ rustup component add rust-src
$ cargo run core
$ cargo run alloc
$ cargo run collections
$ cargo run fixedbitset

petgraphに対する検証条件の出力

petgraphに対する検証条件の出力はやや面倒である。まずpetgraphを取得してビルドする。

$ git submodule update --init
$ cd thys/petgraph/src
$ cargo build
$ cd ../../..

次に thys/petgraph/config.toml を編集して、libfixedbitsetのrlibのハッシュを適切に置き換える。例えば、

rustc_args = "thys/petgraph/src/src/lib.rs --crate-name petgraph --crate-type lib -L dependency=thys/petgraph/src/target/debug/deps --extern fixedbitset=thys/petgraph/src/target/debug/deps/libfixedbitset-0ba3fe99bd419295.rlib"

targets = [
  "algo.scc",
]

とすると以下が通る。

$ cargo run petgraph

Lean2のビルド

Leanは現在、過去の証明との互換性のために残されている0.2.0系列と、最新の3.0.0系列がある。Electrolysisに適しているのは0.2.0系列なので、そちらを使う。

また、lean2のビルドスクリプトにはninjaを取得する部分があるが、ninjaの取得先が削除されてしまっているので、以下のパッチを当てる必要がある。(以下これをlinja.patchと呼ぶ)

diff --git a/bin/linja.in b/bin/linja.in
index 926f33e..10ee37d 100755
--- a/bin/linja.in
+++ b/bin/linja.in
@@ -239,7 +239,7 @@ def show_download_progress(*data):
     log_nonewline("Download: size\t= %i kb, packet: %i/%i" % (file_size, downloaded_packets, total_packets+1))
 
 def get_ninja_url():
-    prefix = "https://leanprover.github.io/bin/"
+    prefix = "https://github.com/leanprover/leanprover.github.io/raw/8fb36e926a3c4df8b84bfafedb7f39687f24b93b/bin/"
     if platform.architecture()[0] == "64bit":
         if platform.system() == "Linux":
             return prefix + "ninja-1.5.1-linux-x86_64"
$ sudo apt install python3 git libgmp-dev libmpfr-dev
$ git clone https://github.com/leanprover/lean2.git
$ cd lean2
$ patch -p1 < path/to/linja.patch
$ mkdir -p build/release
$ cd build/release
$ cmake -DCMAKE_BUILD_TYPE=Release ../../src
$ make -j4 install DESTDIR=.

上の例ではDESTDIR=.を指定することで./usr/localにインストールしているが、これを外せば/usr/localにインストールされる。

検証条件に対するLEAN2の実行

lean2にはlean3のような--makeオプションがついていない。以下のようなMakefilethysの直下に置くとよい。(LEANDIRを適切に変更する)

#!/usr/bin/make -f

LEANDIR = /somewhere/lean2/build/release/usr/local
LEAN = $(LEANDIR)/bin/lean

LEAN_SOURCES = $(shell find . -name '*.lean')
LEAN_BINARIES = $(LEAN_SOURCES:.lean=.olean)
LEAN_DEPFILES = $(LEAN_SOURCES:.lean=.d)

all:
  $(MAKE) deps
  $(MAKE) all2

deps: $(LEAN_DEPFILES)

all2: $(LEAN_BINARIES)

clean:
  $(RM) $(LEAN_DEPFILES) $(LEAN_BINARIES)

.PHONY: all deps all2 clean

%.d: %.lean
  (echo $<:; $(LEAN) --deps $<) | tr '\n' ' ' > $@

%.olean: %.lean
  $(LEAN) $< -o $@

-include $(LEAN_DEPFILES)

これを配置した上で thys 直下で make を実行すると、証明がコンパイルされる。

まとめと感想

Electrolysisの機能を一通り動かすことができた。

実は別のRustバージョンや別のLeanバージョンで動かせないか検討したがかなり困難であることがわかった。

Rustの検証プロジェクトではむしろRustBeltが有名で、メンバーから考えてもかなり期待が持てる。RustBeltとElectrolysisは以下のように異なる。

  • 検証の目的: RustBeltはunsafeな動作を含むより低レベルな操作に対し、UBを踏まないなどの証明をターゲットにしている。Electrolysisはより高級な変換で、アルゴリズムの正当性や計算量の検証を目指している。
  • ロジック: RustBeltは高階並行分離論理フレームワークIrisに立脚している。
  • 証明支援系: RustBeltはCoqで検証する。ElectrolysisはLeanで検証する。
  • 検証条件の抽出: Electrolysisは実際のRustコード(MIR)からの抽出に対応している。RustBeltは今のところMIRからの抽出には対応していない(Coq側の対応するコードは手動で書かれている)が、Ralf Jung氏が最近MIRの改造に取り組んでいるところから見るに、そのうち対応すると思われる。

Rust組込みトレイトのコヒーレンス

以下のトレイトは通常のコヒーレンス規則に加えて、特別なコヒーレンス規則が適用される。

Sized, Unsize

Sized, Unsize の手動実装を与えることはできない

Fn, FnMut, FnOnce

Fn, FnMut, FnOnce の手動実装は安定版では禁止されており、 #![feature(unboxed_closures)] が必要である

Drop

Dropはユーザー定義の構造体・列挙型・共用体にのみ定義できる。

また、(なぜかコヒーレンスチェッカーではなくDropチェッカーの一部になっているが)Drop は元の構造体・列挙型・共用体のジェネリクスを特殊化してはならない。これにより Drop は、各ADT型に対して定義されるか、定義されないかのどちらかになる。

Copy

Copy の実装は以下の条件を満たしている必要がある。

  • Self はユーザー定義の構造体・列挙型・共用体である。
  • その impl に課された境界から、各フィールドが Copy であることを結論づけられる。
  • この構造体・列挙型・共用体は Drop を実装していない。

CoerceUnsized

CoerceUnsized の実装は以下の条件を満たしている必要がある。

  • 両辺ともポインタ/参照型であるか、両辺とも構造体である。
  • ポインタ/参照型の場合、 (これは libcore で網羅されている)
    • ポインタからポインタ、ポインタから参照、参照から参照のいずれかである必要がある。
    • mut から mut, mut から const, const から const のいずれかである必要がある。
    • 参照から参照への場合は、大きいリージョン(部分型づけの意味では小さい)から小さいリージョン(部分型づけの意味では大きい)への変換である必要がある。
  • 構造体の場合、
    • 両辺が同じ定義を指している必要がある。
    • 両辺のフィールドをそれぞれ単一化したとき、ちょうど1個だけが失敗する必要がある。
    • 単一化が失敗したフィールドに対して同様に CoerceUnsized が成り立っている必要がある。