基于限界约束的安全相关性质的推理证明

摘要

Security-relevant properties such as access control in a complex environment play a very important role.In terms of procedural verification,not only the safety and activity verification are considered,but the nature of some security policies,such as non-interference,should also be considered.These security policies that cannot be described by the general nature can be considered as "hypersafety".Boundary constraints are common to represent different degrees of access frequency restrictions.They are one of the effective auxiliary methods in safety-related property verification,and have wide application value in the attribute verification of wireless sensor network protocols,embedded systems and other important fields.Based on the above description,we propose an approach for extracting deductive proof of security-relevant properties under bounded constraints.%安全相关的性质如访问控制等在复杂环境下有十分重要的作用.从程序验证方面来说,不仅考虑安全性和活性的验证,还要考虑一些安全策略的性质,如非干涉性,这些不能用一般的性质来描述的安全策略可以被看作“超安全性质”.限界约束可通用地表示不同程度的访问频次限制,是安全相关性质验证中有效的辅助方法之一,在无线传感器网络协议、嵌入式系统等重要领域的性质验证方面具有广泛的应用价值.主要研究网络安全策略中的安全相关性质的限界表达及基于该限界约束的验证规则.