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

计算机科学 ›› 2006, Vol. 33 ›› Issue (5): 98-103.

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

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
国家自然科学基金资助项目（60473094）、国家杰出青年科学基金资助项目（60125205）.

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

摘要： 审计系统作为安全信息系统的一个重要组成部分，对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分，本文利用时序Petri网对审计缓冲区管理的实现方案进行建模，进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了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--tem

Key words: Audit,Temporal Petri nets, Buffer, Verification

. 审计缓冲区的形式化模型及其验证[J]. 计算机科学, 2006, 33(5): 98-103. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed