Software permeates every facet of our lives, improving their convenience and efficiency, and its sphere of influence continues to expand, leading to novel applications and services. However, as software grows in complexity, it increasingly exposes vulnerabilities within the intricate landscape of security threats. Program analysis emerges as a pivotal technique for constructing software that is secure, reliable, and efficient. Despite this, existing methodologies predominantly rely on rules and heuristics, which necessitate substantial manual tuning to accommodate the diverse components of software. In this dissertation, I introduce our advancements in data-driven program analysis, a novel approach in which we employ machine learning techniques to comprehend both the structures and behaviors of programs, thereby enhancing the analysis and security of software applications. Besides focusing on traditional software, I also elaborate on our work in the systematic testing and formal verification of learned software components, including neural networks. I commence by detailing a succession of studies centered on the ambitious goal of learning execution-aware program representations. This is achieved by training large language models to understand program execution semantics. I illustrate that the models equipped with execution-aware pre-training attain state-of-the-art results in a range of program analysis tasks, such as detecting semantically similar code, type inference, memory dependence analysis, debugging symbol recovery, and generating invariants. Subsequently, I outline our approach to learning program structures and dependencies for disassembly and function boundary recovery, which are building blocks for downstream reverse engineering and binary analysis tasks. In the final part of this dissertation, I delve into DeepXplore, the inaugural white-box testing framework designed for deep learning systems, and VeriVis, a pioneering verification framework capable of proving the robustness guarantee of neural networks with only black-box access, extending beyond norm-bounded input transformations.

This thesis proposes an implementation for a decentralized version of the Git version controlsystem. This is achieved using a simple distributed DAG ledger. The thesis analyzeshow the decentralization of Git affects security. Use and misuse cases are used to compareand evaluate conventional Git web services and a decentralized version of Git. Theproposed method for managing the state of the Git project is described as a voting systemwhere participants in a Git project vote on changes to be made. The security evaluationfound that the removal of privileged roles in the Git version control system, mitigated thepossibility of malicious maintainers taking over the project. However, with the introductionof the DAG ledger and the decentralization, the possibility of a malicious actor takingover the network using Sybil attack arises, which in turn could cause the same issues as amalicious maintainer.

Software systems are becoming increasingly complex, with developers frequentlyutilizing numerous dependencies. In this landscape, accurate tracking and understanding of dependencies within JavaScript and TypeScript codebases are vital formaintaining software security and quality. However, there exists a gap in how existing vulnerability scanning tools, such as Dependabot, convey information aboutthe usage of these dependencies. This study addresses the problem of providing amore comprehensive dependency usage overview, a topic critical to aiding developers in securing their software systems. To bridge this gap, a custom pipeline wasimplemented to supplement Dependabot, extracting the dependencies identified asvulnerable and providing specific information about their usage within a repository.The results highlight the pros and cons of this approach, showing an improvement inthe understanding of dependency usage. The effort opens a pathway towards moresecure software systems.

