This thesis presents a collection disjointness analysis to find disjointness relations between collections in Java. We define the three types of disjointness relations between collections: must-shared, may-shared and not-may-shared. The collection- disjointness analysis is implemented following the way of a forward data-flow analysis using Soot Java bytecode analysis framework. For method calls, which are usually difficult to analyze in static analysis, our analysis provide a way of generating and reading annotations of a method to best approximate the behavior of the calling methods. Finally, this thesis presents the experimental results of the collection-disjointness analysis on several tests.

In a context of heightened requirements for safety-critical embedded systems and ever-increasing costs of verification and validation, this research proposes to advance the state of formal analysis for control software. Formal methods are a field of computer science that uses mathematical techniques and formalisms to rigorously analyze the behavior of programs. This research develops a framework and tools to express and prove high level properties of control law implementations. One goal is to bridge the gap between control theory and computer science. An annotation language is extended with symbols and axioms to describe control-related concepts at the code level. Libraries of theorems, along with their proofs, are developed to enable an interactive proof assistant to verify control-related properties. Through integration in a prototype tool, the process of verification is made automatic, and applied to several example systems.In a context of heightened requirements for safety-critical embedded systems and ever-increasing costs of verification and validation, this research proposes to advance the state of formal analysis for control software. Formal methods are a field of computer science that uses mathematical techniques and formalisms to rigorously analyze the behavior of programs. This research develops a framework and tools to express and prove high level properties of control law implementations. One goal is to bridge the gap between control theory and computer science. An annotation language is extended with symbols and axioms to describe control-related concepts at the code level. Libraries of theorems, along with their proofs, are developed to enable an interactive proof assistant to verify control-related properties. Through integration in a prototype tool, the process of verification is made automatic, and applied to several example systems.

Dans ce début du troisième millénium, nous sommes témoins d'un nouvel âge. Ce nouvel âge est caractérisé par la transition d'une économie industrielle vers une économie basée sur la technologie de l'information. C'est l’âge de l'information. Aujourd’hui le logiciel est présent dans pratiquement tous les aspects de notre vie. Une seule vulnérabilité logicielle peut conduire à des conséquences dévastatrices. La détection de ces vulnérabilités est une tâche qui devient de plus en plus dure surtout avec les logiciels devenant plus grands et plus complexes. Dans cette thèse, nous nous sommes intéressés aux vulnérabilités de sécurité impactant les applications développées en langage C et particulièrement les vulnérabilités provenant de l'usage des fonctions de ce langage. Nous avons proposé une liste de vérifications pour la détection des portions de code causant des vulnérabilités de sécurité. Ces vérifications sont sous la forme de conditions rendant l'appel d'une fonction vulnérable. Des implémentations dans l'outil Carto-C et des expérimentations sur la base de test Juliet et les sources d'applications réelles ont été réalisées. Nous nous sommes également intéressés à la détection de vulnérabilités exploitables au niveau du code binaire. Nous avons défini en quoi consiste le motif comportemental d'une vulnérabilité. Nous avons proposé une méthode permettant de rechercher ces motifs dans les traces d'exécutions d'une application. Le calcul de ces traces d'exécution est effectué en utilisant l'exécution concolique. Cette méthode est basée sur l'annotation de zones mémoires sensibles et la détection d'accès dangereux à ces zones. L'implémentation de cette méthode a été réalisée dans l'outil Vyper et des expérimentations sur la base de test Juliet et les codes binaires d'applications réelles ont été menées avec succès / In the beginning of the third millennium we are witnessing a new age. This new age is characterized by the shift from an industrial economy to an economy based on information technology. It is the Information Age. Today, we rely on software in practically every aspect of our life. Information technology is used by all economic actors: manufactures, governments, banks, universities, hospitals, retail stores, etc. A single software vulnerability can lead to devastating consequences and irreparable damage. The situation is worsened by the software becoming larger and more complex making the task of avoiding software flaws more and more difficult task. Automated tools finding those vulnerabilities rapidly before it is late, are becoming a basic need for software industry community. This thesis is investigating security vulnerabilities occurring in C language applications. We searched the sources of these vulnerabilities with a focus on C library functions calling. We dressed a list of property checks to detect code portions leading to security vulnerabilities. Those properties give for a library function call the conditions making this call a source of a security vulnerability. When these conditions are met the corresponding call must be reported as vulnerable. These checks were implemented in Carto-C tool and experimented on the Juliet test base and on real life application sources. We also investigated the detection of exploitable vulnerability at binary code level. We started by defining what an exploitable vulnerability behavioral patterns are. The focus was on the most exploited vulnerability classes such as stack buffer overflow, heap buffer overflow and use-after-free. After, a new method on how to search for this patterns by exploring application execution paths is proposed. During the exploration, necessary information is extracted and used to find the patterns of the searched vulnerabilities. This method was implemented in our tool Vyper and experimented successfully on Juliet test base and real life application binaries.level. We started by defining what an exploitable vulnerability behavioral patterns are. The focus was on the most exploited vulnerability classes such as stack buffer overflow, heap buffer overflow and use-after-free. After, a new method on how to search for this patterns exploring application execution paths is proposed. During the exploration, necessary information is extracted and used to find the patterns of the searched vulnerabilities. This method was implemented in our Vyper tool and experimented successfully on Juliet test base and real life application binaries

