セキュリティ・キャンプ2024 全国大会【開発】S1～S19ゼミ

• 木藤 圭亮
• 内田 公太
• 松岡 航太郎
• hikalium

• 上田 蒼一朗
• 野崎 愛

• WebAssembly
• システムプログラミング

WebAssembly（Wasm）をご存知ですか？
Wasmは仮想命令セットです。ブラウザで実行するものというイメージが強いかもしれませんが、現在ではブラウザに限らず、FaaSやIoT、コンテナ、さまざまなプラグインでもWasmが実行されるようになり注目度が高まっています。

なぜWasmが注目されているのでしょうか？それは仕様によって定められたWasmの性質にあります。例えば、WasmはどのOS・どのCPUアーキテクチャにも依存しません。また、複数のプログラミング言語からコンパイルして生成することができます。Wasmはサンドボックス環境で動作するため、信頼できないWasmプログラムもある程度安全に実行可能です。このような性質が各分野のニーズにうまくマッチし、応用範囲が広い技術です。

本ゼミはWasmランタイムを作りながらWasmへの理解を深めることを目的としています。もう少し具体的には、次の3つを目標としています。まず仕様に慣れること。Wasmは仕様で定められるものであり、かつ策定中のものも多くあります。どのような仕様があるか、なぜそれが必要なのか、把握しておくことは今後Wasmの動向を追いかける上でも大切です。2つ目にWasmに対して手を動かせるようになること。Wasmランタイムを作る過程では、Wasmのバイナリとの格闘やOSSのツールを使ったデバッグが身につくはずです。最後にWasmの最新の動向に触れること。Wasmは現在注目されており動きの速い領域です。事例を紹介しつつ、Wasmの嬉しさを考えられたらと思っています。開発物については、アイディアのある方はWasmランタイムに限らず好きなものを開発してもらうことも可能です。

Wasmは魅力的な技術です。Wasmの何が嬉しいのか、理解を深めることで、「こんな応用をしたい」「この分野と融合したい」と考える土台やきっかけとなるはずです。ぜひ一緒にWasmを学びましょう！

• 井田 健太

• CPU
• RISC-V
• FPGA

普段なにげなくCPUをつかってプログラムを実行していますが、このCPUを作ってみたいと思ったことが少なからずあるのではないかと思います。 CPUの自作というと難しそうに感じるかもしれませんが、実はそこまで難しくありません。

特に、近年ではオープンソースの命令セット・アーキテクチャ規格であるRISC-Vの登場により、CPUコアを実装して実際に動作させるハードルがかなり下がっています。
CPUを作って動かすには、CPU自体の動作を設計して何かしらの方法で実装するだけでなく、そのCPUの上で動かすプログラムを作成するためのツールチェインの準備が必要ですが、RISC-Vの命令セットを実装すれば既存のRISC-Vツールチェインをそのまま使うことができ、CPU自体の設計に集中できます。

本講義ではRISC-V CPUコアの作成を通じて、CPUの内部構造と動作原理を学びます。
作成するCPUコアは非常に単純なものではありますが、動作原理を理解することによりSpectreやMeltdownといったCPUの動作に関連した脆弱性の理解につながります。

講義の内容としては、書籍「RISC-VとChiselで学ぶ はじめてのCPU自作」で解説する RISC-Vの規格で定められる RV32I 命令セットを実装したCPUコアを、FPGA上に実装できるように修正して動作を確認します。
FPGA上にはCPUコアおよび動作に必要な周辺回路を実装します。またCPUコア上で実行するプログラムも作成します。

キャンプ期間の3日間でFPGAボードの基本的な使い方からRISC-VコアのFPGA実装のすべてを行うのは難しいため、事前学習期間に書籍およびFPGAボードを配ります。

使用するFPGAボードはある程度周辺回路構成を変更可能なものを用意しますので、
CPUの周辺回路を実装することにより、LEDの点灯制御やスイッチ入力、UARTによる通信、Ethernetによる通信、DVI出力によるディスプレイへの映像表示などを試すことができます。

• 櫻井 碧

• TEE
• SGX
• 秘密計算
• 脆弱性
• サイドチャネル攻撃

近年頭角を現しつつある比較的新しい技術に「TEE（Trusted Execution Environment; 信頼可能な実行環境）」というものがあります。
TEEとは、ハードウェア（多くの場合CPU）の機能でRAM上に（ユーザが動作定義を実装可能な）保護領域を生成し、秘密情報をその保護領域と安全なCPUパッケージ内でのみ取り扱い処理を進める事で、秘密データを徹頭徹尾厳重に保護しながら処理する事を実現できる技術です。

