概率信息流安全属性分析 被引量：6

1

作者 赵保华 陈波 陆超 《计算机学报》 EI CSCD 北大核心 2006年第8期1447-1452,共6页

以进程代数作为分析信息流安全属性的工具,将安全进程代数(SPA)扩展到概率系统,形成概率安全进程代数.使用概率安全进程代数对概率系统建模,在弱概率互拟等价的基础上,讨论了概率信息流安全属性,提出了P_PBNDC,S_PBNDC,CP_PBNDC等基于... 以进程代数作为分析信息流安全属性的工具,将安全进程代数(SPA)扩展到概率系统,形成概率安全进程代数.使用概率安全进程代数对概率系统建模,在弱概率互拟等价的基础上,讨论了概率信息流安全属性,提出了P_PBNDC,S_PBNDC,CP_PBNDC等基于复合的不可演绎的属性,分析了这些安全属性之间的关系,并给出了一个实际的概率系统的例子. 展开更多

关键词 信息流安全 概率配置 进程代数 无干扰 弱互拟

下载PDF 职称材料

隐蔽通道发现技术综述 被引量：5

2

作者 夏耐 林志强 +1 位作者 茅兵 谢立 《计算机科学》 CSCD 北大核心 2006年第12期1-5,共5页

本文首先解释了隐蔽通道的概念,介绍了隐蔽通道的分类。然后花主要精力,结合实例概述了当代国际上已经使用过的隐蔽通道的方法。并且对目前已有的这些方法从不同的方面给出了对比性的评价。在文章的讨论部分,作者基于目前的形势以及传... 本文首先解释了隐蔽通道的概念,介绍了隐蔽通道的分类。然后花主要精力,结合实例概述了当代国际上已经使用过的隐蔽通道的方法。并且对目前已有的这些方法从不同的方面给出了对比性的评价。在文章的讨论部分,作者基于目前的形势以及传统发现方法的限制给出了针对隐蔽通道发现方法建设性的见解和展望。 展开更多

关键词 隐蔽通道 安全系统 机密性 安全保护 信息流安全

下载PDF 职称材料

基于Yosys的硬件信息流安全验证与漏洞检测 被引量：4

3

作者 陈春雷 王省欣 +2 位作者 谭静 朱嘉诚 胡伟 《计算机应用研究》 CSCD 北大核心 2021年第6期1865-1869,共5页

针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为... 针对基于功能验证和侧信道分析的硬件安全漏洞检测方法的不足,提出了一种结合Yosys形式化验证能力和门级信息流追踪方法对集成电路设计进行安全验证和漏洞检测的方案。首先,使用Yosys对硬件电路设计进行逻辑综合,生成门级网表。其次,为电路设计中各信号的每个比特位添加污染标签,并采用二进制位粒度的污染标签传播策略为基本逻辑单元生成门级信息流模型,进而以此为基本单元构建整个电路的信息流模型。然后,描述电路设计中关键数据的机密性和完整性属性,并将其映射为Yosys可识别的安全约束。最后,结合Yosys和电路的信息流模型对电路设计的安全属性进行验证,安全验证中捕捉到违反安全属性的事件,即表明硬件设计中存在安全漏洞。实验表明,该方法能够准确检测到AES加密电路中植入的一种可满足性无关项木马。实验结果验证了该方法能够在不依赖功能验证和侧信道分析的前提下检测到安全漏洞,因而适用范围更广。 展开更多

关键词 硬件安全 信息流安全 安全验证 漏洞检测 Yosys

下载PDF 职称材料

L4虚拟内存子系统的形式化验证

4

作者 章乐平 赵永望 +2 位作者 王布阳 李悦欣 冯潇潇 《软件学报》 EI CSCD 北大核心 2023年第8期3527-3548,共22页

第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟... 第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等;形式化了功能正确性、功能安全和信息安全三方面的属性;通过部分正确性、不变式以及展开条件的推理,在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中,发现源代码在功能正确性和信息安全方面共存在3点问题,给出了相应的解决方案或建议. 展开更多

关键词 L4 形式化验证 内存管理 映射 信息流安全 Isabelle/HOL

下载PDF 职称材料

