WEKO3
アイテム
Coqで検証可能なTEEシェル基盤の実装
https://ipsj.ixsq.nii.ac.jp/records/217890
https://ipsj.ixsq.nii.ac.jp/records/2178905698cf74-fd39-4900-aae4-ea9917be97b2
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-IOT22057008.pdf (919.6 kB)
|
Copyright (c) 2022 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2022-05-12 | |||||||||||
| タイトル | ||||||||||||
| タイトル | Coqで検証可能なTEEシェル基盤の実装 | |||||||||||
| タイトル | ||||||||||||
| 言語 | en | |||||||||||
| タイトル | Implementation of TEE shell infrastructure verifiable by Coq | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | CSEC | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | 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）は電子計算機のセキュアデータを保護する技術の一つであり，広く利用されているシステムである．一方で，C 言語で実装されているものが多いため，メモリ管理に対する脆弱性が依然として存在する．そこで我々は，Barematalisp TEE の API 定義用言語 Blisp から Coq へトランスパイルするプログラムを Rust 言語を用いて構築した．Coq は定理証明支援系システムであり，関数や式を形式的に証明する．このプログラムはメモリ安全性と意味的正しさを兼ね備えた Trusted Shell 実装の一助となり，一般的なシェルと同様の動的なプログラムの注入と実行を可能にする． | |||||||||||
| 論文抄録(英) | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | Trusted Execution Environment (TEE) is a widely used software system that is one of the technologies to protect secure data in computers. However, since many TEEs are implemented in C, vulnerabilities to memory management still exist. Therefore, we constructed a program to transpile Blisp, the API definition language of Barematalisp TEE, to Coq using Rust. Coq is a theorem proving support system that formally proves functions and expressions. This program helps to implement a Trusted Shell implementation that is both memory-safe and semantically correct, and allows dynamic program injection and execution similar to a general shell. | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AA12326962 | |||||||||||
| 書誌情報 |
研究報告インターネットと運用技術（IOT） 巻 2022-IOT-57, 号 8, p. 1-8, 発行日 2022-05-12 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-8787 | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