TEEには、データを保護したままでの計算（秘密計算）に利用されるような関連技術、即ち準同型暗号や秘密分散と比較してみても計算コストが小さめで効率的であり、その上で高度な安全性を提供できるというメリットがあります。
一方で、ハードウェアに依存する以上ベンダを信頼する必要がある、サイドチャネル攻撃にはデフォルトでは脆弱といった独特な性質などにより、特に準同型暗号には相対的に安全面で劣ります。
殊に、TEEの代表的な実例である「Intel SGX（Software Guard Extensions）」は、そういったTEEの性質や、CPU及びSGX自身の抱える脆弱性を突かれ、おびただしい数の攻撃の餌食となっています。

本講義では、TEEの基本的な背景をご紹介した後、特にIntel SGXを用いた開発を実践的に行います。
SGXを用いた基礎的なプログラミングから、最終的にはSGXを利用したパスワード管理ソフトウェアやご自身の好きなSGXプロダクトの開発を行う事で、現代の情報技術における安全性と速度のトレードオフの最適解の1つである「TEE」という技術の魅力に迫ります。

そして、上記のようにSGXアプリケーションを「ビルド」した後は、それらに対してSGX攻撃を仕掛ける事で「スクラップ」します。
つまり、TEE特有の性質やSGXに対する攻撃についても実践的に体験し、TEEが決して秘密計算実現の上でのワイルドカードではない事を確かめます。
SGXに対する攻撃には、Controlled-Channel Attacks、Foreshadow、ZombieLoad、LVI、Downfall、?PIC Leakなど、名だたる高度かつ難しい攻撃が無尽蔵に存在しますが、あくまでもゼミ内で取り扱える範囲に簡略化して実践していきます。

TEEという技術は、暗号技術、OS、コンピュータアーキテクチャ、果てには攻撃を仕掛けるのであれば時に電磁気学まで入り乱れる、カオスながらも非常に魅力的な技術です。
TEEを「ビルド＆スクラップ」するという一見狂気的にも見える本講義を通じて、そんなTEEの魅力に迫りましょう。

• 緑川 志穂

• 暗号
• 実装
• プロトコル
• プリミティブ
• 解読

暗号技術は"理論"と"実装"が巧妙に組み合わさった上で成立します. どちらかが欠けても脆弱性を作ってしまいますし, 実際にはこれに加えて"その使われ方"も影響します. このため「暗号を実装する」とは一言で言えますが, 実際にはそう簡単には行きません. 正しい暗号実装と呼ばれるためには「既存の暗号解読手法の影響をどのぐらい受けるのか」「将来の計算能力向上を見据え, 危殆化を前提とした設計をする必要の有無はどうか」「そもそも実装に誤りはないか?」といった数々の検討をクリアーしなければなりません. これはとても難しく, 「暗号関係のコードは絶対に自分で書くな」と言われる所以です.

この話はAESやRSAといった具体的な暗号方式の実装にしか適用できない話ではなく, TLSやSSHといったプロトコルの世界でも成立しますし, またTPMのようなハードウェア寄りの世界でも成立します. 暗号解読でさえ, 「この手法はどんな場面で危険性が高まるのか」の検討が最も重要視されることから, 無関係とは言えません. このような意味で, 暗号実装には上(利用される側)から下(具体的な実装, 理論的根拠)までの, いわば"フルスタックな"視点が求められます.

当ゼミでは, そのようなフルスタックな暗号実装を実際に行っていただきます. 内容はプロトコルでもプリミティブでも, 或いは暗号解読や認証・認可でも何でもよいです. 事前学習開始時に相談して決めましょう. 自分が興味を持った暗号実装をやりながら, その暗号の様々な視点を学べることを目標としたいわけです.

残念ながらキャンプ期間というものは極めて短いので, たとえば「OpenSSL互換のライブラリを一切の外部ライブラリを使わずに再実装する」というような壮大な計画を立てても実装はしきれないでしょう. しかしながら, 小さくとも十分に検討し尽くしたコードを開発した経験があれば, 壮大な計画を現実化するために必要な道筋ぐらいは見えるかもしれません. 当ゼミはその一歩目を間違いなく踏み出すためのサポート役です.

• hikalium

• OS
• x86_64
• Rust
• アセンブリ
• システムプログラミング

「OSを作ってみたいなあ、でも自分には無理かも……」
と思った事はありませんか？確かに、OSと聞いてみなさんが思い浮かべるものは、おそらく巨大かつ複雑で、長い歳月をかけて多くの人々によって手が加えられてきた、とても敷居の高い魔法の物体に感じられるかもしれません。しかし、OSは基本的な部分に限ってみれば、ひとりでも思ったより簡単に書けるものなんです。

この「OS自作ゼミ」では、趣味としてのOS自作を続けていたら、いつの間にかOS開発が仕事になってしまった講師が、アプリケーションとハードウェアの狭間にあるシステムソフトウェアの世界へと皆さんをご案内します。既に自分のOSを作りはじめている方はもちろん、このゼミをきっかけに作り始めようとする方も、チャレンジ精神さえあれば幅広く対応します。また、講師が作っているOSを改造したいという方や、既存のオープンソースで開発されているOSに独自の改造を施してみたいという方も、OSづくりに帰着できることならば何でも大歓迎です！

