Decompilation or reverse compilation is the process of translating low-level machine-readable code into high-level human-readable code. The problem is non-trivial due to the amount of information lost during compilation, but it can be divided into several smaller problems which may be solved independently. This report explores the feasibility of composing a decompilation pipeline from independent components, and the potential of exposing those components to the end-user. The components of the decompilation pipeline are conceptually grouped into three modules. Firstly, the front-end translates a source language (e.g. x86 assembly) into LLVM IR; a platform-independent low-level intermediate representation. Secondly, the middle-end structures the LLVM IR by identifying high-level control flow primitives (e.g. pre-test loops, 2-way conditionals). Lastly, the back-end translates the structured LLVM IR into a high-level target programming language (e.g. Go). The control flow analysis stage of the middle-end uses subgraph isomorphism search algorithms to locate control flow primitives in CFGs, both of which are described using Graphviz DOT files. The decompilation pipeline has been proven capable of recovering nested pre-test and post-test loops (e.g. while, do-while), and 1-way and 2-way conditionals (e.g. if, if-else) from LLVM IR. Furthermore, the data-driven design of the control flow analysis stage facilitates extensions to identify new control flow primitives. There is huge potential for future development. The Go output could be made more idiomatic by extending the post-processing stage, using components such as Grind by Russ Cox which moves variable declarations closer to their usage. The language-agnostic aspects of the design will be validated by implementing components in other languages; e.g. data flow analysis in Haskell. Additional back-ends (e.g. Python output) will be implemented to verify that the general decompilation tasks (e.g. control flow analysis, data flow analysis) are handled by the middle-end. / <p>BSc dissertation written during an ERASMUS exchange from Uppsala University to the University of Portsmouth.</p>

