2023年まとめ

2023年は、久々に書籍執筆をしていない年で、心に余裕をもって日々を過ごすことが出来た。雑誌の執筆はいくつか行ったが、書籍に比べればマシだった。というわけで、2023年も暮れになったので、本年を振り返ってみる。

2023年の成果

2023年の成果は以下となる。民間企業に転職して、はじめての国際会議論文を投稿できた。発表もいくつか行っており、2月に一回は対外的になにかしら発表している計算になる。頑張りすぎている。

国際会議(査読あり)
  • Yuuki Takano, “Deadlock- and Starvation-free Formally Verified Client Library for Robots”, IEEE International Conference on System Reliability and Safety (ICSRS), Nov. 2023
国内研究会
  • 高野 祐輝, 神戸 隆太, “自動運転向けOSとその形式検証”, ComSys 2023 企業展示, 2023年12月
  • 尾崎 純平, 高野 祐輝, 宮地 充子, “eBPF検証用の双方向通信フレームワークの提案”, 情報処理学会 第194回マルチメディア通信と分散処理・第100回コンピュータセキュリティ合同研究発表会, 2023年3月
  • 斎藤 文弥、高野 祐輝、宮地 充子, “安全な機能拡張性を持つTEEシェルの実装”, 情報処理学会 第194回マルチメディア通信と分散処理・第100回コンピュータセキュリティ合同研究発表会, 2023年3月
その他発表
  • 高野 祐輝, “安全性の高いRustをChatGPTで書いてしまおう”, CQ出版 インターフェース 2023年12月号
  • 高野 祐輝, “Rustでつくるロボットソフトウェア”, Rust、何もわからない… #8, 2023年5月
  • 高野 祐輝, “質実剛健Rust言語”特集内の記事3本, CQ出版 インターフェース 2023年5月号
  • 高野 祐輝, “seL4チュートリアル”, TIER IV Computing System Workshop, 2023年3月
  • 高野 祐輝, “safe_drive: ROS2向けのRustクライアントライブラリと形式手法を用いた検証”, ROS Japan UG #49 LT大会, 2023年1月

『ゼルダの伝説 ティアーズ オブ ザ キングダム』と『Finaly Fantasy 16』をクリアした

題名の通り、『ゼルダの伝説 ティアーズ オブ ザ キングダム』と『Finaly Fantasy 16』をクリアした。どちらもビッグタイトルでクオリティが高かく楽しめた。前者はオープンワールドで、後者はほぼ一本道の従来のRPGという感じだが、どちらも戦闘はアクションがメインというのが共通している。また、宝箱を空ける際は、主人公であるリンクとクライブの両方とも、蹴って開けていたのが気になった。エルデンリングだと、宝箱はちゃんと屈んで空けていたが、こちらでは、蹴って開けるのである。蹴って開けると宝が手に入る。

ゼルダの伝説 ティアーズ オブ ザ キングダム

ゼルダの伝説オープンワールドで、前作のブレスオブザワイルドとほぼ同じテイストとなっている。今回は、ゾナウギアという機械仕掛けのロボットを自作することが出来るというのが大きな違いである。ティアーズ オブ ザ キングダムをやり始めた当初、パラセールの代わりにゾナウギアになったのかと思った。パラセールとは空を滑空するためのアイテムで、ゾナウギアでも空を滑空できる。序盤の方では、いくつかのほこら(ダンジョンのようなもの)をパラセール無しでクリアしてたのだが、あまりに難しく、難易度上げてきたなあと思ったが、単純にパラセールを未取得だったため、やたら高難易度になっていたのだった。

パラセール取得後は、そこそこすんなりと進められて、頑張った結果、無事にFinal Fantasy 16発売までにクリアできた。しかし、攻略情報をまったく見ずに進めていたため、最後のほこら数個がどうしても見つからずタイムアップとなってしまった。オープンワールドで、隅々まで探索するのはかなり難しい。コログとまよいは諦めた。人間諦めが肝心である。

Final Fantasy 16

