基于形式化技术的IPSec安全策略冲突发现研究  

Research on IPSec inter-policy conflict discovering based on formal modeling technology

作　　者：金民华[1] 黄俊[2] 

机构地区：[1]浙江大学计算机学院,浙江杭州310027 [2]中国计量学院计算机系,浙江杭州310018

出　　处：《计算机工程与设计》2007年第15期3582-3584,3607,共4页Computer Engineering and Design

基　　金：浙江省自然科学基金项目(Y109456)

摘　　要：基于安全策略形式化技术,提出了通过有序两元判定图表(OBDD)提供全面IPSec安全策略冲突的识别和分类的通用架构模型。基于这架构模型,研究了在通用IPSec策略配置过程中发现策略内部的冲突问题的技术。实验测试证明了该架构模型和技术在发现和解决策略冲突问题的有效性。Based on formal modeling technology and ordered binary decision diagrams, a generic model that captures various filtering policy semantics using Boolean expressions is presented. The model is used to derive a canonical representation for IPSec policies using ordered binary decision diagrams. A comprehensive framework is developed to classify and identify conflicts that could exist in a single IPSec device （intra-policy conflicts） in enterprise networks. The test and evaluation study on different network environments demonstrates the effectiveness and efficiency of the approach.

关 键 词：网络安全 安全策略 防火墙 内部策略冲突 形式化模型 有序两元判定图表 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]