講義内容は、みなさんの興味や希望にあわせて柔軟に対応します。コードの読み書きだけでなく、必要に応じて仕様書や研究論文の読み方など、実践的なスキルを身につけるお手伝いもします。この講義を通じて獲得した低レイヤの確かな知識は、高性能でセキュアなソフトウェアを開発する際にも大いに役立つでしょう。

このゼミに応募する上で一番大事なのは、OS自作にかける熱い想いです。皆さんからの御応募、お待ちしております!!

• 佐藤 弘崇

• コンパイラ
• 言語処理系
• C言語
• アセンブリ

普段何気なく書いているプログラミング言語というものが、いったいどうやって実装されているのか、気になったことがある人も多いでしょう。プログラムを書く人であればコンパイラはそれなりに身近な存在かと思いますが、コンパイラが内部で何をしているのか、どのようにできているのかという点に目を向けてみたらますます面白いと思いませんか？

本ゼミでは、C言語のソースコードを受け取って対応するアセンブリを出力する「Cコンパイラ」をゼロから自作します。自分の力でゼロからCコンパイラを作り上げていくことで、身近で遠い存在だったコンパイラの中身がどんどんと明らかになり、C言語の仕様やアセンブリの知識も自然と身についていきます。

コンパイラなどという複雑怪奇で大きなソフトウェアを作るなんて大変そうだと思うかもしれませんし、実際簡単なことではありません。ですが、最初は極限まで小規模なものから始め、そこから少しずつ機能を増やしていくので、実装・テスト・デバッグの繰り返しを続けるうちにどんどんコンパイルできるコードが増えていきます。あっという間に書いている本人よりもコンパイラの方が賢くなっていって驚くことでしょう。その過程を十全に楽しめるよう、大会期間前には多めに事前学習期間を設けてじっくりと開発できるようにします。実装のためのテクニックやC言語のややこしい仕様に関するフォロー、豊富なテストの提供やデバッグなどといった様々な面でサポートしていきますので、ご安心ください。

C言語は長年にわたって多岐にわたる使われ方をしてきた言語ですから、Cコンパイラを自作することにより様々な目標を狙うことができます。たとえば、自作コンパイラのソースコードを自作コンパイラ自身でコンパイルする「セルフホスト」。自分のコードのバグが予測外の箇所に悪影響を及ぼし、頭を抱えながらバグを探す経験は、セルフホスト以外ではなかなか味わえない醍醐味と言えるでしょう。他にも、既存のOSSの大きなコードを動かすことを目標としても面白いでしょう。そんなのをコンパイルできるほど完成度を上げるなんて気が遠くなると思うかもしれませんが、穴だらけの自作コンパイラであっても実は既存資産が結構読めたり動かせたりします。他人の書いた実用的なコードをコンパイルする過程で自分の実装の思わぬミスを見つけることができるため、何を動かせて何をまだ動かせないか調べていくことでコンパイラがどんどん磨かれていきます。

もちろん、これらの目標を達成できるコンパイラを作るには、それなりに多くの構文や仕様に対応する必要がありますし、出力される大量のアセンブリをかき分けてデバッグする必要もあり、決して簡単な道筋ではありません。しかしながら、このゼミを通じて、低レイヤと高レイヤの橋渡しをするための共通言語としての地位を確立している言語である C 言語と必ずや真剣に向き合うことができるでしょう。皆さんが今後どのような道を進むのかは我々には知るよしもありませんが、そのような経験は、今後いかなる方面でセキュリティや低レイヤに触れようとも必ず役立つものとなると信じております。皆さんの応募、お待ちしております。

• 中尾 圭佐

• SDR
• 無線
• IoT

無線通信ハッキングゼミでは、実際の無線通信で使われている技術を学んだ後、SDR（Software Defined Radio）を使用して実際の無線通信を受信し、通信内容の解析を行います。また、無線機を解析したり、実際にジャミングやリプレイ攻撃などを行って、意図しない動作を起こせるかどうかの検証も行います。
無線通信に興味がある方、ちょっと違うレイヤーのセキュリティを学んでみたい方の応募をお待ちしています。

• 三村 聡志

• IoT
• 解析
• ハードウェア

IoT機器の分解・解析を通して、組込機器が動く動作を明らかにするリバースエンジニアリング手法について学びます。
また脆弱性の有無についても検討を行い、ハードウェアとファームウェアが協調動作する環境での脆弱性の発見も試みます。

今後 IoT 製品がどんどん増えていく世の中に向けて、分解しながら物作りのためのアイディアの源泉を得るもよし、徹底的に分解を進めてすべてを明らかにする喜びを全力で満たすもよしの内容となっています。仕組みを知ること、解析することに興味がある方からの応募をぜひお待ちしています。

• 松浦 幹人

• コンパイラ
• 言語処理系
• C言語
• セキュアコーディング

