In a software life-cycle Source code repositories serve as vast storage areas for program code, ensuring its maintenance and version control throughout the development process. It is not uncommon for these repositories to house programs with hidden errors, which only manifest under specific input conditions, causing the program to deviate from its intended functionality. The growing intricacy of software design has amplified the time and resources required to pinpoint and rectify these issues. These errors, often unintended by developers, can be challenging to identify and correct. While there are techniques to auto-correct faulty code, the expansive realm of potential solutions for a single bug means there's a scarcity of tools and datasets for effective evaluation of the corrected code. This study presents FIXEVAL, a benchmark that includes flawed code entries from competitive coding challenges and their corresponding corrections. FIXEVAL offers an extensive test suite that not only gauges the accuracy of fixes generated by models but also allows for the assessment of a program's functional correctness. This suite further sheds light on time, memory limits, and acceptance based on specific outcomes. We utilize cutting-edge language models, trained on coding languages, as our reference point and juxtapose them using match-based (essentially token similarity) and execution-based (focusing on functional assessment) criteria. Our research indicates that while match-based criteria might not truly represent the functional precision of fixes generated by models, execution-based approaches offer a comprehensive evaluation tailored to the solution. Consequently, we posit that FIXEVAL paves the way for practical automated error correction and assessment of code generated by models. Dataset and models for all of our experiments are made publicly available at https://github.com/mahimanzum/FixEval. / Master of Science / Think of source code repositories as big digital libraries where computer programs are kept safe and updated. Sometimes, these programs have hidden mistakes that only show up under certain conditions, making the program act differently than planned which we call bugs or errors. As software gets more complex, it takes more time and effort to find and fix these mistakes. Even though there are ways to automatically fix these errors, finding the best solution can be like looking for a needle in a haystack. That's why there aren't many tools to check if the automatic fixes are right. Enter FIXEVAL: our new tool that tests and compares faulty computer code from coding competitions and their fixes. It has a set of tests to see how well the fixed code works and gives insights into its performance and results. We used the latest computer language tools to see how well they fix code, comparing them in two ways: by looking at the code's structure and by testing its function. Our findings? Just looking at the code's structure isn't enough; we need to test how it works in action. We believe FIXEVAL is a big step forward in making sure automatic code fixes are spot-on. Dataset and models for all of our experiments are made publicly available at https://github.com/mahimanzum/FixEval.

<p>Binary analysis, a cornerstone technique in cybersecurity, enables the examination of binary executables, irrespective of source code availability.</p> <p>It plays a critical role in understanding program behaviors, detecting software bugs, and mitigating potential vulnerabilities, specially in situations where the source code remains out of reach.</p> <p>However, aligning the efficacy of binary analysis with that of source-level analysis remains a significant challenge, primarily due to the uncertainty caused by the loss of semantic information during the compilation process.</p> <p><br></p> <p>This dissertation presents an innovative probabilistic approach, termed as <em>probabilistic binary analysis</em>, designed to combat the intrinsic uncertainty in binary analysis.</p> <p>It builds on the fundamental principles of program sampling and probabilistic inference, enhanced further by an iterative refinement architecture.</p> <p>The dissertation suggests that a thorough and practical method of sampling program behaviors can yield a substantial quantity of hints which could be instrumental in recovering lost information, despite the potential inclusion of some inaccuracies.</p> <p>Consequently, a probabilistic inference technique is applied to systematically incorporate and process the collected hints, suppressing the incorrect ones, thereby enabling the interpretation of high-level semantics.</p> <p>Furthermore, an iterative refinement mechanism is deployed to augment the efficiency of the probabilistic analysis in subsequent applications, facilitating the progressive enhancement of analysis outcomes through an automated or human-guided feedback loop.</p> <p><br></p> <p>This work offers an in-depth understanding of the challenges and solutions related to assessing low-level program representations and systematically handling the inherent uncertainty in binary analysis. </p> <p>It aims to contribute to the field by advancing the development of precise, reliable, and interpretable binary analysis solutions, thereby setting the groundwork for future exploration in this domain.</p>