[pt] Os defeitos nas especificações de requisitos podem ter consequências graves durante o ciclo de vida de desenvolvimento de software. Alguns deles resultam em uma falha geral do projeto devido a características de qualidade incorretas ou ausentes, como segurança. Existem várias preocupações que tornam a segurança difícil de lidar; por exemplo, (1) quando as partes interessadas discutem os requisitos gerais nas reuniões, muitas vezes não estão cientes que também devem discutir tópicos relacionados à segurança. (2) Normalmente as equipes de desenvolvimento não possuem conhecimentos de segurança suficientes. Isto geralmente leva a aspectos de segurança não especificados ou mal definidos. Essas preocupações tornam-se ainda mais desafiadoras em contextos de desenvolvimento ágil, nos quais a documentação leve geralmente está envolvida. O objetivo desta dissertação é projetar e avaliar uma abordagem para suportar a revisão de aspectos relacionados à segurança em especificações de requisitos ágeis de aplicativos web. A abordagem projetada considera estórias de usuário e especificações de segurança como entradas e relaciona essas estórias de usuário a propriedades de segurança através de técnicas de Processamento de Linguagem Natural. Com base nas propriedades de segurança relacionadas, nossa abordagem identifica os requisitos de segurança de alto nível do OWASP (Open Web Application Security Project) a serem verificados e gera uma técnica de leitura focada para dar suporte aos revisores na detecção de defeitos. Avaliamos nossa abordagem rodando dois experimentos controlados. Comparamos a eficácia e a eficiência de inspetores novatos que verificam aspectos de segurança em requisitos ágeis usando nossa técnica de leitura contra o uso da lista completa de requisitos de segurança de alto nível do OWASP. Os resultados (estatisticamente significativos) indicam que o uso da nossa abordagem tem um impacto positivo (com tamanho de efeito muito grande) no desempenho dos inspetores em termos de eficácia e eficiência. / [en] Defects in requirements specifications can have severe consequences during the software development life cycle. Some of them result in overall project failure due to incorrect or missing quality characteristics such as security. There are several concerns that make security difficult to deal with; for instance, (1) when stakeholders discuss general requirements in (review) meetings, they are often not aware that they should also discuss security-related topics, and (2) they typically do not have enough expertise in security. This often leads to unspecified or ill-defined security aspects. These concerns become even more challenging in agile development contexts, where lightweight documentation is typically involved. The goal of this dissertation is to design and evaluate an approach to support reviewing security-related aspects in agile requirements specifications of web applications. The designed approach considers user stories and security specifications as input and relates those user stories to security properties via Natural Language Processing (NLP). Based on the related security properties, our approach then identifies high-level security requirements from the Open Web Application Security Project (OWASP) to be verified and generates a focused reading technique to support reviewers in detecting defects. We evaluate our approach via two controlled experiment trials. We compare the effectiveness and efficiency of novice inspectors verifying security aspects in agile requirements using our reading technique against using the complete list of OWASP high-level security requirements. The (statistically significant) results indicate that using our approach has a positive impact (with very large effect size) on the performance of inspectors in terms of effectiveness and efficiency.

This work presents the implementation of the the IEEE 1609.2 WAVE Security Services Standard. This implementation provides the ability to generate a message signature, along with the capability to verify that signature for wave short messages transmitted over an unsecured medium. Only the original sender of the message can sign it, allowing for the authentication of a message to be checked. As hashing is used during the generation and verification of signatures, message integrity can be verified because a failed signature verification is a result of a compromised message. Also provided is the ability to encrypt and decrypt messages using AES-CCM to ensure that sensitive information remains safe and secure from unwanted recipients. Additionally this implementation provides a way for the 1609.2 specific data types to be encoded and decoded for ease of message transmittance. This implementation was built to support the Smart Drive initiative’s VANET testbed, supported by the National Science Foundation and is intended to run on the Vehicular Multi-technology Communication Device (VMCD) that is being developed. The VMCD runs on the embedded Linux operating system and this implementation will reside inside of the Linux kernel. / Includes bibliography. / Thesis (M.S.)--Florida Atlantic University, 2016. / FAU Electronic Theses and Dissertations Collection