abstract: Web applications are ubiquitous. Accessible from almost anywhere, web applications support multiple platforms and can be easily customized. Most people interact with web applications daily for social media, communication, research, purchases, etc. Node.js has gained popularity as a programming language for web applications. A server-side JavaScript implementation, Node.js, allows both the front-end and back-end to be coded in JavaScript. Node.js contains many features such as dynamic inclusion of other modules using a built-in function named require which dynamically locates and loads code. To be effective, web applications must perform actions quickly while avoiding unexpected interruptions. However, dynamically linked libraries can cause delays and thus downtime, because dynamically linked code must load multiple files, often from disk. As loading is one of the slowest operations a computer performs, seeking from disk can have a negative impact on performance which causes the server to feel less responsive for users. Dynamically linked code can also break when the underlying library is updated. Normally, when trying to update a server, developers will use test servers. However, if the developer accidentally updates a library in a dynamically linked system, it may be incompatible with another portion of the program. Statically linking code makes it more reliable and faster (to load) than dynamically linking code. The static linking process varies by programming language. Therefore, different static linkers need to be developed for different languages. This thesis describes the creation of a static linker, called FrozenNode, for the popular back-end web application language, Node.js. FrozenNode resolves Node.js applications into a single file that does not rely on dynamic libraries. FrozenNode was built on top of Closure Compiler to accurately process JavaScript. We found that the resolved application was faster and self-contained yielding significant advantages over the dynamically loaded application. Furthermore, both had the same output. Vulnerabilities in web applications can be found using static analysis tools, however static analysis tools must reason about dynamically linked application. FrozenNode can be used to statically link a Node.js application before being used by a JavaScript static analysis tool. / Dissertation/Thesis / Masters Thesis Computer Science 2018

