面向程序可达性验证的数组处理循环压缩方法

计算机软件的安全性和健壮性逐渐成为一个非常重要的问题,而自动软件形式化验证是一种验证软件程序安全性和健壮性的可靠性较高的方法。在自动软件形式化验证中,大规模数组和复杂循环导致状态爆炸,使得验证器无法在规定时间内完成验证,因此如何在保证验证正确性的前提下压缩数组规模是一个值得研究的课题。文章提出复杂循环等价类的定义和相关命题,并提出一种面向程序可达性验证的数组处理循环压缩方法,先利用控制流自动机和系统依赖图进行静态分析划分等价类,再根据循环依赖关系对等价类进行压缩,用压缩后程序的验证结果代替原始程序的验证结果。实验结果表明,文章提出的方法能够在保证验证正确性的前提下压缩程序的规模,提高验证效率。

基于异质信息网络的安卓虚拟化程序检测方法

考虑到安卓应用虚拟化技术的功能特性,精确检测安卓虚拟化程序是识别其隐藏安全风险的基础和必要前提。为此,提出了基于异质信息网络的安卓虚拟化程序检测方法,并实现了原型系统Aiplugin。根据安卓虚拟化程序的特点,提取四类静态程序特征,并将程序特征映射到异质信息网络上,以元路径的形式将不同程序关联起来。采用异质图注意力网络表征算法和OC-SVM算法,融合不同视图的程序语义信息,实现对安卓虚拟化程序的表征和分类。实验结果表明,相较于当前的代表性工具VAhunt,Aiplugin可有效检测包括平行空间等更多类型的安卓虚拟化程序。

基于SmartVerif的比特币底层协议算力盗取漏洞发现

比特币引入了一种新的P2P(Peer to Peer)交易方法,并依靠其底层协议实现去中心化交易.然而,由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模,比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则,系统地抽象了多协议组合运行考虑下的比特币协议实体交互,完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比,本文更细粒度地建模了比特币协议实体及其相关操作,并全面设计了满足比特币各实体需求的安全属性.此外,本文利用自动化形式化验证系统SmartVerif实现了无需额外手工推导证明的形式化验证实验,通过将本文所建模的符号模型规则与引理作为SmartVerif的输入,发现了比特币底层协议算力盗取攻击.

安卓应用中无声音频的收集与检测

在安卓系统中,一些安卓应用为了避免被系统杀死,会通过各种方式在后台占用系统的CPU,内存等资源,实现后台保活.这类行为会加速安卓系统的电量消耗.其中一种后台保活的方式是在后台持有Audiomix锁并播放无声音频.针对这种行为,本文设计了相应的方案来检测这个问题.通过对安卓源码进行修改,收集到安卓应用正在播放的音频数据,再通过检测脚本对音频进行实时检测,来判断安卓应用是否在后台播放无声音频来实现保活.实验分析了50个安卓应用,结果表明该方法可以有效检测此类行为.

一种面向安卓网络传输任务的智能感知节能技术

电量是移动设备的一种关键资源。在移动应用的所有操作中,网络操作是电量消耗的主要部分,而网络数据传输是网络操作中最消耗电量的操作之一。如果能够确定网络传输任务的状态,那么就能为后续针对网络的电量优化提供更多有价值的信息。提出一种面向安卓网络传输任务的智能感知节能技术,通过重传报文、传输任务的关联文件状态、传输速率变化等特征来识别当前网络传输任务所处的状态,并针对不同状态应用相应的节能方案。实验结果显示,该智能感知节能技术能准确识别传输任务的状态,并有效降低网络传输任务的电量消耗。