Coqに入門した感想
最近、定理証明支援のCoqを入門している。というのは、以前の職場にいたときの職場でもCoqをやっている先輩がいて、今回の職場でも定理証明支援系を使っている同僚がいて、しかも最近自分はプログラミング言語実装をやっているためか、Coqや依存型について聞かれることがあるので、一念発起して取り組み始めた。
しかし、案の定、何から始めたらいいのかわからず入門に躓いてしまい、かなり難しいと感じた。しかも一番最初に読み始めた本が、Certified Programming with Dependent Typeという初心者向けではない本だったため、事態は混迷を極めていた。
そんな難関を乗り越えて2ヶ月、ようやく基本的な証明をできるまでたどり着いたので、メモ代わりにどう入門すればよいか残しておこうと思う。
1. 関数型のプログラミング言語を学ぶ
自分は関数型プログラミング言語の処理系を設計・実装したことがあり、型システム、型推論、λ計算についてはある程度知っていたため、Coqで用いる型や式については初見でもなんとなくわかったが、関数型言語について知らない人は厳しいのでまずOCamlかHaskellをやったほうが良いと思う。
例えば、CoqではFixpointという宣言で再帰関数を定義するのだが、これはαコンビネータなどの不動点コンビネータについて知識があると納得するはずである。しかし、これらをしらないと、何なのかさっぱりわからなくなるのではと思う。
2. 形式的証明について学ぶ
この形式的証明も自分はある程度やったことがあるためそれほど困らなかったのだが、そもそも形式的証明について知らない場合、なんのこっちゃわからないと思う。形式的証明については、以下の本がおすすめだと思う。
あたりまえだが、Coqは証明していくためにあるので、そもそも証明とは何かをわかっていないとやっていくのはきつい。
3. Emacsを学ぶ（おまけ）
これはおまけだが、CoqはEmacs上でProof Generalというソフトウェアを動かして使うのが使いやすいように思った。自分はターミナルの中でEmacsを起動して使っている。Coq IDEもあるが、Emacsでバシバシ書けるのは快適なので、Emacsを使ったほうが良いと思う。
4. 適切な入門書を選ぶ
自分が躓いたのはここだった。
入門で利用すべきは、Software FoundationsのVolume 1だったのだ。これは大変わかりやすく、これを読めばだいたい分かるので、まずこれを読んだほうが良い。日本語だと、ソフトウェアの基礎に少し古いバージョンのがあるので、こちらを読めば良いと思う。このどちらかで一通り証明を体験した後、Certified Programming with Dependent Typeを読めば、かなり納得して読めるようになる。間違っても、いきなりこれを読んではいけない。
最近はSSReflect/Mathcompを使うこともあるそうだが、おそらく入門はSoftware Foundationsの方がCoqの基礎がわかって良いと思った。Coqを解説した日本語記事もWebには散見されるが、だいたいわかりにくいので、ソフトウェアの基礎あたりを読んで、演習問題を解いていくのがいいのではないかと思う。
証明の仕方はわかりつつあるので、今後は実際のRunning Codeに活かしていきたい。いまはRust言語でOSを実装しているので、それに対して証明を与えられないかと思っている。それでは皆さん、良いハッキングライフを。
自粛期間について
コロナウィルスはコロナ禍とも形容されるように、世界中で多くの死者を出してしまい、大変痛ましい結果になっている。日本は比較的に清潔意識が高く欧米程ひどいことにはなっていないようなので、不幸中の幸いではあるだろう。
自粛期間もあり外に出られない状態が続いていたが、自分的には大変良かった。自粛となった結果いろいろな出張、飲み会がキャンセルとなり、時間ができたので自前のオペレーティングシステムとプログラミング言語処理系実装が出来上がった。充実した自粛期間である。やはり研究が進むのは会議や飲み会ではなくて時間があることであると強く感じた。
しかし、新たに1年生となった人々は大変だと思う。友人や同僚もいない中で、社会から孤立してしまったように感じたのではないだろうか。これに対する妙案があればいいのだが、そうそう最高な案などでるはずもなく、オンラインミーティングを行ってお茶を濁すしかないのが現状である。今後VRが劇的に進化するか、あるいは脳に電極を差し込めるようになるといった技術革新がないと難しいかもしれない。
大学に限って言うと、普段世間では、大学はもう必要ない、大学の講義など役に立たないなどと言われてはいるものの、いざ講義の延期などになると、大学で講義を受けれないのはなんとかしろと論調がでてきてどっちやねんとも思ったりする。なんだかんだいって大学に期待しているのだろうか。ツンデレか？
自分自身、大学で何か勉強になったことはあまりないように思い、ほぼ独学で勉強していたので、大学の必要性に疑問を持ったこともあった。しかし、実際に大学で教えてみると、興味はあるけれど何から手を付けて良いのかわからない人が存外に多く、やっぱり大学って必要なんだなと思い直した。
そういえば以前読んだ本でも、物事を教えるのではなく導くのが重要であると書いてあったので、そのとおりなんだろう。特に初学者だと何が分からないかが分からないとなりがちなので、そこを導けるだけでもだいぶ違ってくるように感じる。例を挙げると、当初はUnixカーネルって何、レジスタって何と言っていた学生も、今ではLinuxカーネルをコンパイルして、Qemu上でinitrdからhello worldしているし、成長するもんだなあと感心している。
というわけで、そういうマンツーマンに近い指導は、コロナウィルスの自粛でやりにくくなったなと思う。大学の講義はオンラインでも良い気もするが、重要な個人指導をどうするかだと感じる。どうしようかなあ。
ただ、そろそろ大学への登校も緩和されつつあるので、第n波が来ない限りは大丈夫そうではあるけれど。
Finaly Fantasy 7 リメイクをクリアしたぞ
Finaly Fantasy 7リメイク（FF7R）をクリアした。プレイ時間は45時間程度で、想定の範囲内でクリアできた。ドラクエ11は100時間程度もかかったのに比べると、標準的なプレイ時間内におさまったと思う。
自分がFFシリーズをプレイしたのは小学校の時だと思う。たしか、FF3な気がする。FFシリーズには当時から弱点という概念があり、的に適切な攻撃を当てないと戦闘が苦戦するようになっていた。例えば、FF3では、ハイン戦では学者のみやぶるを、ガルーダ戦では竜騎士のジャンプを、暗黒の洞窟では魔剣士を使っていかないと、なかなか苦戦するようになっている。
FF7Rは往年のFFシリーズのように、ちゃんと敵の弱点をついていかないと苦戦するような難易度になっている。序盤こそ、懐かしいなと思いながらプレイしていたものの、だんだん敵が強くなっていきだんだん本気になってくる。はじめはマテリアも適当に装備していたのだが、はんいかヘイストや、はんいかバリアを使いだし段々ガチになっていった。FF7当時もぜんたいかヘイストには大変お世話になったものだ。
人生の起点となるFF7
元祖FF7は初代Play Station (PS)で登場し、FF7がでるというのでNintendo 64でもセガサターンでもなくPSを選択したような気もする。PSで初めて購入したソフトウェアは闘神伝だったような覚えがある。いや、リッジレーサーかもしれない。とにかくPSのゲームはすごくて、FF7のグラフィックには衝撃を受けた。PSのゲームをみて、これから情報産業が来るぞと確信し、3DCGやC++の勉強をひたすらにしていた。どれぐらいハマったかというと、当時専攻していた電気工学科の必修科目である電気回路や電子回路がさっぱりわからなくなってしまったために留年してしまうぐらいである。そのかわりに、C++でインバースキネマティクスやメタボールを実装できるまでになっていた。いや、留年したのはバーチャロンにハマったからかもしれないが。
当時は、ゲームにもハマっていたが、プログラミングにもハマっていた。プログラミングというのはすごくて、マニュアルを読んでロジックを考えると、そのとおりに物が動くのである。こいつは面白いとのめり込んでいると、あれよあれよと、情報科学の修士、博士までとり、今は大学で情報科学を教えている。実際には現在へ至るには四苦八苦したのだが、今にして思うとあれよあれよである。FF7は、そんな人生の起点となったゲームでもあるので、感慨深いものがある。
エオルゼアから出張シヴァ
FFは人生でかなり長時間お世話になっているゲームである。FF14などはリアル友人たちとよくプレイしていて、極蛮神などもクリアしていた。極タイタンは最高に面白くて、8人協力プレイなのにちょっと失敗してステージ外へ落下してしまうと、落下しした自キャラの死体を眺めつつ、残った仲間のプレイ音声だけ聞かされるという恥辱を味わわされる。あまりにも悔しくて必死に練習したものだ。自分はFF14は紅蓮でやめてしまったのだが、またいつかエオルゼアに行きたいなあ。ストーリーも溜まっているだろうし。
ちなみに、FF7Rの召喚マテリアは召喚獣を倒したあとに手に入るのだが、FF7Rのシヴァ戦がまんまFF14で、一瞬起動するゲームを間違えたかと思うぐらいで笑ってしまった。しかも、FF14のシヴァと同じ、ヘヴンリーストライクやアイシクルインパクトを使ってくるしで、完全に蒼天のイシュガルドです。ありがとうございました。
色々と言いたいことは沢山ありますが、とにかくFF7Rのティファは最高でした。特に懸垂と雲梯は最高でしたね。それでは皆さん、よいゲームライフを。
Rustでベアメタルプログラミングをやってみた（その2）
前回はQEMUでビデオメモリへの描画まではできたが、実機で描画はできていなかった。その後色々と試行錯誤した結果、実機でもマンデルブロ集合を描画することに成功した。現状、Raspberry Pi 4でのベアメタルプログラミングの記事が多くないため、思い返すと大変つまらないことで難儀していた（というか、そもそもベアメタルプログラミングの記事が少ない）。
実機での描画からEL3での起動までの道
7日目（2月24日）
実機で試してみたところ、どうにも動かないので、一旦ペリフェラルのコードをRustではなく、C言語に置き換えた。Rustの吐き出すアセンブリコードを眺めていたところ、アラインメントあたりが怪しい気がした。
8日目（2月25日）
いろいろ調べた結果、Rustでコンパイルする際に指定するターゲットアーキテクチャが間違っていたようなので、ターゲットを変えて試してみたところ無事に実機でも動いた。
9日目（2月26日）
シリアルコンソールにボードのバージョンなどいろいろな情報を出すようにしていた。
10日目（2月28日）
仮想メモリを実装しようとMMUに手を入れようとしたが、先に例外ハンドラを実装。その後、EL3で自作カーネルを動かそうとしたがうまく動かず、色々とドキュメントを見て調べていた。
11日目（2月29日）
EL3で動かすためにはファームウェアを書き換えないといけないっぽいので、ファームウェアのコードを自分のコードにポーティング。その結果EL3で起動させることに成功。
というわけで、色々と試行錯誤した結果、基本的なコードは実機でも動くようになった。一時はRustで動かないために焦ったが、無事に動いてなによりである。それでは皆さん、良いハッキングライフを。ソワカ。
Rustでベアメタルプログラミングをやってみた
ベアメタルプログラミングとはOSなどを利用せずに、直接ハードウェア上にプログラムを走らせるプログラミング手法である。要するにOSなどを自分で作る練習にもってこいなのである。また、Rust言語は型安全なプログラミングであるにも関わらず、メモリへの直接アクセスなどを行えるため、このベアメタルプログラミングが可能な言語である。
というわけで、今回はRustでベアメタルプログラミングをやってみたので感想を述べたい。とはいっても、現状はQEMUで動かしているだけので、いずれ実機でも試してみたいところである。ちなみに、Rustもベアメタルプログラミングも今回はじめてである。
今回行ったことは、1つのCPUコアのみ動作させて、UART0からシリアルでHello Worldを出したあと、グラフィック描画のフレームバッファを取得してマンデルブロ集合を描画するという、比較的単純なものである。他の仕事もやりつつ、実質6日程度でグラフィック描画までできたので、ちょっと試して見るだけならハードルはそれほど高くないと思う。今ならWeb上に色々と資料もあるし、お手本となるC言語の実装もあるため簡単である。
ちなみに、実機でやっていない理由は、QEMUで利用可能なターゲットはRaspberry Pi 3であり、実際に手元にあるのはRaspberry Pi 4と少しハードウェアが違うためである。しかも、Raspberry Pi 4でのベアメタルプログラミング関連資料が少ないため、まだ、若干ハードルが高いように思う。
グラフィック描画までの道
1日目（2月14日）
1日めはコンパイルのためのDocker環境を整えて、手元のマシンでQEMUを動かして試せるようにした。RustのコンパイルはDockerコンテナ内で行い、QEMUの起動はホストOS（Mac）で動かすようにした。
2日目（2月15日）
2日目はRustのマングリングと出力バイナリの調査を行った。これはアセンブリでRustの関数を呼んだり、Rustからアセンブリコードを読むのに必須なので、objdump等で色々調べていた。
3日目（2月16日）
3日目はお手本のC言語ソースコードをRustにポーティングして、UART1のシリアルからHello World!を出力するようにした。
その後、しばらく仕事が忙しくて手を付けられず。
4日目（2月21日）
4日目はMailbox関連のコードをRustにポーティングした。MailboxとはCPUとGPU間のインターフェースのことである。
5日目（2月22日）
Mailboxのコードを更に修正し、UART1ではなく、UART0からシリアルでHello World!を出力できるようにした。Mailboxの仕様がいまいちわからなかったため、ドキュメントを主に読んでいた。
6日目（2月23日）
グラフィック周りの仕様がわかったため、マンデルブロ集合を描画してみた。
感想
やり始める前は、いくらメモリアクセスが簡単にできると言っても、少し難しいのではないかと思っていたが、思いの外簡単であった。また、1日のすべてをプログラミングに費やしていたわけではないので、時間のある学生時代なら2〜3日ぐらいでできたのではないかと思う。
Rustももう少しハマるかと思ったが、こちらも特に問題はなかった。以前、線形型システムとリージョンベースのメモリ管理手法を勉強していたので、構文を調べるだけで実装はできたように思う。いざとなればインラインアセンブラもかけるので、どうにでもなる。正直、Haskellより簡単だと思う。
ただ、やはりメモリアクセスのところはunsafeの嵐になるので、Rustといえども注意してプログラミングしなければならない。しかし、unsafeから抜け出すと型システムの庇護下にあるため大変安心である。
というわけで、これからは低まった人たちにも心置きなくRustを勧めていこうと思う。
あとは仮想メモリや、スケジューラあたりを書けばOSモドキなのも作れるだろう。いまのところOSを実装する予定はないが。
続き↓
長門の存在証明
何かが存在するかどうかということを突き詰めて考えていくと、何も存在しないような結論に思い至ってしまう。例えば、いまこれを読んでいるあなたは、実は脳みそが取り出されてビーカーに保存されている状態にあり、その脳みそに刺された電極から刺激を受け取ってあたかもこの世界が存在しているように感じているだけかもしれない。古にはかのデカルトも同じようなことを考え、その結果、我思うゆえに我ありという有名な台詞を残した。
デカルトは次のように考えた。私が考えるということは、バーチャルかどうかはわからないがとにかく存在するということである。私は考えないようにしようとすればするほど、考えるということについて考えてしまう。よって私は考えるということであり、つまり、私は存在する。
俺の嫁問題
このように、存在するかどうかを突き詰めて考えていくとなかなか難しい問題にぶち当たる。例えば、長門は俺の嫁（若干古いか）などと、存在しないはずのキャラクターに対してあたかも存在するように愛着を抱くことさえある。たしかに長門有希は情報統合思念体であるため、我々の知らぬ間に至るところに偏在しているのかもしれない。しかし、それはあくまでも長門が存在するということを否定できないだけであり、その存在を証明するわけではない。
ところで二次キャラ以外にも、実際に存在はしていないフィクションでバーチャルな存在はある。それは長門らと同じように完全にバーチャルな存在のはずだが、世の中の誰もがその存在を信じている。それは何かというと、1つは国でもう1つはお金である。
国は別に物理的法則によって存在しているわけではなく、人間が恣意的に想像したバーチャルの存在である。しかしあたかも人々は国というものが存在するかのようにふるまい、あまつさえ国が原因で殺し合いまでしてしまう。お金も同じで高々紙切れ、電子データになにか価値があるかのように皆が振る舞っている。
国、お金、これらは完全にバーチャルな存在であるのに、あたかも実在するかのように皆が考えているため、これはもう実在すると言ってよいのではないだろうか。とすると、同じ理屈で長門も存在すると言ってよいのではないだろうか。いや、これはもう存在する。間違いない。
フィクションのお断り
いやしかし、流石に長門が実在するとはちょっと受け入れがたい。長門も国もお金もやはり仮想的な存在ではないだろうか。
ところで、作り話に対するよくある断りとして、「この作品はフィクションであり実在の団体及び人物とは一切関係がありません」という文章があるが、実在の人物というのはわかるが、実在の団体とは一体何を意味しているのだろうか。団体とは国と同じで極めて恣意的でバーチャルな存在なので実在の団体という文言はおかしいのではないか。
ということはやはり、国やお金は存在すると考えるしかないだろう。当然長門も存在する。でもちょっと待てよ、とすると作中の団体、例えばSOS団も実在するということにはならないだろうか。そう考えると、「実在の団体とは関係ありません」が何を言わんとしているのかますますわからなくなってしまう。SOS団は実在するし関係あるだろ。
実在とは一体…ウゴゴゴ…
というような感想を以下の本を読んで抱いた。
2019年総括
2019年はずっと講義と演習の準備を行っていたように思う。それでも、合間に1、2ヶ月程度は時間があったため言語処理系の実装もすすめていたが、やはりそれほど進まなかった。講義準備以外にも雑用がジャカジャカふってくるため、きついもんがある。さらに、正直、有意義とは言えないような出張も多くあるためになかなか厳しい。しかし、これはもうしょうがないだろう。
2019年の研究成果
2019年の研究成果だが、結果的に、ジャーナル1本、国際会議論文1本、国内研究会4本となった。
ジャーナル
- Yuuki Takano, Ryosuke Miura, Shingo Yasuda, Kunio Akashi, and Tomoya Inoue, "Design and Implementation of a Scalable and Flexible Traffic Analysis Platform", 日本ソフトウェア科学会学会誌『コンピュータソフトウェア』, Vol.36, No.3 (2019), pp.85-103, 2019/8
国際会議
- Nobuyuki Kanaya, Yu Tsuda, Yuuki Takano, Daisuke Inoue, "Byakko: Automatic Whitelist Generation based on Occurrence Distribution of Features of Network Traffic", IEEE Workshop CyberHunt 2019, 2019/12
国内研究会
- 宮地 充子、高野 祐輝、河内 亮周、中正 和久、"プライバシーを保護した多機関データ突合システムについて", 第39回医療情報学連合大会、2019年11月
- 金谷 延幸、津田 侑、高野 祐輝、井上 大介、"サイバー攻撃観測における対象ネットワーク特化型ホワイトリスト作成手法の提案"、情報処理学会 コンピュータセキュリティシンポジウム 2019 (CSS 2019) 論文集、2019年10月
- 竹中 幹、高野 祐輝、宮地 充子、"Deceptionネットワークを構成するフレームワークの提案"、Computer Security Group (CSEC2019-03), IPSJ SIG Tech. Rep, Vol. 2019-DPS-178(5),1-7, 2019年2月
- 金谷 延幸、津田 侑、高野 祐輝、井上 大介、"サイバー攻撃観測のモデル化とデータ生成・変換手法"、暗号と情報セキュリティシンポジウム 2019 (SCIS 2019)、2019年1月
ジャーナル論文は、2015年にUSENIX LISA 2015で発表した内容の発展版で、論文の内容的には2017年にはほぼ出来ていたのだが、なかなか時間がかかってしまったと思う。ジャーナルは良いとして、今年一番の成果は、国際会議論文のByakkoだろう。ようやく英語の査読付き論文として投稿できたため感慨深いものがある。
学生と一緒にやっていた論文はまだ1本しかないが、今月はSCIS 2020へ2本投稿することができたため、これから徐々に増えていくだろうと思う。SCIS 2020へ投稿した論文は以下の通り。
- 西口 朋哉、高野 祐輝、宮地 充子、"セッション型を用いたアクセスコントロール機構の設計と実装"、SCIS 2020
- 竹中 幹、高野 祐輝、宮地 充子、"XDPを用いたネットワーク型欺瞞的防御システムの設計と実装"、SCIS 2020
まだまだPreliminary Studyな感じはあるが、ようやく足元が固まりつつあるため、今後クオリティを上げて国際会議論文やジャーナル論文にしていきたいところである。
2019年の講義
2019年は、離散数学と計算の理論、実践情報セキュリティとアルゴリズム、の講義を2つと、高度サイバーセキュリティPBLのIとIIを行った。分野的には、数理論理学、λ計算、型システム、形式手法、ネットワークセキュリティ、ファイアウォール、デバッガ・動的解析、正規表現、アセンブリ・コード生成という感じで、分野が広すぎてなかなか大変だった。自分の専門である、コンピュータネットワーク、分散システム、コンパイラあたりならもう少し余裕を持ってできると思うのだが、なかなかそうは行かないもんである。
来年はさらに上に加えて、線形型システムとリージョンベースのメモリ管理手法を行い、Rust言語を支える技術について講義を行おうと思う。自分に出来るかは心配であるが、既存のコードを、RustやHaskellといった安全なプログラミング言語に置き換えていくのはソフトウェア業界の課題であるため、なんとかやり遂げたい。
2020年の抱負
2020年は、研究予算をとり、将来的には幅広な合宿に学生を連れていけるようになると良いと思っている。他大学の優秀な学生と交流できる機会があるのは、それなりに意義のあるものだと思うので。
また、本も書きたいし、言語処理系実装もすすめたいし、論文も書きたいし、とやりたいことが多すぎるが、これらは時間を見つけて少しずつすすめるしかない。もう少し時間があれば研究成果も増やせると思うのだが、悩ましいところである。
鬼が笑うので、抱負はこの辺にしておこう。それでは皆さん良いお年を。
