毕业设计外文资料翻译-安卓程序的静态分析

1、毕业设计外文资料翻译学 院： 专业班级： 学生姓名： 学 号： 指导教师： 外文出处：Etienne Payet,Fausto Spoto.Information and software technology.EISCI2012 11 附 件：1.外文资料翻译译文 2.外文原文 指导教师评语： 查找期刊文献进行翻译，基本符合翻译要求。签名： 年 月 日外文资料翻译译文安卓程序的静态分析抽象上下文：Android是基于Java程序设计语言和操作系统的嵌入式移动设备，其上层被写入Android语言本身。作为一种语言，它具有扩展基于事件的库，并在XML的布局文件图形声明视图动态的通货膨胀。Andr

2、oid方案静态分析必须考虑这些特点，正确性和准确性。目的：我们的目标是扩大Julia静态分析的基础上，抽象解释，执行的Android方案的形式上正确的分析。本文是一个扩展深入的对我们面对我们获得的成果和困难的说明，。方法：我们扩展了Julia分析仪，它坐落在许多其他分析的心脏的阶级分析，考虑一些Android的关键功能如多入口点的可能存在一个程序和从XML图形视图通胀进行反射。我们还已经显著改善Android电子节目NULL的含量分析的精度。结果：我们与Julia分析大部分由谷歌Android的示例应用程序和几个较大的开源程序。我们已经申请几十项静态分析，包括classcast，死代码，NUL

3、L的含量和终止分析。Julia发现，自动，臭虫，缺陷和INE FFI ciencies无论是在谷歌的样品还是在开放源代码的应用程序中都存在。结论：Julia是第一部基于Android程序的基础上的有声静态分析仪，基于如抽象解释的正式的基础上。我们的研究结果表明，它可以分析真实的第三方Android应用程序，无需任何代码的用户注释，在标准硬件上产生正式正确的结果在最多不超过7分钟。因此，它已准备好在第一工业使用。关键词：程序验证，静态分析，抽象解释，Android邮箱: etienne.payetuniv-reunion.fr(Etienne Payet), fausto.spotounivr.

4、it (Fausto Spoto)2012年5月24日印刷版提交给Elsevier。1.简介Android是在操作系统市场上为移动和EM-床设备的主要参与者，如手机，平板电脑和电视机。它是为这类设备提供的一个操作系统，其上层被写入在编程语言中，也称为Android。作为一种语言，Android是带扩展库移动和交互应用的Java语言，因此，基于事件驱动的架构。任何Java编译器可以支持Android应用程序，但由此产生的Java字节码必须转化为最终的，非常优化，Dalvik的字节以便在设备上运行。Android应用程序静态分析是很重要的，因为质量和可靠性是在Android市场2成功的关键。越野车

5、的应用得到了负反馈，并立即被他们的潜在用户放弃。因此，Android的程序员要确保它们的方案都是无缺陷，例如，他们不抛出任何意外的异常和不挂设备。但Android应用也日益在关键上下文部署，甚至在军事方案中，在安全性和可靠性是极为重要的。由于这些原因，一个产业的演员，如Klocwork的16已经将其静态分析工具从Java扩展到Android，我们知道的为Android获得唯一的静态分析。它是相对有限的电力，据我们从他们的网页推断。我们无法得到一个免费的评估许可证。如像Klocwork的一个工具是基于语法检查。这意味着，错误是通过查找代码典型的句式，往往含有错误认定。使用语法检查可以非常快速和实

6、用的进行分析。但是，bug的代码不遵循分析仪已知的预定义模式时它无法识别错误。这种情况下如错误发现在其中的基于形式化方法的人工智能工具的基础上，语义工具如Julia也一直没有能够证明一个程序段不包含错误。第二种情况是更为复杂并且计算昂贵的，但提供了稳健的业绩的保证：如果（有些类）没有潜在的错误被发现，再有就是类的代码中没有错误。在其他方面，语法工具是快，但不健全。这两种方法信号误报，也就是说，实际上不是一个真正的错误潜在的bug。精密（即真正的错误量WRT警告的数量）是在这里关键的问题，因为误报的数量不应该压倒工具的用户。这是通过大多数静态分析工具开发确认。比如，我们可以给Coverity公司

7、的网页7：“通过提供业界最准确的分析解决方案和最低的误报率，你可以专注于真正的和相关的缺陷，而不是浪费开发周期”。因此，大多数的静态分析器的显影剂的电子是朝着误报的数量减少努力。这对声音分析仪更加困难，因为他们不能随便扔掉警告，仍然留声。在任何情况下，如Klocwork公司存在这个市场上表明行业认识到Android代码的静态分析的重要性。 更科学的方法是突出SCanDroid工具14，目前仅限于Android应用程序的安全验证。它执行的Android应用程序的化流量分析，通过应用联盟的跟踪组件间省交通阳离子通过意图和潜在的非法获取安全特权。其基础是代码的基于约束的分析，并有一个健全性的保证，至