TaintPoint:使用活跃轨迹高效挖掘污点风格漏洞 被引量：3

5

作者 方浩然 郭帆 李航宇 《软件学报》 EI CSCD 北大核心 2022年第6期1978-1995,共18页

覆盖反馈的灰盒Fuzzing已经成为漏洞挖掘最有效的方式之一.广泛使用的边覆盖是一种控制流信息,然而在面向污点风格(taint-style)的漏洞挖掘时,这种反馈信息过于粗糙.大量污点无关的种子被加入队列,污点相关的种子数量又过早收敛,导致Fuz... 覆盖反馈的灰盒Fuzzing已经成为漏洞挖掘最有效的方式之一.广泛使用的边覆盖是一种控制流信息,然而在面向污点风格(taint-style)的漏洞挖掘时,这种反馈信息过于粗糙.大量污点无关的种子被加入队列,污点相关的种子数量又过早收敛,导致Fuzzing失去进化方向,无法高效测试Source和Sink之间的信息流.首先,详细分析了现有反馈机制在检测污点风格漏洞时不够高效的原因;其次,提出了专门用于污点风格漏洞挖掘的模糊器TaintPoint.TaintPoint在控制流轨迹的基础上加入了活跃污点这一数据流信息,形成活跃轨迹(livetrace)作为覆盖反馈,并围绕活跃轨迹分别在插桩、种子过滤、选择和变异阶段改进现有方法.在UAFBench上的实验结果表明:TaintPoint检测污点风格漏洞的效率、产出和速度优于业界领先的通用模糊器AFL++及定向模糊器AFLGO;此外,在两个开源项目上发现了4个漏洞并被确认. 展开更多

关键词 静态分析 模糊测试 覆盖反馈 信息流安全 污点分析

下载PDF 职称材料

TrustZone中断隔离机制的形式化验证

6

作者 付俊仪 张倩颖 +3 位作者 王国辉 李希萌 施智平 关永 《小型微型计算机系统》 CSCD 北大核心 2023年第9期2105-2112,共8页

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断... TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道. 展开更多

关键词 TRUSTZONE 可信执行环境 中断隔离 信息流安全 形式化验证

下载PDF 职称材料

动态环境中的概率信息流安全 被引量：2

7

作者 赵保华 陈波 陆超 《西安交通大学学报》 EI CAS CSCD 北大核心 2006年第8期874-877,954,共5页

在概率安全进程代数的基础上,研究了概率系统在动态环境中的信息流安全,以解决可动态配置的恶意进程对系统带来的危害.同时,提出了动态环境中的概率互拟复合不可演绎性质,即持久P-PBNDC.使用敌意环境下的弱概率互拟和动态敌意环境等概... 在概率安全进程代数的基础上,研究了概率系统在动态环境中的信息流安全,以解决可动态配置的恶意进程对系统带来的危害.同时,提出了动态环境中的概率互拟复合不可演绎性质,即持久P-PBNDC.使用敌意环境下的弱概率互拟和动态敌意环境等概念讨论了P-PBNDC是概率系统在动态环境中合适的信息流安全性质,该性质能够揭露出概率互拟复合不可演绎性质(PBNDC)所不能暴露的潜在的安全隐患.最后,证明了P-PBNDC和SBSPNI性质的一致性,在限制算子和前缀算子下的P-PBNDC具有复合性质,而在并行算子下不具有复合性质. 展开更多

关键词 信息流安全 进程代数 动态环境

下载PDF 职称材料

信息流安全技术回顾与展望 被引量：3

8

作者 张迎周 刘玲玲 《南京邮电大学学报（自然科学版）》 2011年第5期87-96,共10页

随着计算机和网络技术的迅猛发展,计算机系统和开放式的网络系统受到的攻击也日益增多。访问控制、入侵检测、加密等传统的安全机制只注重控制信息的释放,不能充分保证信息端到端的安全。信息流的方法通过分析系统中信息的流动,确保流... 随着计算机和网络技术的迅猛发展,计算机系统和开放式的网络系统受到的攻击也日益增多。访问控制、入侵检测、加密等传统的安全机制只注重控制信息的释放,不能充分保证信息端到端的安全。信息流的方法通过分析系统中信息的流动,确保流动的信息都是合法的。介绍了信息流的基本模型、信息流分析的几种典型方法及其应用,并对它们进行了分析比较,最后给出了现有的信息流分析方法中存在的问题和未来的研究方向。结果表明采用信息流分析方法实现信息端到端的安全是可行的。 展开更多

