A lightweight approach to component-level exception mechanism for robust android apps

Recent researches have reported that Android programs are vulnerable to unexpected exceptions. One reason is that the current design of Android platform solely depends on Java exception mechanism, which is unaware of the component-based structure of Android programs. This paper proposes a component-level exception mechanism for programmers to build robust Android programs with. With the mechanism, they can define an intra-component handler for each component to recover from exceptions, and they can propagate uncaught exceptions to caller component along the reverse of component activation flow. Theoretically, we have formalized an Android semantics with exceptions to prove the robustness property of the mechanism. In practice, we have implemented the mechanism with a domain-specific library that extends existing Android components. This lightweight approach does not demand the change of the Android platform. In our experiment with Android benchmark programs, the library is found to catch a number of runtime exceptions that would otherwise get the programs terminated abnormally. We also measure the overhead of using the library to show that it is very small. Our proposal is a new mechanism for defending Android programs from unexpected exceptions.     

All about activity injection: Threats,semantics, detection,and defense

Android supports seamless user experience by maintaining activities from different applications (apps) in the same activity stack. Although such close inter-app communication is essential in the Android framework, the powerful inter-app communication contains vulnerabilities that can inject malicious activities into a victim app's activity stack to hijack user interaction flows. In this article, we demonstrate activity injection attacks with a simple malware, and formally specify the activity activation mechanism using operational semantics. Based on the operational semantics, we develop a static analysis tool, which analyzes Android apps to detect activity injection attacks. Our tool is fast enough to analyze real-world Android apps in 6 seconds on average, and our experiments found that 1761 apps out of 129,756 real-world Android apps inject their activities into other apps' tasks. Moreover, we propose a defense mechanism, dubbed signature-based activity access control (SAAC), which completely prohibits activity injection attacks. The defense mechanism is general enough to keep the current Android multitasking features intact, and it is simple enough to be independent of the complex activity activation semantics, which does not increase activity activation time noticeably. With the extension of the formal semantics for SAAC, we prove that SAAC correctly mitigates activity injection attacks without any false alarms.     

以太坊中间语言的可执行语义

智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台（Ethereum）上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.本工作对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义（executable semantics）,由120个Yul语言程序组成的测试集进行测试.本工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.     

虚拟环境中装配设计语义的表达、传递与转化研究

研究了虚拟环境产品装配建模过程中装配语义的表达、装配语义与装配约束的转化技术,提出了采用语义－约束图对装配设计语义与约束进行维护。通过语义－约束图可以从语义层次和约束层次对产品装配模型进行编辑和维护。提出了采用模糊参量表达和处理产品装配设计中的模糊语义。基于模糊参量的语义表达不仅为设计信息输入提供了更大的自由度,而且扩展了计算机对模糊信息的处理能力,有利于产品设计意图的维护。通过产品装配信息从抽象到具体、从模糊到精确的转化,实现了虚拟装配设计系统对抽象、模糊设计信息的表达、传递与处理。     

A calculus for the construction of modular prolog programs

We present a module language for PROLOG based on the theory of modularity underlying the Standard ML module system. The language supports the construction of hierarchically structured programs from parametrized components and provides a form of structural data abstraction. A formal semantics is given for the system which translates modular programs into conventional programs     

一种基于双层语义的Android原生库安全性检测方法

原生代码已在Android应用中广泛使用,为恶意攻击者提供了新的攻击途径,其安全问题不容忽视。当前已有Android恶意应用检测方案,主要以Java代码或由Java代码编译得到的Dalvik字节码为分析对象,忽略了对原生代码的分析。针对这一不足,提出了一种基于双层语义的原生库安全性检测方法。首先分析原生方法Java层语义,提取原生方法函数调用路径,分析原生方法与Java层的数据流依赖关系以及原生方法函数调用路径的入口点。对于原生代码语义,定义了数据上传、下载、敏感路径读写、敏感字符串、可疑方法调用5类可疑行为,基于IDA Pro和IDA Python对原生代码内部行为进行自动分析。使用开源机器学习工具Weka,以两层语义作为数据特征,对5336个普通应用和3426个恶意应用进行了分析,最佳检测率达到92.4%,表明所提方法能够有效检测原生库的安全性。     

