• 中国精品科技期刊
  • CCF推荐A类中文期刊
  • 计算领域高质量科技期刊T1类
高级检索

基于接口精化的广义无干扰性研究

孙聪, 习宁, 高胜, 张涛, 李金库, 马建峰

孙聪, 习宁, 高胜, 张涛, 李金库, 马建峰. 基于接口精化的广义无干扰性研究[J]. 计算机研究与发展, 2015, 52(7): 1631-1641. DOI: 10.7544/issn1000-1239.2015.20140306
引用本文: 孙聪, 习宁, 高胜, 张涛, 李金库, 马建峰. 基于接口精化的广义无干扰性研究[J]. 计算机研究与发展, 2015, 52(7): 1631-1641. DOI: 10.7544/issn1000-1239.2015.20140306
shu
Sun Cong, Xi Ning, Gao Sheng, Zhang Tao, Li Jinku, Ma Jianfeng. A Generalized Non-interference Based on Refinement of Interfaces[J]. Journal of Computer Research and Development, 2015, 52(7): 1631-1641. DOI: 10.7544/issn1000-1239.2015.20140306
Citation: Sun Cong, Xi Ning, Gao Sheng, Zhang Tao, Li Jinku, Ma Jianfeng. A Generalized Non-interference Based on Refinement of Interfaces[J]. Journal of Computer Research and Development, 2015, 52(7): 1631-1641. DOI: 10.7544/issn1000-1239.2015.20140306
shu
孙聪, 习宁, 高胜, 张涛, 李金库, 马建峰. 基于接口精化的广义无干扰性研究[J]. 计算机研究与发展, 2015, 52(7): 1631-1641. CSTR: 32373.14.issn1000-1239.2015.20140306
引用本文: 孙聪, 习宁, 高胜, 张涛, 李金库, 马建峰. 基于接口精化的广义无干扰性研究[J]. 计算机研究与发展, 2015, 52(7): 1631-1641. CSTR: 32373.14.issn1000-1239.2015.20140306
shu
Sun Cong, Xi Ning, Gao Sheng, Zhang Tao, Li Jinku, Ma Jianfeng. A Generalized Non-interference Based on Refinement of Interfaces[J]. Journal of Computer Research and Development, 2015, 52(7): 1631-1641. CSTR: 32373.14.issn1000-1239.2015.20140306
Citation: Sun Cong, Xi Ning, Gao Sheng, Zhang Tao, Li Jinku, Ma Jianfeng. A Generalized Non-interference Based on Refinement of Interfaces[J]. Journal of Computer Research and Development, 2015, 52(7): 1631-1641. CSTR: 32373.14.issn1000-1239.2015.20140306
shu

基于接口精化的广义无干扰性研究

  • 1(西安电子科技大学网络与信息安全学院 西安 710071)

  • 2(中央财经大学信息学院 北京 102206) (suncong@xidian.edu.cn)

基金项目: 长江学者和创新团队发展计划项目(IRT1078)；国家自然科学基金委员会——广东联合基金重点基金项目(U1135002)；国家科技重大专项基金项目(2011ZX03005-002)；国家自然科学基金项目(61303033，61272398)；陕西省自然科学基础研究计划项目(2013JQ8036)；中央高校基本科研业务费专项资金项目(JB140309)；航空科学基金项目(2013ZC31003，20141931001)
详细信息

  • 中图分类号: TP309.2

A Generalized Non-interference Based on Refinement of Interfaces

  • 1(School of Cyber Engineering, Xidian University, Xi’an 710071)

  • 2(School of Information, Central University of Finance and Economics, Beijing 102206)

