Browsing by Author "Gaeddert, Joseph Daniel"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Enhancing Communications Aware Evasion Attacks on RFML Spectrum Sensing Systems
    Delvecchio, Matthew David (Virginia Tech, 2020-08-19)
    Recent innovations in machine learning have paved the way for new capabilities in the field of radio frequency (RF) communications. Machine learning techniques such as reinforcement learning and deep neural networks (DNN) can be leveraged to improve upon traditional wireless communications methods so that they no longer require expertly-defined features. Simultaneously, cybersecurity and electronic warfare are growing areas of focus and concern in an increasingly technology-driven world. Privacy and confidentiality of communication links are both more important and more difficult than ever in the current high threat environment. RF machine learning (RFML) systems contribute to this threat as they have been shown to be successful in gleaning information from intercepted signals, through the use of learning-enabled eavesdroppers. This thesis focuses on a method of defense against such communications threats termed an adversarial evasion attack in which intelligently crafted perturbations of the RF signal are used to fool a DNN-enabled classifier, therefore securing the communications channel. One often overlooked aspect of evasion attacks is the concept of maintaining intended use. In other words, while an adversarial signal, or more generally an adversarial example, should fool the DNN it is attacking, this should not come at the detriment to it's primary application. In RF communications, this manifests in the idea that the communications link must be successfully maintained with friendly receivers, even when executing an evasion attack against malicious receivers. This is a difficult scenario, made even more so by the nature of channel effects present in over-the-air (OTA) communications, as is assumed in this work. Previous work in this field has introduced a form of evasion attack for RFML systems called a communications aware attack that explicitly addresses the reliable communications aspect of the attack by training a separate DNN to craft adversarial signals; however, this work did not utilize the full RF processing chain and left residual indicators of the attack that could be leveraged for defensive capabilities. First, this thesis focuses on implementing forward error correction (FEC), an aspect present in most communications systems, in the training process of the attack. It is shown that introducing this into the training stage allows the communications aware attack to implicitly use the structure of the coding to create smarter and more efficient adversarial signals. Secondly, this thesis then addresses the fact that in previous work, the resulting adversarial signal exhibiting significant out-of-band frequency content, a limitation that can be used to render the attack ineffective if preprocessing at the attacked DNN is assumed. This thesis presents two novel approaches to solve this problem and eliminate the majority of side content in the attack. By doing so, the communications aware attack is more readily applicable to real-world scenarios.
  • Thumbnail Image
    Facilitating Wireless Communications through Intelligent Resource Management on Software-Defined Radios in Dynamic Spectrum Environments
    Gaeddert, Joseph Daniel (Virginia Tech, 2011-01-18)
    This dissertation provides theory and analysis on the impact resource management has on software-defined radio platforms by investigating the inherent trade-off between spectrum and processing effciencies with their relation to both the power consumed by the host processor and the complexity of the algorithm which it can support. The analysis demonstrates that considerable resource savings can be gained without compromising the resulting quality of service to the user, concentrating specifically on physical-layer signal processing elements commonly found in software definitions of single- and multi-carrier communications signals. Novel synchronization techniques and estimators for unknown physical layer reference parameters are introduced which complement the energy-quality scalability of software-defined receivers. A new framing structure is proposed for single-carrier systems which enables fast synchronization of short packet bursts, applicable for use in dynamic spectrum access. The frame is embedded with information describing its own structure, permitting the receiver to automatically modify its software configuration, promoting full waveformfl‚exibility for adapting to quickly changing wireless channels. The synchronizer's acquisition time is reduced by exploiting cyclostationary properties in the preamble of transmitted framing structure, and the results are validated over the air in a wireless multi-path laboratory environment. Multi-carrier analysis is concentrated on synchronizing orthogonal frequency-division multiplexing (OFDM) using offset quadrature amplitude modulation (OFDM/OQAM) which is shown to have significant spectral compactness advantages over traditional OFDM. Demodulation of OFDM/OQAM is accomplished using computationally effcient polyphase analysis filterbanks, enabled by a novel approximate square-root Nyquist filter design based on the near-optimum Kaiser-Bessel window. Furthermore, recovery of sample timing and carrier frequency offsets are shown to be possible entirely in the frequency domain, enabling demodulation in the presence of strong interference signals while promoting heterogeneous signal coexistence in dynamic spectrum environments. Resource management is accomplished through the introduction of a self-monitoring framework which permits system-level feedback to the radio at run time. The architecture permits the radio to monitor its own processor usage, demonstrating considerable savings in computation bandwidths on the tested platform. Resource management is assisted by supervised intelligent heuristic-based learning algorithms which use software-level feedback of the radio's active resource consumption to optimize energy and processing effciencies in dynamic spectrum environments. In particular, a case database-enabled cognitive engine is proposed which abstracts from the radio application by using specific knowledge of previous experience rather than relying on general knowledge within a specific problem domain.
  • Thumbnail Image
    Toward Bridging the Semantic Gap Between x86-64 Software Binaries and Abstract Languages for Formal Verification and Security
    Roessle, Ian Henry (Virginia Tech, 2025-01-13)
    Formal verification of software systems has historically focused on verifying properties at the source code (abstract language) level (e.g., C++, Java, Python), as the language semantics are more amenable to use by mathematical libraries. However, this approach comes with limitations. Firstly, not all software has source code. Secondly, the source code may be unavailable for licensing reasons. Thirdly, even if the source code is available, formal verification at the source code level generally assumes that the compiler is trustworthy and mathematically sound. This dissertation addresses challenges with lifting the abstraction of software binaries to support formal verification and reasoning toward bridging the semantic gap. The semantic gap is the loss and obfuscation of program meaning that occurs as a result of compiling source code into software binaries. This work's primary application is verifying safety-critical systems where source code is unavailable. The x86-64 Instruction Set Architecture (ISA) was chosen due to its applicability to a wide range of relevant deployed software. As a necessary dependency for the formal verification of software binaries, a machine model of the ISA is required. The machine model is analogous to the language semantics necessary when reasoning over source code. The x86-64 ISA was also chosen because, in addition to being complex, it lacked a formal specification, making it a more challenging target. Historically, much research in the area of reasoning over x86 software binaries has focused on small fragments of code, utilizing a small subset of the ISA that could be handwritten formally, limiting research to a small subset of real-world software. The first contribution of this dissertation addresses these limitations, presenting a robust hardware-derived formal executable machine model of the x86-64 ISA, supporting 1,625 instruction variants expressed as small-step operational semantics embedded within an Interactive Theorem Prover (ITP) (a 4-fold increase over prior work). The second contribution of this dissertation presents a largely automated methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big-step operational semantics. These formally proven abstract representations of software binaries allow one to construct correctness proofs per block. To support this, we developed improved Decompilation-into-logic and formal symbolic execution techniques. We then applied this methodology to several case studies, including examples heavily relying on floating-point instructions and real-world examples. This dissertation's third contribution presents efforts to bridge the semantic gap further and tie the results to formal verification techniques commonly utilized over source code. It presents a first-of-the-art approach to leveraging a hardware-derived model derived from machine learning in software binary formal verification efforts. It introduces a library of 628 proven simplification lemmas designed to lift the abstraction of big-step operational semantics to a form more useful to proof engineers. A methodology for performing axiomatic reasoning across blocks is presented, with case studies demonstrating, for software binaries, standard formal verification techniques typically applicable to source code. Lastly, this dissertation explores a methodology for sound software binary diversity to employ a moving target defense strategy with associated security benefits. Toward bridging the semantic gap between software binaries and source code, this work demonstrates large-scale black-box software binary formal verification in settings where source code is unavailable, on a hardware-derived machine model, as well as a sound software binary diversity approach for moving target defense.