【読書メモ】哲学とは何か、ゴルギアス・テーゼ
いま、「哲学とは何か」という本を読んでいるのだが、この前半部分に出てくるゴルギアス・テーゼについて理解が難しかったので、自分なりの解釈をメモしておこうと思う。実は、「哲学とは何か」はまだ前半部分しか読んでいないが、ゴルギアス・テーゼを理解しないことには先に進めなそうなので、少し考察してみる。
ゴルギアス・テーゼ
ゴルギアス・テーゼとは以下の3つが成り立つという主張のことである。
- 何物も存在しない
- 何かが存在したとしても、それを認識できない
- 何かを認識できたとしても、それを言語化できない
これの意味することは明らかだが、これの証明（と言われているもの）は不明瞭で、本書でも詳細は語られていない。Webを検索してもいまいちな説明しか無いため、もう少し形式化して考えてみようと思う。
形式化
まず、ゴルギアス・テーゼの形式化を考えてみる。おそらく以下のようになると思う。
E(x): xは存在する
R(x): xは認識できる
L(x): xは言語化できる
述語を決めて、限量子で量化しているだけである。
何物も存在しない
1のテーゼの否定を仮定する。つまり、次を真と仮定する。
何かが存在するとする。その何かは無から生まれたか、別の何かから生まれたかのどちらかである。無からは何も生まれないので、無から生まれたのは誤り。別の何かから生まれたとすると、その別の何かの誕生を証明しないといけない。別の何かの、そのまた別の何かのという論法は無限遡行と言って、これは論理的な誤りであるとされる。というわけで仮定は誤り。背理法よりテーゼ1は真となる。
無限遡行はいろいろな場所に出てくる。例えば因果律の説明で、因果律を認めるためには、物事の因果の因果の、そのまた因果をたどることが出来る必要があるが、これは無限遡行に陥る。あるいは、ある地点では原因が無くても結果が起きる必要がある。よって、因果律は認められない。
何かが存在したとしても、それを認識できない
次に2のテーゼを証明してみる。
なので、この否定が真であると仮定する。つまり、
となる。しかし、テーゼ1より何物も存在しないのでこれは誤り。よって、背理法よりテーゼ2は正しいと証明された。テーゼ3もほぼ同じように証明される。
梵我一如
ゴルギアスは古代ギリシアの哲学者であるが、古代インドのウパニシャッド哲学の梵我一如も大体同じようなことを言っている。梵（ブラフマン）は宇宙の普遍的な実在で、我々には認知できない。我（アートマン）は自身の中心的な実在であり、我々自身では認識できない。結論だけ言うと、梵と我は同じであるというのが梵我一如の教えとなる。
ギリシアとインド、全く違う土地だが、同じような結論に至っているのは面白い。ただ、どちらも我々のような凡夫にはよくわからないというのが大きな特徴である。
宇宙は無限か存在しない
無限遡行が問題なのは、この世が有限だからという前提があるからのように思える。我々の宇宙が誕生したのは138億年前と言われているが、ではこの宇宙は何から生まれて、その何かは何から生まれたかのという疑問が残る。つまり、何物かが存在する、あるいは因果律が成立するためには、多元宇宙論的な宇宙が存在して、さらにそれが無限に続く存在でなければ説明がつかない。
因果律はともかく、何物も存在しないというテーゼは受け入れがたい。我々が存在するという証明を残したのは、かの有名な「我思う、故に我あり」を残したデカルトだが、少なくともデカルトの言うように何物かが存在するならば、宇宙は無限ということになる。
以上、つらつらと書いたが単なる感想なので笑い飛ばしていただければと思う。ソワカ。
2020年まとめ
コロナで大変だった。以上。
今年はずっと文章を書いていた気がする。ただそれも終盤に差し掛かってきているため、来年の頭ぐらいには終わらせたい。特に、コロナで自粛しており自宅待機が多かったため、時間的な余裕が取れて文章が進んだのが大きかった。また、文章を書いている途中で、面白いことができそうだなと思いつき、OSと言語処理系を実装して国内研究会へ発表した。こちらは手をつけ始めたばかりなので、来年にはもう少し発展させたい。
学生も研究する時間がいっぱい取れただろうなと思いきや、思いの外に進んでいなかったようだ。聞くところによると、ゲームばかりしていたか、今年はオンライン講義が多かったために課題が例年の1.5倍あったためらしい。やはり、普段と違う生活になってしまうと、色々と問題が起きるようである。
自分的には家の方が作業しやすくて、文章や研究も進むのだが、多くの人にとっては大学や、あるいは職場ではないと作業が進まないのだろうと感じる。一応、自粛期間中でもオンラインでのミーティングを行ったのだが、やはり研究指導は対面の方がやりやすい。一方、講義の方はオンラインの方が好評であったと思う。対面とオンラインの両方選択できるようにはしているが、対面に来る学生は、1〜3名だけであった。
というわけで、今年の研究成果は以下の通りとなった。
本
- Akinori Kawachi, Atsuko Miyaji, Kazuhisa Nakasho, Yiying Qi, and Yuuki Takano, "Secure primitive for big data utilization", In Atsuko Miyaji and Tomoaki Mimoto, editors, "Security Infrastructure Technology for Integrated Utilization of Big Data - Applied to the Living Safety and Medical Fields", pp. 35–63. Springer, 2020.
国際会議
- Seitaro Mishima, Kazuhisa Nakasho, Kousuke Takeuchi, Naohiro Hayaishi, Yuuki Takano, Atsuko Miyaji, "Development and Application of Privacy-preserving Distributed Medical Data Integration System", 2020 IEEE International Conference on Consumer Electronics-Taiwan (ICCE-Taiwan), pp. 1-2.
国内研究会
- Sai Veerya Mahadevan, Yuuki Takano, Atsuko Miyaji 、"PRSafe: Primitive Recursive Function Based Domain Specific Programming Language Using LLVM"、情報処理学会 コンピュータセキュリティシンポジウム 2020 (CSS 2020) 論文集、pp. 94-100、2020年10月
- 高野 祐輝、金谷 延幸、津田 侑、"Make TrustZone Great Again"、情報処理学会 コンピュータセキュリティシンポジウム 2020 (CSS 2020) 論文集、pp. 422-429、2020年10月
- 細谷 昂平、高野 祐輝、宮地 充子、"F*言語を用いたネットワークファンクションの設計と実装"、Computer Security Group (CSEC2020-03)、2020年3月
- 岡 大貴、高野 祐輝、鄭 振牟、宮地 充子、"ZoKratesのドメイン固有言語に対するLispベースの拡張とVariant型の提案"、Computer Security Group (CSEC2020-03)、2020年3月
- 西口 朋哉、宮地 充子、高野 祐輝、"セッション型を用いたアクセス制御システムの評価"、第50回情報通信システムセキュリティ研究会 (ICSS)、2020年3月
- 竹中 幹、高野 祐輝、宮地 充子、"XDPを用いたネットワーク型欺瞞的防御システムの設計と実装"、SCIS 2020、2020年1月
- 西口 朋哉、高野 祐輝、宮地 充子、"セッション型を用いたアクセスコントロール機構の設計と実装"、SCIS 2020、2020年1月
本当なら、国際会議がもう少し多く、今頃はジャーナルぐらいは行けるかなと思っていたのだが、思わぬ誤算であった。ただ、今月に学生の書いた国際会議論文がアクセプトされて来年頭に発表があり、別の国際会議論文も来年頭には投稿予定なので、来年こそは発表を増やしていきたいところである。
それでは皆さん、良いお年を。
大学でRustを教えた話
このブログ記事は、Advent Calender 2020, Rust 3、23日目の記事となります。自分は現在大学で教員をしていまして、セキュリティ系の研究室に所属しています。現在はセキュリティの講義を担当しており、そこでRust言語を教えているため、その内容を紹介しようと思います。
はじめに
皆さんご存知のようにソフトウェアの脆弱性は今でも大きな問題となっていますが、それを完全ではないにしろ根本から解決するための技術的手法として型システムが注目されています。型システムの考え自体は古くからありますが、最近ではRust言語が登場し、OSなどいわゆる低レイヤーなソフトウェアも型システムの恩恵を預かることができるようになってきました。SMTソルバや定理証明などと言った難しい（かつ面白い）手法でC言語やC++言語で書かれたソフトウェアを解析する方法もありますが、セキュアソフトウェアを語る上では、現在では、まず型安全なプログラミング言語を利用するのが先決だという信念から、セキュリティの講義でRust言語を教えました。
講義の受講者は、大阪大学、京都大学、北陸先端科学技術大学院大学、奈良先端科学技術大学院大学らの大学院生と社会人学生となっており、基本的に情報系の大学院生と社会人を対象としています。大学院の講義なので、単なるHow toを教えるのではなく、Rust言語の裏側にある理論的背景から説明するように心がけました。逆にいうと、理論的なことは教えるのですが、データコンテナやCargoなどの使い方は自習が求められる構成となっているため、ある程度は自分で調べる必要があります。
講義の内容
Rustに関する講義は以下の通りとなっています。いずれも1回90分の講義となっています。
- ソフトウェア技術についての概要説明（GC、型システム、様々なバグ）
- Rust言語について
- 線形論理と線形型システム
- 線形型システムの実装
- 並行プログラミングとRust
ソフトウェア技術について
まずはじめに、ソフトウェアとソフトウェアテストに関する技術について概要を説明し、以降で説明するRust言語についての立ち位置を明確にするように心がけました。この文章を読んでいる方はRust言語の存在は当たり前に知っているとは思いますが、Rust言語はまだまだマイナーな言語で、その存在すら知らなかったという学生や社会人の方も多くいらっしゃいました。その中で、他にもいろいろなプログラミング言語があるのに、何故Rustというマイナー言語を新たに学ぶ必要があるのかという手厳しい質問も頂戴しました。
これは難しい質問で、確かに、他にもOCamlやHaskellと言った先駆者があり、それら言語であればRustの借用と言った複雑な機能に煩わされることも無いのは確かです（Haskellのモナドが借用より簡単かと言えば難しいところですが）。ですが、現状の流れを見ると、OCamlやHaskellが主流になることはしばらくは無さそうですが、RustがCやC++の代替となる可能性は十分にあり得ます。ICTインフラがますます普及し、ソフトウェアが我々の命までも支えるようになってきた昨今では、C、C++をRust等のメモリ安全な言語で置き換えることは、ソフトウェア業界の最重要課題と言っても過言ではありません。このような状況を鑑み、本講義ではRust言語を選択しました。
Rust言語の説明
ソフトウェア技術の概要を説明した後は、Rust言語についてざっと説明しました。この回で基本的な構文や、借用について説明し、コンパイルの仕方も簡単に説明しました。2回目の講義レポートでは、AArch64アセンブリの簡易版エミュレータをRust言語で実装してもらいました。簡易版ですので、命令セットは四則演算と、条件分岐だけという簡素なものですが、この課題でenum型やパターンマッチ、moveセマンティクスなどの諸概念について体感してもらいます。
実際のレポート課題としては、以下のようなアセンブリファイルを読み込んで実行するようなものとなります。エミュレータと言っても、機械語ではなくアセンブリ言語をそのまま解釈するためスクリプト言語処理系と言った方が正確かもしれません。
線形型システム
次に、線形型システムについて説明しました。ここでは、Rust言語の理論的背景的にある線形型システムについて（実際はアフィン型ですが）、線形型言語をもとに説明しました。内容的にはATTaPL (*1) の線形型言語にいくつか改良を行ったものを用いました。型付け規則から説明して、型付け規則を用いた証明まで行うため、何故Rust言語でuse after freeやdouble freeが防げるのかを、理論的な側面から理解できるようになります。
この講義のレポートでは、次のような型付けに関する証明を行ってもらいましたが、多くの学生がしっかりと証明できていました。正直、ATTaPLを独習して証明までできるようになる人は多くはいないと思うのですが、本講義を90分受講して課題にとりくむと証明できるようになっていますので、これは凄いことだと思います。
その後、線形型言語の型検査アルゴリズムを、Rustを用いて実装してもらいました。アフィン型の言語であるRustを用いて、線形型システムを実装することで、Rust言語自体がよりよくわかるようになるという寸法です。この講義よりも前に初学者にRust言語を教えたことがあるのですが、moveセマンティクスの理解に時間がかかるようでしたが、これら課題を行うと完璧に理解できます。
(*1) ATTaPL: Advanced Topics in Types and Programming Language
並行プログラミング
この講義はつい先ほど行ったものですが、ここではRustでの並行プログラミングについて説明しました。Rustは並行プログラミングについても非常によく設計されております。その実現には、借用とトレイト制約が重要な役割を果たしていますが、それらについて講義をしました。ここではRustだけではなく、クリティカルセクションやレースコンディションなどの一般的な諸概念と、アトミック命令を用いたスピンロックアルゴリズムの紹介も行います。この回でRustに関する講義は終わりになるのですが、続く回ではモデル検査機のAlloyを用いてスピンロックやRWロックアルゴリズムの検証を行っていく予定です。
以上が講義の内容となります。回数自体は多くありませんが、Rustの基礎的なところや何故Rustなのかぐらいは分かる内容ではと思います。
まとめ
本講義ではRust言語とその理論的背景となる型システムまで教えましたが、自分はプログラミング言語理論は専門ではなく、どちらかというと、OSやネットワークなどのシステムソフトウェア、並行プログラミングの実装などが専門となります。そのため、線形型などの理論をどう教えたものかと大変悩みましたが、結果的には理論と実装をバランス良く扱うことができたかなと思います。本当はOSやネットワークスタックをRustで実装するような内容にしたいのですが、しょうがありません。
世間では、「大学では古い技術しか教えていない。トヨタなどで使っている最新鋭の技術を教えるべきだ」、などと言ったご意見もありますが、本講義のように、トヨタでも少数の人しか使っていないであろう、そこそこ最新の技術も多少は教えられているのではと思います。
それでは皆さん、メリークリスマス。
Rust言語によるOSと言語処理系ができるまで
タイムライン
Rust言語で簡単なファームウェア、OS、言語処理系を作成したが、そのタイムラインはだいたい以下のようなものであった。もともとは、Rustでどの程度できるか検証するために始めた実装で、OSを作る予定ではなかったのだが、やっていくうちに面白そうなことができそうなので、どんどん作っていったら、そこそこ動くものが出来上がった。
2020年
2月13日：cargoでリポジトリ作成してgithubに登録
2月16日：シリアルコンソールへ出力
3月9日：MMUの有効化に成功
3月15日：同期処理コードを追加
3月29日：slab allocator有効化
4月2日：言語処理系の設計・実装開始
4月10日：FF7リメイク発売のためしばらく停滞
6月7日：言語処理系の実装終了
7月5日：Pine64+へ移植
8月5日：電源周りの実装開始
8月28日：電源周りの実装が一段落
9月2日：セキュアワールドとノーマルワールドのコンテキストスイッチを実装
9月16日：buddy allocator実装
所感
作ってみると、Rustにはスライスがあるため、unsafeであってもメモリの保護はかなり強力に出来るというのがわかった。また、代数的データ型もあるため、unsafeなコードであってもエラーハンドリングを忘れづらいというのも良い。ただし、グローバル変数にアクセスすると、レースコンディション関係は正真正銘unsafeとなるので、注意する必要がある。
Rust自体の難しさはそれほどなかったが、MMUや電源周りの仕様などを読み解くほうが苦労した。あとは、GICを制御できれば基本的な機能はできるはずなので、その後に隔離機構の設計・実装を行っていきたい。また、現在は、基本がCのコードで、Rustの機能をフルに活かしているとは言い難いため、そちらも改良していきたいと思っている。
ただ、いまは別の仕事をしているため、まずはそれを仕上げてからかなと思う。こちらもRustをふんだんに使っているので、仕上がったらまた公開したい。
この研究は現在は完全に個人研究で行っており、そろそろ研究予算をとってこないと色々とつらいため、何とかしたいところである。
Rust言語でファームウェア、OS、言語処理系を実装して、CSS 2020で発表した
先月、国内最大のセキュリティ研究会であるコンピュータセキュリティシンポジウム 2020（CSS 2020）が開催され、そこで、Rust言語を用いてファームウェア、OS、言語処理系を設計・実装した話を発表しました。本来、CSS 2020はリアルで開催されるはずでしたが、コロナ禍の影響でオンライン開催となり発表動画作成が求められました。せっかく作った動画をこのまま捨て置くのももったいないと思い、ここで供養したいと思います。
概要
内容は、Rust言語を用いて、AArch64のセキュアワールド内で動作するファームウェア、OS、プログラミング言語処理系を実装した話となります。と言っても、まだまだ基本的な部分しか実装しておらず、実現目標に対して2〜3割と言ったところですが、どうぞご笑覧ください。
ブート部分は多少アセンブリ言語を使っていますが、その他の部分はRustでフルスクラッチで実装しています。修正したい箇所も多く残っていますが、まだまだ出来ていません。
対応ハードウェアは、今のところPine64+のみでUSBケーブルからのブートが必要ですが、機能縮小板はQemuのRaspi3エミュレーションで動作します。
言語処理系
言語処理系はまぁまぁ凝っており、構文はLispっぽく、型システムはOCamlやHaskellっぽく設計・実装しています。ですので、代数的データ型、末尾呼び出し最適化、ジェネリクス、型推論、パターンマッチなどの機能が利用できます。ただし、高カインド型は未対応のため、モナドは使えません。型システムは形式的に定義しているため、検証もしやすいと思います（手をつけられていませんが…）。
さらに、効果系と呼ばれる機能を適用しているため、副作用のある関数と、そうでない関数を完全に分離可能になり、安全にセキュアワールド内へプログラムを注入することができます。本当はRustとの連携をもっと強固にしたいところですが、まだ実現できておらず、今後の予定となっています。
なお、ソースコードはオープンソースライセンスで公開しており、以下より取得できます。
もう少し時間があれば設計や実装も進めることができそうですが、大学はやたら忙しく、日々ワード、エクセルと格闘しているため、最近はあまり進捗はありません。今の担当講義が終わったら、また時間を見つけて研究を進めたいところです。
SFはいいぞ
最近、プログラミング系の本しか読んでおらず、少し息を抜きたいと思いSF本を買って読んだりしていた。SF本と言っても、気軽に読める短編集である。SF短編集といえば、小学生の頃に星新一をよく読んでいたのを思い出すが、今回読んだのは複数著者の作品が収録されているため、アンソロジーというやつになる。最近はこのアンソロジー本が結構あるようでありがたい。読んだ本は、「日本SFの臨界点 怪奇篇 ちまみれ家族」と「ベストSF2020」である。
日本SFの臨界点 怪奇篇 ちまみれ家族
「日本SFの臨界点 怪奇篇 ちまみれ家族」で個人的に特に気に入ったのは、中島らもの「DECO-CHIN」と、山本弘の「怪奇フラクタル男」である。DECO-CHINは幸福とは何かという普遍的でよくあるテーマが題材だと思うが、オチが飛び抜け過ぎていて呆気に取られてしまった。最後にタイトルの伏線を回収するのだが、まさかまさかの回収の仕方であった。怪奇フラクタル男はフラクタルを題材にした話で、これもまた突拍子のない発想で、どうやったらこんな話が思い浮かぶのかと、あまりに驚いた。
フラクタルというと中学生ごろにフラクタルに興味を持って色々調べていたのだけれど、その頃専門書を買って読んでも全然理解できなかった。中学生の自分にはハウスドルフ次元は難しすぎた。その後、高専に入ってプログラミングが出来るようになってマンデルブロ集合やらを描画していたのを思い出す。最近もRaspberry Piでマンデルブロ集合を描画していたため、技術は一度身につけると色々と役に立つもんだなぁと思う。
他の話も普通に面白いのだけれど、この2作はぶっ飛び方が凄くて衝撃だった。息抜きで読んだけれど、やっぱりSFは面白いなあと再確認。
ベストSF2020
「ベストSF2020」で個人的に特に気に入ったのは、草上仁の「トビンメの木陰」、草野原々の「断φ圧縮」である。ドビンメの木陰は最後あたりまではわりと普通かなと読んでいたんだけれど、最後の落ちあたりがとても綺麗に纏まっていて大変感心した。手法としてはオーソドックスなのかもしれないけれど、こうきたかぁ。うまいなぁ。と夜布団の中で読みながらしきりにうなづいていた。断φ圧縮は怪奇フラクタル男に通じるところがあるような気もするが、こちらはフラクタルではなくカルノーサイクルが題材である。
カルノーサイクルは熱サイクルで、断熱圧縮、等温膨張、断熱膨張、等温圧縮を繰り返すサイクルである。熱機関やエンジンは高専の当時に必修科目であったのだが、全く興味が持てなかったため現在でも理解が曖昧で、作品を120%楽しめなかった。悔しい。フラクタルは必修どころか選択でもなんでもなかったがよく覚えているのに。将来SFを楽しむために、ちゃんと勉強はしておくもんである。
というわけで、2冊を読んだが存外に面白かったので、これからも定期的に買って読もうかなと思った次第です。それでは、皆さん良いSFライフを。
Bloodstained: Ritual of the Nightをクリアした
悪魔城ドラキュラの精神的続編
悪魔城ドラキュラといえば、ファミコン時代からある横スクロール型のアクションゲームである。もともともはアーケードゲームだったらしいが、そのころは子供だったので不良のたまり場になどいけるはずもなく、ファミコンで悪魔城ドラキュラをプレイしていた。
と言っても、自分がプレイしていたのは、悪魔城ドラキュラシリーズの2作目であるドラキュラII 呪いの封印だった。呪いの封印はディスクシステムだったので、ロードがやたら遅かった気がする。しかも、謎解きが難しく、○○に祈りを捧げよと言うヒントが当時は全く理解できず、クリアできなかった覚えがある。ちなみに、○○に祈りを捧げよは、ある場所でしゃがみ続けると良いらしいのを大人になってから知り、そりゃわからんわって思った。
そんなドラキュラシリーズはこれまでに幾つものシリーズを出していたのだが、最近、プロデューサのIGA氏が独立で悪魔城ドラキュラっぽいゲーム、Bloodstinedを出したと言うのでプレイしてみたところ、これが全く悪魔城ドラキュラだった。
懐かしすぎて逆に新鮮味がある横スクロール型アクションRPG
最近のゲームといえば、カメラは主観かもしくは背中からの第三者視点でゲームを進めていくものがほとんどだが、Bloodstainedは悪魔城ドラキュラと同じ横スクロールアクションで逆に新鮮に感じた。昔は横スクロールアクションばっかりだったのだが。
昔の横スクロール型のアクション物といえば、コナミワイワイワールドがあるがこれもめちゃくちゃプレイした気がする。キャラクターにはコナミキャラが沢山いて、がんばれゴエモンシリーズの五右衛門やら悪魔城ドラキュラシリーズのシモンなんかを使えた。実は、Bloodstainedの別シリーズであるCurse of the Moonは8bitテイストで、コナミワイワイワールドらしいので、こちらもいずれはやってみたい。
最新版ドゥエリスト
悪魔城ドラキュラシリーズといえば、ジャンプキックをすると高速に移動でき、その際にキャラクターが発する「ドゥエ！」と言う掛け声を連発して移動するのがおなじみである。そのような姿で移動するキャラは通称ドゥエリストと呼ばれるのだが、Bloodstainedでもお馴染みの移動ができて感涙である。
悪魔城ドラキュラHD（協力プレイがメイン）にはユリウスというキャラクターがいた。ユリウスは「色即是空」という高速移動技を持っており、この色即是空もキャンセルして連発可能である。大体の協力プレイでは、ユリウスが開幕に「よろしく」というチャットと色即是空を組み合わせるのが通例になっており、「よろｼｷｿｼｷｿｼｷｿｼｷｿ…」と言い残して他の仲間を置き去りにして画面端に走り去ってしまうこともしばしばあった。そんなドラキュラHDなのだったが、Bloodstainedのあるキャラは空即是色という高速移動術を持っており、初めてみた瞬間、これユリウスやん！ってなったのであった。
そんなこんなで、楽しくBloodstainedをプレイしクリアした。本当はGhost of Tsushimaをプレイしようとしたが、売ってなかったのでBloodstainedにしたのだけど、こちらで正解であった。
ちなみに、自分は北米版を買ったのだが、普通に日本語でプレイできた。
