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にしたのだけど、こちらで正解であった。
ちなみに、自分は北米版を買ったのだが、普通に日本語でプレイできた。
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で動かないために焦ったが、無事に動いてなによりである。それでは皆さん、良いハッキングライフを。ソワカ。