Formal characterization of the memory used by a program is an important basis for security analyses, compositional verification, and identification of noninterference. However, soundly proving memory usage requires operating on the assembly level due to the semantic gap between high-level languages and the code that processors actually execute. Automated methods, such as model checking, would not be able to handle many interesting functions due to the undecidability of memory usage. Fully-interactive methods do not scale well either. Sound control flow recovery (CFR) is also important for binary decompilation, verification, patching, and security analysis. It lifts raw unstructured data into a form that allows reasoning over behavior and semantics. However, doing so requires interpreting the behavior of the program when indirect or dynamic control flow exists, creating a recursive dependency. This dissertation tackles the first property with two contributions that perform proof generation combined with interactive theorem proving in a semi-automated manner: an untrusted tool extracts as much information as it can from the functions under test and then generates all the necessary proofs to be completed in a theorem prover. The first, Floyd-style approach still requires significant manual effort but provides good flexibility and ensures no paths are analyzed more than once. In contrast, the second, Hoare-style approach sacrifices some flexibility and avoidance of repeated path evaluation in order to achieve much greater automation. However, neither approach can handle the dynamic control flow caused by indirect branching. The second property is handled by the second set of contributions of this dissertation. These two contributions provide fully-automated methods of recovering control flow from binaries even in the presence of indirect branching. When such dynamic control flow cannot be overapproximatively resolved, it is clearly noted in the resultant output. In the first approach to control flow recovery, a structured memory representation allows for general analysis of control flow in the presence of indirection, gaining scalability by utilizing context-free function analysis. It supports various aliasing conditions via the usage of nondeterminism, with multiple output states potentially being produced from a given input state. The second approach adds function context and abstract interpretation-inspired modeling of the C++ exception handling (EH) application binary interface (ABI), allowing for the discovery of previously-unknown paths while maintaining or increasing automation. / Doctor of Philosophy / Modern computer programs are so complicated that individual humans cannot manually check all but the smallest programs to make sure they are correct and secure. This is even worse if you want to reduce the trusted computing base (TCB), the stuff that you have to assume is working right in order to say a program will execute correctly. The TCB includes your computer itself, but also whatever tools were used to take the programs written by programmers and transform them into a form suitable for running on a computer. Such tools are often called compilers. One method of reducing the TCB is to examine the lowest-level representation of that program, the assembly or even machine code that is actually run by your computer. This poses unique challenges, because operating on such a low level means you do not have a lot of the structure that a more abstract, higher-level representation provides. Also, sometimes you want to formally state things about a program's behavior; that is, say things about what it does with a high degree of confidence based on mathematical principles. You may also want to verify that one or more of those statements are true. If you want to be detailed about that behavior, you may need to know all of the chunks, or regions, in random-access memory (RAM) that are used by that program. RAM, henceforth referred to as just ``memory'', is your computer's first place of storage for the information used by running programs. This is distinct from long-term storage devices like hard disk drives (HDDs) or solid-state drives (SSDs), which programs do not normally have direct access to. Unfortunately, there is no one single approach that can automatically determine with absolute certainty for all cases the exact regions of memory that are read or written. This is called undecidability, and means that you need to approximate those memory regions a lot of the time if you want to have a significant degree of automation. An underapproximation, an approach that only gives you some of the regions, is not useful for formal statements as it might miss out on some behavior; it is unsound. This means that you need an overapproximation, an approach that is guaranteed to give you at least the regions read or written. Therefore, the first contribution of this dissertation is a preliminary approach to such an overapproximation. This approach is based on the work of Robert L. Floyd, focusing on the direct control flow (where the steps of a program go) in an individual function (structured program component). It still requires a lot of user effort, including having to manually specify the regions in memory that were possibly used and do a lot of work to prove that those regions are (overapproximatively) correct, so our tests were limited in scope. The second contribution automated a lot of the manual work done for the first approach. It is based on the work of Charles Antony Richard Hoare, who developed a verification approach focusing on the syntax (the textual form) of programs. This contribution produces what we call formal memory usage certificates (FMUCs), which are formal statements that the regions of memory they describe are the only ones possibly affected by the functions under test. These statements also come with proofs, which for our work are like scripts used to verify that the things the FMUCs assert about the corresponding functions can be shown to be true given the assumptions our FMUCs have. Sometimes those proofs are incomplete, though, such as when there is a loop (repeated bit of code) in a function under test or one function calls (executes) another. In those cases, a user has to finish the proof, in the first case by weakening (removing information from) the FMUC's statements about the loop and in the second by composing, or combining, the FMUCs of the two functions. Additionally, this second approach cannot handle dynamic control flow. Such control flow occurs when the low-level instructions a program uses to move to another place in that program do not have a pre-stored location to go to. Instead, that location is supplied as the program is running. This is opposed to direct control flow, where the place to go to is hard-coded into the program when it is compiled. The tool also cannot not deal with aliasing, which is when different state parts (value-holding components) of a program contain the same value and that value is used as the numeric address or identifier of a location in memory. Specifically, it cannot deal with potential aliasing, when there is not enough information available to determine if the state parts alias or not. Because of that, we had to add extra assumptions to the FMUCs that limited them to those cases where ambiguous memory-referencing state parts referred to separate memory locations. Finally, it specifically requires assembly as input; you cannot directly supply a binary to it. This is also true of the first contribution. Because of this, we were able to test on more functions than before, but not a lot more. Not being able to deal with dynamic control flow is a big problem, as almost all programs use it. For example, when a function reaches its end, it has to figure out where to return to based on the current state of the program (in the previous contribution, this was done manually). This means that control flow recovery (CFR) is very important for many applications, including decompilation (converting a program back into a higher-level form), patching (updating a program in place without modifying the original code and recompiling it), and low-level analysis or verification in general. However, as you may have noticed from earlier in this paragraph, in order to deal with such dynamic control flow you need to figure out what the possible destinations are for the individual control flow transfers. That can require knowing where you came from in the program, which means that analysis of dynamic control flow requires context (in this context, information previously obtained in the program). Even worse, it is another undecidable problem that requires overapproximation. To soundly recover control flow, we developed Hoare graphs (HGs), the third contribution of this dissertation. HGs use memory models that take the form of forests, or collections of tree data structures. A single tree represents a region in memory that may have multiple symbolic references, or abstract representations of a value. The children of the tree represent regions used in the program that are enclosed within their parent tree elements. Now, instead of assuming that all ambiguous memory regions are separate, we can use them under various aliasing conditions. We have also implemented support for some forms of dynamic control flow. Those that are not supported are clearly marked in the resultant HG. No user interaction is required even when loops are present thanks to a methodology that automatically reduces the amount of information present at a re-executed instruction until the information stabilizes. Function composition is also automatic now thanks to a method that treats each function as its own context in a safe and automated way, reducing memory consumption of our tool and allowing larger programs to be examined. In the process we did lose the ability to deal with recursion (functions that call themselves or call other functions that call back to the original), though. Lastly, we provided the ability to directly load binaries into the tool, no external disassembly (converting machine code into human-readable instructions) needed. This all allowed much greater testing than before, with applications to multiple programs and program libraries. The fourth and final contribution of this dissertation iterates on the HG work by narrowing focus to the concept of exceptional control flow. Specifically, it models the kind of exception handling used by C++ programs. This is important as, if you want to explore a program's behavior, you need to know all the places it goes to. If you use a tool that does not model exception handling, you may end up missing paths of execution caused by unwinding. This is when an exception is thrown and propagates up through the program's current stack of function calls, potentially reaching programmer-supplied handling for that exception. Despite this, commonplace tools for static, low-level program analysis do not model such unwinding. The control flow graph (CFG) produced by our exception-aware tool are called exceptional interprocedural control flow graphs (EICFGs). These provide information about the exceptions being thrown and what paths they take in the program when they are thrown. Additional improvements are a better methodology for handling dynamic control flow as well adding back in support for recursion. All told, this allowed us to explore even more programs than ever before.

