资源描述：
《利用逻辑编程方法进行形式化的网络安全策略验证》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、利用逻辑编程方法进行形式化的网络安全策略验证第27卷第5期2010年5月计算机应用与软件ComputerApplicationsandSoftwareV0l_27No.5Mav2010利用逻辑编程方法进行形式化的网络安全策略验证李鼎周保群赵彬(解放军信息工程大学电子技术学院河南郑州450004)摘要高级安全策略又称为安全需求,低级策略配置是高级策略的实现,正确的低级策略配置必须能够满足安全需求.网络安全取决于低级策略配置的正确性,由于策略配置异常复杂,并且缺乏准确描述安全需求的方法,这为策略的正确性分析提出了巨大的挑战.采用逻辑编程方法来分析网络安
2、全策略,通过将低级策略配置,高级策略,漏洞信息等元素转化为逻辑程序,将网络中所有可能存在的访问与安全需求进行对比,判定策略配置是否满足安全需求,并给出所有不满足安全需求的策略配置.关键词XSB逻辑编程系统策略层次策略验证USINGLoGICPRoGRAMMINGFoRFoRMALVERIFICATIoNOFNETWoRKSECURITYPOLICYLiDingZhouBaoqunZhaoBin(InstituteofElectronicTechnology,PInformationEngineeringUniversity,Zhengzhou450
3、004,Henan,China)AbstractWetreathigh—levelpolicyassecurityrequirementandlow—levelpolicyastheimplementationofthehigh-levelpolicy,aproperlow—levelpolicyconfigurationmustmeetthesecurityrequirement.NetworkSecuritydependsonthecorrectnessoflow—levelpolicyconfigura—tion,butforthesakeo
4、fextremecomplexityinpolicyconfigurationaswellaslackingthemeansofaccuratedescriptionofthesecurityrequire—ment,thevalidityanalysisofthepoliciesisposedaterriblechallenge.Weuselogicprogrammingtoperformpolicyanalysisonnetworksecur-ity.Bytranslatinglow—levelpolicyconfiguration,high—
5、levelpolicyandvulnerabilitydatabaseintologicprogramandcontrastingallkindsofpossibleaccesseswithsecurityrequirements,thepolicyconfigurationcanbedeterminedofwhetherornottohavemetthesecurityrequire-ment,togetherwithalistofallthosepolicyconfigurationsunsatisfyingthesecurityrequire
6、ment.KeywordsXSBlogicprogrammingsystemPolicyhierarchyPolicyverification0引言网络安全策略分为高级策略和低级策略,一般将高级策略视为需求,将低级策略视为高级策略的实现.高级策略用自然语言描述,例如网站的保密性策略,企业的安全策略,安全和保密性法律等.低级策略由形式化语言,如ASL和Alloy定义,如防火墙,路由器配置规则.由于低级策略配置的定义通常独立于需求分析,可能会造成策略配置与安全需求不一致.随着网络规模的不断扩大,策略定义语言越来越难以理解,策略的配置变得异常复杂.对策略
7、进行正确的配置,使低级策略配置能够真正满足安全需求,是一项具有很大难度的任务.因此,在策略实施之前,对策略进行安全性验证是十分必要的.由于策略配置条目众多,涉及的主体,客体权限较多,并且缺乏准确描述安全需求的方法,对策略进行手工验证不现实,亟需一种自动化的,严格的策略分析方法和工具.而形式化分析是一种非常有效的策略验证方法.目前主要有两种基本的策略形式化分析方法:基于逻辑编程的策略分析和基于模型检测分析.而模型检测分析过于复杂,查询能力较差,交互性不强,并且只能对策略配置是否正确作出回答,而不能举出违反安全需求的策略配置实例,缺乏对策略优化改进的指
8、导意义.本文基于SUNYatStonyBrook开发的XSB逻辑编程系统对策略进行分析与验证,采用Prolog作为建模语言