8、少一个受限制的一种字节码。Klocwork公司目前不执行Android应用程序的任何信息流分析。Julia是Java字节码一个静态分析器，基于抽象interpreta-tion 6，以确保，自动，所分析的应用程序不包含大的的编程隐错。它适用于不平凡的整个程序，过程间和语义静态分析，包括一流的演员阵容，死代码，NULL的含量和终止分析。它配备了一个正确的保证，因为它通常是在抽象解释社会的情况：如果应用包含了一个错误，由分析仪算是一种，那么Julia会报告。这使得分析的结果更显著。尽管Java和Android是相同的语言，有着不同的库集，Julia到Android应用程序也不是立竿见影，我们必须解

9、决之前许多问题，Julia可以用正确和精确的方式分析Android的程序。许多都涉及到不同的库集，其他人使用XML来构建应用程序的一部分。在这篇文章中，我们提出这些问题并向他们提供我们的解决方案而且向他们展示，所产生的系统分析不平凡的Android方案，精确度高，并找出第三方代码中的错误。本文不详细描述由Julia提供的，在其他地方已公布的静态分析，但只有适应它分析的Android分析仪和。特别是，我们的阶级分析，在简单的检查，如classcast和死代码分析的心脏，在27中描述;我们的NULL的含量分析描述在25，26;我们终止分析文献28中描述。必须指出，我们的Julia分析仪反射存在不健

10、全，Java的类加载机制和多线程的重新定义。这并不意味着，使用这些功能的程序不能被分析，而只是结果可能不正确。实际上，我们的工作中的一个主要的成就在于教Julia有关特定使用反射是在Android的XML布局膨胀期间完成的，因此，该分析的结果在这种情况下依然良好（但不包括反射的其他用途）。我们的分析假定是一个封闭的世界，某种意义上说，例如，它假定，在入口点，变量可以被绑定到每个其声明的类型相容的类别上，可以在任何可能的方式或保持空下共享。相同的假设不能对库制成，可以扩展，其行为可以通过子类进行修改。因此，我们不是一个模块化的分析库，因为我们只分析完整（关闭）的Android应用程序。有许多静态

11、的分析仪，它能够分析Java源代码，并发现错误，或国家统计局FFI ciencies。他们中的大多数是基于语法分析（Checkstyle的4，Coverity的7，FindBugs的11，3，PMD23），或者使用国际集团的定理证明的一些简化（和一般不健全的）假设（ESC /Java12）。由于Android的语言是Java，只有库的变化，它可能在原则上可以应用这些分析仪Android源代码。然而，正如我们将展示在下面的章节中，有新的语言特性，如XML通货膨胀，不由这些工具和影响相同程序的控制流图的施工，通常是通过一个类型进行理解推理分析称阶级分析20;有许多种Android的代码中的新的错误

12、，因为库的使用方式，这不是典型的Java。因此，无论是静态分析假定这些功能是不存在的这些漏洞不会发生（不健全），或者必须处理这些问题，可能用一个合理的方式。我们认为，我们强调本文中的解决方案可以适用于那些静态分析为好，因为它们不局限于选择我们的具体的静态分析。本文的其余部分安排如下。部2证明机器人程序的静态分析的困难。第3节介绍与本文相关的Android的概念。第4节更相关的静态分析，我们对Android的代码执行。第5，第6和第7描述我们如何提高Julia工作在Android上。特别是，第5节讨论声音控制流图的通过类分析的结构，以XML通货膨胀的存在。第8条提出了从标准的谷歌分布和较大的开放

13、源代码项目的许多不平凡的Android方案的实验结果;它表明Julia发现这些程序的一些实际的错误。第9节总结全文。这篇文章是在2011年22提出了在CADE较短的会议论文的扩展版本。宗全experimen河谷的评价。 8没有出现在22。此外，宗4第二节5宗6提供了一个更深入的介绍我们扩展Julia的方式，相比于22的相应部分。Julia是一种商品（），可以通过网页界面可从公司，其功率由超时和分析的最大尺寸的限制的网站自由使用。Fausto Spoto是该公司的董事长，他在2010年11月成立该公司。他也是Julia软件的主要开发者。Etienne Payet目前在留尼旺岛（法国）副教授。他不

