セキュリティ・キャンプ2025 全国大会【開発】Lゼミ

• 松岡 航太郎
• 三村 聡志
• hikalium
• 凌翔太

• 松下 祐介

• Rust
• 形式検証
• 論理
• コンパイラ
  
• 言語処理系

現代、私たちの暮らしを様々な場所で支えているソフトウェア。そうしたソフトウェアの中に忍び込む「バグ」は、社会における脅威とすらなりえます。

2015年に生まれた「Rust」は、C/C++ のように低レベルのメモリ・スレッド操作を許しながら、「所有権型」という強力な仕組みによって高い安全性を実現する、画期的な言語です。これまで C/C++ で書かれたソフトウェアは有名な Heartbleed を含む多くの深刻な脆弱性をもたらしていました。Rust はそうした領域で脆弱性を防げると、広く期待されていて、産業界でも注目を集めています。

更に先進的なアプローチとして、「形式検証」があります。これは、ソフトウェアのソースコードを論理の力で解析して、バグがないことを証明する技術です。特に、航空機・宇宙開発など、バグが致命的になりうる場所で、形式検証が実用されています。近年、Rust プログラムに対する形式検証が注目されています。特に、Microsoft Research のプロジェクトから生まれた「Verus」という Rust 検証器が最近活躍しています。

• Verus GitHub

このゼミでは、Rust プログラムに対する自作の形式検証器を Rust で開発していきます。特に、自作の検証器で面白い Rust プログラムを検証できるようにすることを目指します。具体的にどのような検証器にするかは、皆さんに自由に考えてもらおうと思います。チャレンジングではありますが、Rust コンパイラの内部表現、Rust の所有権型の仕組み、実践的な形式検証などを学べる、刺激的で充実したゼミになると思います。意欲溢れる皆さんの応募を待っています！！

## 参考: 昨年の講義

私が昨年講師を務めた、セキュリティ・キャンプ全国大会 2024 開発コース「S15 Rust プログラム検証ゼミ」では、受講生2人に自作の Rust プログラム検証器を作ってもらいました。

• 昨年の様子（X）

これについて、受講生の1人のisanさんが詳しいブログ記事を書いてくれたので、ぜひ読んでみてください。

• 「Rustで預言を使ったプログラム検証器を自作しよう」

• 岡村 淳一

• 半導体
• 高位言語
• RTL
• GDSII
• 合成
• P&R
• TinyTapeout
• XLS
• CoLab
• OpenLane

高位言語（XLS）から RTL 出力を確認、OpenLane toolcahin を使った 論理合成、配置配線（P&R）、物理レイアウト（GDSII）までの設計ワークフローを Google Colab 上で実行、Github から TinyTapeout を介してのチップ発注までを3日間で学びます。

ソフトウェアで記述する処理をハードウェアに実装する経験を実体験することで、コンパイラや機械語より更に下層の、独自ハードウェアでの処理の高速化のイメージに興味がある人に最適。

• ーーー 関連URL ーーー
• google/xls(github)
• The-OpenROAD-Project/OpenLane(github)
• Google Colab
• Tiny Tapeout

• ーーー 参考URL ーーー
• 技術用語集(github)
• 【京都賞記念講演】カーヴァー・ミード「情報革命の時代を生きて」(Youtube)

• 櫻井 碧

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

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

TEEには、データを保護したままでの計算（秘密計算）に利用されるような関連技術、即ち準同型暗号や秘密分散と比較してみても計算コストが小さめで効率的であり、その上で高度な安全性を提供できるというメリットがあります。
一方で、ハードウェアに依存する以上ベンダを信頼する必要がある、サイドチャネル攻撃からの保護機能を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、AEPIC Leakなど、名だたる高度かつ難しい攻撃が無尽蔵に存在しますが、あくまでもゼミ内で取り扱える範囲に簡略化して実践していきます。

• 佐藤 弘崇

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

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

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

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

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

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