面向方面程序的动态语义研究

目前,针对面向方面程序,许多研究者已定义了各种各样的形式语义。但是,没有一种语义能被软件设计者和开发者所理解。针对该问题,在已有研究的基础上,应用统一程序理论中的设计来定义面向方面的动态语义。同时,以一个例子来说明该语义的使用。     

Android智能手机天气预报系统设计及实现

在分析讨论Android应用系统设计原理的基础上,提出了Android智能手机天气实况预报系统用户界面以及获取并解析城市列表数据的设计方法,给出了在用户界面上呈现列表数据的设计过程,实现了一个简单的Android智能手机城市天气实况预报系统.系统在模拟器上通过调试并正常运行.     

图卷积网络的抗混淆安卓恶意软件检测

自安卓发布以来,由于其开源、硬件丰富和应用市场多样等优势,安卓系统已经成为全球使用最广泛的手机操作系统。同时,安卓设备和安卓应用的爆炸式增长也使其成为96%移动恶意软件的攻击目标。现存的安卓恶意软件检测方法中,忽视程序语义而直接提取简单程序特征的方法检测速度快但精确度不理想,将程序语义转换为图模型并采用图分析的方法精确度高但开销大且扩展性低。为了解决上述挑战,本文将应用的程序语义提取为函数调用图,保留语义信息的同时采用抽象API技术将调用图转换为抽象图以减少运行开销并增强鲁棒性。基于得到的抽象图,以Triplet Loss损失训练构建基于图卷积神经网络的抗混淆安卓恶意软件分类器SriDroid。对20246个安卓应用进行实验分析之后,发现SriDroid可以达到99.17%的恶意软件检测精确度,并具有良好的鲁棒性。     

面向服务架构软件实现前的可靠性评价方法

为了在软件实现前评估其可靠性,针对基于面向服务架构(SOA)设计的软件提出了一种可靠性评价方法：用OWL-S描述软件的需求和设计信息,利用Maude为OWL-S过程模型的控制结构定义形式化语义,使用分布函数构建软件的操作剖面,在Maude中增加软件的操作剖面信息和体系结构信息如何参与可靠度计算的描述,在Maude系统的支持下,通过重写得到软件的可靠度,并基于此方法设计开发了一个软件可靠性预计工具——SRPT。所提出的软件可靠性评价方法综合考虑了数据流、控制流、构件和软件操作剖面信息以及体系结构信息对软件可靠性的影响,能够在软件实现前根据软件设计预测其可靠度,为软件的开发设计提供了工程指导。     

A WSDL-based type system for asynchronous WS-BPEL processes

We tackle the problem of providing rigorous formal foundations to current software engineering technologies for web services, and especially to WSDL and WS-BPEL, two of the most used XML-based standard languages for web services. We focus on a simplified fragment of WS-BPEL sufficiently expressive to model asynchronous interactions among web services in a network context. We present this language as a process calculus-like formalism, that we call ws-calculus, for which we define an operational semantics and a type system. The semantics provides a precise operational model of programs, while the type system forces a clean programming discipline for integrating collaborating services. We prove that the operational semantics of ws-calculus and the type system are ‘sound’ and apply our approach to some illustrative examples. We expect that our formal development can be used to make the relationship between WS-BPEL programs and the associated WSDL documents precise and to support verification of their conformance.     

改进随机森林在Android恶意软件检测中的应用

为解决Android恶意软件检测问题,提出一种利用多特征基于改进随机森林算法的Android恶意软件静态检测模型。模型采用了基于行为的静态检测技术,选取Android应用的权限、四大组件、API调用以及程序的关键信息如动态代码、反射代码、本机代码、密码代码和应用程序数据库等属性特征,对特征属性进行优化选择,并生成对应的特征向量集合。最后对随机森林算法进行改进,并将其应用到本模型的Android应用检测中。实验选取了6?000个正常样本和6?000个恶意样本进行分类检测,结果表明该方法具有较好的检测效果。     

面向方面程序的静态语义研究

