利用逻辑编程方法进行形式化的网络安全策略验证

USING LOGIC PROGRAMMING FOR FORMAL VERIFICATION OF NETWORK SECURITY POLICY

高级安全策略又称为安全需求,低级策略配置是高级策略的实现,正确的低级策略配置必须能够满足安全需求。网络安全取决于低级策略配置的正确性,由于策略配置异常复杂,并且缺乏准确描述安全需求的方法,这为策略的正确性分析提出了巨大的挑战。采用逻辑编程方法来分析网络安全策略,通过将低级策略配置、高级策略、漏洞信息等元素转化为逻辑程序,将网络中所有可能存在的访问与安全需求进行对比,判定策略配置是否满足安全需求,并给出所有不满足安全需求的策略配置。

We treat high-level policy as security requirement and low-level policy as the implementation of the high-level policy,a proper low-level policy configuration must meet the security requirement.Network Security depends on the correctness of low-level policy configuration,but for the sake of extreme complexity in policy configuration as well as lacking the means of accurate description of the security requirement,the validity analysis of the policies is posed a terrible challenge.We use logic programming to perform policy analysis on network security.By translating low-level policy configuration,high-level policy and vulnerability database into logic program and contrasting all kinds of possible accesses with security requirements,the policy configuration can be determined of whether or not to have met the security requirement,together with a list of all those policy configurations unsatisfying the security requirement.