To improve quality of software systems, change-based fault prediction and scope-bounded checking have been used to predict or detect faults during software development. In fault prediction, changes to program source code, such as added lines or deleted lines, are used to predict potential faults. In fault detection, scope-bounded checking of programs is an effective technique for finding subtle faults. The central idea is to check all program executions up to a given bound. The technique takes two basic forms: scope-bounded static checking, where all bounded executions of a program are transformed into a formula that represents the violation of a correctness property and any solution to the formula represents a counterexample; or scope-bounded testing where a program is tested against all (small) inputs up to a given bound on the input size. Although the accuracies of change-based fault prediction and scope-bounded checking have been evaluated with experiments, both of them have effectiveness and efficiency limitations. Previous change-based fault predictions only consider the code modified by a change while ignoring the code impacted by a change. Scope-bounded testing only concerns the correctness specifications, and the internal structure of a program is ignored. Although scope-bounded static checking considers the internal structure of programs, formulae translated from structurally complex programs might choke the backend analyzer and fail to give a result within a reasonable time. To improve effectiveness and efficiency of these approaches, we introduce local semantic analysis into change-based fault prediction and scope-bounded checking. We use data-flow analysis to disclose internal dependencies within a program. Based on these dependencies, we identify code segments impacted by a change and apply fault prediction metrics on impacted code. Empirical studies with real data showed that semantic analysis is effective and efficient in predicting faults in large-size changes or short-interval changes. While generating inputs for scope-bounded testing, we use control-flow to guide test generation so that code coverage can be achieved with minimal tests. To increase the scalability of scope-bounded checking, we split a bounded program into smaller sub-programs according to data-flow and control-flow analysis. Thus the problem of scope-bounded checking for the given program reduces to several sub-problems, where each sub-problem requires the constraint solver to check a less complex formula, thereby likely reducing the solver’s overall workload. Experimental results show that our approach provides significant speed-ups over the traditional approach. / text