O sistema de televisão é considerado o principal meio de comunicação e entretenimento no Brasil. Com o início das transmissões do sistema de televisão digital brasileiro no final de 2007, os principais impactos da digitalização do sistema de TV são: a alta definição de imagens e som, a mobilidade e a portabilidade. Com o tempo, outras funcionalidades serão incorporadas: a multiprogramação (mais de um programa no mesmo canal) e a interatividade. E é a partir da TV interativa que passa a ser possível o oferecimento de serviços para a população. Este trabalho tem como objetivo sistematizar as questões relacionadas com segurança no âmbito da televisão digital terrestre, além de propor e avaliar contribuições para uma arquitetura de segurança considerando o cenário expandido da televisão digital brasileira; especialmente no que tange a proteção de direitos autorais em TV aberta e a autenticação de aplicativos e serviços para TV interativa. A pesquisa realizada considera a realidade brasileira, suas necessidades específicas e as tecnologias disponíveis mais adequadas a elas, viabilizando o uso de serviços com alto valor agregado. Para atingir estes objetivos, foi realizado um amplo levantamento de tecnologias e sistemas existentes relacionados com o tema de segurança em TV digital. Com base neste levantamento, o trabalho apresenta uma sistematização da segurança para a televisão digital terrestre e aberta no Brasil na qual são identificados casos de uso e requisitos. É proposto o SPDA-BR, um sistema de proteção de direitos autorais adequado ao parque de televisores nacional e com menor impacto no custo de receptores; é proposto também o AUTV, um mecanismo de autenticação de aplicativos flexível (que possa ser utilizada para atualização de software, instalação de drivers, aplicativos interativos), compatível com padrões abertos e com a ICP Brasil. Esta dissertação forneceu subsídios para a escrita da norma de segurança para o Sistema Brasileiro de Televisão Digital, gerou publicações de artigos científicos e técnicos, e a comprovação de viabilidade, tanto do SPDA-BR como do AUTV, através de simulações e prova de conceito, respectivamente. / In Brazil, the television system is considered an important source of communication and entertainment. The Brazilian digital transmissions started on December 2007 and first offered functionalities were the high definition, mobility and portability. In a later moment other functionalities will be added: multiprogramming (more than one service per channel) and interactivity. With the interactivity it is possible to offer digital services to the public. This work goals are to present a systematic DTV security issues overview, to propose and analyze DTV security issues contributions; specifically to the digital rights protection, considering free to air DTV, and the services and applications to interactive TV. This research considers the Brazillian requirements and identifies the most suitable technologies to these requirements, allowing high value services integration to the television system. In order to achieve these goals, it was done a wide state of the art research and the DTV security use cases identification and its requirements specification. The SPDA-BR and AUTV were proposed. The SPDA-BR is a digital rights protection system suitable to the Brazilian scenario with the minimum cost impact. The AUTV is a flexible authentication mechanism (that can be applied to software update, driver installation and interactive DTV applications), compatible to the open standards and to the Brazilian Public Key Cryptographic Infrastructure. This text contributed to the DTV Brazilian system, generated scientific and technical publications, and specified as well as proved the feasibility of both SPDA-BR and AUTV, through simulation and proof of concept, respectively.

O sistema de televisão é considerado o principal meio de comunicação e entretenimento no Brasil. Com o início das transmissões do sistema de televisão digital brasileiro no final de 2007, os principais impactos da digitalização do sistema de TV são: a alta definição de imagens e som, a mobilidade e a portabilidade. Com o tempo, outras funcionalidades serão incorporadas: a multiprogramação (mais de um programa no mesmo canal) e a interatividade. E é a partir da TV interativa que passa a ser possível o oferecimento de serviços para a população. Este trabalho tem como objetivo sistematizar as questões relacionadas com segurança no âmbito da televisão digital terrestre, além de propor e avaliar contribuições para uma arquitetura de segurança considerando o cenário expandido da televisão digital brasileira; especialmente no que tange a proteção de direitos autorais em TV aberta e a autenticação de aplicativos e serviços para TV interativa. A pesquisa realizada considera a realidade brasileira, suas necessidades específicas e as tecnologias disponíveis mais adequadas a elas, viabilizando o uso de serviços com alto valor agregado. Para atingir estes objetivos, foi realizado um amplo levantamento de tecnologias e sistemas existentes relacionados com o tema de segurança em TV digital. Com base neste levantamento, o trabalho apresenta uma sistematização da segurança para a televisão digital terrestre e aberta no Brasil na qual são identificados casos de uso e requisitos. É proposto o SPDA-BR, um sistema de proteção de direitos autorais adequado ao parque de televisores nacional e com menor impacto no custo de receptores; é proposto também o AUTV, um mecanismo de autenticação de aplicativos flexível (que possa ser utilizada para atualização de software, instalação de drivers, aplicativos interativos), compatível com padrões abertos e com a ICP Brasil. Esta dissertação forneceu subsídios para a escrita da norma de segurança para o Sistema Brasileiro de Televisão Digital, gerou publicações de artigos científicos e técnicos, e a comprovação de viabilidade, tanto do SPDA-BR como do AUTV, através de simulações e prova de conceito, respectivamente. / In Brazil, the television system is considered an important source of communication and entertainment. The Brazilian digital transmissions started on December 2007 and first offered functionalities were the high definition, mobility and portability. In a later moment other functionalities will be added: multiprogramming (more than one service per channel) and interactivity. With the interactivity it is possible to offer digital services to the public. This work goals are to present a systematic DTV security issues overview, to propose and analyze DTV security issues contributions; specifically to the digital rights protection, considering free to air DTV, and the services and applications to interactive TV. This research considers the Brazillian requirements and identifies the most suitable technologies to these requirements, allowing high value services integration to the television system. In order to achieve these goals, it was done a wide state of the art research and the DTV security use cases identification and its requirements specification. The SPDA-BR and AUTV were proposed. The SPDA-BR is a digital rights protection system suitable to the Brazilian scenario with the minimum cost impact. The AUTV is a flexible authentication mechanism (that can be applied to software update, driver installation and interactive DTV applications), compatible to the open standards and to the Brazilian Public Key Cryptographic Infrastructure. This text contributed to the DTV Brazilian system, generated scientific and technical publications, and specified as well as proved the feasibility of both SPDA-BR and AUTV, through simulation and proof of concept, respectively.

