@techreport{oai:ipsj.ixsq.nii.ac.jp:00203350,
 author = {長谷, 亮 and 松浦, 陽平 and Ryo, Hase and Yohei, Matsuura},
 issue = {4},
 month = {Feb},
 note = {パブリッククラウド上に構築された情報システムのセキュリティを向上するためには，計算機リソースの設定ミスを削減する仕組みが特に重要となる．手作業による設定ミスを防ぐ方法として，テキストに記載した仕様から計算機リソースを自動構築する Infrastructure as Code (IaC) がある．一方，IaC の設計で定義した仕様に誤りがあれば，構築した計算機リソースにも設定ミスが混入する．本稿では，形式手法のモデル検査を行うツールである Alloy Analyzer を活用した，IaC の設計時点で仕様の正当性を検証する方式の検討結果を報告する．, 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.},
 title = {Alloy Analyzerを活用したInfrastructure as Codeの正当性検証},
 year = {2020}
}