コードサニタイザとは、コンパイル時に追加の命令を挿入することでプログラム中のバグを実行時に検出するコンパイラ内蔵機能のことです。
「そんなもの使ったこともない！」と思うかもしれませんが、静的検査では検知できないバグも発見することができるため、LinuxやChromiumの開発などに使われている便利機能となっています。
サニタイザは、検出されるバグの種類によりいくつかの種類に分類できるのですが、代表的なものはアドレスサニタイザ(ASan)といい、ポインタの扱いを誤ることなどによるメモリ管理のバグを発見することができます。

本ゼミは、既存のコンパイラを改造することで手っ取り早くサニタイザのような付加的機能を実装する部分を楽しむことを目標としています。
大会期間中には、各種サニタイザか受講生の考案した独自のサニタイザを実装する形で進行していこうと思っています。
サニタイザの実装には、コンパイラ側のコード生成の改造とともに、時として`malloc()`などのランタイムライブラリの変更が必要となるため、双方に関する知見を深める良い機会になると信じています。
コンパイラに興味がある方、ランタイムでの保護に興味がある方、それらに限らず、皆さんのご応募をお待ちしております。

• 松岡 航太郎

• TFHE
• 準同型暗号
• 秘密計算
• 暗号理論

「暗号のままで計算ができる」のが準同型暗号です. このゼミではその中でも「任意の回数論理演算ができる」TFHEという暗号を実装します. このゼミは「準同型暗号の応用」より「準同型暗号そのものを構成するにはどうしたらよいか？」という「暗号学の理論とその実装」を軸としたゼミです. 本ゼミでは「暗号のままで計算ができる」ということを目指します. 準同型暗号の「暗号としての安全性や攻撃法」はあまり扱いません.
進め方としてはまず暗号を数式として考え, それをプログラムに落とし込むということを繰り返して進めます. そのため, 数学へ忌避感がないことが望ましく, 初等的なベクトルと確率がわかっているとベターです.
私は未踏期間中にTFHEの独自実装(https://github.com/virtualsecureplatform/TFHEpp)をフルスクラッチした経験が有ります. TFHEは簡潔で, 数学として美しく, エンジニアリングとしても高速化や応用の余地があって楽しいものです. 準同型暗号は近年活発な分野で, 今も新しい研究成果が次々に出ています. 皆さんのやる気次第ではこのゼミの内容が学術的未踏領域に入ることもありえるでしょう. 誰もやったことのないことに挑戦する意志のある人を期待しています.

• 紫関 麗王

• Rust
• Linux
• アンチウィルス
• システムプログラミング

皆さんが手元で使っているマシンのOSはWindowsやMacOSが多数でも、多くのサーバではLinuxが稼働しています。
また、StatCounterの集計によると、Linuxデスクトップの割合も4%を超えました。( https://gs.statcounter.com/os-market-share/desktop/worldwide )
Linuxを対象とするアンチウィルスは、市場規模はWindowsと比較して小さいものの、攻撃者に狙われないわけではありません。

当ゼミでは、Rustを用いてLinux向けのアンチウィルス、及びそのコンポーネントの開発を目標としています。

アンチウィルスを構成する要素は非常に多く、「完成」はありません。
今回は短い期間でゴールを設定し、そのゴールに向かって開発をしていく予定です。

自分で検知手法を考えたり、逆にそのバイパス手法を考えたりしていきましょう。

Rustやアンチウィルス、Linuxについての知識が無い方でも、とりあえず応募して当日までになんとかするのも手です。

「自分にはできないかも」とは考えず、とりあえず課題に取り組んでみて下さい。

Rustが好きな方、アンチウィルスが好きな方、Linuxが好きな方、それらに興味があり、これからやっていきたい方のご応募をお待ちしております。

• 森 真誠

• Hypervisor
• VMM
• ハイパーバイザ
• 仮想マシン
• UEFI
• Rust
• アセンブリ
• 軽量ハイパバイザ
• Arm64

「ハイパーバイザ」「仮想マシンモニタ」という言葉をご存知ですか？
"VirtualBox"や"QEMU-KVM"というとピンとくる方もいるかもしれません。
名前は知らなくても、「OSの上で別のOSを動かす事のできるソフトウェア」を使ったことがある方は多いのではないでしょうか。
近年ではクラウドのVPSなどで気軽に自分で用意したOSやソフトウェアを利用できるようになりましたが、これもハイパーバイザの仮想化技術のおかげです。

もはや必須となった仮想化技術ですが、中身については案外知られてはいません。
ハイパーバイザはどうやって複数のOSを一つのマシンの上で動かしているのでしょうか。どんなOSでも動かすことはできるのでしょうか。

世の中で主に使われているハイパーバイザは非常に良くできており、これらと同等のものを一から作り上げるのは時間と労力を要します。
しかし実装する機能を絞れば、少ない実装量でも複数のOSを一つの物理マシン上で動かすことが可能です。

ハイパーバイザを自作することでコンピュータシステムを深く理解することができます。
ハイパーバイザはOSやアプリケーションと言ったソフトウェア側とCPUやデバイスなどのハードウェアを仲介する、「ハードウェアのふりをするソフトウェア」です。
そのためOSとは違い、ハイパーバイザは出来るだけ存在感がないことが求められます。その割には処理内容が巨大で難しく、デバッグも困難です。
そのようなハイパーバイザを自作するということは、ハードウェアの作りとOSなどのソフトウェアの実装を理解する必要があります。CPUがどうやってソフトウェアを実行しているか、デバイスはどのように作られてどのように使用されるのかなど幅広い知識が身につきます。
そのような知識はセキュリティやシステムソフトウェア開発全般においてとても役に立ちます。

本ゼミでは、フルスクラッチでハイパーバイザを自作し仮想化技術の仕組みやコンピュータシステムについて理解することを目標とします。
ハイパーバイザはArm64 CPUを対象し、ハードウェアの上で直接動作するType-I ハイパーバイザと呼ばれるものを想定しています。

他にも、軽量ハイパバイザと呼ばれるハイパーバイザ上で動くOSを一つに限定したハイパーバイザの自作や改造も可能です。
OSが一つしか動かないならば何のためのハイパーバイザか、と思われるかもしれませんがOSとハードウェアの間に挟まることで、双方のやり取りを監視することが可能であり、OSやアプリケーションの解析をしたり改変することが可能です。また本来のハードウェアに追加で機能を実装することも可能でマシンの機能の拡張なども行えます。

どのような講義をするかは受講生の方と相談しながら決定する予定です。一からハイパーバイザを作って複数のOSを動作させたいというのも良いですし、既存のハイパーバイザを持ってきて改造したいというのも良いです。軽量ハイパバイザを用いてデバイスの機能拡張を実現するも良いですし、OSの解析をするというのも良いです。
セキュリティ・キャンプ期間中だけでハイパーバイザを理解し実装することは難しいため、事前学習期間中に手を動かしてもらう予定です。
講師はCPUアーキテクチャはArmの64bitモード(AArch64)、プログラミング言語はC/C++/Rustのサポートが可能です。
それ以外のアーキテクチャを使用することも可能ですが、皆さんの知識や手を動かせる時間などと相談の上決定します。

低レイヤーが初めてという方も、「OS自作したから今度はハイパーバイザを」という方も、熱意のある方ならどなたでも歓迎します。
皆様のご応募をお待ちしております。

• 末田 卓巳

• 改造
• Linux
• 工作
• IoT
• Web

本ゼミでは、市販の無線ルーターに部品をくっつけてラジコンに変貌させます。その過程で、電気回路からHTTPに至る全てのレイヤーに触れるため、コンピューターを構成する技術スタックの全体像を具体的に知ることができます。電波法令に定められた技術基準適合証明（いわゆる「技適」）への対応も含むので、魔改造にあたって遵守する事柄も同時に理解できます。コードは書けるけど低いレイヤーに触れたことがない、一風変わった技術の学び方に興味がある、見た目に楽しいハードを作ってみたい、改造の具体的手法が知りたい…といった方を主に想定しています。

• 川畑 公平

• Detection-as-Code
• Detection Engineering
• Adversary Emulation
• BlueTeam

Detection-as-Code（DaC）は、検知ロジックをコードとして記述し、管理することで、ソフトウェア開発のベストプラクティスを脅威検知プロセスに適用するモダンな手法です。Gitを使ったバージョン管理、プルリクエストによるコードレビュー、CI/CDパイプラインによる自動テストとデプロイメントを活用した検知ルールの開発を通じて、常に進化している現代のサイバーセキュリティ環境における効果的な脅威検知を目指します。

本ゼミでは、DaCの基本から始めて、以下の技術スタックで構成されたDetection Engineeringプラットフォームを活用し、セキュリティ演習を通じて検知ルールを開発します。

テレメトリの収集: Sysmon、SilkETW、DTrace on Windows
検知ルールのバージョン管理とCI/CD: GitHub、GitLab
検知ルールの記述: Sigma、YARA
検知ルールのテスト: Chainsaw
検知の可視化: Grafana

演習は、Redチーム役の講師による、実際に悪用されている攻撃手法を模倣した攻撃（Adversary Emulation）からスタートします。受講生はBlueチーム役として、収集したテレメトリデータを基に攻撃を分析します。その後、受講生はDaCに従い検知ルールを開発し、再度の攻撃試行を検知できるか実際にテストします。発展課題として、テレメトリ収集機能の拡張やCI/CDパイプラインの高度化にチャレンジすることも可能です。

講師による個別サポートを受けることができるため、これまで脅威について学んできて最近開発にも興味が出てきた方、逆に開発について学んできて最近脅威にも興味が出てきた方など、技術的なバックグラウンドは問いません。本ゼミを通じて脅威に対抗するための実践的なDetection Engineeringスキルを一緒に磨いていきましょう！

• 松下 祐介

• Rust
• プログラム検証
• 形式検証
• RustHorn
• Creusot

ソフトウェアが複雑で巨大になり、社会のあちこちでソフトウェアが使われている現代において、ソフトウェアの安全性はとても重要です。

## Rust

2015年にリリースされた Rust というプログラミング言語は、C/C++ のような低レベルのメモリ操作を許す一方で、所有権型システムという高度な仕組みを導入し、不正なアクセス競合を防ぎ、ソフトウェアの安全性を大きく高めました。

例えば、Google の Android OS は C/C++ に加えて近年 Rust を採用し、セキュリティ上の脆弱性を大きく減らすことに成功しています。

• Memory Safe Languages in Android 13

## プログラム検証

ソフトウェアの安全性を高める特に確実な方法が、プログラムを解析して動作の正しさを数学的に保証する「プログラム検証」です。
例えば、宇宙船や航空機の制御系、セキュリティ基盤、オペレーティングシステムなど、バグがあったら困る、という場所で、プログラム検証が活躍しています。

## RustHorn、Creusot

Rust の所有権型システムは、メモリ安全性を保証してくれるという意味で、ある意味で軽量なプログラム検証を行っています。
しかしそれにとどまらず、プログラムの入出力の正しさといったより強い性質も、Rust の型の保証を上手く利用することで効率良く検証できる、ということが分かってきました。

講師 松下 は RustHorn という、Rust プログラムを検証するための新しい手法を提案しました。可変借用を通した破壊的更新を扱うのが難しかったところ、「預言」という未来を先取りするアイデアによって、これを一般的に解決しました。
この研究は2021年にトップジャーナル ACM TOPLAS で出版されました。

• RustHorn: CHC-based Verification for Rust Programs

さらに最近、RustHorn の技術を基盤として、Creusot という本格的な Rust 検証ツールが生まれて、注目されています。
特に、Rust で書かれた SAT ソルバ（論理の問題を解くソルバ）が Creusot を使って検証されました。

• Creusot（github）

## このゼミ

この開発ゼミでは、Rust プログラム検証の分野の第一線で研究する松下が講師となり、最先端の技術に触れ、頭と手を動かし、研究の世界の一端を体験してもらうこと、プログラム検証の楽しさを知ってもらうことを目指します。

具体的に何をやるかは受講者の意向に応じて相談して決めたいと思います。
例えば、Creusot を使って本格的な Rust プログラムを検証してみること、RustHorn や Creusot を改造してみること、あるいは Rust 検証ツールを自分で作ってみること、などが考えられます。

意欲溢れる皆さんの応募を待っています！！

• 凌 翔太

• AI
• ペネトレーションテスト
• LLM

• ChatGPTをはじめとしたLLMを組み込んだシステムは世界的な広がりを見せています。同時にこうしたシステムに対する攻撃手法としてプロンプトインジェクションが注目を浴びています。誤字脱字を利用したものから、感情に訴えてくるもの、多言語を用いたものまで、様々な手法があります。
  プロンプトインジェクションを経由して、SQLインジェクション、XSS、SSRF、RCEを経て、システムの破壊や機密データを漏洩につながるため、影響範囲は広いです。一方で残念ながら、手法が体系立てられておらず、テスト手法が確立していません。
  本講義では世界で通用するオープンソースのツール（注釈）を開発することを目的とし、プロンプトインジェクションの攻撃パターンを網羅的に生成するツールを開発します。また、既存のプロンプトインジェクションの対策（オープンソース、商用）も用いて、それらの検知率、検知回避策手法を研究します。
  
  （注釈）2022年のセキュリティ・キャンプの講義では米国ラスベガスで開催されたセキュリティカンファレンス「Black Hat USA」にて開発したツールを発表しました。参考URL：https://blog.security-camp.or.jp/posts/z9-blackhat/
  

• 坂本 優太

• 宇宙開発
• 探査機
• 人工衛星
• 組み込みシステム
• Rust
• システムズ・エンジニアリング
• 開発体験
• チーム開発

一緒に探査機を作ってみませんか？

このゼミでは惑星探査機の開発を題材として，複雑なシステム開発への向き合い方を，実際に手を動かしながら考えます．

惑星探査機や人工衛星，宇宙開発と聞くと，一見遠い世界のことのように思うかもしれません．しかし，現代の我々は宇宙と切っても切れない関係にあります．便利な天気予報は常に雲などを観測している気象衛星があってこそですし，スマートフォンの位置情報取得機能はGPS/GNSS衛星によって成り立っています．地震や洪水などの災害時においても，地形がどのように変化したかなどの観測における人工衛星の役割は非常に大きなものとなっています．

即座に生活の役に立つものではなくとも，人類の知や活動の領域を押し広げるという面でも宇宙は大きな領域です．我々が理科の教科書などで月の裏側や太陽系の惑星の詳細な様子を知っているのも，人類がそこまで探査機を送り込んできたからです．近年では，「はやぶさ2」のカプセルの帰還や，小型月着陸実証機の SLIM の成功なども話題になりました．

みなさんは，人工衛星や惑星探査機のような宇宙機がどのような仕組みで動いているか，どのように作られているか考えてみたことはあるでしょうか？

宇宙機は非常に複雑なシステムです．なぜ非常に複雑なのかと言えば，考えなければならないことが多いからです．まず，宇宙にコンセントはありません．そのため，自分で発電能力を持つ必要があります．多くは発電手段として太陽電池を用いますが，そこまでパワーのある発電手段ではなく，使える電力にかなりの制限がかかります．太陽電池があったら発電自体は安泰というわけでもなく，適切に太陽の方向を向くために制御しないといけません．制御しやすいような機構も考えた方がいいかもしれません．そもそも制御するためには自分が向いている方向や太陽の方向をどうにかして得ないといけません．ずっと太陽の方向を向いていても，放熱ができず部品の温度が数百度になって不可逆的に破壊されてしまうかもしれません．

先述のように非常に複雑なシステムは，一人で作ることはほぼ不可能です．機械的な構造，熱や電力の収支，姿勢決定/制御，コンピュータ・ボード，そしてソフトウェアなどすべてを設計し，開発する必要があります．特に宇宙機はデプロイ環境やワークロードが特殊だということもあり，それぞれの設計に特有の難しさがあり，プロフェッショナルが必要になります．それだけでなく，太陽電池の例からも分かるように，それぞれ別々の専門領域を持った人間同士が適宜連携し，調整しながら開発を行う必要があります．

つまり，個々の他分野の高い技術が必要になるだけでなく，適切に連携させる必要があります．この点に個別の技術とは異なる別の難しさがあるのです．この複雑な連携のための方法論として，システムズ・エンジニアリングという分野があるのですが，これはアポロ計画，つまり実際の宇宙開発プロジェクトを大きな契機として発達しています．

このゼミでは，模擬的な惑星探査機の自作を通して，システムズ・エンジニアリング的な観点を持ってチーム開発を体感してほしいと考えています．他の受講生と，そして講師と協力しながら，ひとつの探査機というシステムを作っていきましょう．自分より上ないし下のレイヤや，別の人が開発しているサブシステム，システム全体，開発体制のことを考えながらものづくりをする経験は，宇宙開発に限らず，あなたが将来大きなものづくりに関わる時に確実に役に立つと信じています．皆さんの応募をお待ちしています．

【ミッション概要】
現在，ある惑星の探査がホット・トピックになっています．この惑星には，既に周回軌道上に探査機が送り込まれており，データが送られてきています．ただし，周回軌道上からの観測手段や精度は限られており，現地に降りてみないと分からないこともたくさんあります．そこで，今進行しているのが着陸型の探査機の開発プロジェクトです．プロジェクトがまだ採択されたばかりなので，詳細はあまり決まっていません．サイエンス・チームが周回機から送られてくるデータを吟味し，段々と探査候補も決まってくることでしょう．

着陸機を開発するのは技術的にもコスト的にも大変なので，とても大きな期待がかかっています．あまりリスクは取れません．確実に何かがありそうなことが分かっているもののみを調査したいです．とはいえ，降りてみないと分からないことがあるから着陸してみるのに，降りずに判断したもののみを調査するのはある種本末転倒です．そこで，この着陸機には子機を搭載することになりました．子機は親機とは別に行動し，親機やまた別の探査機による詳細観測を行う価値がありそうなものを探すことが目的です．あなた方のチームはこの子機を開発することになりました．


【受講を考えている方へ】
ものづくりが好きな人を歓迎します．
宇宙開発に興味がある人ももちろん歓迎しますが，宇宙開発はあくまで題材であり，宇宙関係の知識や興味は特に要求しません（あるとより楽しめるかもしれません）．

このゼミではチーム開発を行い，ハードウェアも扱う都合上，講義・開発の大部分を事前学習期間中（6~8月）に行うことになります．事前学習期間中にできるだけ開発を進め，最低週1程度適宜オンラインで話す機会を設けたいと考えています．そのため，余裕を持った予定の確保・確認をお願いします．実際の予定調整は受講生同士の都合などもあるため柔軟に行います（テスト期間などでは学業を優先してください）．

このゼミで自作する探査機は色々とデータを取得し，移動することが求められます．そのため，各種センサやアクチュエータをマイコンで制御することになります．この探査機本体の制御や，探査機とやりとりする地上局側において，ソフトウェア開発をすることになります．

ソフトウェアの開発には Rust とC言語を用います．そのため，C言語の基礎的な文法は一通り分かり，なにかしらのプログラムを書いて動かしたことがあるのが望ましいです（ただし，未経験でも応募後や事前学習期間中に自走できる熱意がある場合は応募をためらわないでください）．
Rust については入門からサポートしますが，『The Rust Programming Language』や『The Rustonomicon』『The Embedded Rust Book』などをなんとなくでもやっておいてもらえると，スムーズに実践的な開発ができる時間が増えると思います．


また，受講にあたり，『Kerbal Space Program』ないし『Kerbal Space Program 2』を多少プレイしておくと，宇宙開発がどのような世界観か分かりやすくなると思います．ただし，ハマって時間を溶かして応募できなくなってしまうと本末転倒なので，プレイするのは応募後にしましょう．お金に余裕が無い人や，ハマりすぎてしまうのが怖い人は，ニコニコ動画や YouTube にあるCeVIO実況プレイ動画をいくつか観てみると面白いと思います．個人的なおすすめは『Kerbal宇宙開発日誌~ニコニコ重工~』（https://www.nicovideo.jp/user/1631016/series/11971）です．量が多いので観すぎに注意ですが，チラっと見る分には気分転換や応募課題の参考にもなるかもしれません．

• 内田 公太

• CPU
• コンパイラ
• アセンブラ
• FPGA
• Verilog
• C言語

このゼミでは独自のCPUとコンパイラを作ります。自作コンパイラ（とアセンブラ）が自作CPU用の機械語を出力し、それを自作CPUで実行するという流れです。CPUとコンパイラは既存のアーキテクチャを参考にはしますが、模倣せず自分で一から仕組みを考えます。このゼミではCPUはVerilog、コンパイラはCで作るのが標準ですが、慣れている言語があればそちらでもOKです。

このゼミの特徴は、単に「どっちも作る」だけではなく、両方を「並行して作る」ところにあります。相互に影響を与えながら作っていきます。最初は整数を表示するだけのCPU（機能が少ないためCPUとは呼べないかもしれない）と、1つだけ整数を読み込むコンパイラを作ります。次はCPUを加算に対応させ、コンパイラが「整数+整数」を認識できるようにする、というように、段々と機能を追加していきます。このゼミでの目標は加減算と乗算が実行できるCPUとコンパイラを作ることですが、余裕のある人は独自の機能をいくつ追加してもかまいません。

CPUとコンパイラを作る場合、普通はCPUのISA（命令セット）をまず決めて、CPUとコンパイラをそのISAに準拠するように作っていきます。このゼミでは、あえて最初にISAを決めず、CPUとコンパイラを並行して作りつつ決め、必要に応じて修正を加えていきます。CPUとコンパイラを並行して作ることで、両方を学ぶことができるという自明な点以外に、次のような利点があります。
A.コンパイラの実現に必要な最小限の機能をCPUに追加すれば済むため、プロジェクトをコンパクトに維持できる。
B.CPUとコンパイラの両者が作りやすいように、互いの役割分担を調整できる。

CPUの作り方は様々ですが、このゼミではCPUボードをはんだ付けで組み立てるところから始めます。CPUボードはFPGAボードを中核として、いくつかの表示素子、スイッチ、USBシリアル変換モジュール等から構成されています。キャンプ期間でそれらを組み立て、自作CPUのプログラムを書き込み、動作させます。集中して取り組める開発期間は3日間しかなく、非常に短いです。事前学習期間に受講者の皆さんにFPGAボードを配る予定ですので、キャンプ当日までにFPGAの扱い方を練習しておくことをお勧めします。

コンピュータがプログラムを実行する仕組みを一気通貫で体験したい、自分でその仕組みを作ってみたい方の応募をお待ちしております。3日間という短期間でCPUとコンパイラを作る必要があるため、それらの開発に必要なスキルを持っている必要があります。具体的にはVerilogとC（あるいは同類の言語）を使いこなせる必要があります。ただし、今それらが未経験であっても、熱意があり、応募時点までにある程度の知識を身につけられたなら、是非応募してください！

• 田村 康将

• 耐故障性
• 分散合意
• リーダー選挙
• 並行プログラミング

現代では，コンピュータシステムは基本的には常時アクセスが可能で，動き続けていてくれるような安心感のあるものになっているかもしれません．しかしながら，コンピュータだって機械ですので，裏で動いているモノは「すでに故障しているもの」か「まだ故障していないもの (いずれ故障するもの)」のどちらかです．また，物理的な故障だけではなく，ソフトウェアの不良動作や悪意のある不正動作に対する備えも重要です．このような様々な故障に対応しながらサービスを継続的に提供する能力 (耐故障性) は，コンピュータシステムの信頼性を支える重要な役割を担っています．

このゼミでは耐故障性を高める基盤技術としての「分散システム」と，それをうまく動かすための仕組みの一つである「分散合意」について，代表的なプロトコルの実装を通して学びます．多くの方にとってあまり馴染みのないテーマかと思いますが，複数のコンピュータが通信によって一つのシステムのように振る舞う仕組みや，通信が必要であることから生じる課題とその解決方法などに興味がある方の参加を歓迎いたします．

ゼミの性質上，想定する開発言語としてGo言語を設定しています．
一方で，自分の得意なプログラミング言語で頑張りたいという受講生も歓迎します．