基于模型的应用软件的静态检测方法研究

李忠慧

摘要：该文把静态分析技术与基于模型的演绎验证结合起来提供了一个框架，分析应用源代码，自动生成一个分析器，它能够推断关于给定程序行为的逻辑约束方面的信息。该文引入了一阶逻辑断言来描述API调用语义。这些断言构成分析器使用的模型。通过实验，该方法可被用来识别Java程序中的关于安全的逻辑错误。

关键词： Android；软件安全；静态分析

中图分类号：TP393 文献标识码：A 文章编号：1009-3044（2015）20-0182-02

Research of Static Detection Method Based on Model

LI Zhong-hui

（College of Information Engineering in Yancheng Teachers University， Yancheng 224002，China）

Abstract： This paper introduces a framework， which combines the static analysis technology and the deductive verification based on model. It is used for analysis of application source code， automatically generating an analyzer， which can give the inferred information on the logic of a given constraints of program behavior. This paper introduces first-order logic assertions to describe semantics of the API calls. These assertions constitute the model used by the analyzer. Through the experiment， this method can be used to identify the logic errors about the security in Java program.

Key words： Android；software security； static analysis

1 引言

Android系统是主要用于移动智能设备上的源代码开放的操作系统。由于其开源性和高额市场占有率，Android系统成为攻击者的主要攻击对象。软件可能包含恶意代码或漏洞，攻击者利用来泄露敏感数据，执行恶意的操作，修改有价值信息。因此，软件的正确性和可靠性至关重要。

缓冲区溢出、空引用都可能被恶意应用程序用来创建安全漏洞，以此来泄露的机密数据。许多这类错误很容易被忽视，直到很久以后引起灾难性的后果。系统的运行时错误处理机制很难确保系统复苏。另外，一个更重要的问题是缺乏适当的工具支持检测应用程序中的应用依赖的逻辑错误。很多软件故障事件是由软件的应用依赖的逻辑错误导致的[1][2]。这类逻辑错误是深层次的，单独使用目前的测试技术是难以检测。

本文将静态分析技术和基于模型的演绎验证相结合，对应用软件的源代码分析，自动生成一个能够推断关于依赖逻辑信息的分析结果。由于很多时候，我们并不能得到应用软件的源代码，转而分析该软件的模型，基于模型的方法是必需的。所以，本文采用的静态分析和模型技术相结合的方法。

2 相关工作

软件验证技术主要分为三大类[3]。第一类是非形式化，动态方法，如软件测试和监控等。这些技术扩展性好，是最常用的技术。软件测试在软件开发工作中占百分之四十到六十。然而，传统的软件测试方法不能保证系统需要满足的高层逻辑属性的形式化规范和验证。在安全关键的软件领域，指数级爆炸处理是不可避免的，传统的测试技术很难被用来处理这种状况。第二类是形式化方法。模型检测等传统形式方法和定理证明通常太繁琐，需要相当大的手动工作，因而在实践中很少使用。模型检测是一种自动验证方法，主要在处理有限状态系统。第三类是静态分析技术[4]和抽象解释[5]。静态分析是指在编译时自动推断一个程序的行为的技术。虽然静态分析工具取得巨大的实际成功，经常结合先进的编译器，这类工具缺乏演绎能力，只能检测浅显的简单错误。传统的静态分析工具无法检测死锁的存在或并发程序违反互斥。抽象解释是收集、比较、结合程序的语义的技术。它已经成功地用于推断出程序的运行时性能，可用于程序优化。近年来，在软件的静态分析上，已经完成了大量的工作。

Uno、Splint、Polyspace等静态分析工具[6]执行轻量级数据流分析。Astree是一个静态程序分析器，旨在证明嵌入式程序没有运行时错误。Astree只能处理一个C语言子集，而不是完整的C语言。同时，它只适用于特定的运行时错误，而不是程序的一般属性。Halbwachs等人使用线性关系分析来发现程序的数值变量之间的不变的线性不等式。Alur等人使用谓词抽象来分析混合动力系统，创建有限状态自动机。

3 Android平台简介

Android系统是一个用于移动设备的软件堆栈，包括操作系统、中间件和关键应用程序。Android允许应用程序与系统中其它应用程序共享数据和函数[7]。Android系统没有一个单一的入口点（没有main（）函数）。系统已有基本组件，可以根据需要进行实例化和运行。四大组件是：Activity、Service、Broadcast Receivers、Content Providers。Android使用Intent激活前3个组件。对于Activity和Service，Intent是。接收机需要采取预定义的动作来处理数据。在我们的分析框架中，Intent是关键。我们使用Intent对象来执行数据流分析和函数调用分析。