FF16は凄く期待していたが、バトルが簡単すぎたのがやや不満だった。個人的にはS級リスキーモブぐらいの敵は、メインストーリー中で出てきても良いのではと感じた。S級もたいして強くない。
ストーリーも腑に落ちない点が多い。例えば以下である。

  • 火の召喚獣が二人いて、イフリートはクライブであることがわかっている。すると消去法的に残りの一人はフェニックスのジョシュアしかいない。しかし、そのことについて主人公達は仮説すら立てずにいる。
  • ストーリー中盤でジョシュアがクライブを助けるが、その後しばらく何故かジョシュアはクライブから隠れるように行動する。しかし、その後しばらくして普通に再開する。何故クライブから隠れていたのかがまったくわからない。
  • クライブがジョシュアを殺した(と思っていた)のは自分だとわかったとき、自分を強く責めるが、はっきり言って責めるのは母親のアナベラである。自分じゃないだろクライブ!目を覚ませ!

ストーリーや難易度には不満はあるが、キャラクターはとても魅力的でビジュアルも派手でその点は素晴らしい。バグらしいバグもなく、ソフトウェアとしての出来も良い。普通に良作だとは思う。
ストーリーや戦闘以外の部分では、Final Fantasy 14のオマージュが色々とあったのでニヤリとした。例えば、ガルーダがスパルナとチラーダを従えていたり、タイタンがランスラ、激震、重みを繰り出してきたりと、これFF14でやったやつだ!となった。

次に控えている、Final Fantasy 7Rも楽しみである。

2022年まとめ

2022年は戦争がはじまり、時代が逆行したような年でした。我々は技術者・研究者であるので、社会的・政治的には時代が逆行しても、科学と技術を進歩させ、科学技術で社会問題を解決してきたい所存であります。

『ゼロから学ぶRust』を執筆した

2022年12月13日に講談社より『ゼロから学ぶRust』が発売されました。本書は私の2作目となります。1作目は2021年8月にオライリー・ジャパンより発売された『並行プログラミング入門』となります。どちらも好評発売中ですので、よろしくお願いいたします。

『ゼロから学ぶRust』の執筆と苦労した点

『ゼロから学ぶRust』の執筆依頼を受けたのが、2021年7月頃で、その頃はちょうど『並行プログラミング入門』の執筆が終了したときに思います。『並行プログラミング入門』の執筆が終了し、ようやく一息つけると思った折りに依頼が舞い込み、正直断ろうと思いました。しかし、『並行プログラミング入門』には収録できなかった、システムソフトウェアに関する内容や、線形型システムについても書きたく思っていたので、引き受けることにしました。書籍の執筆はかなり大変で、個人的な金銭的面からのみ考えると、かけた労力に見合うものではありません。ですが、Rust言語の普及はコンピュータサイエンスとしても重要な課題であると考えていたので、引き受けることにしました。『並行プログラミング入門』が3年半ぐらい、『ゼロから学ぶRust』が1年半ぐらいの執筆期間なので、5年は連続して執筆していたことになります。

『ゼロから学ぶRust』ですが、執筆に関して重要視していたのはライブラリの説明や言語の説明に終始しないことです。Rustでは、Rustの公式チュートリアルが非常に良く書かれているため、Rust自体の解説だけする書籍の価値は低いと考えています。また、ライブラリは流行り廃りが激しく、数ヶ月で時代遅れになることはざらにあります。そこで、本書では、なるべく公式チュートリアルとは異なる側面からRustを解説し、文法解説以上の説明をRustで行うように心がけました。特に、私が当時は大学で講義をしていたことから、大学の情報系学部での利用に耐えうるような、コンピュータサイエンスの内容を含めたものにしたつもりです。

そのため、本書はプログラミング言語の書籍ではありますが、オートマトン正規表現、シェル、デバッガ、線形型システムなどの基本的な事も学べる内容となっています。当然、Rustでプログラミングする際にもこれら概念は重要になります。大学、高専、専門学校の場合、単純にプログラミング言語を教えるのではなく、アルゴリズムコンピュータサイエンスと関連付けて教える場合が多いと重いのですが、それを意識しました。

