Thesis (Ph. D.)--Cornell University, January, 2009. / Vita. Includes bibliographical references (leaves 192-205).

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

General Relativity (GR) is one theory amongst a wider range of plausible descriptions of the Universe. The aim of this thesis is to examine the behaviour of so-called screened theories, which are designed to avoid local tests of modified gravity (MG). We establish that these theories may be treated in a unified manner in the context of halo formation. A prerequisite for this is the clarification that the quasi-static approximation can be applied in cosmologically-plausible scenarios. Amongst the plethora of MG theories, we select three, each of which exhibit a different form of screening. This describes a self-concealing property whereby each theory behaves like GR in the conditions of the local Universe. Only at regions of high energy density (chameleon), large coupling to matter (symmetron) or large derivatives of the scalar field (Vainshtein) does their modified behaviour emerge. We examine f(R), symmetron and DGP gravity in the context of non-linear gravitational collapse for the remainder of the thesis. Relativistic scalar fields are ubiquitous in our modern understanding of structure formation. They arise as candidates for dark energy and are at the heart of many modified theories of gravity. While there has been tremendous progress in calculating their effects on large scales there are still open questions on how to best quantify their effects on smaller scales where non-linear collapse becomes important. In these regimes, it has become the norm to use the quasi-static approximation in which the time evolution of perturbations in the scalar fields are discarded, akin to what is done in the context of non-relativistic fields in cosmology and the corresponding Newtonian limit. We show that considerable care must be taken in this regime by studying linearly perturbed scalar field cosmologies and quantifying the error that arise from taking the quasi-static limit. We focus on f(R) and chameleon models to assess the impact of the quasi-static approximation and discuss how it might affect studying the non-linear growth of structure in N-body numerical simulations. The halo mass function (HMF) n(M) dM is the number of haloes with mass in the range [ M, M+dM ] per unit volume. It has two remarkable properties which render it a useful probe of extensions to general relativity (GR). On the one hand, it is (nearly-)universal, in the sense that it can be written in a form (f(v) which is (practically) insensitive to changes in redshift and cosmological parameters and redshift. We develop a method to generalise fitting functions derived in GR to a variety of screened MG theories, in order to examine whether they are universal in the sense of being insensitive to MG. On the other hand, the HMF is sensitive to both the expansion history of the universe and the non-linear behaviour of spherical collapse via the critical density parameter and the matter power spectrum via the halo resolution. This greatly complicates the theoretical framework required to calculate the HMF, particularly given the sensitivity of chameleon MG to the surrounding environment. We explore a variety of new and existing methods to do so. Finally we re-calibrate the MG halo mass functions with the same rigour as has been done in GR. An important indicator of modified gravity is the effect of the local environment on halo properties. This paper examines the influence of the local tidal structure on the halo mass function, the halo orientation, spin and the concentration-mass relation. We generalise the excursion set formalism to produce a halo mass function conditional on large-scale structure. Our model agrees well with simulations on large scales at which the density field is linear or weakly non-linear. Beyond this, our principal result is that f(R does affect halo abundances, the halo spin parameter and the concentration-mass relationship in an environment-independent way, whereas we find no appreciable deviation from LCDM for the mass function with fixed environment density, nor the alignment of the orientation and spin vectors of the halo to the eigenvectors of the local cosmic web. There is a general trend for greater deviation from LCDM in under-dense environments and for high-mass haloes, as expected from chameleon screening. Given the broad spectrum of MG theories, it is important to design new probes of MG. Despite the fact that we examine only three theories of MG, the techniques and methodology developed in this thesis can be applied to a wide variety of theories and can be extended to improve the results in this work.

Submitted by LARISSA DELMONT COLACITI null (larissadelaciti@yahoo.com.br) on 2016-03-24T18:37:11Z No. of bitstreams: 1 Dissertação Larissa (texto e pré-textual)1.pdf: 1132631 bytes, checksum: 90947c8e89157bc2af02930316e36ae6 (MD5) / Approved for entry into archive by Ana Paula Grisoto (grisotoana@reitoria.unesp.br) on 2016-03-24T19:53:07Z (GMT) No. of bitstreams: 1 colaciti_ld_me_bauru.pdf: 1132631 bytes, checksum: 90947c8e89157bc2af02930316e36ae6 (MD5) / Made available in DSpace on 2016-03-24T19:53:07Z (GMT). No. of bitstreams: 1 colaciti_ld_me_bauru.pdf: 1132631 bytes, checksum: 90947c8e89157bc2af02930316e36ae6 (MD5) Previous issue date: 2016-02-26 / A postura corporal é um dos indícios mais relevantes que a comunicação não verbal exerce no ser humano, podendo revelar até mesmo estados emocionais. As posturas abertas ou expansivas, com cabeça erguida e membros em extensão sugerem dominância, autoridade e poder sobre uma situação; e as posturas fechadas ou retraídas, com cabeça baixa e membros em flexão suscitam sentimentos mais depressivos, inseguros e negativos. Esta pesquisa tem o objetivo de verificar a influência das posturas abertas e fechadas sobre o equilíbrio estático, a autoestima, a frequência cardíaca e a saturação de oxigênio. Participaram 40 universitários, média de idade 21,25 anos, que realizaram as posturas abertas (dois minutos), aferiram a frequência cardíaca e a saturação de oxigênio, subiram na plataforma de força para verificar o equilíbrio estático, e responderam o escala de autoestima de Rosenberg, depois permaneciam em posturas fechadas (dois minutos) e realizaram as mesmas tarefas descritas. Os resultados mostraram que as posturas abertas e fechadas afetaram significantemente a autoestima, a frequência cardíaca e o equilíbrio estático, sendo que, os participantes realizando as posturas abertas tiveram maior escore na autoestima, na frequência cardíaca e também melhoram a estabilidade postural nas variáveis, área e deslocamento total do centro de pressão. Realizando-se as posturas fechadas diminuíram o escore da autoestima, da frequência cardíaca e menor estabilidade postural. / The body posture is one of the most important evidence that non-verbal communication exercises in humans may reveal even emotional states. Open or expansive postures, with raised head and limbs in extension suggests dominance, authority and power over a situation; and postures closed or retracted, with head and limbs in flexion raise more depressive, insecure and negative feelings. This research aims to investigate the influence of the open and closed positions on the static balance, self-esteem, heart rate and oxygen saturation. Attended by 40 students, average age 21.25 years, who underwent open positions (two minutes), measured the heart rate and oxygen saturation, they were up on the force platform to check the static equilibrium, and responded to the self-esteem scale Rosenberg, then remained in closed positions (two minutes) and performed the same tasks described. The results showed that the open and closed positions significantly affected the self-esteem, heart rate and static balance, with the participants holding open positions had higher scores on self-esteem, heart rate and also improve postural stability in variable area and total displacement of the center of pressure. By performing the closed postures decreased the score of self-esteem, heart rate and less postural stability.

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

Orientador: Renata Soares Junqueira / Banca: Maria Lúcia Outeiro Fernandes / Banca: Annie Gisele Fernandes / Resumo: Este marinheiro procura estabelecer pontos de diálogo entre o drama estático O Marinheiro, de Fernando Pessoa, e algumas de suas obras poéticas posteriores mostrando que, naquele, residem as sementes destas. Procura, também, fazer uma análise dos temas e dos postulados filosóficos que perpassam o drama estático, bem como da forma poética construída pelo Pessoa dramaturgo, deixando derivar dessa análise a comparação com sua poesia e seu multifacetado processo de criação. / Abstract: This work aims to establish dialogue points between the static drama O Marinheiro, by Fernando Pessoa, and some of his later poetical works, showing that in the former are reside the similarities of the latters. It also aims to do an analysis of the themes and the philosophical postulates which pass the static drama like as the poetical form constructed by Pessoa dramatist, and from this analysis deflects a comparision with his poetic work, and his multifaceted process of creation. / Mestre

[pt] Os compensadores estáticos são equipamentos modernos que estão sendo cada vez mais utilizados nos sistemas de potência. Existem basicamente três tipos de compensadores estáticos: reatores saturáveis, reator controlado e tiristores (RCT) e capacitor chaveado a tiristores (CCT). Os dois últimos são compostos basicamente por reatores, capacitores, válvulas de tiristores e um sistema de controle. As válvulas de tiristores e o sistema de controle são os itens tecnologicamente mais importantes e representam cerca de 30% do custo. Por isso este trabalho aborda um dos aspectos mais importante do projeto da válvula; as sobretensões de comutação. Estas sobretensões ocorrem repetitivamente nas condições normais de operação e são inerentes às características do equipamento e às características dos tiristores. Este trabalho analisa a influência destas características e apresenta um modelo digital de tiristor que permite representar detalhadamente estas sobre tensões. Finalmente, os resultados obtidos com este modelo e com o programa SPICE são comparados com a análise teórica e com resultados medidos em laboratório. / [en] The Static Var Compensators are modern equipments which are been more and more used in power systems. There is three types of static var compensators; saturable reactors, thyristor controlled reactors and thyristor switched capacitors. The thyristor valves and control system are, from the technological point view, the most important items of the last two types and represent about 30% of its cost. Therefore, this work treats with one of the most important aspects of the design of thyristor’s valves; the commutation overvoltages. These overvoltages occur repeatedly under normal conditions and are caused by intrinsic characteristics of the equipment and by the intrinsic characteristics of the thyristors. This works analyses the influence of these characteristics and presents a thyristor digital model which permits the detailed representation of these overvoltages. Finally, the results obtained with this model and with the digital program SPICE are compared with the theoretical analysis and with measured results.

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.