Miyaji Laboratory

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