<p dir="ltr">Deep Neural Networks (DNNs) have been deployed on edge devices for numerous applications, ranging from computer vision, speech recognition, and anomaly detection. When deployed on edge devices, dedicated DNN compilers are used to compile DNNs into binaries to exploit instruction set architectures’ (ISAs’) features and hardware accelerators (e.g., NPU, GPU). These DNN binaries on edge devices process sensitive user information, conduct critical missions, and are considered confidential intellectual property.</p><p dir="ltr">From the security standpoint, the ability to reverse engineer such binaries (i.e., recovering the original, high-level representation of the implemented DNN) enables several applications, such as DNN models stealing, gray/white-box adversarial machine learning attacks and defenses, and backdoor detection. However, no existing reverse engineering technique can recover a high-level representation of a DNN model from its compiled binary code.</p><p dir="ltr">In this dissertation, we propose the following pioneering research for reverse engineering DNN on the edge device. (i) We design and implement the first compiler- and ISA-agnostic DNN decompiler, DnD, with the static analysis technique, capable of extracting DNN models from DNN binaries running on CPU-only devices without the hardware accelerator. We show that our decompiler can perfectly recover DNN models from different DNN binaries. Furthermore, it can extract DNN models used by real-world micro-controllers and enable white-box adversarial machine learning attacks against the DNN models. (ii) We design and implement a novel data-driven approach, NeuroScope, based on dynamic analysis and machine learning to reverse engineer DNN binaries. This compiler-independent and code-feature-free approach supports a larger variety of DNN binaries across different DNN compilers and hardware platforms. We demonstrate its capability by using it to reverse engineer DNN binaries unsupported by previous approaches with high accuracy. Moreover, we showcase how NeuroScope can be used to reverse engineer a proprietary DNN binary compiled with a closed-source compiler and enable gray-box adversarial machine learning attacks.</p>

<p>Static program analyzers are vital tools to produce useful insights about programs without executing these programs. These insights can be used to improve the quality of programs, e.g., detecting defects in programs, or optimizing programs to use fewer resources. However, building static program analyzers that are simultaneously sound, performant, and flexible is notoriously challenging.</p> <p>This dissertation aims to address this challenge by exploring the potential of applying correct-by-construction metaprogramming techniques to build static program analyzers. Metaprogramming techniques manipulate and transform programs as data objects.  In this thesis, we consider static program analyzers as the objects to be manipulated or transformed. We show that metaprogramming techniques can improve our understanding, the construction, flexibility, and performance of program analyzers.</p> <p>We first study the inter-derivation of abstract interpreters. Using off-the-shelf program transformation techniques such as refunctionalization, we demonstrate that big-step abstract interpreters can be mechanically derived from their small-step counterparts, thus building a functional correspondence between two different styles of abstract interpretation.</p> <p>To build high-performance program analyzers, we exploit the first Futamura projection to build compilers for abstract interpretation and symbolic execution. The first Futamura projection states that specializing an interpreter with respect to an input program is a process equivalent to compilation, thus providing a practical way to repurpose interpreters for compilation and code generation. We systematically apply this idea to build program-analysis compilers by writing analyzers as staged interpreters using higher-level abstractions. The staged interpreter can be used for generating sound and performant analysis code given a specific input program. Moreover, the approach enables using abstractions without regret: by using higher-level program abstractions, the analyzer can be written in a way that is close to its high-level specification (e.g. big-step operational semantics), and by compilation, the analyzer is performant since it does not need to pay the runtime overhead of using these abstraction mechanisms.</p> <p>We also develop novel type systems that track sharing and separation in higher-order imperative languages. Such type systems are useful both for general-purpose programming languages and for optimization of domain-specific metaprograms such as those program-analysis compilers.</p> <p><br></p>

<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>

