审计缓冲区的形式化模型及其验证  

Formalization Model and Verification of Audit Buffers

作　　者：丁志军[1,2] 刘海峰 蒋昌俊[1] 

机构地区：[1]同济大学计算机科学与技术系 [2]山东科技大学信息科学与工程学院 [3]北京信息安全测评中心

出　　处：《计算机科学》2006年第5期98-103,共6页Computer Science

基　　金：国家自然科学基金(60473094);国家杰出青年科学基金(60125205)

摘　　要：审计系统作为安全信息系统的一个重要组成部分,对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分,本文利用时序 Petri 网对审计缓冲区管理的实现方案进行建模,进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了 Petri 网缺乏描述系统事件之间时序关系的局限性,同时发挥了 Petri 网对系统并发和物理结构的有效描述及分析的优势,达到了系统验证的目的。As a very important component of secure information system, audit system plays a key role in monitoring the system, insuring proper implementing of security policy and building Intrusion Detection System. This paper introduces a subclass of Petri net--temporal Petri nets which is used to build a model for implementing the management scheme of audit buffers. Based on it, we analyzed and verified the properties of system safety and liveness. By using temporal logic, this method can break the limitations imposed by Petri nets, which lack the ability to describe the temporal relations between system events. Moreover, temporal Petri nets exert the advantages of Petri nets which can effectively describe and analyze the system concurrency and physical structures for the purpose of system verification.

关 键 词：审计 时序PETRI网 缓冲区 验证 

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