When practicing secure programming, it is important to understand the restrictive influence programmed entities have on the propagation of authority in a program. To precisely model authority propagation in patterns of interacting entities, we present a new formalism Knowledge Behavior Models (KBM). To describe such patterns, we present a new domain specific declarative language SCOLL (Safe Collaboration Language), which semantics are expressed by means of KBMs. To calculate the solutions for the safety problems expressed in SCOLL, we have built SCOLLAR: a model checker and solver based on constraint logic programming. SCOLLAR not only indicates whether the safety requirements are guaranteed by the restricted behavior of the relied-upon entities, but also lists the different ways in which their behavior can be restricted to guarantee the safety properties without precluding their required functionality and (re-)usability. How the tool can help programmers to build reliable components that can safely interact with partially or completely untrusted components is shown in elaborate examples.

The nodes in wireless sensor networks (WSNs) utilize the radio frequency (RF) channel to communicate. Given that the RF channel is the primary communication channel, many researchers have developed techniques for securing that channel. However, the RF channel is not the only interface into a sensor. The sensing components, which are primarily designed to sense characteristics about the outside world, can also be used (or misused) as a communication (side) channel. In our work, we aim to characterize the side channels for various sensory components (i.e., light sensor, acoustic sensor, and accelerometer). While previous work has focused on the use of these side channels to improve the security and performance of a WSN, we seek to determine if the side channels have enough capacity to potentially be used for malicious activity. Specifically, we evaluate the feasibility and practicality of the side channels using today's sensor technology and illustrate that these channels have enough capacity to enable the transfer of common, well-known malware. Given that a significant number of modern robotic systems depend on the external side channels for navigation and environment-sensing, they become potential targets for side-channel attacks. Therefore, we demonstrate this relatively new form of attack which exploits the uninvestigated but predominantly used side channels to trigger malware residing in real-time robotic systems such as the iRobot Create. The ultimate goal of our work is to show the impact of this new class of attack and also to motivate the need for an intrusion detection system (IDS) that not only monitors the RF channel, but also monitors the values returned by the sensory components.

Software obfuscation is a protection technique for making code unintelligible to automated program comprehension and analysis tools. It works by performing semantic preserving transformations such that the difficulty of automatically extracting the computational logic out of code is increased. Obfuscating transforms in existing literature have been designed with the ambitious goal of being resilient against all possible reverse engineering attacks. Even though some of the constructions are based on intractable computational problems, we do not know, in practice, how to generate hard instances of obfuscated problems such that all forms of program analyses would fail. In this thesis, we address the problem of software protection by developing a weaker notion of obfuscation under which it is not required to guarantee an absolute blackbox security. Using this notion, we develop provably-correct obfuscating transforms using dependencies existing within program structures and indeterminacies in communication characteristics between programs in a distributed computing environment. We show how several well known static analysis tools can be used for reverse engineering obfuscating transforms that derive resilience from computationally hard problems. In particular, we restrict ourselves to one common and potent static analysis tool, the static slicer, and use it as our attack tool. We show the use of derived software engineering metrics to indicate the degree of success or failure of a slicer attack on a piece of obfuscated code. We address the issue of proving correctness of obfuscating transforms by adapting existing proof techniques for functional program refinement and communicating sequential processes. The results of this thesis could be used for future work in two ways: first, future researchers may extend our proposed techniques to design obfuscations using a wider range of dependencies that exist between dynamic program structures. Our restricted attack model using one static analysis tool can also be relaxed and obfuscations capable of withstanding a broader class of static and dynamic analysis attacks could be developed based on the same principles. Secondly, our obfuscatory strength evaluation techniques could guide anti-malware researchers in the development of tools to detect obfuscated strains of polymorphic viruses. / Whole document restricted, but available by request, use the feedback form to request access.