【摘 要】
：
基于无干扰理论和Hoare公理方法,针对并发进程中不可信代码带来的信息泄露问题,提出一种隐私性分析模型CPNIAM,一方面把并发程序功能正确性证明分化为对程序中所有并发进程的
【机 构】
：
武汉大学计算机学院/空天信息安全与可信计算教育部重点实验室,湖北武汉430072
【出 处】
：
第六届中国可信计算与信息安全学术会议
论文部分内容阅读
基于无干扰理论和Hoare公理方法,针对并发进程中不可信代码带来的信息泄露问题,提出一种隐私性分析模型CPNIAM,一方面把并发程序功能正确性证明分化为对程序中所有并发进程的形式化验证,以达到复杂程序简单化证明的目的;另一方面,可以在进程的功能正确性验证的基础上进行并发进程间的无干扰性分析.实例分析表明,相对于传统的无干扰模型,本文提出的模型可以在程序设计及实现阶段的形式化验证过程中,对由不可信代码导致的进程间隐私泄露问题进行分析,分析结果可指导程序设计者用于不可信代码定位和修改.
其他文献
为研究公兔在急性热应激过程中相关基因的表达及响应的分子机制,本研究以齐兴肉兔公兔为实验对象,构建热应激公兔睾丸精子发生模型,提取热应激组和对照组睾丸组织总RNA,反转
取是本事,舍是智慧。人生最大的智慧,还是舍得,少年时舍其不能有,壮年时舍其不当有,老年时舍其不必有。就是要提得起放得下,舍掉一些东西。舍得这个词很妙,有舍才有得。人的
Although there exist a few good schemes to protect the kernel hooks of operating systems,attackers are still able to circumvent existing defense mechanisms
超宽带通信系统(UWB)所占用的带宽非常宽,研究超宽带通信系统和其它通信系统间的电磁兼容问题对多通信系统的共存应用具有十分重要的实际意义。本文通过有针对性地选取无线信
针对加性水印中嵌入强度因子的自适应问题进行了研究,提出了一个基于信噪比的自适应音频水印算法.该算法在保证听觉质量的同时,利用信噪比自适应地调节嵌入强度因子,并将水印
针对某些恶意页面利用搜索引擎的局限性隐藏在搜索结果排名较靠前的位置这一问题,本文提出了基于Hits算法的Web安全改进模型.该模型在Hits算法的基础上,结合向量空间模型来评
提出了一种适用于无线多跳网络的基于故障诊断与恢复技术的拓扑容错控制方案,采用了基于比较的故障诊断方法来探测故障,并对节点故障的恢复方法进行了研究,实现了网络的拓扑
To protect against algebraic attacks,a high algebraic immunity is now an important criterion for Boolean functions used in stream ciphers.In this paper,a ne
本文从跨层感知的概念出发,将网络的多个层面和多个角度的态势信息作为评估工作的数据源,并建立了反映网络各方面态势信息的完整指标体系.采用模糊层次分析法构建了网络不同
分析了射频识别系统中匿名RFID认证协议存在的安全缺陷,指出攻击者可利用该协议存在的异或运算使用不当的安全缺陷发起身份假冒攻击.为此,提出了一种改进的RFID双向认证协议,