1、畢業(yè)設(shè)計外文資料翻譯學 院： 專業(yè)班級： 學生姓名： 學 號： 指導教師： 外文出處：Etienne Payet,Fausto Spoto.Information and software technology.EISCI2012 11 附 件：1.外文資料翻譯譯文 2.外文原文 指導教師評語： 查找期刊文獻進行翻譯，基本符合翻譯要求。簽名： 年 月 日外文資料翻譯譯文安卓程序的靜態(tài)分析抽象上下文：Android是基于Java程序設(shè)計語言和操作系統(tǒng)的嵌入式移動設(shè)備，其上層被寫入Android語言本身。作為一種語言，它具有擴展基于事件的庫，并在XML的布局文件圖形聲明視圖動態(tài)的通貨膨脹。Andr

2、oid方案靜態(tài)分析必須考慮這些特點，正確性和準確性。目的：我們的目標是擴大Julia靜態(tài)分析的基礎(chǔ)上，抽象解釋，執(zhí)行的Android方案的形式上正確的分析。本文是一個擴展深入的對我們面對我們獲得的成果和困難的說明，。方法：我們擴展了Julia分析儀，它坐落在許多其他分析的心臟的階級分析，考慮一些Android的關(guān)鍵功能如多入口點的可能存在一個程序和從XML圖形視圖通脹進行反射。我們還已經(jīng)顯著改善Android電子節(jié)目NULL的含量分析的精度。結(jié)果：我們與Julia分析大部分由谷歌Android的示例應(yīng)用程序和幾個較大的開源程序。我們已經(jīng)申請幾十項靜態(tài)分析，包括classcast，死代碼，NUL

3、L的含量和終止分析。Julia發(fā)現(xiàn)，自動，臭蟲，缺陷和INE FFI ciencies無論是在谷歌的樣品還是在開放源代碼的應(yīng)用程序中都存在。結(jié)論：Julia是第一部基于Android程序的基礎(chǔ)上的有聲靜態(tài)分析儀，基于如抽象解釋的正式的基礎(chǔ)上。我們的研究結(jié)果表明，它可以分析真實的第三方Android應(yīng)用程序，無需任何代碼的用戶注釋，在標準硬件上產(chǎn)生正式正確的結(jié)果在最多不超過7分鐘。因此，它已準備好在第一工業(yè)使用。關(guān)鍵詞：程序驗證，靜態(tài)分析，抽象解釋，Android郵箱: etienne.payetuniv-reunion.fr(Etienne Payet), fausto.spotounivr.

4、it (Fausto Spoto)2012年5月24日印刷版提交給Elsevier。1.簡介Android是在操作系統(tǒng)市場上為移動和EM-床設(shè)備的主要參與者，如手機，平板電腦和電視機。它是為這類設(shè)備提供的一個操作系統(tǒng)，其上層被寫入在編程語言中，也稱為Android。作為一種語言，Android是帶擴展庫移動和交互應(yīng)用的Java語言，因此，基于事件驅(qū)動的架構(gòu)。任何Java編譯器可以支持Android應(yīng)用程序，但由此產(chǎn)生的Java字節(jié)碼必須轉(zhuǎn)化為最終的，非常優(yōu)化，Dalvik的字節(jié)以便在設(shè)備上運行。Android應(yīng)用程序靜態(tài)分析是很重要的，因為質(zhì)量和可靠性是在Android市場2成功的關(guān)鍵。越野車

5、的應(yīng)用得到了負反饋，并立即被他們的潛在用戶放棄。因此，Android的程序員要確保它們的方案都是無缺陷，例如，他們不拋出任何意外的異常和不掛設(shè)備。但Android應(yīng)用也日益在關(guān)鍵上下文部署，甚至在軍事方案中，在安全性和可靠性是極為重要的。由于這些原因，一個產(chǎn)業(yè)的演員，如Klocwork的16已經(jīng)將其靜態(tài)分析工具從Java擴展到Android，我們知道的為Android獲得唯一的靜態(tài)分析。它是相對有限的電力，據(jù)我們從他們的網(wǎng)頁推斷。我們無法得到一個免費的評估許可證。如像Klocwork的一個工具是基于語法檢查。這意味著，錯誤是通過查找代碼典型的句式，往往含有錯誤認定。使用語法檢查可以非?？焖俸蛯?/p>

6、用的進行分析。但是，bug的代碼不遵循分析儀已知的預定義模式時它無法識別錯誤。這種情況下如錯誤發(fā)現(xiàn)在其中的基于形式化方法的人工智能工具的基礎(chǔ)上，語義工具如Julia也一直沒有能夠證明一個程序段不包含錯誤。第二種情況是更為復雜并且計算昂貴的，但提供了穩(wěn)健的業(yè)績的保證：如果（有些類）沒有潛在的錯誤被發(fā)現(xiàn)，再有就是類的代碼中沒有錯誤。在其他方面，語法工具是快，但不健全。這兩種方法信號誤報，也就是說，實際上不是一個真正的錯誤潛在的bug。精密（即真正的錯誤量WRT警告的數(shù)量）是在這里關(guān)鍵的問題，因為誤報的數(shù)量不應(yīng)該壓倒工具的用戶。這是通過大多數(shù)靜態(tài)分析工具開發(fā)確認。比如，我們可以給Coverity公司

