信息流安全

作品数:27被引量:53H指数:4
导出分析报告
相关领域:自动化与计算机技术更多>>
相关作者:黄海军孙聪陈意云习宁秦保力更多>>
相关机构:中国科学技术大学西安电子科技大学华中科技大学中国科学院软件研究所更多>>
相关期刊:《技术与创新管理》《航空计算技术》《中国电子商务》《山东大学学报(理学版)》更多>>
相关基金:国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家科技重大专项更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-10
视图:
排序:
多时间无干扰性验证方法
《软件学报》2024年第10期4729-4750,共22页刘乔森 孙聪 魏晓敏 曾荟铭 马建峰 
国家自然科学基金(62272366,61872279);陕西省重点研发计划(2023-YBGY-371);陕西省自然科学基础研究计划(2021JQ-207)。
安全关键嵌入式软件的运行时行为通常具有严格时间约束,对安全属性的执行提出额外要求.针对嵌入式软件的信息流安全保护要求,以及现有安全性验证方法面向单一属性且存在假阳性等问题,首先从现实场景的安全需求出发,提出一种新的时间无...
关键词:无干扰性 时间自动机 精化关系 可达性分析 信息流安全 
TrustZone中断隔离机制的形式化验证被引量:1
《小型微型计算机系统》2023年第9期2105-2112,共8页付俊仪 张倩颖 王国辉 李希萌 施智平 关永 
国家自然科学基金项目(61802375,61602325,61876111,61877040)资助;北京市教委科技计划一般项目(KM201910028005)资助;中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题项目(CARCH201920)资助;国防科技创新特区项目(18-163-11-ZT-005-038-05)资助;中央支持地方建设-“双一流”建设项目(20531120005)资助.
TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断...
关键词:TRUSTZONE 可信执行环境 中断隔离 信息流安全 形式化验证 
L4虚拟内存子系统的形式化验证被引量:1
《软件学报》2023年第8期3527-3548,共22页章乐平 赵永望 王布阳 李悦欣 冯潇潇 
国家自然科学基金(62132014);浙江省尖兵计划(2022C01045)。
第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟...
关键词:L4 形式化验证 内存管理 映射 信息流安全 Isabelle/HOL 
TaintPoint:使用活跃轨迹高效挖掘污点风格漏洞被引量:3
《软件学报》2022年第6期1978-1995,共18页方浩然 郭帆 李航宇 
国家自然科学基金(61562040);江西省教育厅科技项目(GJJ200313)。
覆盖反馈的灰盒Fuzzing已经成为漏洞挖掘最有效的方式之一.广泛使用的边覆盖是一种控制流信息,然而在面向污点风格(taint-style)的漏洞挖掘时,这种反馈信息过于粗糙.大量污点无关的种子被加入队列,污点相关的种子数量又过早收敛,导致Fuz...
关键词:静态分析 模糊测试 覆盖反馈 信息流安全 污点分析 
基于Yosys的硬件信息流安全验证与漏洞检测被引量:6
《计算机应用研究》2021年第6期1865-1869,共5页陈春雷 王省欣 谭静 朱嘉诚 胡伟 
国家自然科学基金资助项目(61672433)。
针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为...
关键词:硬件安全 信息流安全 安全验证 漏洞检测 Yosys 
基于无干扰理论的构件系统安全
《山东大学学报(理学版)》2020年第3期35-42,共8页徐明迪 靳朝阳 崔峰 张帆 
国家自然科学基金资助项目(61502438)。
研究一种构件系统中多安全等级的信息流无干扰问题。在现有接口结构的基础上,使用安全进程代数描述构件系统动态行为语法和语义来构建接口自动化计算模型。研究基于互模拟的无干扰属性,构造适用于构件系统的接口安全无干扰性质SIA_NI,...
关键词:信息流安全 无干扰 接口安全 
多级安全信息流控制关键技术研究
《航空计算技术》2019年第2期87-90,95,共5页黄凡帆 尹超 
装备预研联合基金项目资助(6141B05060401)
目前机载嵌入式系统平台呈现开放式的特点,通过支持TCP/IP协议和多种网络服务来方便部署各种应用,使得功能多样化的需求得以满足。这也导致系统更容易遭受网络攻击,应用网络安全协议可保护网络传输数据的信息安全属性。但目前机载嵌入...
关键词:多级安全 分区通信 信息流安全 IPSEC协议 
服务组合安全隐私信息流静态分析方法被引量:2
《软件学报》2018年第6期1739-1755,共17页彭焕峰 黄志球 刘林源 李勇 柯昌博 
国家自然科学基金(61772270;61602262;61562087);国家高技术研究发展计划(863)(2015AA015303);江苏省自然科学基金(BK20150865;BK20130735);江苏省高校自然科学基金(15KJD520001;13KJB520011)~~
用户为使用服务组合提供的功能,需要提供必要的个人隐私数据.由于组合的业务逻辑对用户是透明的,且用户与成员服务之间缺乏隐私数据使用的相关协议,如何保证组合执行过程中不发生用户隐私信息的非法泄露,成为当前服务计算领域的研究热...
关键词:服务组合 隐私保护 信息流安全 安全模型 静态分析 工作流网 
基于接口精化的广义无干扰性研究被引量:2
《计算机研究与发展》2015年第7期1631-1641,共11页孙聪 习宁 高胜 张涛 李金库 马建峰 
长江学者和创新团队发展计划项目(IRT1078);国家自然科学基金委员会--广东联合基金重点基金项目(U1135002);国家科技重大专项基金项目(2011ZX03005-002);国家自然科学基金项目(61303033;61272398);陕西省自然科学基础研究计划项目(2013JQ8036);中央高校基本科研业务费专项资金项目(JB140309);航空科学基金项目(2013ZC31003;20141931001)
在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题.针对当前构件化软件设计过程中,信息流安全属性仅...
关键词:信息流安全 无干扰性 接口自动机 精化 构件化设计 
基于模型检测的服务链信息流安全可组合验证方法被引量:3
《通信学报》2014年第11期23-31,共9页习宁 马建峰 孙聪 卢笛 张涛 
国家自然科学基金资助项目(U1135002;61303033);国家科技部重大专项基金资助项目(2011ZX03005-002);航空科学基金资助项目(2013ZC31003);陕西省自然科学基础研究计划基金资助项目(2013JQ8036)~~
提出了一种可组合的服务链信息流安全验证方法。在保证单一组件信息流安全的基础上,给出相邻组件可组合的信息流安全条件和验证算法。实验和仿真结果表明,相比传统模型检测方法,所提的可组合验证算法能够有效减小验证开销,提高验证效率。
关键词:模型检测 服务链 信息流安全 可组合 
检索报告 对象比较 聚类工具 使用帮助 返回顶部