针对面向方面程序,许多研究者已定义了各种各样的形式语义。但是这些语义都不能够全面、准确地对面向方面程序的规范和方面声明部分进行描述。针对该问题,首先定义一种统一的面向方面程序的规范语言;其次对面向方面程序中的连接点和切点这两个重要概念进行形式化定义;再次引入结构变量表示面向方面程序的基本结构;最后应用统一程序理论中的设计定义面向方面的静态语义,并对其可靠性进行证明。同时,用一个例子说明该语义的使用。     

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

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

Modeling high assurance agent-based Earthquake Management System using formal techniques

Disaster management systems are complex applications due to their distributed and decentralized nature. Various components execute in parallel with high need of coordination with each other. In such applications, interaction and communication issues are difficult to model and implement. In this paper, we have proposed agent-based Earthquake Management System (EMS) which is modeled and analyzed using formal approach. Traditionally, such systems undergo through various transformations starting from requirement models and specification to analysis, design and implementation. A variety of formal approaches are available to specify systems for analyzing their structure and behavior; however, there are certain limitations in using these techniques due to their expressiveness and behavior requirements. We have adopted combination of Pi-calculus and Pi-ADL formal languages to model EMS from analysis to design. The formal approach helps to enhance reliability and flexibility of the system by reducing the redundant information. It reduces chances of errors by explicitly mentioning working flow of information. Additionally, a prototype application is presented as proof of concept in EMS context. We have also evaluated our formal specification by using ArchWare and ABC tools; also, comparison of prototype application with major existing techniques is highlighted.     

以操作系统为中心的存储一致性模型--线程一致性模型

分布共享存储系统为保证程序的正确执行，必须通过存储一致性模型对共享存储访问顺序加以限制，而现有模型在可扩展性和操作系统级实现方面存在不足。结合多线程的特点，提出了一种以操作系统为中心的线程一致性模型，通过并行程序执行过程中线程状态的变化来观察和限制存储访问事件的正确顺序，有利于系统的可扩展性、一致性维护信息获取的方便性和完备性以及操作系统本身的设计和实现。分别从模型的定义、正确性证明、实现方案和性能分析等几个方面展开了论述。     

可解释的基于图嵌入的Android恶意软件自动检测

Android恶意软件的几何式增长驱动了Android恶意软件自动检测领域的发展。一些工作从可解释性的角度来分析Android恶意软件,通过分析模型获取最大影响的特征,为深度学习模型提供了一定的可解释性。这些方法基于特征相互独立的强假设,仅仅考虑特征各自对模型的影响,而在实际中特征之间总是存在着耦合,仅考虑单个特征对模型的影响,难以反映耦合作用,不能刻画不同类型软件中敏感API的组合模式。为解决该问题,将Android软件刻画成图,并结合图的结构信息和图节点内部的信息提出了一种基于图嵌入的方法来检测Android恶意软件。该方法通过注意力机制学习Android软件的低维稠密嵌入表示。实验结果表明,使用学到的嵌入表示进行恶意软件检测,不仅具有较高的分类精度,还可以通过分析注意力分数较大的路径寻找影响模型决策的模式以及定位恶意行为所涉及的敏感API序列。     

结合CNN和Catboost算法的恶意安卓应用检测模型

针对恶意安卓应用程序检测中存在的特征维度大、检测效率低的问题,结合卷积神经网络CNN良好的特征提取和降维能力以及catboost算法无需广泛数据训练即可产生较好分类结果的优点,构建一个CNN-catboost混合恶意安卓应用检测模型。通过逆向工程获取安卓应用的权限、API包、组件、intent、硬件特性和OpCode特征等静态特征并映射为特征向量,再在特征处理层使用卷积核对特征进行局部感知处理以增强信号。使用最大池化对处理后的特征进行下采样,降低维数并保持特征性质不变。将处理后的特征作为catboost分类层的输入向量,利用遗传算法的全局寻优能力对catboost模型进行调参,进一步提升分类准确率。对训练完成的模型,分别使用已知和未知类型的安卓应用程序数据集作实际应用测试。实验结果表明CNN-catboost模型调参用时较少,在预测精度和检测效率上也展示出较为良好的效果。