【摘要】 审计系统作为安全信息系统的一个重要组成部分,对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分,本文利用时序 Petri 网对审计缓冲区管理的实现方案进行建模,进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了 Petri 网缺乏描述系统事件之间时序关系的局限性,同时发挥了 Petri 网对系统并发和物理结构的有效描述及分析的优势,达到了系统验证的目的。更多还原

【Abstract】 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 rela- tions between system events.Moreover,temporal Petri nets exert the advantages of Petri nets which can effectively de- scribe and analyze the system concurrency and physical structures for the purpose of system verification.更多还原