英语原文共 4 页，剩余内容已隐藏，支付完成后下载完整资料
对安卓app的核验
摘要
本篇文章着重研究一种用模型检测分析安卓app的代替式方法。我们开发出了一个Java路径寻找的拓展程序，这个叫JPF的安卓程序被用来在安卓平台外部确认安卓应用程序。JPF是一个强大的Java模型检测器和分析引擎，它在检测边角状况和难以被发现的错误时十分高效，这是因为其具有良好的根基分析能力。JPF安卓提供了一个简化的安卓app框架模型在这个模型上，安卓app可以运行同时也可以产生输入事件，或者解析具有特定序列的输入脚本，这些脚本能驱动app的运行。JPF安卓能贯穿所有的app执行路径，这种贯穿是通过模拟输入事件和检测常见的违反运行原则的错误（例如卡顿和运行时间错误）来实现的。JPF安卓同时也引入了用户定义的叫做检测列表的执行路径来确认app执行。
引言
具有大量外部引用和依赖的软件app是很难分析和核查的。这些外部的依赖形成了app执行的一部分实体内容，这种依赖也被叫做app的环境。为了使app在分析后运行的流畅和正确，一个适应性的受控的环境则需要被搭建，这种环境将流畅和持续的运行。安卓app形成了开源app的一部分，因为他们有很多的外部引用和
外部依赖。安卓app的环境由安卓软件堆叠形成，其内部有客户端-服务端设计部分，app应用建立在安卓app框架的顶部。框架提供了app的核心应用工具，包括事件处理和解决，app组成部分的管理资源与IPC设施和其他应用于系统服务。设备上所有app状态由系统服务器控制，系统服务器由一些列共享设备（如窗口管理器，封装管理器和一个活动管理器构成，活动管理器控制设备上运行的所有app的状态。这些事件包括UI和通过系统服务器发送到合适的app的系统事件。
安卓app环境对分析工具来说有三个挑战：一、安卓app十分依赖安卓应用框架，但是系统服务在软件堆叠之外并不是可运行的。二、因为安卓app有很多异步设计，这些设计具有很多入口点，所以分析它们需要一个驱动器去执行app。三、由于app的异步性、多线路设计、反射和本地方法呼叫，很难掌控app执行过程中的错误。 所以，如果app是在软件堆叠上执行，执行的有效性甚至更具有挑战性，因为软件堆叠更需要被编辑和重新编译或者为每个安卓版本去构建。
常用的分析安卓app的方法是静态分析和动态分析。静态分析通常需要测试条件下的系统是兼容的，所以一般不会要求测试驱动器的产生。然而，静态分析仍然需要本地代码模型和对外的潜在依赖，同时也需要明确需要核验的性能（记忆链接，无效指针，特定的运用对象）分析结果通常是一种近似值，但是对于安卓app，一些错误会被忽略，因为代码模型需要在app工具上运行。而静态分析也可以并不提供给用户一个事件序列，因为这种序列可能导致在确认意图的时候产生一个可能的错误。
相比较下，动态分析需要在测试状态下的系统能运行，同时也需要测试驱动的产生。另外，单元测试需要产生模拟对象。这种类型的测试用到了测试管理和测试推断来保障程序内容的正确执行，动态分析提供了一个在对app分析下的一个近似估计，但是它面临的主要挑战是产生一个包含一个具有理想封装的app代码的输入事件。
模型检测是一个成熟的鉴别技术，可以在app应用中用作证明是否有违反权限的依据（这是在状态空间有限的情况下）。然而，在大多数情况下模型检测是用于寻找漏洞（甚至在状态空间足够的情况下).查询空间在运用状态寻找和回溯法的时候会被减少，当在一个封闭的环境下动态执行app的时候这种减少情况会产生。而在空间匹配的时候，模型检测会由于存在状态空间搜寻问题和实际环境在减少状态空间时经常被削减，而会受到影响。由于模型检测需要对于app运行有良好的根基控制，一个适应性的、自定义的模型是需要被构建的。
本次研究我们着重于通过运用基于普通的Java app校验工具来校验安卓app，更准确的说，我们拓展了JPF，它在校验和分析安卓app时是一个强大的模型检测工具和分析引擎。我们运用JPF是因为他是在Java app环境下被开发的，同时它具有很多拓展功能所以可以被运用于多种安卓app环境（如符号性路径寻找工具）。同时，因为安卓app是在动态情况下运行，所以我们面临同样的来自于一些动态分析工具的挑战。我们需要产生具有好的封装的app代码的输入事件。另外，我们需要一个拓展的环境工具去运行app。JPF给我们提供了一个更容易控制的、更具适应性的环境去简化难以被发现的边角错误，这些错误通常在被目前可用的安卓分析工具检测时不易被发现，因为app对外部环境具有依赖性。JPF同时也给我们提供了特征框架，在字节代码的水平下去掌控app的运行。更重要的是，如果特征违反情况发生，JPF可以提供给用户一个输入事件序列去检测出违反情况。
预期情况下本次研究的贡献是展示模型检测的安卓app是怎样在一个受控的、适应性的环境下运行，通过JPF具有运用良好根基的分析能力的特点，可以简化平时在各种复杂设计的安卓app中检测错误的过程。
方法概要
作为本次研究的一部分，我们开发了一个基于JPF环境的JPF安卓程序。我们的方法在表二中有展现。这个工具需要输入一个含有不确定的输入事件的脚本，来驱动app的运行，而安卓app的代码是由Java字节代码和检测名单堆叠而成，它们一般用作特征具体化作用，来确认app的顺利运行。JPF安卓程序提供了一个模型环境，在这个环境下可以运用输入脚本中的事件执行app，然后程序会追溯app的执行并在对属性监听和检测名单监听下核验app。
目前有几种可能的运行结果，第一种结果是，JPF工具在app中找到了属性违反或者错误。这种情况下回立即终止程序的运行，并向用户报告导致违反或者错误的序列。因为本次设计的工具的正确运行是建立在模型环境之上的，我们需要确认在实际情况中确实存在该错误。由于这个缘故，我们也要提供一种翻译器，这种翻译器可以在设备上运用动态测试工具（如MonkeyRunner或者Dynodroid）运行错误的事件序列。第二种结果是，工具完成了对状态空间的查找，同时并没有发现违反属性。在这种情况下，用户可以选择完成一个更加复杂的查找，这种对app的查找是运用工具的动态输入产生驱动。我们期待发现模型测试可以实现一个对app代码的高度封装，因为搜寻器具有强大无限搜寻能力，可以根据特定的长度混杂着相应的状态匹配，去查询每一个可能的事件序列，由此来减少搜寻空间。第三种结果是，状态空间太大以至于JPF安卓程序永远不可能停止运行或者运行到没有记忆空间。在这种情况下，我们尝试着通过限制app的状态，这种限制是基于移除部分改变很快以至于没有匹配的状态的空间。
在接下来的部分，我们将讨论JPF安卓程序如何解决分析安卓app时面临的三个主要的挑战。
A.环境模型
在安卓环境中构建模型内容有两个主要的原因。第一个是，构架不可用的或者本地代码的行为有可能不会被执行或者分析。安卓app是依赖于安卓app框架和系统服务器来运行的。不幸的是，这些库不能在Java虚拟机上正确的执行，因为他们可用的需要本地库文件和驱动器。基于这个原因，我们需要构建本地行为去让安卓app在软件框架外也能被执行。所以第二个构建环境中的行为或者组成部分，是一种对他们正式使用的概括和或者简化。概括是一种非常重要的模型检测，因为其减少了探寻状态空间的大小。
在我们之前的工作中，我们创造了一个安卓环境模型，人工的运用JPF去核验安卓app。我们发现，安卓环境是一个非常复杂的环境，其中的各种组成部分经常会有引用和对于系统其他部分的依赖，或者对于本地库文件有依赖。没有了这些外部依赖，环境将无法正确设置或者将不会运行。人工构建一个模型是一个十分耗费时间的工作，需要大量的专业领域知识。对于我们目前的研究，我们通过确认使用工具的具体位置，提升了人工方法的效率。
我们运用了不同的方法去构建基于具体实际功能的模型。最基本的方法是构建一个类或者部分组成内容去创建一个空的末梢区域。这些末梢区域保持了公共的方法和空间，同时，如果被授权或者被调用，将会返回默认值，但是他们没有对于app或者对于环境的副作用。他们同时对于模型类别很有用处，不会影响对app的校验（例如Logging类）。这种类型的建模工作在概括和轻松地产生模型下，工作的很顺利。自动使用静态分析工具如OCSEGen和Modgen也能正常工作。
为了保持特定内容（类别）的行为但同时减少复杂度，我们也可以产生更智能的末梢区域，运用OCSEGen和Modgen。OCSEGen可以产生维持边界效应（改变）的末梢区域，它们是适用于特定的环境，通过利用边界效应分析。Modgen是一种切片化代码的工具，专注于通过末梢化功能类别来实现简便化，从而最大化库的类别。这种类别的模型构建对于GUI组成是有益的，在这种构建中，功能性是关联于组成部分的视觉层面，因此对于校验目的来说并不重要，同时也可以被移除但是在维持、可视化和监听寄存方面会保留。
有时候我们要求有更过的复杂的内容模型去确认组成部分的应用，或者当组成部分对于app的运行十分重要。在这种情况下，我们需要研究组成部分的特殊化情况或者使用运行控制器去概化组成部分行为的一个模型。由此我们能人工编写一个模型去模拟相应的行为或者使用如OCSEFen的工具，去产生一个具有很多特殊化分支的模型。这种类型的建模对于资源（如MediaPlayer或者Camera）是有益的，当我们需要更多的拓展工具，而这些工具需要组成部分的特殊化去确保app使用资源的正确性。
B.驱动app的执行
安卓app拥有一个事件型设计，这种设计的执行是被输入事件所触发的。安卓app对很多不同类型的输入事件都有响应（包括物理按钮按压、设备的旋），app从发射器和WiFi连接开始执行。这些输入事件可以混杂进数百万不同长度的独特事件序列中。这些序列中的每个序列都可以潜在的触发错误的app行为。因为执行所有的序列是不实际的，我们需要产生可以获得最大化代码封装的输入事件，同时给予最小化数量的输入事件。
JPF安卓程序在两个方面支持驱动app，用户可以通过编写输入事件序列或者实现更耗费时间的搜寻方式（运用JPF动态输入产生驱动器）。编写环境允许开发者编写封装的不定向的输入事件的序列。这些事件在app处于闲置状态或者等待输入事件的时候一个个的被执行再删除。尽管这种方法提供了一个具有最大化输入序列的工具，编写输入脚本却变成了一个枯燥的过程，而脚本也有可能错过正常序列而导致错误。因此，我们开发了一个产生输入事件的驱动器，它可以在运行时间内自动的产生输入序列。我们预期JPF安卓程序将会减少输入序列的数量和长度，而在一个先前状态已经达到的情况下，通过运用状态匹配停止执行app。对于产生时间的数据范围，我们打算运用对结合的、小型的app组成部分，象征性地执行。以此可以在对app的模型检测前，确认运行值。
我们同样开发了一个可以执行事件序列的翻译器，当属性发生违反，并显示于实际设备或模拟器时，序列从JPF安卓程序返回。这也使用户能确认被JPF安卓所检测到的错误。
C.属性特殊化
在模型检测中，逻辑方程式的特殊化被用来校验app的执行情况。这些特殊化可以描述安全的属性特征，例如没有校验的例外情况和长期存在的属性（包括僵局和快速运转情况）。属性特殊化也可以被用来确认具体的app执行情况达到了预期要求。 JPF安卓通过提供一个Checklist属性监听器在方法层面上去追溯app的执行情况，简化了具体化属性的过程。Checklist可以用来确认特定方法是可以在特殊化顺序下被实现的。这种情况十分重要，因为其提供了一个自动的方法确认一个app可以在测试期间能满足实现预期的功能。Checklist同样可以编写后确认各种类别的属性，包括持续性和安全问题属性,它是属性特殊化的一种类型，可以使用JPF的属性监听功能去执行。一旦安卓app可以在JPF上运行，很多其他的属性监听器也会被设计出来当作样本资源和存储链接，也可以当作对API的错误使用。JPF安卓也支持代码封装的运算，运用Java的PathFinder在封装计算监听器中的作用。代码的封装将会指示代码是否在Checklist和其他属性违反情况下被彻底的检测。在我们未来的工作中，我们打算构建一个安卓特殊化的监听器去确认强大的分析过程是可以运用JPF安卓来实现的。
D.估计
为了评估我们的研究方法，我们将在一系列开源安卓app上运行JPF安卓程序，而这些app被我们预先设定有一些错误。我们首先确认在分析过程中所找到的错误，再运用翻译器去执行导致这些错误的序列。然后我们将对比结果和封装数据，通过其他动态分析工具来对比(如Dynodroid和Monkey）
三、进程
本次研究已经在ACM SIGSOFT软件工程协会上发表了三篇论文。第一篇论文标题为“在Java路径寻找中校验安卓app”，此篇论文描述了JPF安卓程序的具体功能的设计。第二篇文章是“在JPF安卓上的具体运行和属性特殊化”，此篇讨论了JPF安卓程序输入事件脚本的阵列，同时也展示了事件是如何在测试时在app上进行模拟，是如何在Checklist的状态下受控和确认安卓app的良好运行。评估我们的研究面临的主要挑战是，一系列的app和驱动app运行的测试脚本需要环境模型。为了让设计的工具能在大多数app上运行，我们让一些尝试趋于更加自动化。同时，为了使创建环境模型可以实施，我们研究了最近可用的建模技术并了解到他们是如何帮助用户的（具体在我们第三篇文章中有介绍）。最后，我们也拓展了JPF安卓程序，去自动产生一些输入序列。
四、相关工作
静态分析通常是对app的浅层分析，是面向十分具化的属性，如缓存溢出。因为静态分析是十分有效的，在app运用中追溯数据流，大多数对于安卓app的静态分析工具都着重于呈现一些数据流分析，如隐私泄露等。大多数动态分析工具都是在模拟机或者设备上运行app。尽管app可以正常的在这种环境上运行，但是要控制环境的状态是不可能的。而虚拟机，比方说，不会有WiFi功能，也不可能掌控在具体设备上的电池状态
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[146533]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
