著者

斎藤 文弥 高野 祐輝 宮地 充子

雑誌

研究報告コンピュータセキュリティ(CSEC) (ISSN:21888655)

巻号頁・発行日

vol.2023-CSEC-100, no.60, pp.1-8, 2023-02-27

---

Trusted Execution Environment (TEE) はファームウェアや OS といった基盤システム内の機微情報を保護することを目的とした隔離環境技術である.先行研究では,TEE アーキテクチャの一つである Arm TrustZone をベースとしてメモリ安全性と効果系という概念を主軸に設計した Baremetalisp TEE,およびその TEE の API 定義用言語である BLisp を構築した.さらに作成した BLisp のコードを Coq にトランスパイルし形式的検証も可能な手法を提案した.TEE は他の隔離環境技術である Trusted Platform Module (TPM) 等とは異なりユーザーが自由にセキュリティ仕様を構築できることが特徴として挙げられるが,Baremetalisp では独自の言語 BLisp を用いているため拡張できる機能に制限が存在していた.そこで本研究では Baremetalisp を構成している Rust から関数を BLisp へ組み込み可能にすることによって,柔軟な機能の拡張性を実現した.組み込み関数にも効果系が適用することができ,メモリ安全性と形式的な正しさを保証しつつ安全な機能アップデートが可能な TEE Shell を実現した.