@techreport{oai:ipsj.ixsq.nii.ac.jp:00217890,
 author = {斎藤, 文弥 and 高野, 祐輝 and 宮地, 充子},
 issue = {8},
 month = {May},
 note = {Trusted Execution Environment（TEE）は電子計算機のセキュアデータを保護する技術の一つであり，広く利用されているシステムである．一方で，C 言語で実装されているものが多いため，メモリ管理に対する脆弱性が依然として存在する．そこで我々は，Barematalisp TEE の API 定義用言語 Blisp から Coq へトランスパイルするプログラムを Rust 言語を用いて構築した．Coq は定理証明支援系システムであり，関数や式を形式的に証明する．このプログラムはメモリ安全性と意味的正しさを兼ね備えた Trusted Shell 実装の一助となり，一般的なシェルと同様の動的なプログラムの注入と実行を可能にする．, 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.},
 title = {Coqで検証可能なTEEシェル基盤の実装},
 year = {2022}
}