Les systèmes critiques, parmi lesquels les systèmes embarqués construits autour d'un microprocesseur mono-cœur exécutant un logiciel d'application, ne sont pas à l'abri d'interférences naturelles ou malveillantes qui peuvent provoquer des fautes transitoires. Cette thèse porte sur des protections qui peuvent être implantées pour détecter les effets de telles fautes transitoires sans faire d'hypothèses sur la multiplicité des erreurs générées. De plus, ces erreurs peuvent être soit des erreurs de flot de contrôle soit des erreurs sur les données. Une nouvelle méthode de vérification de flot de contrôle est tout d'abord proposée. Elle permet de vérifier, sans modifier le système initial, que les instructions du programme d'application sont lues sans erreur et dans le bon ordre. Les erreurs sur les données sont également prises en compte par une extension de la vérification de flot de contrôle. La méthode proposée offre un bon compromis entre les différents surcoûts, le temps de latence de détection et la couverture des erreurs. Les surcoûts peuvent aussi être ajustés aux besoins de l'application. La méthode est mise en œuvre sur un prototype, construit autour d'un microprocesseur Sparc v8. Les fonctions d'analyse de criticité développées dans le cadre de la méthodologie proposée sont également utilisées pour évaluer l'impact des options de compilation sur la robustesse intrinsèque du logiciel d'application. / Critical systems, including embedded systems built around a single core microprocessor running a software application, can be the target of natural or malicious interferences that may cause transient faults. This work focuses on protections that can be implemented to detect the effects of such transient faults without any assumption about the multiplicity of generated errors. In addition, those errors can be either control flow errors or data errors. A new control flow checking method is first proposed. It monitors, without modifying the original system, that the instructions of the microprocessor application program are read without error and in the proper order. Data errors are also taken into account by an extension of the control flow checking. The proposed method offers a good compromise between overheads, latency detection and errors coverage. Trade-offs can also be tuned according to the application constraints. The methodology is demonstrated on a prototype built around a Sparc v8 microprocessor. Criticality evaluation functions developed in the frame of the proposed methodology are also used to evaluate the impact of compilation options on the intrinsic robustness of the application software.

