{"id":217866,"updated":"2025-01-19T15:21:11.136550+00:00","links":{},"created":"2025-01-19T01:18:17.614183+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00217866","sets":["1164:3925:10844:10907"]},"path":["10907"],"owner":"44499","recid":"217866","title":["Coqで検証可能なTEEシェル基盤の実装"],"pubdate":{"attribute_name":"公開日","attribute_value":"2022-05-12"},"_buckets":{"deposit":"ea6c3522-f0e0-4a59-ba4a-bb3d7f5ace35"},"_deposit":{"id":"217866","pid":{"type":"depid","value":"217866","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"Coqで検証可能なTEEシェル基盤の実装","author_link":["565267","565268","565266"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Coqで検証可能なTEEシェル基盤の実装"},{"subitem_title":"Implementation of TEE shell infrastructure verifiable by Coq","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"CSEC","subitem_subject_scheme":"Other"}]},"item_type_id":"4","publish_date":"2022-05-12","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"大阪大学"},{"subitem_text_value":"株式会社ティアフォー"},{"subitem_text_value":"大阪大学／北陸先端科学技術大学院大学"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Osaka University","subitem_text_language":"en"},{"subitem_text_value":"Osaka University / Japan Advanced Institute of Science and Technology","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/217866/files/IPSJ-CSEC22097008.pdf","label":"IPSJ-CSEC22097008.pdf"},"date":[{"dateType":"Available","dateValue":"2024-05-12"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-CSEC22097008.pdf","filesize":[{"value":"919.6 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"30"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"453eac99-3698-4f9a-b471-a48b41b8666e","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2022 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"斎藤, 文弥"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"高野, 祐輝"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"宮地, 充子"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11235941","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"2188-8655","subitem_source_identifier_type":"ISSN"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"Trusted Execution Environment（TEE）は電子計算機のセキュアデータを保護する技術の一つであり，広く利用されているシステムである．一方で，C 言語で実装されているものが多いため，メモリ管理に対する脆弱性が依然として存在する．そこで我々は，Barematalisp TEE の API 定義用言語 Blisp から Coq へトランスパイルするプログラムを Rust 言語を用いて構築した．Coq は定理証明支援系システムであり，関数や式を形式的に証明する．このプログラムはメモリ安全性と意味的正しさを兼ね備えた Trusted Shell 実装の一助となり，一般的なシェルと同様の動的なプログラムの注入と実行を可能にする．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"8","bibliographic_titles":[{"bibliographic_title":"研究報告コンピュータセキュリティ（CSEC）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2022-05-12","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"8","bibliographicVolumeNumber":"2022-CSEC-97"}]},"relation_version_is_last":true,"weko_creator_id":"44499"}}