WEKO3
-
RootNode
アイテム
安全な機能拡張性を持つTEEシェルの実装
https://ipsj.ixsq.nii.ac.jp/records/224736
https://ipsj.ixsq.nii.ac.jp/records/224736f77718b0-590e-43da-a5ef-0d764c4c466f
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-CSEC23100060.pdf (975.3 kB)
|
Copyright (c) 2023 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2023-02-27 | |||||||||||
| タイトル | ||||||||||||
| タイトル | 安全な機能拡張性を持つTEEシェルの実装 | |||||||||||
| タイトル | ||||||||||||
| 言語 | en | |||||||||||
| タイトル | Implementation of TEE shell with safe extensibility of functionality | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | システムセキュリティ | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||
| 資源タイプ | technical report | |||||||||||
| 著者所属 | ||||||||||||
| 大阪大学 | ||||||||||||
| 著者所属 | ||||||||||||
| 株式会社ティアフォー | ||||||||||||
| 著者所属 | ||||||||||||
| 大阪大学／北陸先端科学技術大学院大学 | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University / Japan Advanced Institute of Science and Technology | ||||||||||||
| 著者名 |
斎藤, 文弥
× 斎藤, 文弥
× 高野, 祐輝
× 宮地, 充子
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 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 を実現した． | |||||||||||
| 論文抄録(英) | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 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. | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AA11235941 | |||||||||||
| 書誌情報 |
研究報告コンピュータセキュリティ（CSEC） 巻 2023-CSEC-100, 号 60, p. 1-8, 発行日 2023-02-27 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-8655 | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