Les smartphones sont devenus omniprésents dans notre vie quotidienne à cause des options qu'ils proposent. Aujourd'hui, Android est installé sur plus de 80% des smartphones. Les applications mobiles recueillent une grande quantité d'informations sur l'utilisateur. Par conséquent, Android est devenu une cible préférée des cybercriminels. Comprendre le fonctionnement des malwares et comment les détecter est devenu un défi de recherche important. Les malwares Android tentent souvent d'échapper à l'analyse statique en utilisant des techniques telles que l'obfuscation et le chargement dynamique du code. Des approches d'analyse ont été proposées pour exécuter l'application et surveiller son comportement. Néanmoins, les développeurs des malwares utilisent des bombes temporelles et logiques pour empêcher le code malveillant d'être exécuté sauf dans certaines circonstances. Par conséquent, plus d'actions sont requises pour déclencher et surveiller leurs comportements. Des approches récentes tentent de caractériser automatiquement le comportement malveillant en identifiant les endroits du code les plus suspicieux et en forçant leur exécution. Elles se basent sur le calcul des graphes de flot de contrôle (CFG) qui sont incomplets, car ils ne prennent pas en considération tous les types de chemins d'exécution. Ces approches analysent seulement le code d'application et ratent les chemins d'exécution générés quand l'application appelle une méthode du framework, qui appelle à son tour une autre méthode applicative. Nous proposons GPFinder, un outil qui extrait automatiquement les chemins d'exécution qui mènent vers les endroits suspicieux du code, en calculant des CFG qui incluent les appels interprocéduraux explicites et implicites. Il fournit aussi des informations clés sur l'application analysée afin de comprendre comment le code suspicieux a été injecté dans l'application. Pour valider notre approche, nous utilisons GPFinder pour étudier une collection de 14224 malwares Android. Nous évaluons que 72,69% des échantillons ont au moins un endroit suspicieux du code qui n'est atteignable qu'à travers des appels implicites. Les approches de déclenchement actuelles utilisent principalement deux stratégies pour exécuter une partie du code applicatif. La première stratégie consiste à modifier l'application excessivement pour lancer le code ciblé sans faire attention à son contexte originel. La seconde stratégie consiste à générer des entrées pour forcer le flot de contrôle à prendre le chemin désiré sans modifier le code d'application. Cependant, il est parfois difficile de lancer un endroit spécifique du code seulement en manipulant les entrées. Par exemple, quand l'application fait un hachage des données fournies en entrée et compare le résultat avec une chaîne de caractères fixe pour décider quelle branche elle doit prendre. Clairement, le programme de manipulation d'entrée devrait inverser la fonction de hachage, ce qui est presque impossible. Nous proposons TriggerDroid, un outil qui a deux buts : forcer l'exécution du code suspicieux et garder le contexte originel de l'application. Il fournit les événements framework requis pour lancer le bon composant et satisfait les conditions nécessaires pour prendre le chemin d'exécution désiré. Pour valider notre approche, nous avons fait une expérience sur 135 malwares Android de 71 familles différentes. Les résultats montrent que notre approche nécessite plus de raffinement et d'adaptation pour traiter les cas spéciaux dus à la grande diversité des échantillons analysés. Finalement, nous fournissons un retour sur les expériences que nous avons conduites sur différentes collections, et nous expliquons notre processus expérimental. Nous présentons le dataset Kharon, une collection de malwares Android bien documentés qui peuvent être utilisés pour comprendre le panorama des malwares Android. / The last years have known an unprecedented growth in the use of mobile devices especially smartphones. They became omnipresent in our daily life because of the features they offer. They allow the user to install third-party apps to achieve numerous tasks. Smartphones are mostly governed by the Android operating system. It is today installed on more than 80% of the smartphones. Mobile apps collect a huge amount of data such as email addresses, contact list, geolocation, photos and bank account credentials. Consequently, Android has become a favorable target for cyber criminals. Thus, understanding the issue, i.e., how Android malware operates and how to detect it, became an important research challenge. Android malware frequently tries to bypass static analysis using multiple techniques such as code obfuscation and dynamic code loading. To overcome these limitations, many analysis techniques have been proposed to execute the app and monitor its behavior at runtime. Nevertheless, malware developers use time and logic bombs to prevent the malicious code from executing except under certain circumstances. Therefore, more actions are needed to trigger it and monitor its behavior. Recent approaches try to automatically characterize the malicious behavior by identifying the most suspicious locations in the code and forcing them to execute. They strongly rely on the computation of application global control flow graphs (CFGs). However, these CFGs are incomplete because they do not take into consideration all types of execution paths. These approaches solely analyze the application code and miss the execution paths that occur when the application calls a framework method that in turn calls another application method. We propose in this dissertation a tool, GPFinder, that automatically exhibits execution paths towards suspicious locations in the code by computing global CFGs that include edges representing explicit and implicit interprocedural calls. It also gives key information about the analyzed application in order to understand how the suspicious code was injected into the application. To validate our approach, we use GPFinder to study a collection of 14,224 malware samples, and we evaluate that 72.69% of the samples have at least one suspicious code location which is only reachable through implicit calls. Triggering approaches mainly use one of the following strategies to run a specific portion of the application's code: the first approach heavily modifies the app to launch the targeted code without keeping the original behavioral context. The second approach generates the input to force the execution flow to take the desired path without modifying the app's code. However, it is sometimes hard to launch a specific code location just by fuzzing the input. For instance, when the application performs a hash on the input data and compares the result to a fixed string to decide which branch of the condition to take, the fuzzing program should reverse the hashing function, which is obviously a hard problem. We propose in this dissertation a tool, TriggerDroid, that has a twofold goal: force the execution of the suspicious code and keep its context close to the original one. It crafts the required framework events to launch the right app component and satisfies the necessary triggering conditions to take the desired execution path. To validate our approach, we led an experiment on a dataset of 135 malware samples from 71 different families. Results show that our approach needs more refinement and adaptation to handle special cases due to the highly diverse malware dataset that we analyzed. Finally, we give a feedback on the experiments we led on different malware datasets, and we explain our experimental process. Finally, we present the Kharon dataset, a collection of well documented Android malware that can be used to understand the malware landscape.