本書執筆で一番苦労したのは、ページ制限です。ページ数が300ページ以内と制限があったため、いかにページ内で説明するかを考えるのが大変でした。ページ内におさめるために、すべてのソースコードを本に載せるのではなく、似たようなコードは省略し、GitHubソースコードを参照してもらうようにしました。これにより、説明がコンパクトで重要な点のみにしぼられるため重要な点のみ理解すればよくなります。一方、すべてのコードがないので、残りは読者が自分で考える必要があります。一長一短ありますが、今回はコンパクトにまとめることを優先したので、この形に落ち着きました。
書籍中に省略したソースコードGitHubから御覧ください。

GitHub - ytakano/rust_zero

ちなみに、電子書籍版は2023年春頃予定だそうです。

今後のRust本

Rust関連書籍が充実してきました。書店をみると、Rustというコーナーが出来ており、Rustが広く認知され始めていることが実感できます。Rust関連で欲しい書籍は、やはり、アルゴリズムの書籍に思います。残念ながら私はアルゴリズムの専門家ではないため書けませんが。個人的には、Rustで本格的にOSを実装する本を書きたい気もしますが、OS実装の本はどれも超大作なのでキツそうだなあという印象です。RustでRustをつくるというのも挑戦したいのですが、時間がなく進んでいません。こういった教科書の執筆は本来ならば大学の先生の仕事だったのでしょうが、いまは教科書執筆のような本質作業はほとんど評価されず、海外経験、社会人経験、性別などといったレア属性であったり、予算獲得能力が評価されるので、なかなか厳しそうですね。

大学から民間企業に転職した

もともとは大学へ残ろうと思っていたのですが、色々なご縁があり、民間企業に転職しました。民間企業は正直不安でしたが、技術レベルについては特に問題ないかなと思います。大学教員をしていた都合上、大学の学部レベルの情報系学問はほぼ修得していたので、問題はなさそうでした。逆に言うと、技術的な話のみでいうなら、大学や国研の方が最先端です。これは、最先端技術が必ずしも飯の種になるとは限らないからに思います。しかし、私のいるところはディープテックなベンチャー企業なので、大学や国研レベルの最先端を目指していくつもりで日々奮闘しています。最先端をめざすには、やはり論文を読んだ方が良いというのが国研、大学、民間企業を経験してみた結論です。

Stack Overflow創業者は以下のように語っていますが、論文を読んで実装できる、というのは新しい領域を開拓したい場合には全く間違っているので、真に受けない方が良いと思います。Stack Overflowが使っているであろうクラウドサービスでは、GoogleAWSMicrosoftから発表された論文に基づく技術が山のように使われているのは言うまでもありません。

大学や国研にいると、論文を読むことが多くあります。多く読む分、イマイチな論文も沢山読むことになるのですが、そうすると論文の価値について半信半疑となってしまいます。しかし、民間企業へ来て、論文の価値を再評価できたのは良かったです。最近ではUSENIXやACMも、論文の再現性について重要視しているので、一時期よりも質が向上しているように思います。その分、書くのは大変になりましたが。

今年は業務でROS2というロボティクス用のミドルウェアを触っていたのですが、それのRustクライアントライブラリを実装して、SWEST24という組み込みソフトウェアむけのワークショップで発表しました。タイトルは『Rustとモデル検査器を用いたROS2クライアントライブラリの設計と実装および安全性検証』というもので、TLA+というモデル検査器を利用して、デッドロックフリー、スタベーションフリーを検証しており、ソースコードGitHubで公開中です。まだ機能が一部足りませんが近々追加予定です。こちらはSWEST24でベストポスター賞(シルバー)を受賞しました。

github.com

これを皮切りとして、来年もどんどんCutting Edgeなものをリリースしてきたいと思います。大学時代は日々、ワード、エクセル、パワポと戯れていたのですが、民間企業だと開発する時間も多くあり、とても良いですね。Stack Overflowの創業者に言わせると、これも「頭は切れるが役に立たない」という事例なのでしょうか?気になります。

