|
|||||
|
|
| 审计缓冲区的形式化模型及其验证 | |
| 引用本文： | 丁志军,刘海峰,蒋昌俊.审计缓冲区的形式化模型及其验证[J].计算机科学,2006,33(5):98-103. |
| 作者姓名： | 丁志军 刘海峰 蒋昌俊 |
| 作者单位： | 1. 同济大学计算机科学与技术系,上海20092;山东科技大学信息科学与工程学院,青岛266510 2. 北京信息安全测评中心,北京100037 3. 同济大学计算机科学与技术系,上海20092 |
| 基金项目： | 中国科学院资助项目;国家重点基础研究发展计划(973计划) |
| 摘 要： | 审计系统作为安全信息系统的一个重要组成部分，对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分，本文利用时序Petri网对审计缓冲区管理的实现方案进行建模，进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了Petri网缺乏描述系统事件之间时序关系的局限性，同时发挥了Petri网对系统并发和物理结构的有效描述及分析的优势，达到了系统验证的目的。 |
| 关 键 词： | 审计 时序Petri网 缓冲区 验证 |
Formalization Model and Verification of Audit Buffers |
|
| DING Zhi-Jun,LIU Hai-Feng,JIANG Chang-Jun.Formalization Model and Verification of Audit Buffers[J].Computer Science,2006,33(5):98-103. | |
| Authors: | DING Zhi-Jun LIU Hai-Feng JIANG Chang-Jun |
| Affiliation: | Department of Computer Science and Technology, Tongji University, Shanghai 20092;Institute of Information Sci. and Eng. , Shandong University of Science and Technology, Qingdao 266510;Beijing Information Security Test and Evaluation Center, Beijing 100037 |
| 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 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. |
| Keywords: | Audit Temporal Petri nets Buffer Verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机科学》下载全文 | |