信息流安全

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=软件学报x
共 条 记 录，以下是1-5
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
多时间无干扰性验证方法
《软件学报》2024年第10期4729-4750,共22页刘乔森 孙聪 魏晓敏 曾荟铭 马建峰 
国家自然科学基金(62272366,61872279);陕西省重点研发计划(2023-YBGY-371);陕西省自然科学基础研究计划(2021JQ-207)。
安全关键嵌入式软件的运行时行为通常具有严格时间约束,对安全属性的执行提出额外要求.针对嵌入式软件的信息流安全保护要求,以及现有安全性验证方法面向单一属性且存在假阳性等问题,首先从现实场景的安全需求出发,提出一种新的时间无...
关键词：无干扰性 时间自动机 精化关系 可达性分析 信息流安全 
L4虚拟内存子系统的形式化验证被引量：1
《软件学报》2023年第8期3527-3548,共22页章乐平 赵永望 王布阳 李悦欣 冯潇潇 
国家自然科学基金(62132014);浙江省尖兵计划(2022C01045)。
第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟...
关键词：L4 形式化验证 内存管理 映射 信息流安全 Isabelle/HOL 
TaintPoint:使用活跃轨迹高效挖掘污点风格漏洞被引量：4
《软件学报》2022年第6期1978-1995,共18页方浩然 郭帆 李航宇 
国家自然科学基金(61562040);江西省教育厅科技项目(GJJ200313)。
覆盖反馈的灰盒Fuzzing已经成为漏洞挖掘最有效的方式之一.广泛使用的边覆盖是一种控制流信息,然而在面向污点风格(taint-style)的漏洞挖掘时,这种反馈信息过于粗糙.大量污点无关的种子被加入队列,污点相关的种子数量又过早收敛,导致Fuz...
关键词：静态分析 模糊测试 覆盖反馈 信息流安全 污点分析 
服务组合安全隐私信息流静态分析方法被引量：2
《软件学报》2018年第6期1739-1755,共17页彭焕峰 黄志球 刘林源 李勇 柯昌博 
国家自然科学基金(61772270;61602262;61562087);国家高技术研究发展计划(863)(2015AA015303);江苏省自然科学基金(BK20150865;BK20130735);江苏省高校自然科学基金(15KJD520001;13KJB520011)~~
用户为使用服务组合提供的功能,需要提供必要的个人隐私数据.由于组合的业务逻辑对用户是透明的,且用户与成员服务之间缺乏隐私数据使用的相关协议,如何保证组合执行过程中不发生用户隐私信息的非法泄露,成为当前服务计算领域的研究热...
关键词：服务组合 隐私保护 信息流安全 安全模型 静态分析 工作流网 
基于下推系统可达性分析的程序机密消去机制被引量：1
《软件学报》2012年第8期2149-2162,共14页孙聪 唐礼勇 陈钟 
国家自然科学基金(60773163;60821003;60872041;60911140102);国家科技部重大专项(2011ZX03005-002);中央高校基本科研;业务费专项资金(JY100009030 01);装备预研基金(9140A15040210HK6101)
针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程...
关键词：信息流安全 机密消去 下推系统 自动验证 程序分析 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部