7、的網(wǎng)頁7：“通過提供業(yè)界最準確的分析解決方案和最低的誤報率，你可以專注于真正的和相關(guān)的缺陷，而不是浪費開發(fā)周期”。因此，大多數(shù)的靜態(tài)分析器的顯影劑的電子是朝著誤報的數(shù)量減少努力。這對聲音分析儀更加困難，因為他們不能隨便扔掉警告，仍然留聲。在任何情況下，如Klocwork公司存在這個市場上表明行業(yè)認識到Android代碼的靜態(tài)分析的重要性。 更科學的方法是突出SCanDroid工具14，目前僅限于Android應(yīng)用程序的安全驗證。它執(zhí)行的Android應(yīng)用程序的化流量分析，通過應(yīng)用聯(lián)盟的跟蹤組件間省交通陽離子通過意圖和潛在的非法獲取安全特權(quán)。其基礎(chǔ)是代碼的基于約束的分析，并有一個健全性的保證，至

8、少一個受限制的一種字節(jié)碼。Klocwork公司目前不執(zhí)行Android應(yīng)用程序的任何信息流分析。Julia是Java字節(jié)碼一個靜態(tài)分析器，基于抽象interpreta-tion 6，以確保，自動，所分析的應(yīng)用程序不包含大的的編程隱錯。它適用于不平凡的整個程序，過程間和語義靜態(tài)分析，包括一流的演員陣容，死代碼，NULL的含量和終止分析。它配備了一個正確的保證，因為它通常是在抽象解釋社會的情況：如果應(yīng)用包含了一個錯誤，由分析儀算是一種，那么Julia會報告。這使得分析的結(jié)果更顯著。盡管Java和Android是相同的語言，有著不同的庫集，Julia到Android應(yīng)用程序也不是立竿見影，我們必須解

9、決之前許多問題，Julia可以用正確和精確的方式分析Android的程序。許多都涉及到不同的庫集，其他人使用XML來構(gòu)建應(yīng)用程序的一部分。在這篇文章中，我們提出這些問題并向他們提供我們的解決方案而且向他們展示，所產(chǎn)生的系統(tǒng)分析不平凡的Android方案，精確度高，并找出第三方代碼中的錯誤。本文不詳細描述由Julia提供的，在其他地方已公布的靜態(tài)分析，但只有適應(yīng)它分析的Android分析儀和。特別是，我們的階級分析，在簡單的檢查，如classcast和死代碼分析的心臟，在27中描述;我們的NULL的含量分析描述在25，26;我們終止分析文獻28中描述。必須指出，我們的Julia分析儀反射存在不健

10、全，Java的類加載機制和多線程的重新定義。這并不意味著，使用這些功能的程序不能被分析，而只是結(jié)果可能不正確。實際上，我們的工作中的一個主要的成就在于教Julia有關(guān)特定使用反射是在Android的XML布局膨脹期間完成的，因此，該分析的結(jié)果在這種情況下依然良好（但不包括反射的其他用途）。我們的分析假定是一個封閉的世界，某種意義上說，例如，它假定，在入口點，變量可以被綁定到每個其聲明的類型相容的類別上，可以在任何可能的方式或保持空下共享。相同的假設(shè)不能對庫制成，可以擴展，其行為可以通過子類進行修改。因此，我們不是一個模塊化的分析庫，因為我們只分析完整（關(guān)閉）的Android應(yīng)用程序。有許多靜態(tài)

11、的分析儀，它能夠分析Java源代碼，并發(fā)現(xiàn)錯誤，或國家統(tǒng)計局FFI ciencies。他們中的大多數(shù)是基于語法分析（Checkstyle的4，Coverity的7，F(xiàn)indBugs的11，3，PMD23），或者使用國際集團的定理證明的一些簡化（和一般不健全的）假設(shè)（ESC /Java12）。由于Android的語言是Java，只有庫的變化，它可能在原則上可以應(yīng)用這些分析儀Android源代碼。然而，正如我們將展示在下面的章節(jié)中，有新的語言特性，如XML通貨膨脹，不由這些工具和影響相同程序的控制流圖的施工，通常是通過一個類型進行理解推理分析稱階級分析20;有許多種Android的代碼中的新的錯誤

12、，因為庫的使用方式，這不是典型的Java。因此，無論是靜態(tài)分析假定這些功能是不存在的這些漏洞不會發(fā)生（不健全），或者必須處理這些問題，可能用一個合理的方式。我們認為，我們強調(diào)本文中的解決方案可以適用于那些靜態(tài)分析為好，因為它們不局限于選擇我們的具體的靜態(tài)分析。本文的其余部分安排如下。部2證明機器人程序的靜態(tài)分析的困難。第3節(jié)介紹與本文相關(guān)的Android的概念。第4節(jié)更相關(guān)的靜態(tài)分析，我們對Android的代碼執(zhí)行。第5，第6和第7描述我們?nèi)绾翁岣逬ulia工作在Android上。特別是，第5節(jié)討論聲音控制流圖的通過類分析的結(jié)構(gòu)，以XML通貨膨脹的存在。第8條提出了從標準的谷歌分布和較大的開放

13、源代碼項目的許多不平凡的Android方案的實驗結(jié)果;它表明Julia發(fā)現(xiàn)這些程序的一些實際的錯誤。第9節(jié)總結(jié)全文。這篇文章是在2011年22提出了在CADE較短的會議論文的擴展版本。宗全experimen河谷的評價。 8沒有出現(xiàn)在22。此外，宗4第二節(jié)5宗6提供了一個更深入的介紹我們擴展Julia的方式，相比于22的相應(yīng)部分。Julia是一種商品（），可以通過網(wǎng)頁界面可從公司，其功率由超時和分析的最大尺寸的限制的網(wǎng)站自由使用。Fausto Spoto是該公司的董事長，他在2010年11月成立該公司。他也是Julia軟件的主要開發(fā)者。Etienne Payet目前在留尼旺島（法國）副教授。他不

14、是Julia Srl的一員，但他經(jīng)常與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