{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00203350","sets":["1164:6389:10112:10113"]},"path":["10113"],"owner":"44499","recid":"203350","title":["Alloy Analyzerを活用したInfrastructure as Codeの正当性検証"],"pubdate":{"attribute_name":"公開日","attribute_value":"2020-02-24"},"_buckets":{"deposit":"cffb4378-fed7-4063-9892-450b0a0ea0a7"},"_deposit":{"id":"203350","pid":{"type":"depid","value":"203350","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"Alloy Analyzerを活用したInfrastructure as Codeの正当性検証","author_link":["500956","500953","500955","500954"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Alloy Analyzerを活用したInfrastructure as Codeの正当性検証"},{"subitem_title":"A Verification Method of Infrastructure as Code using Alloy Analyzer","subitem_title_language":"en"}]},"item_type_id":"4","publish_date":"2020-02-24","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"三菱電機株式会社"},{"subitem_text_value":"三菱電機株式会社"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Mitsubishi Electric Corporation, Information Technology R&D Center","subitem_text_language":"en"},{"subitem_text_value":"Mitsubishi Electric Corporation, Information Technology R&D Center","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/203350/files/IPSJ-SPT20036004.pdf","label":"IPSJ-SPT20036004.pdf"},"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-SPT20036004.pdf","filesize":[{"value":"2.3 MB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"46"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_login","version_id":"72974029-98d8-4b2e-971e-bbf7dc57822a","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2020 by the Institute of Electronics, Information and Communication Engineers This SIG report is only available to those in membership of the SIG."}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"長谷, 亮"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"松浦, 陽平"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Ryo, Hase","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yohei, Matsuura","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA12628305","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-8671","subitem_source_identifier_type":"ISSN"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"パブリッククラウド上に構築された情報システムのセキュリティを向上するためには，計算機リソースの設定ミスを削減する仕組みが特に重要となる．手作業による設定ミスを防ぐ方法として，テキストに記載した仕様から計算機リソースを自動構築する Infrastructure as Code (IaC) がある．一方，IaC の設計で定義した仕様に誤りがあれば，構築した計算機リソースにも設定ミスが混入する．本稿では，形式手法のモデル検査を行うツールである Alloy Analyzer を活用した，IaC の設計時点で仕様の正当性を検証する方式の検討結果を報告する．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"To enhance security of information systems developped using computing resouces in a public cloud, it is important to consider methods to avoid misconfiguration of the resources. One of the methods to prevent misconfiguration caused by manual setting is Infrastructure as Code (IaC), which automatically configures the resources using definitions specified in text files. However, IaC will also result in misconfiguration of the resources if the specification of IaC defined in a design process is not correct. This paper introduces a method to verify the specification of IaC in a design process using Alloy Analyzer, which is a model checking tool based on formal methods.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"6","bibliographic_titles":[{"bibliographic_title":"研究報告セキュリティ心理学とトラスト（SPT）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2020-02-24","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"4","bibliographicVolumeNumber":"2020-SPT-36"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"id":203350,"updated":"2025-01-19T20:34:42.528946+00:00","links":{},"created":"2025-01-19T01:05:46.939506+00:00"}