2022年の成果

2022年の成果は以下となります。

特許

書籍

  • 高野 祐輝, "ゼロから学ぶRust", 講談社, Dec. 2022.

論文誌(査読有り)

  • Atsuko Miyaji, Kaname Watanabe, Yuuki Takano, Kazuhisa Nakasho, Sho Nakamura, Yuntao Wang, and Hiroto Narimatsu, "Privacy-Preserving Distributed Medical Data Integration Security System for Accuracy Assessment of Cancer Screening: Development Study of Novel Data Integration System", JMIR Preprints, https://preprints.jmir.org/preprint/38922, Dec. 2022.

国際会議(査読有り)

  • Nobuyuki Kanaya, Yu Tsuda, Yuuki Takano, Yoshitada Fujiwara, Ryoichi Isawa, and Daisuke Inoue, "NEMIANA: Cross-Platform Execution Migration for Debugging", The Third ACM/IEEE International Conference on Automation of Software Test, pp.138-147, May 2022
  • Liu Xiaolong, Yuuki Takano, and Atsuko Miyaji, "Design and Implementation of Session Types-based TCP and Unix Domain Sockets", The Eitgh International Conference on Information and Network Technologies, ICINT 2021, May 2022

国内研究会

  • 尾崎 純平, 高野 祐輝, 宮地 充子, "eBPFの動作検証用フレームワーク及びデバッガの提案", (CSEC2022-99), 2022年12月
  • 高野 祐輝, "Rustとモデル検査器を用いたROS2クライアントライブラリの設計と実装および安全性検証", SWEST24, 2022年9月
  • 斎藤 文弥, 高野 祐輝, 宮地 充子, "Coqで検証可能なTEEシェル基盤の実装", 情報通信システムセキュリティ研究会, (CSEC2022-97), 2022年5月

受賞

  • SWEST24, ベストポスター賞(シルバー), 2022年9月

こうして振り返ってみると、思ったよりも色々と行っていますね。日々積み重ねです。それでは皆さん、良いお年を!

【読書】『同志少女よ、敵を撃て』を読んだぞ!

『同志少女よ、敵を撃て』は、ロシアのウクライナ侵攻が始まる前に発売された書籍で、発売当初から個人的に注目していた。発売されたときは、積み本が山のようにあったので見送っていたのだが、情勢も情勢だけに読んでみることにしたが、非常に面白かった。アガサ・クリスティー大賞を受賞されたそうだ。しかし、アガサ・クリスティー賞は長編推理小説に贈られる賞らしいが、「推理小説」とは一体何かわからなくなった。

推理小説というと、『シャーロック・ホームズ』や『江戸川乱歩』など、何かの事件を解決していく小説のように思われるが、『同志少女よ、敵を撃て』は第二次世界大戦独ソ戦あたりを時代背景とした時代小説という感じをうけた。「面白ければよかろうなのだァァァァッ!!(ジョジョの大冒険 第2部 カーズ)」の精神なのかも知れない。内容的には、戦争、復讐、狙撃、男女平等、百合といった要素で閉められていて、推理要素はあまり無かったように思う。

舞台は、最近何かの話題のウクライナ周辺の、ニュースで見たことある地名が多くでてくるので頭に入りやすい。あまりポジティブに捉えるのもどうかと思うが、そのおかげでより世界観に入り込めるのも確かだ。ソ連というと、内務人民委員部、通称NKVDという秘密警察が有名だが、そういった組織や連中も登場するので特殊組織好きにはたまらない。しかも、NKVDの連中と主人公がアレでコレでそうなるのでたまらない(ネタバレのため自粛)。このあたりのストーリーは個人的に特に気に入っている。

ソ連というと、当時は物資がない上に自国民の命を使い捨てすることで有名だ(これは今のロシアもそうかもしれない)。ソ連には武器が足りないため、2人で1丁の銃しか支給されなかったのはあまりにも有名だ。1人が銃を持ち、1人が弾を持ち、銃を持った方が死んだら、弾を持った方が銃を拾って戦うらしい。しかも、敵前逃亡すると味方から射殺され後退は許されない。Welcome to Hell!