Orientador: Aleardo Manacero Junior / Banca: Sergio Azevedo de Oliveira / Banca: Francisco Villarreal Alvarado / Banca: Rodolfo Jardim Azevedo / Banca: André Luiz Moura dos Santos / Resumo: Ofusca c~ao de c odigo tem por nalidade di cultar a detec c~ao de propriedades intr nsecas de um algoritmo atrav es de altera c~oes em sua sintaxe, entretanto preservando sua sem^antica. Desenvolvedores de software usam ofusca c~ao de c odigo para defender seus programas contra ataques de propriedade intelectual e para aumentar a seguran ca do c odigo. Por outro lado, programadores maliciosos geralmente ofuscam seus c odigos para esconder comportamento malicioso e para evitar detec c~ao pelos anti-v rus. Nesta tese, e introduzido um m etodo para realizar an alise com sensitividade ao contexto em bin arios com ofuscamento de chamada e retorno de procedimento. Para obter sem^antica equivalente, estes bin arios utilizam opera c~oes diretamente na pilha ao inv es de instru c~oes convencionais de chamada e retorno de procedimento. No estado da arte atual, a de ni c~ao de sensitividade ao contexto est a associada com opera c~oes de chamada e retorno de procedimento, assim, an alises interprocedurais cl assicas n~ao s~ao con aveis para analisar bin arios cujas opera c~oes n~ao podem ser determinadas. Uma nova de ni c~ao de sensitividade ao contexto e introduzida, baseada no estado da pilha em qualquer instru c~ao. Enquanto mudan cas em contextos a chamada de procedimento s~ao intrinsicamente relacionadas com transfer^encia de controle, assim, podendo ser obtidas em termos de caminhos em um grafo de controle de uxo interprocedural, o mesmo n~ao e aplic avel para mudan cas em contextos a pilha. Um framework baseado em interpreta c~ao abstrata e desenvolvido para avaliar contexto baseado no estado da pilha e para derivar m etodos baseado em contextos a chamada de procedimento para uso com contextos baseado no estado da pilha. O metodo proposto n~ao requer o uso expl cito de instru c~oes de chamada e retorno de procedimento, por em depende do... (Resumo completo, clicar acesso eletrônico abaixo) / Abstract: A code obfuscation intends to confuse a program in order to make it more di cult to understand while preserving its functionality. Programs may be obfuscated to protect intellectual property and to increase security of code. Programs may also be obfuscated to hide malicious behavior and to evade detection by anti-virus scanners. We introduce a method for context-sensitive analysis of binaries that may have obfuscated procedure call and return operations. These binaries may use direct stack operators instead of the native call and ret instructions to achieve equivalent behavior. Since de nition of context-sensitivity and algorithms for context-sensitive analysis has thus far been based on the speci c semantics associated to procedure call and return operations, classic interprocedural analyses cannot be used reliably for analyzing programs in which these operations cannot be discerned. A new notion of context-sensitivity is introduced that is based on the state of the stack at any instruction. While changes in calling-context are associated with transfer of control, and hence can be reasoned in terms of paths in an interprocedural control ow graph (ICFG), the same is not true for changes in stackcontext. An abstract interpretation based framework is developed to reason about stackcontext and to derive analogues of call-strings based methods for the context-sensitive analysis using stack-context. This analysis requires the knowledge of how the stack, rather the stack pointer, is represented and on the knowledge of operators that manipulate the stack pointer. The method presented is used to create a context-sensitive version of Venable et al.'s algorithm for detecting obfuscated calls. Experimental results show that the contextsensitive version of the algorithm generates more precise results and is also computationally more e cient than its context-insensitive counterpart. / Doutor

Orientador: Renato Bertolino Júnior / Banca: Haroldo de Mayo Bernardes / Banca: João Alberto Venegas Requena / Resumo: O presente trabalho tem por objetivo obter numericamente os valores das distribuições de pressões devidas a ação do vento e seus respectivos coeficientes de pressões de formas externos em torres de seção circular. As distribuições de pressões nas torres são determinadas através da simulação numérica, utilizando-se o programa ANSYS 9.0, considerando-se a interação fluido-estrutura. Para a simulação numérica, a geometria da torre foi modelada tridimensionalmente, considerando como fluido o ar no qual a edificação está inserida. As distribuições de pressão foram determinadas para relações geométricas em planta da torre, entre a altura e o diâmetro (h/d), para valores menores ou iguais a 10. Posteriormente, comparam-se os resultados numéricos obtidos na simulação através do ANSYS com os valores apresentados pela norma NBR-6123:1988, a fim de verificar a viabilidade da utilização da simulação numérica na obtenção das distribuições de pressão em outras estruturas. / Abstract: The present work has for objective to obtain the distributions pressures values the wind actions in tower with circular section. The values of the distributions pressures are obtained to the numeric simulation, using the ANSYS 9.0 software and considering the flow structure interaction. In the numeric simulation, the tower geometry was considered in 3D dimension, and the flowed it is the air. The distributions pressures were certain for geometry relationships between the height and the diameter (h/d), for values smaller or equal than 10. Later, the ANSYS numeric results are compared with the presents values by the NBR 6123:1998, in order to verify the viability numeric simulation used for obtaining the pressures distributions in other structures. / Mestre

