@techreport{oai:ipsj.ixsq.nii.ac.jp:00224736,
 author = {斎藤, 文弥 and 高野, 祐輝 and 宮地, 充子},
 issue = {60},
 month = {Feb},
 note = {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 を実現した．, Trusted Execution Environment (TEE) is an isolated environment technology to protect sensitive data in infrastructure systems such as firmware and operating systems. In our previous work, with the concepts of memory-safety and effect system, we developed Baremetalisp TEE based on Arm TrustZone and BLisp, an API definition language for TEE. Furthermore, we proposed a method to enable formal verification by transpiling BLisp code to Coq. Unlike other isolation technologies such as Trusted Platform Module (TPM), TEE enables users to freely build security specifications. However, due to usage of its own language BLisp in Baremetalisp, this system has limitations of extending the functionality. In this study, we realized flexible extensibility of the functionality by making it possible to embed functions into BLisp from Rust, which constitutes Baremetalisp. By allowing effect system to be applied to these functions, we created a TEE shell that guarantees memory-safety, formal correctness and secure function updates.},
 title = {安全な機能拡張性を持つTEEシェルの実装},
 year = {2023}
}