MacがARMになることによって開発者が死ぬ可能性が高い件について
この間のWWDC 2020を見ていて発狂しそうになった。MacがCPUをIntelからARM（Apple Silicon）に移行するらしい。なぜそんなことをするのかさっぱりわからない。たしかに、AppleがISAを変えるのは今に始まったことではないが、今と昔では事情が違う。過去の時代遅れの成功体験に引っ張られてるのではない か？意味がわからない。ジョブズが居なくなったAppleのときみたいに潰れ（かけ）なきゃ良いけどね。。。
私がそう思う理由は、Mac上でx86のVMM（VirtualBoxやParallels）が動かなくなるから。
VMMはISAレベルのエミュレーションを提供するソフトウェアであるが制約がある。物理ISAと同一のISAしかエミュレーションできない。しかしその分エミュレータと比較すると高速に動作する。その秘密は、特権命令やSensitive命令以外は可能な限り直接物理CPUで動かすから。要は、どうしてもエミュレーションしないと問題になるようなインストラクション（mov cr3, eaxとかsgdtとかpushf, popfとかね）以外は全部物理CPUに直接実行させるのである。これが速さの秘訣。I/Oを含んだり、よほどの作為的なプログラムでなければほとんど実CPUで実行してるのと変わらない速度で動作する。
つまりARMに移行されてしまうと、Mac上で（x86の）Linuxを動かして開発することが一切できなくなる。Mac版のDocker使ってる人も同じ。あれはVirtualBox上でLinuxを動かしてその上でDockerを動かしてるわけだからね、一切使えなくなる。
いやいやRosetta 2とやらがあるらしいよ？エミュレーターでx86環境が動くとか？いやだからそれはエミュレーターなんだよね。ソフトウェアでCPUのすべての機能を模倣するわけ。VMMとは比較にならないほど遅い。理由は上述したとおり。今どきVirtualPCにもどりたいの？これは明らかな退行である。
いやいやARM版Windows 10では既存のx86アプリケーションがそのまま実用的な速度で動くだろう？だから、ARMの上で動作するRosetta 2とやらでx86やEMT64のOSも十分実用的な速度でうごくのでは？それは間違ってる。そもそもABIレベルのエミュレーションでなんとかなるようなバイナリと、ISAレベルのエミュレーション（特にMMU込みで）が必要なバイナリを味噌糞一緒にして論じちゃいけない。エミュレーションのコストが段違い。特にMMU周りは本来ハードウェアでやってるはずのTLB周りの挙動なんかをまるっとソフトウェアでそっくり模倣することになるのだからこのオーバーヘッドはかなり大きい。VT-xやAMD-SVMでまたEPTやNested Pagingが実装されてなかった10年以上前に逆戻りしたいの？これも明らかな退行である。
というわけでなんか色々許容できない。
いやわかってるわかってる。そもそも今日びISAなんて意識しないじゃん？みんなJavaScriptしか書いてないじゃん？それかGCPやAWS Lambdaしか使ってないじゃん？どうしてもLinuxが使いたかったらARM版のVMMでARM版のLinux動かせばいいじゃない？
うんそうかもね。でも私は嫌だねそんなの。x86が使いたいよね。x86のLinuxカーネル動かしたいよね。本番環境でARM機なんて使ってるの？使ってないでしょ。
というわけでおそらくMacは開発機としては終わりだろうなと思うわけです。
よくよく考えてみると、今のWindowsにはWSL2なんかもあって、Mac OSに固執する理由などどこにもないかもしれない。が、Retinaが使えなくなるのは寂しい。あのきれいな画面でコーディングできなくなるのだ。この一点においてMacに後ろ髪をひかれる。
とはいえ富岳といいMacといいARMの隆盛は無視できない。ISA全然しらないし。VMMでも作ってみようかな？と思っている。
噂のGoogle製セキュリティスキャナtsunamiを使ってみた
Googleがセキュリティスキャナ作ったってんでニュースになってたので試してみる。
ソースはここ
nmapとncrackが必要とのことなので事前にインストールしないとかないといけない。
あと、スキャナのテスト用に脆弱性をわざと作ったアプリケーションがdockerイメージで配布されてるのでテストにはそれを使うといいようだ。そこらへんはQuick Startに書いてあるんで読んでその通りにやればいい。
なお、Javaで書かれてるようでJavaのインストールが必要。OpenJDKでいける。
今回私は自分が管理してるWebサイトに試してみた（一部IPがわからないようにログを改変してます）
実行してみるとだーーーっと以下のようなログが流れる。
情報: Executing the following command: '/usr/bin/ncrack -T3 --user ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,ec2-user,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant --pass summer,love,ashley,6969,nicole,chelsea,biteme,matthew,access,yankees,987654321,dallas,austin,thunder,taylor,matrix,,123456,password,12345678,qwerty,123456789,12345,1234,111111,1234567,dragon,123123,baseball,abc123,football,monkey,letmein,696969,shadow,master,666666,qwertyuiop,123321,mustang,1234567890,michael,654321,pussy,superman,1qaz2wsx,7777777,fuckyou,121212,000000,qazwsx,123qwe,killer,trustno1,jordan,jennifer,zxcvbnm,asdfgh,hunter,buster,soccer,harley,batman,andrew,tigger,sunshine,iloveyou,fuckme,2000,charlie,robert,thomas,hockey,ranger,daniel,starwars,klaster,112233,george,asshole,computer,michelle,jessica,pepper,1111,zxcvbn,555555,11111111,131313,freedom,777777,pass,fuck,maggie,159753,aaaaaa,ginger,princess,joshua,cheese --pairwise -f ssh://x.x.x.x:22 -oN /tmp/ncrack5895062353493684709.report'
6月 24, 2020 4:38:50 午前 com.google.tsunami.common.command.CommandExecutor execute
情報: Executing the following command: '/usr/bin/ncrack -T3 --user vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,vagrant,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser --pass amanda,summer,love,ashley,6969,nicole,chelsea,biteme,matthew,access,yankees,987654321,dallas,austin,thunder,taylor,matrix,,123456,password,12345678,qwerty,123456789,12345,1234,111111,1234567,dragon,123123,baseball,abc123,football,monkey,letmein,696969,shadow,master,666666,qwertyuiop,123321,mustang,1234567890,michael,654321,pussy,superman,1qaz2wsx,7777777,fuckyou,121212,000000,qazwsx,123qwe,killer,trustno1,jordan,jennifer,zxcvbnm,asdfgh,hunter,buster,soccer,harley,batman,andrew,tigger,sunshine,iloveyou,fuckme,2000,charlie,robert,thomas,hockey,ranger,daniel,starwars,klaster,112233,george,asshole,computer,michelle,jessica,pepper,1111,zxcvbn,555555,11111111,131313,freedom,777777,pass,fuck,maggie,159753,aaaaaa,ginger,princess,joshua --pairwise -f ssh://x.x.x.x:22 -oN /tmp/ncrack13461111013196007040.report'
6月 24, 2020 4:38:53 午前 com.google.tsunami.common.command.CommandExecutor execute
情報: Executing the following command: '/usr/bin/ncrack -T3 --user azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser,azureuser --pass cheese,amanda,summer,love,ashley,6969,nicole,chelsea,biteme,matthew,access,yankees,987654321,dallas,austin,thunder,taylor,matrix --pairwise -f ssh://x.x.x.x:22 -oN /tmp/ncrack3059916208301440638.report'
6月 24, 2020 4:38:56 午前 com.google.tsunami.plugins.detectors.credentials.ncrack.NcrackWeakCredentialDetector detect
情報: Ncrack weak credential detection finished in 1.163 min.
6月 24, 2020 4:38:56 午前 com.google.tsunami.workflow.DefaultScanningWorkflow generateScanResults
情報: Tsunami scanning workflow done. Generating scan results.
6月 24, 2020 4:38:56 午前 com.google.tsunami.workflow.DefaultScanningWorkflow lambda$runAsync$0
情報: Tsunami scanning workflow traces:
Port scanning phase (1.197 min) with 1 plugin(s):
/Tsunami Dev (tsunami-dev@google.com)/PORT_SCAN/NmapPortScanner/0.1
Service fingerprinting phase (183.7 ms) with 0 plugin(s):
Vuln detection phase (1.163 min) with 5 plugin(s):
/Tsunami Team (tsunami-dev@google.com)/VULN_DETECTION/NcrackWeakCredentialDetectorPlugin/0.1 was selected for the following services: ssh (TCP, port 22), http (TCP, port 80), http (TCP, port 443)
/Tsunami Team (tsunami-dev@google.com)/VULN_DETECTION/YarnExposedManagerApiDetector/0.1 was selected for the following services: ssh (TCP, port 22), http (TCP, port 80), http (TCP, port 443)
/Tsunami Team (tsunami-dev@google.com)/VULN_DETECTION/JenkinsExposedUiDetector/0.1 was selected for the following services: ssh (TCP, port 22), http (TCP, port 80), http (TCP, port 443)
/Tsunami Team (tsunami-dev@google.com)/VULN_DETECTION/JupyterExposedUiDetector/0.1 was selected for the following services: ssh (TCP, port 22), http (TCP, port 80), http (TCP, port 443)
/Tsunami Team (tsunami-dev@google.com)/VULN_DETECTION/WordPressInstallPageDetector/0.1 was selected for the following services: ssh (TCP, port 22), http (TCP, port 80), http (TCP, port 443)
# of detected vulnerability: 0.
6月 24, 2020 4:38:56 午前 com.google.tsunami.main.cli.TsunamiCli run
情報: Tsunami scan finished, saving results.
6月 24, 2020 4:38:56 午前 com.google.tsunami.common.io.archiving.RawFileArchiver archive
情報: Archiving data to file system with filename '/tmp/tsunami-output.json'.
6月 24, 2020 4:38:56 午前 com.google.tsunami.main.cli.TsunamiCli run
情報: TsunamiCli finished...
6月 24, 2020 4:38:56 午前 com.google.tsunami.main.cli.TsunamiCli main
情報: Full Tsunami scan took 2.409 min.
ええとこれさ。。。ひょっとしてnmapとncrackをテンプレコマンドで呼び出してるだけ？いや、だけとか言ったら失礼なのかな？そのテンプレに高度なノウハウが詰まっているんだよ！とか言われたらまあそうかなという気がしないでもないけど、でもなんかよく見るnmapやncrackの呼び出しに見える。
あとJava製なんですが、ただのテンプレコマンドをたれ流すだけならPythonとかで書けばいいんでは？なんでJavaで書くの？？？コンパイルすんのだるくない？そこら編の技術的なチョイスも謎い。
というわけで、G製ということで期待したんですが、、、なんかこう肩透かしを食らってアレな感じでした。
Lightsail上のVMにT-Potをインストールしたらネットワークが落ちる
スーパーハカーになりたいので、ハニーポットを運用してマルウェアを集めたいと思いました。ので、AWSのLightsail上でVMインスタンスを借りてT-potをインストール。
ちなみにハニーポットと言えばT-potというぐらい代表的なもののようです。脆弱性のあるサービスになりすますソフトウェアがDocker上で立ち上がって罠を仕掛ける感じ。KibanaでのキレイなWebIFもついてきてて、イケてます。かっこいい！気分はスーパーハカーですよ。
日本国内でもいくつか記事が見つかります。
ISOイメージからインストールする方法もありますが、私はDebianを入れた後、Post-Install手法でやりました。Lightsailだとそうせざるを得ない。
で、T-potインストール自体はすんなり行ったんですが、問題発生。VMを起動して1時間後ぐらいにネットワークが急に落ちます。
LightsailはWebIFからのVMアクセスをSSH経由に限定しているので、こうなってしまうと何もできなくなります。せめて、シリアル経由かレガシーVGA経由でのコンソソールアクセスを用意してほしいもの。。。これだと、例えばiptablesで自分の乗ってる枝を切ってしまったら何もできなくなり、OS再インストールしか手はない。怖い。なんとかしてくれんもんかな。
話がそれましたが、AWS LightsailのWebコンソールから「再起動」かけると再びVMは立ち上がってネットワークも通じるようになってT-potも動き始めます。が、また一時間ぐらい立つとネットワークが落ちます。これでは安定してT-potを起動し続けることができずにまずい。
VMがkernel oopsとかでOSごと落ちているのではなく、単にネットワークインターフェイスが落ちてるだけのように見えるので、ip a listの出力をディスクに書き出すという以下のようなスクリプトをくんでログをとって見てみました。
#!/bin/sh LOG_FILE_NAME=ip.log while :; do /bin/echo -e "====$(date +'%Y/%m/%d:%H:%M:%S')==== \n $(ip a list)" >> ${LOG_FILE_NAME} sleep 10 done
すると、たしかにネットワークIFからIPが消えている。
====2020/06/26:00:22:07====
1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue state UNKNOWN group default qlen 1000
link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00
inet 127.0.0.1/8 scope host lo
valid_lft forever preferred_lft forever
2: eth0: <BROADCAST,MULTICAST,PROMISC,UP,LOWER_UP> mtu 1500 qdisc mq state UP group default qlen 1000
link/ether 06:d0:84:8b:f5:18 brd ff:ff:ff:ff:ff:ff
inet 172.26.3.244/20 brd 172.26.15.255 scope global dynamic eth0
valid_lft 6sec preferred_lft 6sec
====2020/06/26:00:22:17====
1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue state UNKNOWN group default qlen 1000
link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00
inet 127.0.0.1/8 scope host lo
valid_lft forever preferred_lft forever
2: eth0: <BROADCAST,MULTICAST,PROMISC,UP,LOWER_UP> mtu 1500 qdisc mq state UP group default qlen 1000
link/ether 06:d0:84:8b:f5:18 brd ff:ff:ff:ff:ff:ff
というか、単純にvalid_lft 6secと出たあとにIPが消えてるので、DHCPのリース期間が過ぎてそのままIPが消えてるだけのように見えます。
ちなみにLightsailはNATがあって、NAT外側のパブリックIPは固定IPにできますが、NAT内部のプライベートIPはDHCPで動的取得のみのようです。だから、Lightsail VMで外部サービスを起動したい場合、AWS LightsailのWebコンソールからNATのポート開放をしてあげないと外からはつなぎにいけません。
しかしこれ、謎い。なぜリース期間が消えてるのにDHCP再取得しにいかないのか。。。
T-potをインストールしていない他のLightsail VMではこのようなことは当然おこらないので、T-potがなにか設定をいじったのだと思いますが。。。謎い。。。
iptablesの設定でDHCPのパケットが弾かれてるのかな？と思ったので
# dhclient -r -v eth0 && rm /var/lib/dhcp/dhclient.* ; dhclient -v eth0
とやってみたけど、ログを観る限り
$ journalctl -f | grep -Ei 'dhcp' Jun 30 22:48:17 rapidassistance dhclient[19179]: Internet Systems Consortium DHCP Client 4.4.1 Jun 30 22:48:17 rapidassistance dhclient[19179]: For info, please visit https://www.isc.org/software/dhcp/ Jun 30 22:48:17 rapidassistance dhclient[19179]: DHCPRELEASE of 172.26.3.244 on eth0 to 172.26.0.1 port 67 Jun 30 22:48:17 rapidassistance dhclient[19188]: Internet Systems Consortium DHCP Client 4.4.1 Jun 30 22:48:17 rapidassistance dhclient[19188]: For info, please visit https://www.isc.org/software/dhcp/ Jun 30 22:48:17 rapidassistance dhclient[19188]: DHCPDISCOVER on eth0 to 255.255.255.255 port 67 interval 4 Jun 30 22:48:17 rapidassistance dhclient[19188]: DHCPOFFER of 172.26.3.244 from 172.26.0.1 Jun 30 22:48:17 rapidassistance dhclient[19188]: DHCPREQUEST for 172.26.3.244 on eth0 to 255.255.255.255 port 67 Jun 30 22:48:17 rapidassistance dhclient[19188]: DHCPACK of 172.26.3.244 from 172.26.0.1
と、DHCP DISCOVER->DHCP OFFER->DHCP REQUEST->DHCP ACKとDHCP取得がちゃんとできてるので、パケットが弾かれているとは考えにくい。うーん謎い。。。
Let's Encryptの証明書失効から学ぶループと末尾再帰の関係
この間、Let's Encryptがバグで300万近くの証明書を失効させたというニュース流れました。
事の詳しい顛末は以下のBlogにかかれています。かなり詳しく書かれており、どのようなコードでバグが出たのか？というところまで解説されています。
さて、ちょっと話が飛ぶようなのですが、このBlogを読んで「ループと末尾再帰は本当に同等なのか？」という前々から私の頭の片隅にあった疑問がまたむくむくと頭を持ち上げてきましたので書き散らしました。
「ループと末尾再帰は同等である」というのはなんか関数型言語をかじった人の口からよく聞くような気がするのですが、私はそれに対して「そんな簡単に言ってしまっていいのか？」とずっと疑問を抱いていました。今回それを言語化しておこうと思います。
えっ？Let's Encryptの証明書失効と「ループと末尾再帰」になんの関係があるのかって？まぁちょっと話を聞いてください。
詳しくは上述したBlogを読んでほしいのですが、Go言語では以下のようなコードを書くと
func main() { var out []*int for i := 0; i < 3; i++ { out = append(out, &i) } fmt.Println("Values:", *out[0], *out[1], *out[2]) fmt.Println("Addresses:", out[0], out[1], out[2]) }
$ ./test_gomistake Values: 3 3 3 Addresses: 0xc0000160a0 0xc0000160a0 0xc0000160a0
このような結果になるそうです。要はoutに一時変数iの参照を入れてしまい、すると、ループが抜けたあとはiの値はfor文が進むにつれて変化しており最終的には3になります。結果、for文を抜けたあとoutの中身が全部3なってしまうという仕様です。
このgoの仕様をうっかりミスで忘れてしまい、outのなかは0, 1, 2になるという仮定してコードを書いてしまいバグを作り込んでしまったそうです。その結果が300万近くの証明書失効につながったと。恐ろしい。。。
これを受けて、Gauche開発者のShiro Kawaiさんがこんな事をつぶやいておられました
あああ、SchemerがCommon Lispでよくやるミスだ。参照取っちゃう以外にクロージャに閉じ込んじゃうのもありがち。やはりループ変数を破壊的変更するのは人類の手に余るのではhttps://t.co/k6AdNy068V
— Shiro Kawai (@anohana) 2020年3月9日
Shiroさんは「クロージャに閉じ込んじゃうのもありがち。」といってますが、そう。それですよ、私が言いたかったのは。ちょっとCommon Lispで以下のようなコードを書いてみましょうか。
CL-USER 1 > (do ((i 0 (+ i 1)) (j '() (cons #'(lambda () i) j))) ((>= i 3) j)) (#<anonymous interpreted function 21CE99DA> #<anonymous interpreted function 21CCEA4A> #<anonymous interpreted function 20107912>)
このプログラムがやっていることはdoループ構文でiの値を0から3まで回して、lambdaでiの値を返すクロージャを作りそのクロージャのリストを返すプログラムです。つまり、このループが返すのは作ったクロージャへのポインタのリストです。
返ってきたのはクロージャのリストなので、リストの中にあるクロージャを改めて評価してみます。
CL-USER 2 > (mapcar #'funcall *) (3 3 3)
どうでしょう？golangと似たような事が起こりました。もう分かると思いますが、要は、doループ内部のlambdaで束縛したiは、doループ外に出るときにはすでに3になってますので、doループから出たあとにlambdaを評価すると全部3になるんですね。
ちなみに、私はLispWorksを使いましたが、ANSI Common Lispの仕様としてこうなってるはずですので、どの処理系でも同じ結果が得られるはずです。
一方で、次のコードを考えてみましょう。
CL-USER 1 >(defun test () (labels ((rec (acc i) (if (>= i 3) acc (rec (cons #'(lambda () i) acc) (incf i))))) (rec '() 0))) TEST CL-USER 2 > (test) (#<anonymous interpreted function 21ACAE52> #<anonymous interpreted function 21ACAE3A> #<anonymous interpreted function 21ACAE22>) CL-USER 3 > (mapcar #'funcall *) (3 2 1)
こちらは先ほどと同じようにiで3回ループを回してそのiを束縛したlambdaを作りconsでリストに放り込んでいます。傍目には先のdo構文で上げた例と似た結果が得られているように見えます。
しかし、今回はdoループではなく、末尾再帰を使ったコードになっているのがわかるかと思います。
結果を見てましょう。3, 2, 1と異なる結果が得られました。つまり、末尾再帰とループとではiの束縛内容が異なると言えます。
ループの場合がある意味でdynamic binding的な挙動を示すのに対して、末尾再帰を用いた場合、iはlexical closureとして明確にiが閉じ込められていることがわかります。ですので、ループの場合は3, 3, 3となりますが、末尾再帰の場合は3, 2, 1となります（2, 1, 0とならないのはincfを使って破壊的に変更してるからです。やはり怖い破壊的変更）
僕が言いたかったのはこういうことです。ループと末尾再帰は「同じだ」と言われることがある気がするのですが、その実、束縛される変数。つまり環境のことを考えると同じと言えないのではないのでしょうか？また変数がどのように束縛されるかといった多分に言語仕様に依存してくる話だと思うのでそんな乱暴な話でまとめちゃっていいのかなぁと思います。関数型言語を標榜しているがloopもサポートする言語はたくさんあると思うので。
とういわけで、ループと末尾再帰が同じという言を聞くと本当かなぁ？と首を傾げてしまいます。ここらへん理論的にはどうなってんでしょうね？
p.s. いやShiroさんの件のツイートをみてつい懐かしいような気がして書きなぐってしまいした。
TLC Model CheckerをCUI（コマンドライン）で使う
TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。
そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思うんですよね。実はTLA+にはTLA ToolboxというIDEがあって、GUIからマウスポチポチで呼び出して検証することもできるのですが、仕様検証という作業は（仕様規模によりますが）すごいCPUパワーとストレージを食います。
そのため、実務的な観点で言えば、DCとかにおいてある高性能なコンピュータにSSHで入って操作することになると思うのですが、この場合GUIは邪魔になります。
この間公開したスライドでもTLC Model CheckerをCUIで使っています。でもCUIのTLC Model Checkerをどうやってインストールするのかを解説してませんでしたのでここで書いておきます。
このtla-binというツールを使えば簡単にオフィシャルのTLA+環境一式をCUI化してインストールできます。
マニュアルにも書いてありますが、こんな感じでやればインストールできます。インストール先はデフォルトだと /usr/local になりますが、第一引数に与えればインストール先は変えられます。
$ git clone https://github.com/pmer/tla-bin.git $ ./download_or_update_tla.sh $ sudo ./install.sh
やってることは、オフィシャルページのTLA+ Toolboxをダウンロードしてjarを解凍してjavaのclassファイルを取り出し、適切なオプションを付けてJVMで実行しているみたいです。
なお、TLA+のツール一式はJavaで書かれていますのでJavaのインストールも必要です。OpenJDKでは動きません。Oracle JVMじゃないとだめですね。
[xxx@host:~/xxx/tla+/raft]$ tlc -config SPEC.cfg ./first.tla
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first search Model-Checking with fp 82 and seed 1539151492344761609 with 1 worker on 24 cores with 21424MB heap and 64MB offheap memory (Linux 3.10.0-862.9.1.el7.x86_64 amd64, Oracle Corporation 1.8.0_181 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/xxx/xxx/tla+/raft/first.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/TLC.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module first
Starting... (2020-02-13 11:51:47)
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NullPointerException
java.lang.NullPointerException
at tlc2.tool.impl.SpecProcessor.processSpec(SpecProcessor.java:346)
at tlc2.tool.impl.SpecProcessor.<init>(SpecProcessor.java:157)
at tlc2.tool.impl.Spec.<init>(Spec.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:126)
at tlc2.tool.impl.Tool.<init>(Tool.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:116)
at tlc2.TLC.process(TLC.java:930)
at tlc2.TLC.main(TLC.java:247)
Finished in 00s at (2020-02-13 11:51:47)
TLA+の社内勉強会スライド公開します
Raftを使ってDFSを作るという仕事を数年前ぐらいから続けています。そのためか最近、形式仕様記述（特にTLA+）とかModel checkingとかTheorem provingとかが私の中でアツいです。TLA+とかAlloyとかVDM++とかSpin周りのやつです。
ソフトウェアの仕様を形式仕様で厳密に書き下して検証、証明するという手法がある！ということ自体は院生時代に見聞きして知ってたんですが「難しそう」とか「一部のすごい人にしか使えなさそう」といった先入観があってなんとなく敬遠してました。正直、当時は自分の身近な問題であると感じられていませんでした。
あれから10年以上たって最近形式仕様記述とかModel checkingとかTheorem provingというものは「必須なものである」という認識がようやく私の中にも芽生えたようです。仕事で分散システムの開発を通じて「これは人間の頭（複数人の設計レビューとかコードレビューとかテスト）だけではデバッグ不可能なのだ！」というのが骨身にしみてわかったからだと思います。
10年前とはちがって、Amazonでの大規模な形式仕様記述（TLA+）とModel checkingの導入による成功例なども表立って論文の形としてまとまってたりしてて、もうこれはやるっきゃ無いだろという感じです。
今はAWSとかでちょっと気の利いたサービスつくると、もうそれは分散システムになっちゃうんですよね。ここ10年間だけを切り取ってみても、ソフトウェアエンジニアが作るシステムの複雑さが格段に上がっているように見えます。
そんな中で形式仕様記述とかModel checkingとかは今後ソフトウェアエンジニアにとって必須のスキルになっていくんじゃないかなと思っています。ので、みなさんもぜひ見てみてください。
このスライドでTLA+のさわりと、TLC Model Checkerでの仕様バグの検証のやり方とか。一通りわかると思います。
あ、間違ってたらこっそり教えて下さい！
プログラムの正しさを数学的に証明する形式検証への招待
Twitter眺めてたら面白そうなセミナーがあったので申し込んだ。
私はオブジェクトストレージではないPOSIX IFな分散ファイルシステムを作るという面白い仕事をもう数年間ぐらい続けている。
その関係で最近TLA+とTLC Model Checkerを業務で使っている。私が「導入すべき」と宣言して先陣を切った感じ。そのため、形式仕様記述言語やTheorem ProvingやModel checkerへの興味がぐんと増している。せっかくなのでいろいろ教えてもらおう。
定理証明支援系はCoqというものがあるということぐらいしか知らないし、そもそもCoqが何を手伝ってくれるのかすらよく理解してないのでいい機会だと思う。
このセミナーではIsabelleというものを使うそうだが。これは初耳。楽しみ。