This thesis has investigated what different tools for static code analysis, with anemphasis on security, there exist and which of these that possibly could be used in a project at Ericsson AB in Linköping in which a HIGA (Home IMS Gateway) is constructed. The HIGA is a residential gateway that opens up for the possibility to extend an operator’s Internet Multimedia Subsystem (IMS) all the way to the user’s home and thereby let the end user connect his/her non compliant IMS devices, such as a media server, to an IMS network. Static analysis is the process of examining the source code of a program and in that way test a program for various weaknesses without having to actually execute it (compared to dynamic analysis such as testing). As a complement to the regular testing, that today is being performed in the HIGA project, four different static analysis tools were evaluated to find out which one was best suited for use in the HIGA project. Two of them were open source tools and two were commercial. All of the tools were evaluated in five different areas: documentation, installation & integration procedure, usability, performance and types of bugs found. Furthermore all of the tools were later on used to perform testing of two modules of the HIGA. The evaluation showed many differences between the tools in all areas and not surprisingly the two open source tools turned out to be far less mature than the commercial ones. The tools that were best suited for use in the HIGA project were Fortify SCA and Flawfinder. As far as the evaluation of the HIGA code is concerned some different bugs which could have jeopardized security and availability of the services provided by it were found.

Static analysis on source code or binary code retrieves information about a software program. In object-oriented languages, static points-to analysis retrieves information about objects and how they refer to each other. The result of the points-to analysis is traditionally used to perform optimizations in compilers, such as static resolution of polymorphic calls, and dead-code elimination. More advanced optimizations have been suggested specifically for Java, such as synchronization removal and stack-allocation of objects. Recently, software engineering tools using points-to analysis have appeared aiming to help the developer to understand and to debug software. Altogether, there is a great variety of tools that use or could use points-to analysis, both from academia and from industry. We aim to construct a framework that supports the development of new and the improvement of existing clients to points-to analysis result. We present two client analyses and investigate the similarities and differences they have. The client analyses are the escape analysis and the side-effects analysis. The similarities refer to data structures and basic algorithms that both depend on. The differences are found in the way the two analyses use the data structures and the basic algorithms. In order to reuse these in a framework, a specification language is needed to reflect the differences. The client analyses are implemented, with shared data-structures and basic algorithms, but do not use a separate specification language. The framework is evaluated against three goal criteria, development speed, analysis precision, and analysis speed. The development speed is ranked as most important, and the two latter are considered equally important. Thereafter we present related work and discuss it with respect to the goal criteria. The evaluation of the framework is done in two separate experiments. The first experiment evaluates development speed and shows that the framework enables higher development speed compared to not using the framework. The second experiment evaluates the precision and the speed of the analyses and it shows that the different precisions in the points-to analysis are reflected in the precisions of the client analyses. It also shows that there is a trade-off between analysis precision and analysis speed to consider when choosing analysis precision. Finally, we discuss four alternative ways to continue the research towards a doctoral thesis.

Software testing is a fundamental part of the software development process. However, testing is still costly and consumes about half of the development cost. The path explosion problem often necessitates one to consider an extremely large number of paths in order to reach a specific target. Symbolic execution can reduce this cost by using symbolic values and heuristic exploration strategies. Although various exploration strategies have been proposed in the past, the number of Satisfiability Modulo Theories (SMT) solver calls for reaching a target is still large, resulting in longer execution times for programs containing many paths. In this paper, we present two partitioning strategies in order to mitigate this problem, consequently reducing unnecessary SMT solver calls as well. In sequential partitioning, code sections are analyzed sequentially to take advantage of infeasible paths discovered in earlier sections. On the other hand, using dynamic partitioning on SSA-applied code, the code sections are analyzed in a non-consecutive order guided by data dependency metrics within the sections. Experimental results show that both strategies can achieve significant speedup in reducing the number of unnecessary solver calls in large programs. More than 1000x speedup can be achieved in large programs over conflict-driven learning. / Master of Science

This thesis proposes a methodology for an acquisition of dependencies between outputs and inputs in Java programs by using static program analysis on bytecode of Java programs. JaBSSA methodology designed by the author is presented in the thesis. The methodology is based on a construction of context-sensitive call graph of the analyzed program and subsequent construction of directed data flow graph, where nodes containing particular metadata represent inputs and outputs of the analyzed program and edges represent data flows amongst them present in the analyzed program. The program on added CD contains JaBSSA's implemen- tation, which serves as a proof of the proposed concept. Java program examples together with test suite generating results of JaBSSA's implementation upon pre- pared Java program examples are part of the program. These generated results are used for demonstration of capabilities and flaws of the proposed concept. 1