高级检索
    李 超, 殷丽华, 郭云川. 基于ptSPA的概率时间信息流安全属性分析[J]. 计算机研究与发展, 2011, 48(8): 1370-1380.
    引用本文: 李 超, 殷丽华, 郭云川. 基于ptSPA的概率时间信息流安全属性分析[J]. 计算机研究与发展, 2011, 48(8): 1370-1380.
    Li Chao, Yin Lihua, Guo Yunchuan. Analysis for Probabilistic and Timed Information Flow Security Properties via ptSPA[J]. Journal of Computer Research and Development, 2011, 48(8): 1370-1380.
    Citation: Li Chao, Yin Lihua, Guo Yunchuan. Analysis for Probabilistic and Timed Information Flow Security Properties via ptSPA[J]. Journal of Computer Research and Development, 2011, 48(8): 1370-1380.

    基于ptSPA的概率时间信息流安全属性分析

    Analysis for Probabilistic and Timed Information Flow Security Properties via ptSPA

    • 摘要: 基于进程代数的无干扰性分析是分析信息流安全性质的主要方法.为考虑概率时间配置下的信息泄漏,对安全进程代数进行概率时间域上的扩展,提出概率时间安全进程代数ptSPA,给出其形式化语法及语义,引入概率时间弱互拟等价的概念,在此基础上,讨论概率时间信息流安全属性,提出TBSPNI,PTBNDC,SPTBNDC属性,分析属性的包含性,证明提出的属性在表达能力上强于原有属性,最后给出一个实例,对IMP机制在概率时间配置下进行了建模分析,分析结果表明ptSPA对捕获概率时间隐蔽通道的有效性.

       

      Abstract: Information flow analysis is one of the primary approaches for analyzing computer security problems, such as covert channel and data leak. Security process algebra(SPA) is a classic method used in researching information security properties in nondeterministic system. To analyze the information security properties and capture the information leakage in probabilistic and real time system, SPA is extended in probabilistic and time setting. Probabilistic and time security process algebra(ptSPA), an extension of SPA, is proposed by first introducing the probabilistic and time calculus to specify activities constricted by probability and time, and extending the formal syntax and semantic to enhance the SPA. Then, the related notion of probabilistic and time bisimulation equivalence is presented, to describe two observable behavior traces are equivalent when considering probability and time. Based on ptSPA, several information flow security properties in probabilistic and real time system, such as TBSPNI, PTBNDC and SPTBNDC are defined, which can capture probabilistic and time covert channel while the original SPA cannot. The relations among the information flow security properties are analyzed. Finally, a case study is given to show that the expressiveness of calculus in ptSPA is possible to model and analyze probabilistic and time systems.

       

    /

    返回文章
    返回