<p dir="ltr">Cellular-Vehicle to Everything or C-V2X refers to vehicles connected to their surroundings using cellular based networks. With the rise of connected vehicles, C-V2X is emerging as one of the major standards for message transmission in automotive scenarios. The project aims to study the feasibility of C-V2X-based message transmission by building a prototype system, named <b>RampCast</b>, for transmitting traffic information from roadside message boards to vehicles. The RampCast framework would also implement geocasting-based algorithms to deliver messages to targeted vehicles. These algorithms focus on improving location-based message delivery using retransmission and prioritization strategies. The messages used for transmission are selected from the 511 web application built by INDOT, which contains the live traffic information for the state of Indiana which includes Travel Time information, Crash Alerts, Construction Alerts etc.</p><p dir="ltr">The major objectives of this project consist of building the RampCast prototype, a system implementing C-V2X networks using a Software Defined Radio(SDR). The RampCast system implements a Publisher-subscriber messaging architecture with the primary actors being a Road Side Unit(RSU) and a Vehicle Onboard Unit(OBU). A data store containing traffic messages sourced from the 511 API is set up to be the input to the RampCast system. An end-to-end message transmission pipeline is built that would implement message transmission algorithms on the RSU and OBU side. Finally, the performance of message transmission on the RampCast system is evaluated using a metrics-capturing module. The system was evaluated on a test track in Columbus, Indiana. The performance metrics of the system were captured and analyzed, and the system met the key performance indicators for Latency, Packet Delivery Rate, and Packet Inter-reception Rate. The results indicate the satisfactory performance of the C-V2X standard for message transmission in the RampCast traffic guidance scenarios.</p>

Made available in DSpace on 2014-12-17T15:47:58Z (GMT). No. of bitstreams: 1 HeitorMAC_DISSERT.pdf: 3258229 bytes, checksum: 5f7856b140a636bd052147c58ff9dede (MD5) Previous issue date: 2011-03-01 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Through the adoption of the software product line (SPL) approach, several benefits are achieved when compared to the conventional development processes that are based on creating a single software system at a time. The process of developing a SPL differs from traditional software construction, since it has two essential phases: the domain engineering - when common and variables elements of the SPL are defined and implemented; and the application engineering - when one or more applications (specific products) are derived from the reuse of artifacts created in the domain engineering. The test activity is also fundamental and aims to detect defects in the artifacts produced in SPL development. However, the characteristics of an SPL bring new challenges to this activity that must be considered. Several approaches have been recently proposed for the testing process of product lines, but they have been shown limited and have only provided general guidelines. In addition, there is also a lack of tools to support the variability management and customization of automated case tests for SPLs. In this context, this dissertation has the goal of proposing a systematic approach to software product line testing. The approach offers: (i) automated SPL test strategies to be applied in the domain and application engineering, (ii) explicit guidelines to support the implementation and reuse of automated test cases at the unit, integration and system levels in domain and application engineering; and (iii) tooling support for automating the variability management and customization of test cases. The approach is evaluated through its application in a software product line for web systems. The results of this work have shown that the proposed approach can help the developers to deal with the challenges imposed by the characteristics of SPLs during the testing process / Com o uso da abordagem de linhas de produto de software (LPSs), v?rios benef?cios s?o alcan?ados quando comparados aos processos de desenvolvimento convencionais que se baseiam na cria??o de um ?nico sistema por vez. O processo de desenvolvimento de uma LPS se diferencia da constru??o tradicional de software, uma vez que apresenta duas etapas essenciais: a engenharia de dom?nio - quando elementos comuns e vari?veis da LPS s?o definidos e implementados; e a engenharia de aplica??o quando uma ou mais aplica??es (produtos espec?ficos) s?o derivadas a partir do reuso dos artefatos criados na engenharia de dom?nio. Durante a elabora??o da LPS, assim como no desenvolvimento convencional de sistemas, a atividade de teste ? fundamental e tem como objetivo a detec??o de defeitos nos artefatos produzidos. Contudo, as caracter?sticas de uma LPS trazem novos desafios a essa atividade e que precisam ser considerados. Diversas abordagens foram propostas para o processo de teste de linhas de produto, mas elas se mostram limitadas ou fornecem diretrizes muito gerais. Outro fator preocupante ? a escassez de ferramentas que auxiliem na implementa??o, aplica??o e acompanhamento dos testes, bem como na ger?ncia e customiza??o de tais artefatos. Com base nesse contexto relacionado ao processo de teste de LPSs, esta disserta??o tem como objetivo propor uma abordagem sistem?tica para o teste de linhas de produto de software. A abordagem oferece: (i) estrat?gias de testes automatizados para LPSs tanto na engenharia de dom?nio quanto de aplica??o; (ii) diretrizes para a implementa??o e reuso de casos de teste automatizados nos n?veis de unidade, integra??o e sistema tanto para a engenharia de dom?nio quanto de aplica??o; e (iii) suporte ferramental para ger?ncia e customiza??o autom?tica de casos de teste usando t?cnicas de deriva??o autom?tica de software. A abordagem ? avaliada atrav?s da sua aplica??o em uma linha de produto para sistemas web. Os resultados deste trabalho mostram que a abordagem proposta pode ajudar os desenvolvedores a lidar com os desafios impostos pelas caracter?sticas das LPSs durante o processo de testes