Sans exécuter une application, est-il possible de prévoir quelle est la méthode cible d’un site d’appel ? Est-il possible de savoir quels sont les types et les valeurs qu’une expression peut contenir ? Est-il possible de déterminer de manière exhaustive l’ensemble de comportements qu’une application peut effectuer ? Dans les trois cas, la réponse est oui, à condition d’accepter une certaine approximation. Il existe une classe d’algorithmes − peu connus à l’extérieur du cercle académique − qui analysent et simulent un programme pour calculer de manière conservatrice l’ensemble des informations qui peuvent être véhiculées dans une expression.Dans cette thèse, nous présentons ces algorithmes appelés CFAs (acronyme de Control Flow Analysis), plus précisément l’algorithme multivariant k-l-CFA. Nous combinons l’algorithme k-l-CFA avec l’analyse de taches (taint analysis),qui consiste à suivre une donnée sensible dans le flot de contrôle, afin de déterminer si elle atteint un puits (un flot sortant du programme). Cet algorithme, en combinaison avec l’interprétation abstraite pour les valeurs, a pour objectif de calculer de manière aussi exhaustive que possible l’ensemble des comportements d’une application. L’un des problèmes de cette approche est le nombre élevé de faux-positifs, qui impose un post-traitement humain. Il est donc essentiel de pouvoir augmenter la précision de l’analyse en augmentant k.k-l-CFA est notoirement connu comme étant très combinatoire, sa complexité étant exponentielle dans la valeur de k. La première contribution de cette thèse est de concevoir un modèle et une implémentation la plus efficace possible, en séparant soigneusement les parties statiques et dynamiques de l’analyse, pour permettre le passage à l’échelle. La seconde contribution de cette thèse est de proposer une nouvelle variante de CFA basée sur k-l-CFA, et appelée *-CFA, qui consiste à faire du paramètre k une propriété de chaque variante, de façon à ne l’augmenter que dans les contextes qui le justifient.Afin d’évaluer l’efficacité de notre implémentation de k-l-CFA, nous avons effectué une comparaison avec le framework Wala. Ensuite, nous validons l’analyse de taches et la détection de comportements avec le Benchmark DroidBench. Enfin, nous présentons les apports de l’algorithme *-CFA par rapport aux algorithmes standards de CFA dans le contexte d’analyse de taches et de détection de comportements. / Without executing an application, is it possible to predict the target method of a call site? Is it possible to know the types and values that an expression can contain? Is it possible to determine exhaustively the set of behaviors that an application can perform? In all three cases, the answer is yes, as long as a certain approximation is accepted.There is a class of algorithms - little known outside of academia - that can simulate and analyze a program to compute conservatively all information that can be conveyed in an expression. In this thesis, we present these algorithms called CFAs (Control flow analysis), and more specifically the multivariant k-l-CFA algorithm.We combine k-l-CFA algorithm with taint analysis, which consists in following tainted sensitive data inthe control flow to determine if it reaches a sink (an outgoing flow of the program).This combination with the integration of abstract interpretation for the values, aims to identify asexhaustively as possible all behaviors performed by an application.The problem with this approach is the high number of false positives, which requiresa human post-processing treatment.It is therefore essential to increase the accuracy of the analysis by increasing k.k-l-CFA is notoriously known as having a high combinatorial complexity, which is exponential commensurately with the value of k.The first contribution of this thesis is to design a model and most efficient implementationpossible, carefully separating the static and dynamic parts of the analysis, to allow scalability.The second contribution of this thesis is to propose a new CFA variant based on k-l-CFA algorithm -called *-CFA - , which consists in keeping locally for each variant the parameter k, and increasing this parameter in the contexts which justifies it.To evaluate the effectiveness of our implementation of k-l-CFA, we make a comparison with the Wala framework.Then, we do the same with the DroidBench benchmark to validate out taint analysis and behavior detection. Finally , we present the contributions of *-CFA algorithm compared to standard CFA algorithms in the context of taint analysis and behavior detection.