摘要

    摘要
  • 摘要: 在复杂构件化软件的设计和实现过程中，由于安全属性的可组合性难以实现，使得系统整体的安全需求难以得到有效保证，因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题.针对当前构件化软件设计过程中，信息流安全属性仅局限于二元安全级格模型的问题，在现有安全接口结构基础上提出广义安全接口结构，在广义安全接口结构上定义精化关系，并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性，首次将安全多执行的思想应用于构件化系统的信息流安全属性验证.使用Coq定理证明工具实现了接口自动机程序库以及对精化关系的判定过程，并用实例验证说明了无干扰属性定义的特点及判定方法的有效性.
    Abstract: In the design and implementation of complicated component-based softwares, the security requirements on the whole system are hard to achieve due to the difficulty on enforcing the compositionality of the security properties. The specification and verification of security properties are the critical issues in the development of component-based softwares. In this paper, we focus on the generalization on the security lattice over the information flow security properties enforceable on the component-based softwares. The previous definitions of the information flow security properties in the component-based design are restricted on the binary security lattice model. In this work, we extend the interface structure for security to the generalized interface structure for security (GISS). We define a refinement relation and use this relation to give a non-interference definition (SME-NI) based on the principle of secure multi-execution. This is the first application of secure multi-execution on the information flow security verification of component-based systems. The new definition of non-interference can be adapted to any finite security lattice models. The Coq proof assistant is used to implement the certified library for interface automata, as well as the decision procedure for the refinement relation. The experimental results show the characteristics of SME-NI and the validity of decision procedure.
    • HTML全文
    • 参考文献(0)
    • 相关文章
    • 施引文献(27)

  • 期刊类型引用(15)

    1. 吴佳青，任大鹏. 我国人工智能芯片发展探析. 中国工程科学. 2025(01): 133-141 . 百度学术
    2. 仝杰，齐子豪，蒲天骄，宋睿，张鋆，谈元鹏，王晓飞. 电力物联网边缘智能：概念、架构、技术及应用. 中国电机工程学报. 2024(14): 5473-5496 . 百度学术
    3. 万朵，胡谋法，肖山竹，张焱. 面向边缘智能计算的异构并行计算平台综述. 计算机工程与应用. 2023(01): 15-25 . 百度学术
    4. 赵二虎，吴济文，肖思莹，晋振杰，徐勇军. 嵌入式异构智能计算系统并行多流水线设计. 电子学报. 2023(11): 3354-3364 . 百度学术
    5. 李秀敏，陈梓烁，陈雅琪. 我国人工智能芯片产业协同创新网络时空演化特征分析. 科技管理研究. 2023(23): 142-153 . 百度学术
    6. 赵一煊，刘飞阳，高晗，王建生. DNN加速器技术发展及航空计算系统应用展望. 航空计算技术. 2022(03): 130-134 . 百度学术
    7. 谢坤鹏，卢冶，靳宗明，刘义情，龚成，陈新伟，李涛. FAQ-CNN:面向量化卷积神经网络的嵌入式FPGA可扩展加速框架. 计算机研究与发展. 2022(07): 1409-1427 . 本站查看
    8. 蒲明博，李向平，张杨，郑美玲，粟雅娟，曹耀宇，曹暾，徐挺，段宣明，冯帅，孙玲. 芯片制造中的光学微纳加工技术前沿与挑战. 中国科学基金. 2022(03): 460-467 . 百度学术
    9. 高原，杨娇，赵凌，温川飙，张艺凡，罗悦. 运用人工神经网络技术结合穴位敏化理论探索慢性稳定性心绞痛疾病辅助预测模型的构建思路. 世界科学技术-中医药现代化. 2021(02): 628-634 . 百度学术
    10. 渠鹏，陈嘉杰，张悠慧，郑纬民. 实现软硬件解耦合的类脑计算硬件设计方法. 计算机研究与发展. 2021(06): 1146-1154 . 本站查看
    11. 魏东，董博晨，刘亦青. 改进神经网络的图像识别系统设计与硬件实现. 电子与信息学报. 2021(07): 1828-1833 . 百度学术
    12. 张雪怡，曹哲，刘宗宝. 智能芯片技术发展综述及医疗健康领域应用. 中国集成电路. 2021(09): 16-22+36 . 百度学术
    13. 郭经红，梁云，陈川，陈硕，陆阳，黄辉. 电力智能传感技术挑战及应用展望. 电力信息与通信技术. 2020(04): 15-24 . 百度学术
    14. 袁烨，张永，丁汉. 工业人工智能的关键技术及其在预测性维护中的应用现状. 自动化学报. 2020(10): 2013-2030 . 百度学术
    15. 赵晨，周义明. 基于FPGA的模数转换芯片AD7705/AD7706控制电路设计. 北京石油化工学院学报. 2019(04): 54-58 . 百度学术

    其他类型引用(12)

    • 资源附件(0)
计量
  • 文章访问数:  1132
  • HTML全文浏览量:  0
  • PDF下载量:  431
  • 被引次数: 27
出版历程
  • 发布日期:  2015-06-30

目录

摘要
HTML全文
    参考文献(0)
    相关文章
    施引文献(27)
    资源附件(0)

    /

    返回文章
    返回
    邮件订阅 RSS
    微信订阅号<br/>（实时资讯）

    微信订阅号
    （实时资讯）

    微信服务号<br/>（同步网站）

    微信服务号
    （同步网站）

    微信视频号<br/>（视频分享）

    微信视频号
    （视频分享）

    CCF<br/>（扫码入会）

    CCF
    （扫码入会）

    版权所有 © 《计算机研究与发展》编辑部

    本系统由北京仁和汇智信息技术有限公司开发  百度统计