XSM 语义模型及安全需求形式化验证.PDFVIP

第３４卷第６期　　　 计算机应用与软件 Ｖｏｌ３４Ｎｏ．６ ２０１７年６月　　 ＣｏｍｐｕｔｅｒＡｐｐｌｉｃａｔｉｏｎｓａｎｄＳｏｆｔｗａｒｅ Ｊｕｎ．２０１７ ＸＳＭ语义模型及安全需求形式化验证 祝现威　朱智强　孙　磊 （信息工程大学密码工程学院　河南郑州４５０００１） 摘　要　　Ｘｅｎ作为一种开源流行的虚拟化工具，使用越来越频繁。作为Ｘｅｎ的安全框架ＸＳＭ（ＸｅｎＳｅｃｕｒｉｔｙ Ｍｏｄｕｌｅ）也受到广泛的关注。许多研究者通过形式化的方式对现有的操作系统进行正确性的验证，目前已有的形 式化研究主要是验证系统实现的代码正确性。从系统功能角度提出了一种以主体行为为操作系统语义模型对系 统进行形式化建模，并采用ＣＴＬ时序逻辑对ＸＳＭ安全需求进行分析。语义模型作为系统设计合理性和形式化验 证的联系，对ＸＳＭ进行形式化验证，并使用Ｉｓａｂｅｌｌｅ／ＨＯＬ验证功能和安全需求的一致性，以说明ＸＳＭ是否符合 安全需求。 关键词　　ＸＳＭ　语义模型　形式化验证　安全性分析　Ｉｓａｂｅｌｌｅ／ＨＯＬ 中图分类号　ＴＰ３１１　　　　文献标识码　Ａ　　　　ＤＯＩ：１０．３９６９／ｊ．ｉｓｓｎ．１０００３８６ｘ．２０１７．０６．０５６ ＸＳＭＳＥＭＡＮＴＩＣＭＯＤＥＬＡＮＤＦＯＲＭＡＬＶＥＲＩＦＩＣＡＴＩＯＮ ＯＦＳＥＣＵＲＩＴＹＲＥＱＵＩＲＥＭＥＮＴＳ ＺｈｕＸｉａｎｗｅｉ　ＺｈｕＺｈｉｑｉａｎｇ　ＳｕｎＬｅｉ （ＩｎｆｏｒｍａｔｉｏｎＥｎｇｉｎｅｅｒｉｎｇＵｎｉｖｅｒｓｉｔｙ，Ｚｈｅｎｇｚｈｏｕ４５０００１，Ｈｅｎａｎ，Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ　　Ａｓａｐｏｐｕｌａｒｏｐｅｎｓｏｕｒｃｅｖｉｒｔｕａｌｉｚａｔｉｏｎｔｏｏｌｓ，Ｘｅｎｉｓｕｓｅｄｍｏｒｅａｎｄｍｏｒｅｆｒｅｑｕｅｎｔｌｙ．Ｘｓｍ（ＸｅｎＳｅｃｕｒｉｔｙ Ｍｏｄｕｌｅ），ａｓｔｈｅｓｅｃｕｒｉｔｙｆｒａｍｅｗｏｒｋｏｆｔｈｅＸｅｎ，ｈａｓａｌｓｏｂｅｅｎｗｉｄｅｓｐｒｅａｄｃｏｎｃｅｒｎ．Ｔｈｅｒｅａｒｅａｌｏｔｏｆｒｅｓｅａｒｃｈｔｏｖｅｒｉｆｙ ｔｈｅｓｙｓｔｅｍｏｐｅｒａｔｉｏｎｓｃｏｒｒｅｃｔｎｅｓｓｂｙｆｏｒｍａｌｍｅｔｈｏｄ．Ｔｈｅｅｘｉｓｔｉｎｇｆｏｒｍａｌｉｚａｔｉｏｎｒｅｓｅａｒｃｈｉｓｍａｉｎｌｙｃｏｎｃｅｒｎｅｄｗｉｔｈｔｈｅ ｃｏｄｅｃｏｒｒｅｃｔｎｅｓｓｏｆｔｈｅｓｙｓｔｅｍｉｍｐｌｅｍｅｎｔａｔｉｏｎ．Ｔｈｕｓ，ｔｈｅｓｙｓｔｅｍｉｓｍｏｄｅｌｅｄｆｏｒｍａｌｌｙｗｈｉｃｈｓｕｂｊｅｃｔｂｅｈａｖｉｏｒｉｓｔａｋｅｎａｓ ｏｐｅｒａｔｉｎｇｓｙｓｔｅｍｓｅｍａｎｔｉｃｍｏｄｅｌｉｎｔｈｅｐｅｒｓｐｅｃｔｉｖｅｏｆｓｙｓｔｅｍｆｕｎｃｔｉｏｎ，ａｎｄｔｈｅｓｅｃｕｒｉｔｙｒｅｑｕｉｒｅｍｅｎｔｓｏｆＸＭＳｉｓａｎａｌｙｚｅｄ ｂｙａｄｏｐｔｉｎｇｔｈｅＣＬＴｓｅｑｕｅｎｔｉａｌｌｏｇｉｃ．Ａｓｔｈｅｃｏｎｎｅｃｔｉｏｎｏｆｔｈｅｒａｔｉｏｎａｌｉｔｙｏｆｓｙｓｔｅｍｄｅｓｉｇｎａｎｄｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎ，ｔｈｅ ｓｅｍａｎｔｉｃｍｏｄｅｌｉｓｒｅｓｐｏｎｓｉｂｌｅｆｏｒｔｈｅｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎｏｆｔｈｅＸＳＭ，ａｎｄｔｈｅＩｓａｂｅｌｌｅ／ＨＯＬｉｓｕｔｉｌｉｚｅｄｔｏｖｅｒｉｆｙｔｈｅ ｃｏｎｓｉｓｔｅｎｃｙｂｅｔｗｅｅｎｆｕｎｃｔｉｏｎｓａｎｄｓｅｃｕｒｉｔｙｒｅｑｕｉｒｅｍｅｎｔｓｓｏａｓｔｏｄｅｍｏｎｓｔｒａｔｅｗｈｅｔｈｅｒｔｈｅＸＳＭｍｅｅｔｓｔｈｅｓｅｃｕｒｉｔｙｒｅ ｑｕｉｒｅｍｅｎｔｓ． Ｋｅｙｗｏｒｄｓ　　ＸＳＭ　Ｓｅｍａｎｔｉｃｍｏｄｅｌ　Ｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎ　Ｓｅｃｕｒｉｔｙａｎａｌｙｓｉｓ　Ｉｓａｂｅｌｌｅ／ＨＯＬ 在现有云计算环境中得到广泛应用，为了增强其安全 ０　引　言 性，一些研究学者借鉴安全操作系统的理论和技术提