斎藤 文弥
Trusted Execution Environment (TEE) はファームウェアや OS といった基盤システム内の機微情報を 保護することを目的とした隔離環境技術の一つである.TEE の実装には C 言語が広く用いられており,メ モリ管理に対するリスクの除去が課題となっている.また TEE 構造に起因し,汎用 OS のシステム情報に 不正アクセス可能になるブーメランバグが報告されている.そこで我々は,メモリ安全なプログラミング 言語である Rust を用いて実装した Baremetalisp TEE,およびその TEE の API 定義用言語である BLisp を提案する.BLisp では効果系という概念に基づき,プログラム内におけるデータや関数の I/O を明示的 に記述することで意図していない動作を未然に防止する.また,BLisp を Coq にトランスパイルするプロ グラムを構築し,BLisp コードの形式検証を可能にした.さらに,システムを動的にアップデートできるよ うに,外部関数を BLisp に組み込む機能を実装した.この結果,メモリ安全性と意味的正しさを保証しつ つ動的に機能をアップデートすることが可能な TEE Shell を実現した.