たしか、ここら辺の描写が『Call of Duty: World at War』というゲームにあったような気もするが、記憶違いかも知れない。独ソ戦は歴史上最悪の地上戦とされているらしく、『同志少女よ、敵を撃て』の舞台の1つでもあるレニングラードでは、食糧不足のため人肉食もあったそうだ。『同志少女よ、敵を撃て』では、このような事実は幾分マイルドに表現されていて、良くも悪く戦争の悲惨さの描写は薄れていて、エンターテインメントに仕上がっているように感じた。それでも、歴史を多少知っておくと、より楽しめる気がした。

同志諸君、『同志少女よ、敵を撃て』はいいぞ!読むつもりはない?よしわかった、貴様はシベリア送りだ。

大学を辞めエルデンリングをクリアした

個人的に、2022年は大きな出来事が二つあった。一つめは大学を辞めたことと、二つめはエルデンリングをクリアしたことだ。自分はフロムソフトウェアのソウルシリーズはデモンズソウルの頃からやっており、特に協力プレイが大好物だ。侵入も好きだ。侵入者に華麗にパリィを決められてYOU DIEDすると、アドレナリンが脳内から大量に放出され生きている実感を感じる。

エルデンリングは当然予約購入した。発売から3ヶ月たとうとしている現在、総プレイ時間は280時間を超え、300時間に迫ろうとしている。はっきり言ってやり過ぎである。正直、少し飽きてきた。しかし、プレイ時間が300時間に迫ろうとしているのに、まだ二週目をクリアしておらず、今は二週目のミケラの刃、マレニアを知り得ているところだ。レベルも200を超えたところだが、死ぬときは一瞬だ。これは研究者のメタファーである。いくらトップカンファレンスへ論文を通したところで、有期雇用で雇い止めされる。そんな事をエルデンリングは教えてくれる。エルデンリングとは人生である。死ぬときは一瞬だ。だから、使えるときにルーンを使わなければならない。

アインシュタインは言った「科学は素晴らしい、それを職業にしないかぎりは」。至言である。エルデンリングは面白いが、狭間の地で実際に生活しようとは思わない。同じ事だ。そういうわけで、大学を辞めた。無期雇用の道も見えてきたが、そうすると、今度はいじめる側にまわると言うことである。大学教員は辞めればよい。スキルがあるので生きていくには困らないだろう。問題は、学生や子孫達が、高度な教育を受けられなくなっている可能性が大きいと言うことである。以前の研究室では、毎年教員が退職していった。その結果、毎年研究テーマが変わる学生が存在した。はっきり言って、毎年研究テーマが変わってしまっては、いくら優秀でも成果は出ないだろう。

エルデンリングは大変面白いが、不満点もある。一番大きな不満点は、サインだまりが周回時に引き継がれないことと、サインだまりのエリアが狭すぎることである。周回ホストをしていると、召喚サインのある場所とない場所の差が大きすぎるのがわかる。ミケラの刃、マレニアの前にだけ召喚サインが多すぎる。もっと他の地域にもサインを!声を大にして言いたい。

毒沼マップは大好きだ。腐れ谷、病み村、ファランの城塞、腐れ湖。こんな場所を探索させるなんて狂っている。だが、それがいい。毒回復を持っていないホスト、毒沼を走ってくる侵入者、全てが狂気だ。しかし、エルデンリングの腐れ湖は、召喚サインがない。そして召喚されない。もっと、毒沼マップにもサインを!声を大にして言いたい。

このクオリティの作品を作るのに、相当な年月がかかったのではと思う。大きな仕事をやり遂げるには、それなりの時間が必要なのだ。3年やそこらで良い研究は出来ない。エルデンリング、おお、エルデンリング。エルデンリング万歳。

YOU DIED

Rustのasync-stdを利用したRedisサーバクローンが公開されました

