基于下推系统可达性分析的程序机密消去机制
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(60773163, 60821003, 60872041, 60911140102); 国家科技部重大专项(2011ZX03005-002); 中央高校基本科研业务费专项资金(JY10000903001); 装备预研基金(9140A15040210HK6101)


Declassification Enforcement on Program with Reachability Analysis of Pushdown System
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效.

    Abstract:

    The study proposes a verification mechanism based on reachability analysis of pushdown system to enforce existing declassification policies of language-based information flow security. The pushdown rules of store and match primitives are embedded in the abstract model after compact self-composition. The security property with respect to different declassification policies is violated when the illegal-flow state is reached in the pushdown system. The experimental results show improvement in precision, compared with the type-based mechanisms, and growth in effectiveness compared with the RNI-enforcement based on automated verification.

    参考文献
    相似文献
    引证文献
引用本文

孙聪,唐礼勇,陈钟.基于下推系统可达性分析的程序机密消去机制.软件学报,2012,23(8):2149-2162

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2010-10-07
  • 最后修改日期:2011-09-01
  • 录用日期:
  • 在线发布日期: 2012-08-07
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号