多线程程序数据竞争随机森林指令级检测模型

数据竞争是典型的多线程程序并发缺陷。由于多线程程序中存在不确定性的交织,数据竞争很难被检测出来。该文以多线程数据竞争的5个相关属性作为特征,构建了多线程程序数据竞争随机森林指令级检测模型。首先基于happens-before关系与lockset算法指令级检测数据竞争,同时用汇编源码信息来剔除隐形同步对,然后利用happens-before关系与lockset算法的分析结果训练多线程程序数据竞争随机森林检测模型。在Pin上实现了多线程程序数据竞争检测工具AIRaceTest。利用GitHub中多线程程序的插桩结果作为样本集来训练随机森林模型,模型精度可达92.1%。对Google data-race-test、 Parsec基准程序3.1中的经典多线程程序的检测结果表明:AIRaceTest与Eraser、 Djit+以及Thread Sanitizer这3种目前常用的数据竞争检测工具相比,数据竞争的误报和漏报分别降低了约10.6%和12.3%,在线程数较多的情况下,时间和内存开销分别降低了41.8%和22.4%。     

扩展π演算对时间相关移动并发系统的建模与推演

针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。     

基于Pi演算的SDLO学习服务建模研究

根据Pi演算对SDLO学习服务进行建模,并通过实验证明所建立的基于Pi演算的SDLO学习服务模型具有合理性和可行性.     

一种基于系统行为序列特征的Android恶意代码检测方法

基于行为特征建立机器学习模型是目前Android恶意代码检测的主要方法,但这类方法的特征集中各行为特征相互独立,而行为特征间的顺序关系是反映恶意行为的重要因素。为了进一步提高检测准确率,提出了一种基于系统行为序列特征的Android恶意代码检测方法。该方法提取了程序运行发生的敏感API调用、文件访问、数据传输等系统活动的行为序列,基于马尔科夫链模型将系统行为序列转换为状态转移序列并生成了状态转移概率矩阵,将状态转移概率矩阵和状态发生频率作为特征集对SAEs模型进行了学习和训练,最后利用训练后的SAEs实现了对Android恶意代码的检测。实验结果证明,提出的方法在准确率、精度、召回率等指标上优于典型的恶意代码检测方法。     

基于符号模型自动分析隐私保留的用户认证协议安全性

利用大数据特征,PPMUAS协议声称实现了移动用户的隐私保护和认证,但并没有给出严格证明.故本文首先应用Applied PI演算对PPMUAS协议进行形式化描述,然后分别使用非单射一致性和Query对认证性和秘密性进行建模,最后把PPMUAS协议的Applied PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析与证明.结果表明PPMUAS协议具有秘密性,但缺少认证性,并给出了解决方法.     

并发计算的元模型Ⅰ.图模型

借鉴证明论中的一些思想 ,提出了并发计算的一个图模型 .在此模型中 ,计算对象表示为图 ,计算过程表示为图重写 ,重写规则将通信过程视为证明的等价变换过程 .为便于形式化研究图模型 ,提出了模型的形式对应物——图演算 ,该演算类似于进程代数演算 ,与其他进程代数演算的不同之处在于本演算是对称的 .文中用证明论方法研究并行理论 ,为进程代数演算开辟了一条新的研究途径     

并发计算的元模型Ⅰ.图模型

借鉴证明论中的一些思想 ,提出了并发计算的一个图模型 .在此模型中 ,计算对象表示为图 ,计算过程表示为图重写 ,重写规则将通信过程视为证明的等价变换过程 .为便于形式化研究图模型 ,提出了模型的形式对应物——图演算 ,该演算类似于进程代数演算 ,与其他进程代数演算的不同之处在于本演算是对称的 .本文用证明论方法研究并行理论 ,为进程代数演算开辟了一条新的研究途径 .     

动态软件体系结构建模方法研究

针对用现有方法对动态体系结构建模的不足，提出了一种软件体系结构抽象模型（SAAM）．sAAM以两种互为补充的形式化方法——面向对象Petri网OPN和π演算为语义基础，其中OPN可以形象地描述软件体系结构的初始化模型和动态行为，π演算可以描述软件体系结构的动态演化．这两种形式化方法通过SAAM集成在一起，并通过相应的支持工具对模型进行分析．在体系结构演化过程中，SAAM利用π演算的相关分析方法，对组件的演化策略和软件体系结构的一致性进行分析，从而可以在系统开发早期发现体系结构级的错误，提高软件质量．利用SAAM对经典实例自动加油站系统进行的建模与分析表明，SAAM直观、易懂，可以有效地刻画系统动态体系结构．     

温控系统的π-演算的描述与验证

根据温控系统的特征以及需求说明,利用π-演算构建了该系统动态行为的交互模型,依据π-演算的反应规则仿真描述模型的行为交互过程,使用μ-演算和移动工作平台(MWB)工具分析和验证了该交互模型具有温度控制和阈值修改功能,从形式上证明了温控系统的需求说明及其π-演算模型的一致性。结果表明,π-演算能够清楚地描述和分析并发系统的行为交互,而μ-演算可以证明模型的有效性和正确性。     