Made available in DSpace on 2014-12-17T15:48:03Z (GMT). No. of bitstreams: 1 AlexandreSGV_DISSERT.pdf: 2732563 bytes, checksum: ab07c81d7e941ed2d721415180865feb (MD5) Previous issue date: 2012-05-25 / Conselho Nacional de Desenvolvimento Cient?fico e Tecnol?gico / Software Products Lines (SPL) is a software engineering approach to developing software system families that share common features and differ in other features according to the requested software systems. The adoption of the SPL approach can promote several benefits such as cost reduction, product quality, productivity, and time to market. On the other hand, the SPL approach brings new challenges to the software evolution that must be considered. Recent research work has explored and proposed automated approaches based on code analysis and traceability techniques for change impact analysis in the context of SPL development. There are existing limitations concerning these approaches such as the customization of the analysis functionalities to address different strategies for change impact analysis, and the change impact analysis of fine-grained variability. This dissertation proposes a change impact analysis tool for SPL development, called Squid Impact Analyzer. The tool allows the implementation of change impact analysis based on information from variability modeling, mapping of variability to code assets, and existing dependency relationships between code assets. An assessment of the tool is conducted through an experiment that compare the change impact analysis results provided by the tool with real changes applied to several evolution releases from a SPL for media management in mobile devices / Linhas de Produtos de Software (LPS) consiste em um paradigma de desenvolvimento de software, no qual fam?lias de sistemas compartilham caracter?sticas comuns e tornam expl?citas outras caracter?sticas que variam de acordo com o sistema final sendo considerado. Esta abordagem oferece benef?cios ao desenvolvimento de software como redu??o de custos, qualidade do produto final, produtividade e tempo de desenvolvimento reduzido. Por outro lado, a abordagem imp?e novos desafios para a atividade de evolu??o dos artefatos que modelam e implementam a LPS. Trabalhos de pesquisa recentes prop?em abordagens com suporte automatizado de ferramentas de an?lise de impacto de mudan?a no contexto de evolu??o de LPSs. Tais abordagens s?o baseadas em t?cnicas de an?lise de impacto de mudan?as e rastreabilidade de artefatos, por?m apresentam limita??es quanto ? an?lise de impacto de mudan?as em variabilidades de granularidade fina, bem como ? customiza??o dos tipos e estrat?gias de an?lise realizadas. Esta disserta??o prop?e uma ferramenta de an?lise de impacto de mudan?a, denominada Squid Impact Analyzer, que utiliza uma estrat?gia de estimativa de impacto baseada em informa??es de caracter?sticas, mapeamento de tais caracter?sticas em artefatos de c?digo, e depend?ncia existente entre artefatos de implementa??o. A ferramenta ? avaliada atrav?s da condu??o de experimentos que realizam a quantifica??o de m?tricas de cobertura, precis?o e m?dia harm?nica nos resultados de buscas de an?lise de impacto de mudan?a da ferramenta proposta em contraposi??o ?s mudan?as reais realizadas nos artefatos de diversas vers?es de evolu??o de uma LPS para gerenciamento de m?dias em dispositivos m?veis. A ferramenta foi desenvolvida com base em uma infraestrutura que serve de base para a instancia??o de ferramentas de an?lise de propriedades de c?digo de LPSs, e que ? tamb?m parte da contribui??o da disserta??o