关键词 信息流安全 语义模型 类型系统 形式化方法

下载PDF 职称材料

基于模型检测的服务链信息流安全可组合验证方法 被引量：3

9

作者 习宁 马建峰 +2 位作者 孙聪 卢笛 张涛 《通信学报》 EI CSCD 北大核心 2014年第11期23-31,共9页

提出了一种可组合的服务链信息流安全验证方法。在保证单一组件信息流安全的基础上,给出相邻组件可组合的信息流安全条件和验证算法。实验和仿真结果表明,相比传统模型检测方法,所提的可组合验证算法能够有效减小验证开销,提高验证效率。

关键词 模型检测 服务链 信息流安全 可组合

下载PDF 职称材料

服务组合安全隐私信息流静态分析方法 被引量：2

10

作者 彭焕峰 黄志球 +2 位作者 刘林源 李勇 柯昌博 《软件学报》 EI CSCD 北大核心 2018年第6期1739-1755,共17页

用户为使用服务组合提供的功能,需要提供必要的个人隐私数据.由于组合的业务逻辑对用户是透明的,且用户与成员服务之间缺乏隐私数据使用的相关协议,如何保证组合执行过程中不发生用户隐私信息的非法泄露,成为当前服务计算领域的研究热... 用户为使用服务组合提供的功能,需要提供必要的个人隐私数据.由于组合的业务逻辑对用户是透明的,且用户与成员服务之间缺乏隐私数据使用的相关协议,如何保证组合执行过程中不发生用户隐私信息的非法泄露,成为当前服务计算领域的研究热点之一.针对隐私保护特征,提出一种服务组合安全隐私信息流静态分析方法.首先,从服务信誉度、隐私数据使用目的及保留期限这3个维度提出一种面向服务组合的隐私信息流安全模型;其次,采用支持隐私信息流分析的隐私工作流网(privacy workflow net,简称PWF-net)构建服务组合模型,并通过静态分析算法分析组合执行路径,检测组合的执行是否会发生用户隐私信息的非法泄露;最后,通过实例分析说明了方法的有效性,并对方法性能进行了实验分析.与现有的相关工作相比,针对隐私保护特征提出了隐私信息流安全模型,且分析方法考虑了隐私数据项聚合问题,从而能够更为有效地防止用户隐私信息非法泄露. 展开更多

关键词 服务组合 隐私保护 信息流安全 安全模型 静态分析 工作流网

下载PDF 职称材料

基于安全进程代数的信息流模型 被引量：1

11

作者 尹青 周伟 郭金庚 《信息工程大学学报》 2004年第3期5-9,共5页

文章在安全进程代数理论框架内讨论信息流安全模型。基于进程代数语义理论,研究了无干扰性质及不可演绎性质的构造、关系及可复合性。

关键词 安全进程代数 信息流安全 无干扰 不可演绎

下载PDF 职称材料

基于接口精化的广义无干扰性研究 被引量：2

12

作者 孙聪 习宁 +3 位作者 高胜 张涛 李金库 马建峰 《计算机研究与发展》 EI CSCD 北大核心 2015年第7期1631-1641,共11页

在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题.针对当前构件化软件设计过程中,信息流安全属性仅... 在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题.针对当前构件化软件设计过程中,信息流安全属性仅局限于二元安全级格模型的问题,在现有安全接口结构基础上提出广义安全接口结构,在广义安全接口结构上定义精化关系,并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性,首次将安全多执行的思想应用于构件化系统的信息流安全属性验证.使用Coq定理证明工具实现了接口自动机程序库以及对精化关系的判定过程,并用实例验证说明了无干扰属性定义的特点及判定方法的有效性. 展开更多

关键词 信息流安全 无干扰性 接口自动机 精化 构件化设计

下载PDF 职称材料

广义不可推断属性符号化算术验证的研究 被引量：1

