seccamp 2023 講師参加記.md

seccamp 2023 講師参加記

セキュリティキャンプにL1 暗号化通信ゼミ講師として参加していました. しばらくキャンプ関連の記事は書いていなかったのですが, 久々のオフライン開催の後ということもあり, とりあえず書いてみようかなと思う次第です.

プロトコルコースを含めL1全体の方針は同じくL1講師をされていた @tex2e さんの参加記( https://tex2e.github.io/blog/misc/seccamp2023 )によくまとめられているので, この記事ではその点を端折ったプリミティブコース側の視点をメインとしています. なのでこちらも合わせて読んでいただけますとより一層「L1ゼミというゼミは何をやっていたのか」を理解いただけるのではないでしょうか.

私達の担当したL1ゼミは2コースに分かれており, 私は特にプリミティブコースという極めて理論に近いコースを担当させていただきました. その目標設定は大目標である当該論文の全体理解 + 読み進める・実装する上での小目標をその都度, という形で実施しました. また, 小目標のステップを可能な限り小さくとり, それによって漸進的に進めることを考えました.

TL; DR 来年度の受講を考えている方へ

そもそも来年私が講師として呼ばれる保証がない, ということを念頭に置いてください. セキュリティ・キャンプの講師は基本一年単位なのです.

運良く用意された場合, 私が受け持つことになるゼミはおそらく理論系のゼミになりますが, 実装も当然やります. なんとなれば, 「理論はわかるけど実装がわからない」という方はその旨お伝えいただければプログラミング技法に焦点を当てた講義も可能です. あくまで私は今年プリミティブコースで理論系を教える講師を務めたというだけですので, 理論しかできないのかと思われる必要はありません.

基本的には暗号に関する熱意・関心以外は不要です. 難しそうな応募課題がまた出るかと思いますけれども, しかしよく調べるとハードルはそこまで高くないことに気づかれると思います. どうか尻込みせず果敢に立ち向かってほしいと思います.

自然科学・数学を学ぶとはどういうことか

(@tex2eさんがアドラー心理学を推し, そしてそのあたりの記述があったので, counter-partとして記します. まあまあ冗長かつ理念的なものなので, 読み飛ばして頂いても構いません. )

私達のゼミの特色は「目標設定を受講者自らが行うこと」にあり, そしてそれをやり遂げることができるように我々はサポートします. このため, どうしても「この手法を教えるときはこのような道筋がよい」という筋道は立てづらいです. なので今回は自然科学全般に通用する手法のサブセットを基本的な方針に据え, 都度受講者の方向性によって必要な公理を組み替えるような形で議論を進めました. ゆえに私の教え方の基礎には自然科学や数学における一般論が多分に含まれます.

さて, 自然科学の基本的立場に「結果から作った仮説は必ず検証されなければならない」というものがあります. これについては何を当然と思うかもしれません. では「『知っている事柄』と『理解している事柄』の間にはどのような差があるのか」と問われた際にはどうでしょうか. 前者は後者を包括しますが, 後者を特徴付ける条件はよくわかりません. 実際哲学には認識論(Epistemology)と呼ばれる一大分野があり, それはこの条件を希求する学問です. 長くなるので本記事ではこれ以上踏み込みません.

私が数学を学び始めてからしばらく経過したとき, 私はこの「理解とはなにか」問題に直面しました. 今でも答えは出ていない¹のですが, 少なくともわかりやすい基準が一つ存在することは認識しました. それは公理から演繹されるすべての流れを論理学的に整合するか否かという観点から検証することです.

しかし数学がすべてただの検証で終わるわけはありません. 数学を学ぶ過程で最も重要なのは「この結果はこの前提から導ける」というグラフ構造を生み出すために証明を書くことです. 証明を書けることは道のないところに道を創発することであり, そしてその道の論理的整合性を自ら検証できることです². この点で「結果から作った仮説は必ず検証されなければならない」という自然科学の基本的立場を数学も共有していると言えます. もちろん, 一番難しいのは道を創発するその作業であることも共通します.

Peirceは帰納・演繹・仮説形成(アブダクション / レトロダクション)の3種類に論理的推論を分類し, そして帰納的な証拠集め → 仮説形成による創発 → 演繹による検証可能な実験の考案 → 帰納的な証拠集め → ...というループの形で自然科学の営みを定式化しました³. 数学では演繹完了 = 正当ですが, 一般にはそうではありません. たとえば陸地で貝殻の化石が発見されたからといって「ここは昔海だったのだ」と断じるには足りませんし, 「昔海だったならばウミユリの化石もあるはずだ」という主張を演繹したところで見つからなければ意味がありません. 何なら貝塚の可能性もありますし, 湖に生息するウミユリがいた可能性もあります. このように「昔海だったならば」から成立する演繹の先に対する検証は帰納的に実施しなければなりません.

この三分類を用いて言うのであれば, 数学における定理の理解とは次のように言えるでしょう: 定理の前提から定理の結果に至るまでの間の論理的繋がりを自ら演繹的に検証でき, そしてそのつながりを自らの仮説形成の選択肢に組み込めること. Aが正しければBが従うのだとすれば, 究極的には数理論理学でやるように「Aを結論する恒真式からの証明図」を描くことでBを真の意味で理解できるのだとも言えるでしょう.

上の結論は所謂Bourbaki styleとして現代数学では至極当然の結論です. すれば「Éléments de mathématiqueをすべて読みきらなければ我々は数学ができないのか」という疑問にも当然到達します. 実際にはその限りではなく, 特に帰納的に検証されている(有名な)定理に関しては認めることが多いでしょう⁴. その点で数学は一種経験的なものなのかもしれません.

セキュリティ・キャンプにおいて

今回プリミティブコースではSupersingular isogeny diffie-hellman (SIDH)と呼ばれる鍵交換方式に対して提案された攻撃手法(Castryck-Decru Attack)を実装していただきました. この攻撃手法は2022年に提案されたものであり, 特にstate-of-the-artに相当するものです. 使う道具は膨大⁵で, 真の意味で理解するにはセキュリティ・キャンプの期間はあまりに短いです. 一年はほしいですね.

まずやったことは論文の読み方を教えることでした. 最初にVCで何か疑問点はありますか?と問うたところ「仮説の上に仮説を重ねてしまい, 結局正しい主張がどこにあるのかわからなくなる」と悩んでおられたので, ではまず自然科学の方法論を体得してもらうべきだろうと考えたのです.

「体得」というとあまり良くない印象を持ちますが, しかしPolanyiの暗黙知理論⁶のような経験的感覚は言語的伝達の難しいものです. そして「この証明はなんだか成立しなさそうだけど成立するのか」というような感覚は論文を読み慣れた人にはよくある感覚でしょう(小平先生の数覚という言葉⁷にも近いものでしょうか). これこそ自然に論理を積み重ねられるからこそ得られる経験的感覚であるため, まずは無意識に論理的なチェックを済ませられる状態になってもらう必要があると考えたのです.

上述のような方針そのものは受講生にも詳らかに説明しつつゼミを進めました. 教育理論の論者には「教育方針を教えることは良くないことだ」という主張もありますが, 少なくとも私は正解でも不正解でも, 或いは私自身に証明がよくわからなくても, すべての場合に「それは本当ですか?」と問い直すような方針で進めていたので, 所謂「楽をする逃げ道を見つける手助けに教育方針をexploitする」というような状況にはなりませんでした. 寧ろ思考を整理するためのパーツとして説明した方針が役立つことのほうが多かったと感じています.

論理的積み重ね自体がスムーズに進むようになってきたところで, 今度は時間が足りないという問題に直面します. 当初よりそれが難しいことは承知していたので, ここでは「論文の主張を理解することのみに専念する」という方針を取りました. その代わり, 認めて公理として扱った事実を明示的にメモすることを伝えました.

理想的にはすべてを理解したいところですし, 私個人の指針として「微分値が正であれば, その幅がどれだけ小さくても, それは成長である」と思っているところでもあるのですが, でもキャンプ中に動くコードを書きたいという気持ちもあります. ここでは後者に比重を置き, 「30分〜2時間調べてわからなければ一旦認めて先を読む」「一般論は事後課題とし, 論文を先読みして最低限必要な流れに組み込まれているものを優先して読む」という方針で読んでもらうことにしました.

また, この頃から週に一度程度設定していたゼミでは論文の内容を直接書いていってもらうことをやめました. 代わりに「実際にここに書かれている流れはどのような流れか, 疑似コードの形で表現できますか」「このコードはどこに対応し, その根拠はなんですか」といった形で, 読んでいることを前提として実際に何かを生み出す第一歩となる議論を実施するようになりました. テスト期間も重なりここからはあまり議論の時間は取れなくなってしまいましたが, ここから先はほぼ独力で議論を進められるようになっていきました.

時間だけ見れば一番時間を消費したのは論文の読み方に関してです. しかしこのパートは段階を踏むための基礎であり, そして大きな複利効果を持ちます. 実際, キャンプ本番期間が始まってから早くも二日目で実装は完了してしまいました. その頃には既に「参考文献を参照せよ」とされている箇所を読みに行っては読むべき場所の検討を付けてそこだけを重点的に読むようなことができていました. また今回対象にした攻撃には実は参考実装があり, 完全に詰まった際にヒントとして見に行っては理解を再整理してコードに落とし直すようなこともできるようになっていて, 同時に「理解できておらず認めている箇所」もきっちり把握している状態に到達できていました. 私から教えられることはもう殆ど教えてしまったとも言えます.

いきなりキャンプ期間に入ってしまいました. 上記のように2日目までで実装は終わってしまったので, その後は読み飛ばしていた高速化パートを改めて読み直し, 高速化実装を考える作業になりました. ただし, ある高速化手法に関しては期間内の実装が難しいと判断し, 結果としてマルチスレッドの実験実装をする方向に決まりました. SageMathは主にcypari2パッケージ周りでマルチスレッドに対応できておらず, このためSageMathのプロセス自体を複数起動するという原始的な対応をすることになってしまいましたが, 導入前よりは高速にできてよかったのではないでしょうか. オフラインということもありプロトコルコースとの交流もよりしっかりなされていたようでよかったです. でも事前学習期間にあまり交流の時間を取れなかったのは課題ですね.

実はチューターの @anko_9801 さんもSSHプロトコルの実装をされていたので, そちらも時たま見つつ進めていました. OpenSSHにはundocumentedなコンパイル時マクロがいくつかあり, それを使うとデバッグ情報を常にログに吐けるとか, クライアント - サーバ間の通信をデバッグする効率良い方法についてとか, そういったことをそっちでも教えることになっていました. 完全な完成まではいかなかったようですが, 是非完成した状態を見てみたいですね. これは私信です.

また, 私は私でTPMとずっと戯れていました. LT大会で発表したスライドとリポジトリだけ置いておきます:

この詳細もどこかで書きたいのですが, それだけでネクストキャンプの講義一個分ぐらいになってしまうのでどうしたものか. TPMのソフトウェアスタックをフルスクラッチする人はあまりいないんですね.

終わりに

暗号の話とかセキュリティの話をしているのかと思ったら数学の哲学の話をされて困惑された方はどのぐらいおられるでしょうか. すみません. 私は私で未だに理解という言葉の意味がわからないままに数学をやり続けています. Hermann Weyl『数学と自然科学の哲学』やHenri Poincaré『科学と仮説』の話もしたいのですが, 流石に無関係なのでやめておきましょう.

L1ゼミは暗号化通信ゼミという名の通り暗号化通信に関する事柄ならなんでもやるゼミで, 特にプリミティブコースは理論と実装のうち理論を重要視します. キャンプ中は我々のゼミの周り3面がホワイトボードで覆われていて, そこには数式やらネットワークシーケンス図やらが所狭しと書き込まれており, さながら大学の研究室のようでした.

暗号理論は理論と実装の間に位置しており, 両方の視点を必要とします. しかし理論, 実装そして両者の接続部分のギャップを学ぶことは容易ではありません. 私の活動がその一助になれば, という気持ちが一つのモチベーションです.

セキュリティ・キャンプは修了後が本番だとよく言います. このことを念頭に置くと, 我々講師が行うことはさながらロケットの発射角調整のようです. 受講生の方々の中には自分で飛ばせる方がおられるかもしれませんし, いや飛ばせないけどやってみたいという方もおられるでしょう. 我々はそれを飛ばす方法を教え, そして飛ばすために必要なすべての要素を教える用意をしています. 既に飛ばせるのであれば, それをより遠く高く飛ばせるような手助けをしましょう. セキュリティ・キャンプを私はそう考えていますし, そのお手伝い役自体は果たせたかなと思います (2日目と4日目の遅刻は申し訳ないです...).

重要なのは, 個々人の目標点は異なっていて良いというところです. L1ゼミのおふたかたはそれぞれ「最新研究を一本真面目に読み下してみる」「既存製品の利用シチュエーションを増やす」というincomparableな結果を出しています. それをどちらがすごいと言うことは当然できません. また「成果物の全体コード量が少ない」という批判があるかもしれませんが, L1ゼミが(極端な話)コードを書くゼミではないという旨は本記事をお読み頂けた方々にはご理解いただけるかと思います.

最後になりましたが, 事務連絡をしばしば見落とす私に対して辛抱強く連絡頂いたLプロデューサの松岡さんを始めとしたセキュリティ・キャンプのチューター⁸・講師・事務局の皆様, そして何より私がしばしば口走る適当な主張への是正を始めとした無茶へと対応頂きつつ一緒にL1ゼミを実施された@tex2eさんへの感謝を述べます. オフラインはやはり楽しかったので来年もできたらいいですね.

哲学書の主張やその他書籍の記述はあくまで「ある人はこう考えた」というだけであって, 答えではありません. なぜならば, 認識論に限らず哲学の研究対象である"世界そのもの"は検証不可能であるからです. それはただの仮説の束として取り扱うべきであり, もちろん本記事の記述も仮説の束の一本に過ぎません. ↩
極端な主張として「数学における分野の別はすべて蛇足である(すべての数学的営みはこの観点から同一視できる)」という主張もできます. かなり過激な立場ですが... ↩
赤川元昭. 2021. 仮説構築の論理. 白桃書房. ISBN: 978-4-561-86055-6 ↩
証明図を書いてみないことにはそこまでのすべてを理解できたかどうかを検証しきれないためです. 代数幾何学をやるためにHilbert's Nullstellensatzを学ぶぐらいならいいですが, スキームの証明をすべてZFC公理系から描いた証明図で表現するのはどう考えても嫌です. このため我々は「それは前に証明した」や「それに至るまでの道具はすべて証明してきた」とまではいかないかもしれないが「幾度も利用され検証されている」ことは確かだとして「Hilbert's Nullstellensatzより」と省略するわけです. (追記: なお, この省略は「やろうと思えば省略せずとも証明できる」が前提にあります. 数学が厳密な学問であること自体は事実であり, たとえば「中間値の定理を示すためにRCA0があれば十分」という命題の証明は恒真式からの証明図として描けるでしょうし, 選択公理⇒排中律も同様にすべてを論理式として描けるでしょう. ただそれは面倒で冗長なだけの全くつまらない作業なので「省略」されているだけです. 演繹に裏書きされた帰納的検証とも言えるでしょうか. ) ↩
アーベル多様体, 特に種数2の超楕円曲線に関する理論だけでもそこそこにかかるような気がします. J. W. S. Cassels. 1996. Prolegomena to middlebrow of genus 2 curves. Cambridge University Press. のような教科書もあるのですが, これはSilvermanとHartshorneを読めるだけの基礎的数学力を必要とします. ↩
Michael Polanyi (著), 高橋勇夫 (訳). 2003. 暗黙知の次元. 筑摩書房. ISBN: 978-4-480-08816-1. ↩
小平邦彦. 1975. 一数学者の妄想. 東京大学理学部「広報」7巻 1号 pp. 2-3. - https://www.s.u-tokyo.ac.jp/ja/story/newsletter/past/19750200_7_1.pdf ↩
追記前にこの部分がなかったのはひとえに書いたと思い込んでいたためです. すみません... ↩

elliptic-shiho/seccamp 2023 講師参加記.md