14、是Julia Srl的一员，但他经常与Fausto Spoto在科学问题上合作。外文原文Static Analysis of Android ProgramsEtienne PayetLIM-IREMIA, Universit de la Reunion, FranceFausto SpotoDipartimento di Informatica, Universita di Verona, ItalyAbstractContext: Android is a programming language based on Java and an operating system for embe

15、dded and mobile devices, whose upper layers are written in the Android language itself. As a language, it features an extended event-based library and dynamic inflation of graphical views from declarative XML layout files. A static analyzer for Android programs must consider such features, for corre

16、ctness and precision. Objective: Our goal is to extend the Julia static analyzer, based on abstract interpretation, to perform formally correct analyses of Android programs. This article is an in-depth description of such an extension, of the difficulties that we faced and of the results that we obt

17、ained. Method: We have extended the class analysis of the Julia analyzer, which lies at the heart of many other analyses, by considering some Android key specific features such as the potential existence of many entry points to a program and the inflation of graphical views from XML through reflecti

18、on. We also have significantly improved the precision of the nullness analysis on Android programs. Results: We have analyzed with Julia most of the Android sample applications by Google and a few larger open-source programs. We have applied tens of static analyses, including classcast, dead code, n

19、ullness and termination analysis. Julia has found, automatically, bugs, flaws and ineciencies both in the Google samples and in the open-source applications. Conclusion: Julia is the first sound static analyzer for Android programs, based on a formal basis such as abstract interpretation. Our result

20、s show that it can analyze real third-party Android applications, without any user annotation of the code, yielding formally correct results in at most 7 minutes and on standard hardware. Hence it is ready for a first industrial use.Keywords: Program verification, static analysis, abstract interpret

21、ation, AndroidEmail addresses: etienne.payetuniv-reunion.fr (Etienne Payet), fausto.spotounivr.it (Fausto Spoto)Preprint submitted to ElsevierMay 24, 20121. IntroductionAndroid is a main actor in the operating system market for mobile and em-bedded devices such as mobile phones, tablets and televisi

22、ons. It is an operating system for such devices, whose upper layers are written in a programming lan-guage, also called Android. As a language, Android is Java with an extended library for mobile and interactive applications, hence based on an event-driven architecture. Any Java compiler can compile

23、 Android applications, but the re-sulting Java bytecode must be translated into a final, very optimized, Dalvik bytecode to be run on the device.Static analysis of Android applications is important because quality and reliability are keys to success on the Android market 2. Buggy applications get a

24、negative feedback and are immediately discarded by their potential users. Hence Android programmers want to ensure that their programs are bug-free, for instance that they do not throw any unexpected exception and do not hang the device. But Android applications are also increasingly deployed in cri

25、tical contexts, even in military scenarios, where security and reliability are of the utmost importance. For such reasons, an industrial actor such as Klocwork 16 has already extended its static analysis tools from Java to Android, obtaining the only static analysis for Android that we are aware of.

26、 It is relatively limited in power, as far as we can infer from their web page. We could not get a free evaluation licence.A tool such as Klocwork is based on syntactical checks. This means that bugs are identified by looking for typical syntactical patterns of code that often contain a bug. The use

27、 of syntactical checks leads to very fast and practical analyses. However, it fails to recognize bugs when the buggy code does not follow the predefined patterns known by the analyzer. The situation is the opposite for semantical tools such as Julia, where bugs are found where the artificial intelli

28、gence of the tool, based on formal methods, has not been able to prove that a program fragment does not contain a bug. This second scenario is much more complex and computationally expensive, but provides a guarantee of soundness for the results: if no potential bug (of some class) is found, then th

29、ere is no bug of that class in the code. In other terms, syntactical tools are fast but unsound. Both approaches signal false alarms, that is, potential bugs that are actually not a real bug. Precision (i.e., the amount of real bugs w.r.t. the number of warnings) is the key issue here, since the num

30、ber of false alarms should not overwhelm the user of the tool. This is acknowledged by most developers of static analysis tools. For instance, we can quote the web page of Coverity 7: “By providing the industrys most accurate analysis solution and the lowest false positive rate, you can focus on the

31、 real and relevant defects instead of wasting development cycles”. Hence, most of the eort of the developer of a static analyzer is towards the reduction of the number of false positives. This is much more difficult for sound analyzers, since they cannot just throw away warnings and nevertheless sta

32、y sound. In any case, the presence of a company such as Klocwork on this market shows that industry recognizes the importance of the static analysis of Android code.A more scientific approach is underlying the SCanDroid tool 14, currently limited to security verification of Android applications. It