Made available in DSpace on 2014-12-17T15:48:08Z (GMT). No. of bitstreams: 1 EdmilsonBCN_DISSERT.pdf: 2688212 bytes, checksum: bae476692f237de556a79c9741333002 (MD5) Previous issue date: 2013-08-05 / The software systems development with domain-specific languages has become increasingly common. Domain-specific languages (DSLs) provide increased of the domain expressiveness, raising the abstraction level by facilitating the generation of models or low-level source code, thus increasing the productivity of systems development. Consequently, methods for the development of software product lines and software system families have also proposed the adoption of domain-specific languages. Recent studies have investigated the limitations of feature model expressiveness and proposing the use of DSLs as a complement or substitute for feature model. However, in complex projects, a single DSL is often insufficient to represent the different views and perspectives of development, being necessary to work with multiple DSLs. In order to address new challenges in this context, such as the management of consistency between DSLs, and the need to methods and tools that support the development with multiple DSLs, over the past years, several approaches have been proposed for the development of generative approaches. However, none of them considers matters relating to the composition of DSLs. Thus, with the aim to address this problem, the main objectives of this dissertation are: (i) to investigate the adoption of the integrated use of feature models and DSLs during the domain and application engineering of the development of generative approaches; (ii) to propose a method for the development of generative approaches with composition DSLs; and (iii) to investigate and evaluate the usage of modern technology based on models driven engineering to implement strategies of integration between feature models and composition of DSLs / A utiliza??o de linguagens espec?ficas de dom?nios para o desenvolvimento de sistemas de software tem se tornado cada vez mais comum. Elas propiciam um aumento da expressividade do dom?nio, elevando o seu n?vel de abstra??o atrav?s de facilidades para gera??o de modelos ou c?digos de baixo-n?vel, que aumentam assim a produtividade do desenvolvimento de sistemas. Como consequ?ncia, m?todos para o desenvolvimento de linhas de produtos de software e fam?lias de sistemas tamb?m t?m proposto a utiliza??o de linguagens espec?ficas de dom?nio (domain-specific languages DSLs). Estudos recentes t?m investigado os limites de expressividade do modelo de features, e propondo o uso de DSLs em sua substitui??o ou complemento. Contudo, em projetos complexos, uma ?nica DSL muitas vezes ? insuficiente para representar as diferentes vis?es e perspectivas do desenvolvimento, sendo necess?rio trabalhar com m?ltiplas DSLs. Com isso surgem novos desafios, tais como a ger?ncia de consist?ncia entre as DSLs, e a necessidade de m?todos e ferramentas que ofere?am suporte ao desenvolvimento com m?ltiplas DSLs. Ao longo dos ?ltimos anos, diversas abordagens t?m sido propostas para o desenvolvimento de abordagens generativas, entretanto, nenhuma delas considera quest?es relacionadas ? composi??o de DSLs. Assim, visando abordar tal problem?tica, os principais objetivos desta disserta??o s?o: (i) investigar a ado??o do uso integrado de modelos de features e DSLs tanto na engenharia de dom?nio quanto de aplica??o de desenvolvimento de abordagens generativas; (ii) propor um m?todo para o desenvolvimento de abordagens generativas com composi??o de DSLs; e (iii) investigar e avaliar o uso de tecnologias atuais de engenharia dirigida por modelos na implementa??o de estrat?gias de integra??o entre modelos de features e composi??o de DSLs

<p>    </p> <p>Irregular control-flow structures like deeply nested conditional branches are common in real-world software applications. Improving the performance and efficiency of such programs is often challenging because it is difficult to analyze and optimize programs with irregular control flow. We observe that real-world programs contain similar or identical computations within different code paths of the conditional branches. Compilers can merge similar code to improve performance or code size. However, existing compiler optimizations like code hoisting/sinking, and tail merging do not fully exploit this opportunity. We propose a new technique called Control-Flow Melding (CFM) that can merge similar code sequences at the control-flow region level. We evaluate CFM in two applications. First, we show that CFM reduces the control divergence in GPU programs and improves the performance. Second, we apply CFM to CPU programs and show its effectiveness in reducing code size without sacrificing performance. In the next part of this dissertation, we investigate how CFM can be extended to improve dynamic test generation techniques like Dynamic Symbolic Execution (DSE). DSE suffers from path explosion problem when many conditional branches are present in the program. We propose a non-semantics-preserving branch elimination transformation called CFM-SE that reduces the number of symbolic branches in a program. We also provide a framework for detecting and reasoning about false positive bugs that might be added to the program by non-semantics-preserving transformations like CFM-SE. Furthermore, we evaluate CFM-SE on real-world applications and show its effectiveness in improving DSE performance and code coverage. </p>