This work presents development of Human Resource Management System based on analysis of modern development trends as well as fundamentals of key functions and data structures of human resource management systems in organizations. Introduced general-purpose model meets the requirements of human resource management systems and fits for the organizations of any size and structure. The system, mentioned above, was designed using ICONIX, Martin-Odell, RUP, XP, UMM methodologies, tested using black and white box techniques and implemented by means of Lotus Notes/Domino SDK . Created software was installed for the trial period at the joint-stock company 'PTI Technologijos'. The conceptual part of the theses represents component interface specification technique capturing control flow rules. It describes a clear process for moving from business requirements to system specification and identifying system behavior rules conditioning interfaces of the system. Proposed model facilitates dealing with the change and substitutability of business rules, what can be achieved only if the system is properly specified. Interface specification technique was used in practice to design the interface between human resource management system and accountancy system.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T12:21:17Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) 2016-pbsf-msc.pdf: 596422 bytes, checksum: be9375166fe6e850180863e08b7997d8 (MD5) / Made available in DSpace on 2016-08-08T12:21:17Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) 2016-pbsf-msc.pdf: 596422 bytes, checksum: be9375166fe6e850180863e08b7997d8 (MD5) Previous issue date: 2016-03-04 / FACEPE / Implicit or indirect control flow allows a transfer of control to a procedure without having to call the procedure explicitly in the program. Implicit control flow is a staple design pattern that adds flexibility to system design. However, it is challenging for a static analysis to compute or verify properties about a system that uses implicit control flow. When a static analysis encounters a procedure call, the analysis usually approximates the call’s behavior by a summary, which conservatively generalizes the effects of any target of the call. In previous work, a static analysis that verifies security properties was developed for Android apps, but failed to achieve high precision in the presence of implicit control flow. This work presents static analyses for two types of implicit control flow that frequently appear in Android apps: Java reflection and Android intents. In our analyses, the summary of a method is the method’s signature. Our analyses help to resolve where control flows and what data is passed. This information improves the precision of downstream analyses, which no longer need to make conservative assumptions about implicit control flow, while maintaining the soundness. We have implemented our techniques for Java. We enhanced an existing security analysis with a more precise treatment of reflection and intents. In a case study involving ten real-world Android apps that use both intents and reflection, the precision of the security analysis was increased on average by two orders of magnitude. The precision of two other downstream analyses was also improved. / Fluxo de controle implícito, ou indireto, permite que haja uma transferência de controle para um procedimento sem que esse procedimento seja invocado de forma explícita pelo programa. Fluxo de controle implícito é um padrão de projeto comum e bastante utilizado na prática, que adiciona flexibilidade no design de um sistema. Porém, é um desafio para uma análise estática ter que computar e verificar propriedades sobre um sistema que usa fluxos de controle implícito. Quando uma análise estática encontra uma chamada a uma procedimento, geralmente a análise aproxima o comportamento da chamada de acordo com o sumário do método, generalizando de uma forma conservadora os efeitos da chamada ao procedimento. Em trabalho anterior, uma análise estática de segurança foi desenvolvida para aplicações Android, mas falhou em obter uma alta precisão na presença de fluxos de controle implícito. Este trabalho apresenta uma análise estática para dois tipos de fluxos de controle implícito que aparecem frequentemente em aplicações Android: Java reflection e Android intents. Nas nossas análises, o sumário de um método é a assinatura do método. Nossas análises ajudam a descobrir para onde o controle flui e que dados estão sendo passados. Essa informação melhora a precisão de outras análises estáticas, que não precisam mais tomar medidas conservadoras na presença de fluxo de controle implícito. Nós implementamos a nossa técnica em Java. Nós melhoramos uma análise de segurança existente através de um tratamento mais preciso em casos de reflection e intents. Em um estudo de caso envolvendo dez aplicações Android reais que usam reflection e intents, a precisão da análise de segurança aumentou em duas ordens de magnitude. A precisão de outras duas análises estáticas também foi melhorada.