33、performs an informa-tion flow analysis of Android applications, tracking inter-component communi-cation through intents and the potential illegal acquisition of security privileges through a coalition of applications. Its basis is a constraint-based analysis of the code and there is a soundness guar

34、antee, at least for a restricted kind of bytecodes. Klocwork does not currently perform any information flow analysis of Android applications.Julia is a static analyzer for Java bytecode, based on abstract interpreta-tion HYPERLINK /publication/220997507_Abstract_Interpretation_A_Unified_Lattice_Mod

35、el_for_Static_Analysis_of_Programs_by_Construction_or_Approximation_of_Fixpoints?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQYWdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxNzQyMjUzNDkwMg= 6, that ensures, automatically, that the analyzed applications do not con

36、-tain a large set of programming bugs. It applies nontrivial whole-program, interprocedural and semantical static analyses, including classcast, dead code, nullness and termination analysis. It comes with a correctness guarantee, as it is typically the case in the abstract interpretation community:

37、if the applica-tion contains a bug, of a kind considered by the analyzer, then Julia will report it. This makes the result of the analyses more significant. Although Java and Android are the same language, with a different library set, the application of Julia to Android is not immediate and we had

38、to solve many problems before Julia could analyze Android programs in a correct and precise way. Many are related to the dierent library set, others to the use of XML to build part of the application. In this article, we present those problems together with our solu-tions to them and show that the r

39、esulting system analyzes non-trivial Android programs with high degree of precision and finds bugs in third-party code. This paper does not describe in detail the static analyses provided by Julia, already published elsewhere, but only the adaptation to Android of the analyzer and of its analyses. I

40、n particular, our class analysis, at the heart of simple checks such as classcast and dead code analysis, is described in HYPERLINK /publication/220404810_Class_analyses_as_abstract_interpretations_of_trace_semantics?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQY

41、WdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxNzQyMjUzNDkwMg= 27; our nullness analysis is described in HYPERLINK /publication/220896523_The_Nullness_Analyser_of_julia?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQYWdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxN

42、zQyMjUzNDkwMg= 25, 26; our termination analysis is described in HYPERLINK /publication/220404833_A_Termination_Analyzer_for_Java_Bytecode_Based_on_Path-Length?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQYWdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxNzQyMjUzNDk

43、wMg= 28.It must be stated that our Julia analyzer is not sound in the presence of reflection, redefinitions of the class loading mechanism of Java and multithread-ing. This does not mean that programs using those features cannot be analyzed, but only that the results might be incorrect. Actually, on

44、e main achievement of our work has been to teach Julia about the specific use of reflection that is done during the XML layout inflation in Android, so that the results of the analysis remain sound in that case (but not for other uses of reflection).Our analyzer assumes a closed world assumption, in

45、 the sense that, for instance, it assumes that, at the entry points, variables might be bound to every class compatible with their declared type, might share in any possible way or hold null. The same assumption cannot be made for libraries, that can be expanded and whose behavior can be modified by

46、 subclassing. Hence ours is not a modular analysis for libraries since we only analyze complete (closed) Android applications.There are many static analyzers that are able to analyze Java source code and find bugs or ineciencies. Most of them are based on syntactical analyses (Checkstyle 4, Coverity

47、 7, FindBugs HYPERLINK /publication/221321576_Using_FindBugs_on_production_software?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQYWdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxNzQyMjUzNDkwMg= 11, 3, PMD 23) or use theorem prov-ing with some simplifying (and in g

48、eneral unsound) hypotheses (ESC/Java HYPERLINK /publication/2529521_Extended_Static_Checking_for_Java?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQYWdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxNzQyMjUzNDkwMg= 12).Since the Android language is Java, only the lib

49、rary changes, it might be in prin-ciple possible to apply those analyzers to Android source code as well. However, as we show in the next sections, there are new language features, such as XML inflation, that are not understood by those tools and that aect the same con-struction of the control flow

50、graph of the program, usually performed through a type inference analysis known as class analysis HYPERLINK /publication/2265604_Object-Oriented_Type_Inference?el=1_x_8&enrichId=rgreq-d1eeedda-4924-4eda-8528-b199a7a5cd1c&enrichSource=Y292ZXJQYWdlOzIyMDgwNTUxNTtBUzoxNjk0OTY1NDc0Mzg1OTNAMTQxNzQyMjUzND

51、kwMg= 20; there are many new kinds of bugs in Android code, because of the way the library is used, that are not typical of Java. Hence, either a static analyzer assumes that those features do not exist and those bugs do not occur (unsoundness) or must deal with them, possibly in a sound way. We think that the solutions that we high