13

作者 周从华 吴海玲 鞠时光 《计算机研究与发展》 EI CSCD 北大核心 2012年第12期2591-2602,共12页

多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证... 多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证方法——"展开方法"——验证的仅仅是属性成立的一个充分非必要条件,因此是不完备的.基于证伪技术提出一种完备的广义不可推断属性验证方法,该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程.为确保搜索过程能正确终止,即方法的完备性,提出状态转换系统的双构造运算,并在此基础上基于图结构理论给出最短反例的上近似计算.进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现了验证过程的符号化计算.最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用. 展开更多

关键词 广义不可推断属性 信息流安全 量化布尔公式 多级安全系统 隐通道

下载PDF 职称材料

基于下推系统可达性分析的程序机密消去机制 被引量：1

14

作者 孙聪 唐礼勇 陈钟 《软件学报》 EI CSCD 北大核心 2012年第8期2149-2162,共14页

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

关键词 信息流安全 机密消去 下推系统 自动验证 程序分析

下载PDF 职称材料

概率系统的非传递无干扰安全属性分析 被引量：1

15

作者 姜励 平玲娣 +2 位作者 陈小平 潘雪增 李善平 《浙江大学学报（工学版）》 EI CAS CSCD 北大核心 2008年第12期2092-2096,共5页

为了实现概率信息的安全降密和信道控制等重要安全策略,将可信域的概念引入概率安全进程代数,并以此为工具将非传递无干扰信息流安全模型推广到概率系统.在弱概率互拟等价的基础上讨论了非传递概率信息流安全属性,提出了非传递概率互拟... 为了实现概率信息的安全降密和信道控制等重要安全策略,将可信域的概念引入概率安全进程代数,并以此为工具将非传递无干扰信息流安全模型推广到概率系统.在弱概率互拟等价的基础上讨论了非传递概率信息流安全属性,提出了非传递概率互拟强无干扰(I_BSPNI)和非传递概率互拟复合不可演绎(I_PBNDC)安全属性;并要求系统所有可达状态都满足的持久I_PBNDC属性,该性质能够揭露出I_PBNDC在动态环境中不能暴露的安全隐患.为了弥补互拟复合不可演绎类性质难于验证的缺点,使用基于单步状态的展开条件定义了强I_PBNDC属性.最后分析并证明了这些安全属性之间的包含关系. 展开更多

关键词 非传递无干扰 信息流安全 概率系统 进程代数 弱互拟

下载PDF 职称材料

多级安全信息流控制关键技术研究

16

作者 黄凡帆 尹超 《航空计算技术》 2019年第2期87-90,95,共5页

目前机载嵌入式系统平台呈现开放式的特点,通过支持TCP/IP协议和多种网络服务来方便部署各种应用,使得功能多样化的需求得以满足。这也导致系统更容易遭受网络攻击,应用网络安全协议可保护网络传输数据的信息安全属性。但目前机载嵌入... 目前机载嵌入式系统平台呈现开放式的特点,通过支持TCP/IP协议和多种网络服务来方便部署各种应用,使得功能多样化的需求得以满足。这也导致系统更容易遭受网络攻击,应用网络安全协议可保护网络传输数据的信息安全属性。但目前机载嵌入式系统多是不同应用运行在不同分区,分区具有不同信息安全级别,分区之间交互的信息也表现为多级安全。当多级安全信息流在网络上流动时,需要提供安全机制进行不同强度安全防护。传统网络安全协议没有考虑这种多级安全情况,改进IPsec安全协议以提供网络上多级安全信息流控制功能。 展开更多

关键词 多级安全 分区通信 信息流安全 IPSEC协议

下载PDF 职称材料

基于无干扰理论的构件系统安全

17

作者 徐明迪 靳朝阳 +1 位作者 崔峰 张帆 《山东大学学报（理学版）》 CAS CSCD 北大核心 2020年第3期35-42,共8页