Made available in DSpace on 2015-04-22T22:00:44Z (GMT). No. of bitstreams: 1 Francisco.pdf: 2605316 bytes, checksum: ee1fad3d9d9e7780947fc166b5909203 (MD5) Previous issue date: 2011-03-24 / The energy consumption in the past years became a very important issue in embedded system projects. The high production and wide application of mobile devices have forced the emergence of various restrictions to this system, such as: weight, size and lifetime of batteries and multiple functionalities. Mobile devices works under limited power source that autonomy and lifetime are directly related to energy consumption of the running applications. These concerns have contributed significantly to include the energy consumption as metric for project quality in embedded systems. The main goal of this work is to propose metrics, estimative and compare the energy consumption of programs code written in ANSI-C language, based on execution time of embedded systems. In order to support the approach it was improved a tool in algorithm level known as PESTI in multiple scenarios. It was written a program in ANSI-C language and loaded in processor of the ARM 7 family s. Then, it was added into this program flags to signalize start and stop in order to measure execution time of each track in analysis. The estimative tool already modified to attribute multiple scenarios, for a program written in ANSI-C and translated into an annotated control flow graph, with tracks assignments of probabilities. This model is probabilistically simulated by using Monte Carlo methodology. The proposed approach was validate carrying out a series of experimental in order to show the viability of the improved tool of estimation and characterization, which together will make the estimates of energy consumption somewhat more feasible.  Validate the proposed approach added;  Compare the results between simulation time and the tool for characterization PESTI with the same hardware platform embedded (ARM7). The experimental were divided in three steps:  Simulation of the code in the tool PESTI in multiple scenarios;  Characterization of the query code;  Comparison of the characterization tool and PESTI. The experiments were conducted on:  AMD Turion (tm) II Dual Core Mobile Processor M500, 2.20GHz, 4Gb of RAM;  OS Linux Mint Distribution kernel 2.6.22 32-bit; 11  OS Windows 7 32-bit. / Consumo de energia nos últimos anos tornou-se um aspecto importante em projetos de sistemas embarcados. A produção e utilização em larga escala dos dispositivos móveis tem imposto várias restrições como: peso, tamanho, tempo de vida útil da bateria e funcionalidades complexas. Dispositivos móveis operam sob uma fonte de energia limitada cuja autonomia e tempo de vida útil estão diretamente relacionados ao consumo de energia das aplicações. Estas questões contribuíram para incluir o consumo de energia como métrica de qualidade no projeto de sistemas embarcados. Este trabalho tem como objetivo propor uma abordagem de medição, estimação e comparação do consumo de energia de código de programas escritos em linguagem ANSI-C, baseados em ensaios de códigos previamente escolhidos com características de consumo de energia e no tempo de execução. Para dar suporte à abordagem, uma ferramenta de estimação chamada PESTI foi estendida para atender múltiplos cenários probabilísticos. Programas escritos em linguagem ANSI-C são embarcados no processador LPC2148 da família ARM 7. Nesse programa são inseridos flags de sinalização para start e stop, para delimitar o tempo de execução e medirmos o consumo de energia do código. Um hardware chamado de caracterizador de consumo de energia auxiliará na medição em tempo real de execução do código. A ferramenta de estimação chamada PESTI com características probabilísticas e atribuições para múltiplos cenários probabilísticos é usada para estimar o consumo de energia do programa escrito em ANSI-C. Validamos a abordagem proposta, executando um conjunto de experimentos mostrando a viabilidade da extensão da ferramenta de estimação e o caracterizador que, em conjunto, viabilizarão as estimativas de consumo de energia no processador alvo. As atividades realizadas para a execução dos experimentos foram:  Validar a abordagem proposta;  Comparar os resultados medidos e estimados entre a ferramenta PESTI com o caracterizador para a mesma plataforma de hardware embarcada (ARM7). Os experimentos foram divididos em três passos:  Estimação dos códigos na ferramenta PESTI em simples e múltiplos cenários;  Caracterização do código em questão;  Comparação da caracterização e ferramenta PESTI. 9 Onde os resultados obtidos mostram uma diferença entre os valores estimados e simulados e os resultados medidos. Os experimentos foram conduzidos sobre:  AMD Turion(tm) II Dual Core Mobile M500, 2.20GHz, 4GB de RAM;  SO Linux Distribuição Mint kernel 2.6.22;  SO de 32 bits Windows 7.

No description available.