基于Pi-演算的集成P2P模式的网格形式化建模

为了改进传统网格的可扩展性和动态性,提出了一种集成P2P模式的网格资源管理模型,该模型融合了网格计算和对等计算的优点.基于该模型,文中分析了一种集成P2P模式的网格体系结构,并利用Pi-演算可用于对并发和动态变化的系统进行建模的特性,对该体系结构进行描述和建模,分析了有关性能,验证了模型的有效性.结果表明,基于Pi-演算的集成P2P模式的网格形式化系统能够有效地满足网格节点的服务需求.     

基于时序可中断π演算的BPEL和BPEL4People建模

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了πit演算的语法和语义,定义了一类强互模拟关系来判定πit演算进程间的行为等价,然后使用πit演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。     

系统生物模型转换研究--从SBML到 Stochastic Pi Calculus

分析了系统生物标记语言（SBML）模型和用随机Pi演算对生物建模（BioSPI）的不同特点,给出了两种模型之间转换的一系列处理规则;在规则的指导下将具体的SBML模型转换为BioSPI表示的程序语言,并借助分析工具来模拟该SBML模型运动变化过程,提出了自动实现转换的方法以及将转换扩展到其他进程演算形式的构想。     

一种针对Android系统隐私保护机制有效性的评估方法

为了保护用户的隐私数据,Android实现了一套基于权限的安全机制.为此设计了一种针对该机制的评估工具PrivacyMiner,以检测其在隐私保护方面的有效性.首先将Android系统中的隐私数据分为22个类别;然后使用动态检测与静态污点分析相结合的方法,来检测Android系统的安全机制是否能有效地保护它们.用PrivacyMiner工具对12个版本的Android源代码进行了检测,发现其中有7个类别的隐私数据并没有得到有效的保护,恶意软件可以在用户不知情的情况下读取这些隐私,并发送到任意服务器上.这些漏洞在6个Android设备上得到了验证,从Android2.1到最新发布的Android 4.4.2,均得到了Android安全团队的确认.     

Modeling BPEL and BPEL4People with a Timed Interruptable n-Calculus

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了7ci。演算的语法和语义,定义了一类强互模拟关系来判定πit算进程间的行为等价,然后使用πit。演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。     

自动信任协商安全性的形式化分析与验证

为了对自动信任协商(ATN)的安全性进行形式化分析与验证,文中借鉴安全协议的形式化分析方法,提出一种用进程代数Applied π演算对ATN建模并验证其安全性的方法.该方法将ATN形式化为两个协商者进程的并发执行,其中一个协商者的进程就是对其拥有的证书及授权策略的静态建模;ATN的安全性被定义为Applied π演算的观察等价性,从而使该方法不仅能检查授权策略执行的安全性,而且能对协商者的隐私安全进行验证.借助安全协议的自动分析工具ProVerif,文中实现了对ATN安全性的自动分析.实验结果表明,用Applied π演算形式化及验证ATN的安全性是可行的,安全性验证可自动完成,并且效率较高.     

基于π演算的协同商务主体的交互行为描述

对商务主体的协同交互行为的描述是多主体协同电子商务系统模型描述中的重要部分,本文采用π演算的描述方法对商务主体的协同行为(计划)进行形式化描述。     

嵌套式移动Agent的形式化研究

应用任务Agent和巡航Agent构造了移动Agent分布式网络管理模型,采用进程代数方法p演算对该模型中Agent间的嵌套过程、交互行为和验证过程等部分行为进行了形式化的描述,从理论上验证了在大型网络中使用嵌套式移动Agent进行分布式管理的可能性.     

一种面向分布式系统的行为分析和检测方法

提出了一种基于进程代数的行为分析与检测方法.通过静态分析二进制码获得系统的控制流程图,并将其转换为进程表达式;通过消除表达式不确定性、添加并发操作以及约简归并等方式对表达式进行重写;根据并发规则消除进程表达式中的并发算子,建立分布式系统的行为检测模型,并给出行为检测的方法.理论分析和实验表明:所提出的方法降低了行为分析和检测的复杂度,在控制流分析方面具有较好的精确性.     

基于π演算的云服务安全检测

利用π演算对云服务流程进行形式化描述,基于描述结果给出一种针对用户越权访问和服务不完整两种安全性问题的检测方法.基于云环境下的虚拟机部署实例对该方法的流程进行了说明,并将该方法与Bayes网和预测规则集等安全检测方法进行对比.结果表明,该方法能同时保证云服务过程的一致性和安全性.     

基于变精度粗糙集的入侵检测研究

网络行为的复杂性和动态变化使得入侵检测数据中存在大量干扰信息,入侵检测的误警率和漏警率很高,变精度粗糙集增强了粗糙集模型的抗干扰能力,适合分析不确定的数据集合。运用变精度粗糙集为入侵检测系统进行形式化描述,建立入侵检测信息系统和入侵检测模型。设计β参数调整算法,将训练数据集离散化后进行信息系统约简,然后生成入侵检测规则库,根据规则库进行入侵检测。模拟实验证明本方法具有良好的检测性能,可以适应网络行为的动态变化并检测出潜在的攻击行为。