Android框架支持使用手机功能构建应用程序，通过使错误和恶意软件的后果的最小化来保护用户。在Android中，应用程序可以与其他应用程序共享数据和功能。为了安全，这些访问必须严格控制。Android权限允许应用程序有权执行功能，如拍照、使用GPS、或打电话。在应用程序安装时，他们有一个独特的UID，每个应用程序总是运行在特定设备上的UID下。应用程序的UID是用来保护其与其他应用程序共享数据。

4 基于模型的静态检测方法

图1是本文采用的基于模型的静态分析方法的流程图。应用程序的抽象集语义用标记约束表示。API库的语义是未知的，标记是一组应用程序对应的API组合。本文用一阶逻辑断言或约束来描述调用的API语义。这些断言就构成模型，根据约束描述，进行检测，求解得到最终推断结果。

图1 本文分析方法的流程图

本文对应用分析的算法的主要步骤如下：

1） 通过逆向工程手段，得到应用程序的源码、配置文件以及一些资源文件等。根据manifest.xml文件，验证在Java源代码中调用的API的权限。权限验证的结果是用来修改和建立API模型。

2） 对Java源代码分析生成抽象收集语义约束。

3） 导入无语义的方法和对象的模型为断言，和已经生成的约束。

4） 通过添加适当的分析方面的约束生成一个分析器。

5） 通过求解约束分析，得到推断结果。

4.1 权限验证

Android的权限可分为不同的保护级别。应用程序在Mainifest.xml文件中申请所需权限。我们通过分析程序中调用的API，构建所需的权限列表，将其和 从Mainifest.xml文件中检索的权限信息进行比较。如果每个API所需的权限都已提供，我们认为应用程序没有违反权限。否则，任何没有提供适当的权限的API调用将在分析断言中返回1。

4.2 程序语义的收集和推断

为了分析Java程序的深入逻辑属性，我们对其进行过程内和过程间分析。在过程内分析中，从源代码的数据流分析，构建一个约束系统，来捕捉其收集语义。在过程间分析中，建立一个与不同的API调用相关的调用图和定义一些外部规则，检测分析代码是否违反这些规则。

5 实验结果分析

我们分析了Android Bluetooth ChatServices应用的源代码。这个应用程序构建一个蓝牙网络平台，它允许设备与其他蓝牙设备交换数据。它有三个主要功能：发现蓝牙设备、可连接设备、这些设备之间传输数据。应用程序使用了如下的API调用：BluetoothAdapter.getDefaultAdapter（），BluetoothAdapter.getRemoteDevice（address），BluetoothSocket 和BluetoothChatService。对于这个应用程序，我们只是考虑到应用程序可以设置蓝牙服务和可以连接到任何设备发现。所以我们设BluetoothChatService返回一个非null对象，在SMT规范中，我们对API函数值建模为（not ?1）。源代码分析满足规范。我们下载了几个免费的android应用程序源代码，运行源代码静态分析工具。发现应用程序SMSPopup含有命令注入错误；命令声明是一个数组，来自另一个函数，它可能提供一个错误的语句，应用openGPStracker拥有比它实际需要更多的权限，有硬编码的密码。

6 结论

Android应用程序可以使用系统提供机制相互沟通，如文件、活动、服务、BroadcastReceivers、contentprovider。我们的程序分析框架可以帮助开发人员静态地检测违反编程错误和违反权限。开发人员需要了解哪些权限需要正确设置，需要一些逻辑和约束求解的背景知识。我们未来的工作重点是设计一个良好的用户界面，来帮助用户轻松设置约束，揭示程序中的逻辑错误。

参考文献：

[1] 方喆君，刘奇旭，张玉清.Android应用软件功能泄露漏洞挖掘工具的设计与实现[J].中国科学院大学学报.2015，32（1）：127-135.

[2] 杨欢，张玉清，胡予濮，等.基于多类特征的Android应用恶意行为检测系统[J].计算机学报.2014，37（1）：15-27.

[3] 陈楠，王震宇，窦增杰，等.可执行可信软件安全性分析技术研究[J].计算机工程与设计，2010，31（22）：4802-4805.

[4] 匡春光，陈华，张鲁峰.针对Java程序的一种脆弱性静态分析技术[J].计算机系统应用，2008，5：89，94-96.

[5] 屈婉霞，李暾，郭阳，等.模型检验中抽象技术研究综述[J].计算机工程与应用，2006，33：15-19.

[6] 王凯，孔祥营.软件静态分析工具评析[J].指挥控制与仿真，2011，33（2）：109-111，119.

[7] 张玉清，王凯，杨欢，等.Android安全综述[J].计算机研究与发展.2014，51（7）：1385-1396.