大学でセキュリティ関連の演習を行いました。この演習では、大学院生と社会人が研究や実装を通して実践的な学習を行います。トピックはRewrite it in Rust、モデル検査、ゼロトラスト、暗号など色々あるのですが、そのうちRewrite it in Rustのトピックを選択していた社会人の受講生が、async-stdを利用してRedisのクローンを実装して、オープンソースで公開しました。

github.com

ぜひ、GitHubのスターも押してください!

Tokioを利用したRedisクローンの実装は既にあるのですが、こちらはasync-stdを用いています。この演習では新規性ではなく、自分で実装して新しい技術を習得することを目標にしていたので、ネタかぶり上等です。受講者曰く、Rustは書き味が良く、安全で、高速に動作するため、業務でも使っていこうとおっしゃっていました。Rust独特なハマりどころもありますが、習得自体は難しい点はなかったということです。ちなみに、こちらの実装では、シグナルを捕まえてgraceful shutdownするようにしたりと、なかなか凝った作りになっているようです。

こちらは、座学で教員の話を聞くというのではなく、各自用意してきたスライドを発表して質疑しあうということを行いました。自分で調べて実装して、まとめて発表するのが一番自分の頭に残るのではないかと思います。他の受講者は、RustでOSを実装することに挑戦したり、TLA+で並行システムをモデル検査したりとしていました。研究レベルとまではいきませんが、そこそこ先端ではないかと思います。

今後も、Rustで世界を安全にしていきたいところです。

RustでRaspberry Pi 4を操作してみた

RustでRaspberry Pi 4をどれだけ操作できるか興味があったので、連休期間にやってみました。制約は、Rustのasync/awaitを使うこと、rppalというembedded-halベースのライブラリを利用することです。結論から言うと、I2C、SPI、GPIOなどほとんどの操作はRustで出来ることがわかりました。

ソースコードGitHubにアップしてあります。

github.com

実装するにあたり『Raspberry Piで学ぶ電子工作』を参考にしました。

Raspberry Piへの接続は以下のようになります。テスト用にどんどんデバイスを追加していったので、ブレッドボードのスペースが足りなくなりました。もっと大きなブレッドボードを使えば良かったです。

Raspberry Pi 4に各種センサーを接続した図
ラズパイ接続画像

今回、非同期ライブラリにはasync_stdを利用したのですが、rppalと併用にあたって特に困る事はありませんでした。チャネル、ミューテックス、アトミック変数を用いて同期処理をしていますが、かなりバシバシと書けるので、なかなか相性は良いのではないかと思います。

また、今回、Dieselを用いてPostgreSQLにデータを保存しましたが、こちらはasync/awaitと喧嘩するようだったのでスレッドを用いています。PostgreSQLに保存すれば、Grafanaなどを使って簡単にグラフ化できます。便利ですね。

Grafanaによる可視化
Grafanaによる可視化

上記書籍にはPWM制御もありますが、こちらではやっていません。かわりに、CSS811というCO2と揮発性有機化合物を測定できるデバイスを買って接続してみましたが、デバイスの初期化に半日ぐらいかかってしまい、これが一番時間がかかりました。ハードウェア難しい。CSS811は48時間のエイジング期間が必要らしく、まだ値は安定しませんが、データ取得は出来たので良しとしましょう。

正味の実装期間は、2〜3日ぐらいです。実際には5日ぐらいかかったのですが、Amazon秋月電子で発注して待っている期間の方が長かったと思います。Rustはやはり、型がしっかりしているので間違いにすぐに気がつくことが出来るので、とても良いです。

Rustを使う上での注意点は、Rust analyzerはメモリを食いすぎるのでRaspberry Pi 4の4GBメモリバージョンで利用するのは、かなり厳しいと言うことです。今回は、VSCode + rlsで実装しましたがメモリが少ない場合はこちらの方が良いですね。8GBメモリのRaspberry Pi 4も注文しているのですが、一向に届く気配がありません。半導体不足です。

コードはもう少し洗練できそうですが、テストコードならこんなもんですかね。Rustで色々出来るがわかり満足しました。それでは皆さん、良いハッキングライフを。