研究一种构件系统中多安全等级的信息流无干扰问题。在现有接口结构的基础上,使用安全进程代数描述构件系统动态行为语法和语义来构建接口自动化计算模型。研究基于互模拟的无干扰属性,构造适用于构件系统的接口安全无干扰性质SIA_NI,... 研究一种构件系统中多安全等级的信息流无干扰问题。在现有接口结构的基础上,使用安全进程代数描述构件系统动态行为语法和语义来构建接口自动化计算模型。研究基于互模拟的无干扰属性,构造适用于构件系统的接口安全无干扰性质SIA_NI,并证明系统在添加、删除、组合算子等复杂操作下依然满足此安全性。最后举例分析了此无干扰属性在构件化系统中的具体应用,并使用CoPS工具自动检查多安全等级构件系统的安全性,验证接口安全无干扰性质的正确性。 展开更多

关键词 信息流安全 无干扰 接口安全

原文传递

基于抽象解释的C程序信息保密性研究

18

作者 介颂园 钱俊彦 赵岭忠 《计算机工程》 CAS CSCD 北大核心 2010年第24期48-50,共3页

在分析程序具体语义的基础上,提出一种信息保密性检测方法。构造具体语义和抽象语义的对应关系,根据待测程序性质构建抽象语义,同时在抽象基础上,采用限界思想来优化检测的效率。通过该方法降低程序检测的复杂性,减少时间和空间的浪费,... 在分析程序具体语义的基础上,提出一种信息保密性检测方法。构造具体语义和抽象语义的对应关系,根据待测程序性质构建抽象语义,同时在抽象基础上,采用限界思想来优化检测的效率。通过该方法降低程序检测的复杂性,减少时间和空间的浪费,提高了检测的效率和准确度。 展开更多

关键词 信息流安全 模型检测 抽象解释

下载PDF 职称材料

寄存器传输级硬件设计信息流建模与安全验证

19

作者 秦茂源 侯佳滢 +2 位作者 李家乐 唐时博 邰瑜 《西北工业大学学报》 EI CAS CSCD 北大核心 2024年第3期506-513,共8页

近年来,已有大量研究证明信息流分析能够有效地对设计安全属性与安全行为进行建模。然而,现有的门级抽象层次的信息流分析方法往往受制于算力和验证效力等因素难以应对大规模设计,而RTL抽象层次的信息流分析方法需借助类型系统等形式化... 近年来,已有大量研究证明信息流分析能够有效地对设计安全属性与安全行为进行建模。然而,现有的门级抽象层次的信息流分析方法往往受制于算力和验证效力等因素难以应对大规模设计,而RTL抽象层次的信息流分析方法需借助类型系统等形式化语言对硬件设计进行重新描述。因此,提出了一种寄存器传输级硬件设计信息流建模与安全验证方法。该方法在寄存器传输级功能模型的基础上构建附加安全属性的信息流跟踪逻辑模型,从信息流角度建模设计安全行为和安全属性,并利用EDA测试验证工具,以无干扰为策略捕捉违反安全策略的有害信息流,检测硬件设计安全漏洞。以Trust-Hub硬件木马测试集为测试对象的实验结果表明:所提方法能够有效检测设计内潜藏的硬件木马。 展开更多

关键词 硬件安全 信息流安全模型 信息流安全验证 安全漏洞检测

下载PDF 职称材料

用数据流分析方法检查程序信息流安全 被引量：7

20

作者 黄海军 陈意云 《小型微型计算机系统》 CSCD 北大核心 2007年第1期102-106,共5页

程序信息流安全是信息安全的一个重要研究方向.基于类型的分析虽然是检查程序信息流安全的一种有效方法,但过于保守.本文尝试将传统的数据流分析方法用于程序信息流安全的检查,即利用数据流分析来跟踪程序数据间的安全依赖关系,达到检... 程序信息流安全是信息安全的一个重要研究方向.基于类型的分析虽然是检查程序信息流安全的一种有效方法,但过于保守.本文尝试将传统的数据流分析方法用于程序信息流安全的检查,即利用数据流分析来跟踪程序数据间的安全依赖关系,达到检查程序信息流安全的目的.和基于类型的方法相比,数据流分析方法能更加精确地分析程序,具有更大的宽容性.最后,本文对数据流分析方法的可靠性进行了证明. 展开更多

关键词 程序信息流安全 形式语义 静态分析 数据流分析

下载PDF 职称材料