Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 30 of 86

Full-Text Articles in Physical Sciences and Mathematics

Safe And Reliable Software And The Formal Verification Of Prim's Algorithm In Spark, Brian S. Wheelhouse Mar 2023

Safe And Reliable Software And The Formal Verification Of Prim's Algorithm In Spark, Brian S. Wheelhouse

Theses and Dissertations

Despite evidence that formal verification helps produce highly reliable and secure code, formal methods, i.e., mathematically based tools and approaches for software and hardware verification, are not commonly used in software and hardware development. The limited emphasis on formal verification in software education and training suggests that many developers have never considered the benefits of formal verification. Despite the challenging nature of their mathematical roots, software verification tools have improved; making it easier than ever to verify software. SPARK, a programming language and a formal verification toolset, is of particular interest for the AFRL, and will be a primary focus …


Investigating Collaboration In Software Reverse Engineering, Allison M. Wong Mar 2022

Investigating Collaboration In Software Reverse Engineering, Allison M. Wong

Theses and Dissertations

Reverse engineering (RE) is a rigorous process of exploration and analysis to support software design recovery and exploit development. The process is often conducted in teams to divide the workload and take full advantage of engineers' individual expertise and strengths. Collaboration in RE requires versatile and reliable tools that can match the environment's unpredictable and fluid nature. While studies on collaborative software development have indicated common best practices and implementations, similar standards have not been explored in reverse engineering. This research conducts semi-structured interviews with reverse engineering experts to understand their needs and solutions while working in a team. The …


An Investigation Of Data Storage In Entity-Component Systems, Bailey V. Compton Mar 2022

An Investigation Of Data Storage In Entity-Component Systems, Bailey V. Compton

Theses and Dissertations

Entity-Component Systems (ECS) have grown vastly in application since their introduction more than 20 years ago. Providing the ability to efficiently manage data and optimize program execution, ECSs, as well as the wider field of data-oriented design, have attained popularity in the realms of modeling, simulation, and gaming. This manuscript aims to elucidate and document the storage frameworks commonly found in ECSs, as well as suggesting conceptual connections between ECSs and relational databases. This formal documentation of the in-memory storage formats of entity-component systems affords the United States Air Force, the Department of Defense, and the software engineering community a …


An Entity-Component System Based, Ieee Dis Interoperability Interface, Noah W. Scott Mar 2022

An Entity-Component System Based, Ieee Dis Interoperability Interface, Noah W. Scott

Theses and Dissertations

In practice, there are several different methods of organizing data within a given software to fulfil its function. The method known as the Entity-Component System (ECS) is a software architecture where data components define entities. These components are stored as organized lists which are operated upon by systems to inject the system's desired behavior. Data is sent across the networks to communicate between simulation nodes as Protocol Data Units (PDUs). When sending PDUs across a network protocol, each simulation represents a common understanding of the world at the desired level of detail. DIS-compliant simulations are commonly written using an Object-Oriented …


Formal Spark Verification Of Various Resampling Methods In Particle Filters, Osiris J. Terry Mar 2022

Formal Spark Verification Of Various Resampling Methods In Particle Filters, Osiris J. Terry

Theses and Dissertations

The software verification in this thesis concentrates on verifying a particle filter for use in tracking and estimation, a key application area for the Air Force. The development and verification process described in this thesis is a demonstration of the power, limitation, and compromises involved in applying automated software verification tools to critical embedded software applications.


Formal Verification For High Assurance Software: A Case Study Using The Spark Auto-Active Verification Toolset, Ryan M. Baity Mar 2021

Formal Verification For High Assurance Software: A Case Study Using The Spark Auto-Active Verification Toolset, Ryan M. Baity

Theses and Dissertations

Software is an increasingly integral and sophisticated part of safety- and mission-critical systems. Poorly written software can lead to information leakage, undetected cyber breaches, and even human injury in cases where the software directly interfaces with components of a physical system. These systems may range from power facilities to remotely piloted aircraft. Software bugs and vulnerabilities can lead to severe economic hardships and loss of life in these domains. As fast as software spreads to automate many facets of our lives, it also grows in complexity. The complexity of software systems combined with the nature of the critical domains dependent …


Two Published Flight Dynamics Models Rewritten In Rust And Structures As An Ecs, Chad A. Willis Mar 2021

Two Published Flight Dynamics Models Rewritten In Rust And Structures As An Ecs, Chad A. Willis

Theses and Dissertations

This thesis explores using the Entity-Component System (ECS) architecture to implement a Flight Dynamics Model (FDM) by re-implementing two published versions in the Rust programming language using the Specs Parallel ECS (SPECS) [1] for military simulation advancement. One FDM is based on Grant Palmers published textbook titled Physics for Game Programmers [2], and another is based on David Bourgs textbook titled Physics for Game Developers [3]. Furthermore, this thesis uses these models within an interactive flight simulator.The ECS architecture is based on the Data-Oriented Design (DOD) paradigm, where Components contain the data and the Systems implement the behavior which transforms …


Analytic Provenance For Software Reverse Engineers, Wayne C. Henry Sep 2020

Analytic Provenance For Software Reverse Engineers, Wayne C. Henry

Theses and Dissertations

Reverse engineering is a time-consuming process essential to software-security tasks such as malware analysis and vulnerability discovery. During the process, an engineer will follow multiple leads to determine how the software functions. The combination of time and possible explanations makes it difficult for the engineers to maintain a context of their findings within the overall task. Analytic provenance tools have demonstrated value in similarly complex fields that require open-ended exploration and hypothesis vetting. However, they have not been explored in the reverse engineering domain. This dissertation presents SensorRE, the first analytic provenance tool designed to support software reverse engineers. A …


Sliver: Simulation-Based Logic Bomb Identification/Verification For Unmanned Aerial Vehicles, Jake M. Magness Mar 2020

Sliver: Simulation-Based Logic Bomb Identification/Verification For Unmanned Aerial Vehicles, Jake M. Magness

Theses and Dissertations

This research introduces SLIVer, a Simulation-based Logic Bomb Identification/Verification methodology, for finding logic bombs hidden within Unmanned Aerial Vehicle (UAV) autopilot code without having access to the device source code. Effectiveness is demonstrated by executing a series of test missions within a high-fidelity software-in-the-loop (SITL) simulator. In the event that a logic bomb is not detected, this methodology defines safe operating areas for UAVs to ensure to a high degree of confidence the UAV operates normally on the defined flight plan. SLIVer uses preplanned flight paths as the baseline input space, greatly reducing the input space that must be searched …


The Effect Of Modeling Simultaneous Events On Simulation Results, John M. Carboni Mar 2019

The Effect Of Modeling Simultaneous Events On Simulation Results, John M. Carboni

Theses and Dissertations

This thesis explores the method that governs the prioritizing process for simultaneous events in relation to simulation results for discrete-event simulations. Specifically, it contrasts typical discrete-event simulation (DES) execution algorithms with how events are selected and ordered by the discrete-event system specification (DEVS) formalism. The motivation for this research stems from a desire to understand how the selection of events affects simulation output (i.e., response). As a particular use case, we briefly investigate the processing of simultaneous events by the Advanced Framework for Simulation, Integration and Modeling (AFSIM), a military discrete-event combat modeling and simulation package. To facilitate the building …


Instantaneous Bandwidth Expansion Using Software Defined Radios, Nicholas D. Everett Mar 2019

Instantaneous Bandwidth Expansion Using Software Defined Radios, Nicholas D. Everett

Theses and Dissertations

The Stimulated Unintended Radiated Emissions (SURE) process has been proven capable of classifying a device (e.g. a loaded antenna) as either operational or defective. Currently, the SURE process utilizes a specialized noise radar which is bulky, expensive and not easily supported. With current technology advancements, Software Defined Radios (SDRs) have become more compact, more readily available and significantly cheaper. The research here examines whether multiple SDRs can be integrated to replace the current specialized ultra-wideband noise radar used with the SURE process. The research specifically targets whether or not multiple SDR sub-band collections can be combined to form a wider …


Near Real-Time Rf-Dna Fingerprinting For Zigbee Devices Using Software Defined Radios, Frankie A. Cruz Mar 2019

Near Real-Time Rf-Dna Fingerprinting For Zigbee Devices Using Software Defined Radios, Frankie A. Cruz

Theses and Dissertations

Low-Rate Wireless Personal Area Network(s) (LR-WPAN) usage has increased as more consumers embrace Internet of Things (IoT) devices. ZigBee Physical Layer (PHY) is based on the Institute of Electrical and Electronics Engineers (IEEE) 802.15.4 specification designed to provide a low-cost, low-power, and low-complexity solution for Wireless Sensor Network(s) (WSN). The standard’s extended battery life and reliability makes ZigBee WSN a popular choice for home automation, transportation, traffic management, Industrial Control Systems (ICS), and cyber-physical systems. As robust and versatile as the standard is, ZigBee remains vulnerable to a myriad of common network attacks. Previous research involving Radio Frequency-Distinct Native Attribute …


Progressive Network Deployment, Performance, And Control With Software-Defined Networking, Daniel J. Casey Mar 2018

Progressive Network Deployment, Performance, And Control With Software-Defined Networking, Daniel J. Casey

Theses and Dissertations

The inflexible nature of traditional computer networks has led to tightly-integrated systems that are inherently difficult to manage and secure. New designs move low-level network control into software creating software-defined networks (SDN). Augmenting an existing network with these enhancements can be expensive and complex. This research investigates solutions to these problems. It is hypothesized that an add-on device, or "shim" could be used to make a traditional switch behave as an OpenFlow SDN switch while maintaining reasonable performance. A design prototype is found to cause approximately 1.5% reduction in throughput for one ow and less than double increase in latency, …


An Analysis Of Multi-Domain Command And Control And The Development Of Software Solutions Through Devops Toolsets And Practices, Mason R. Bruza Mar 2018

An Analysis Of Multi-Domain Command And Control And The Development Of Software Solutions Through Devops Toolsets And Practices, Mason R. Bruza

Theses and Dissertations

Multi-Domain Command and Control (MDC2) is the exercise of command and control over forces in multiple operational domains (namely air, land, sea, space, and cyberspace) in order to produce synergistic effects in the battlespace, and enhancing this capability has become a major focus area for the United States Air Force (USAF). In order to meet demands for MDC2 software, solutions need to be acquired and/or developed in a timely manner, information technology infrastructure needs to be adaptable to new software requirements, and user feedback needs to drive iterative updates to fielded software. In commercial organizations, agile software development methodologies and …


Quality Of Service Impacts Of A Moving Target Defense With Software-Defined Networking, Samuel A. Mayer Mar 2018

Quality Of Service Impacts Of A Moving Target Defense With Software-Defined Networking, Samuel A. Mayer

Theses and Dissertations

An analysis of the impact a defensive network technique implemented with software-defined networking has upon quality of service experienced by legitimate users. The research validates previous work conducted at AFIT to verify claims of defensive efficacy and then tests network protocols in common use (FTP, HTTP, IMAP, POP, RTP, SMTP, and SSH) on a network that uses this technique. Metrics that indicate the performance of the protocols under test are reported with respect to data gathered in a control network. The conclusions of these experiments enable network engineers to determine if this defensive technique is appropriate for the quality of …


A Tree Locality-Sensitive Hash For Secure Software Testing, Camdon J. Cady Sep 2017

A Tree Locality-Sensitive Hash For Secure Software Testing, Camdon J. Cady

Theses and Dissertations

Bugs in software that make it through testing can cost tens of millions of dollars each year, and in some cases can even result in the loss of human life. In order to eliminate bugs, developers may use symbolic execution to search through possible program states looking for anomalous states. Most of the computational effort to search through these states is spent solving path constraints in order to determine the feasibility of entering each state. State merging can make this search more efficient by combining program states, allowing multiple execution paths to be analyzed at the same time. However, a …


Analysis Of Software Design Patterns In Human Cognitive Performance Experiments, Alexander C. Roosma Mar 2016

Analysis Of Software Design Patterns In Human Cognitive Performance Experiments, Alexander C. Roosma

Theses and Dissertations

As Air Force operations continue to move toward the use of more autonomous systems and more human-machine teaming in general, there is a corresponding need to swiftly evaluate systems with these capabilities. We support this development through software design improvements of the execution of human cognitive performance experiments. This thesis sought to answer the following two research questions addressing the core functionality that these experiments rely on for execution and analysis: 1) What data infrastructure software requirements are necessary to execute the experimental design of human cognitive performance experiments? 2) How effectively does a central data mediator design pattern meet …


Short Message Service (Sms) Command And Control (C2) Awareness In Android-Based Smartphones Using Kernel-Level Auditing, Robert J. Olipane Jun 2012

Short Message Service (Sms) Command And Control (C2) Awareness In Android-Based Smartphones Using Kernel-Level Auditing, Robert J. Olipane

Theses and Dissertations

This thesis addresses the emerging threat of botnets in the smartphone domain and focuses on the Android platform and botnets using short message service (SMS) as the command and control (C2) channel. With any botnet, C2 is the most important component contributing to its overall resilience, stealthiness, and effectiveness. This thesis develops a passive host-based approach for identifying covert SMS traffic and providing awareness to the user. Modifying the kernel and implementing this awareness mechanism is achieved by developing and inserting a loadable kernel module that logs all inbound SMS messages as they are sent from the baseband radio to …


Understanding How Reverse Engineers Make Sense Of Programs From Assembly Language Representations, Adam R. Bryant Mar 2012

Understanding How Reverse Engineers Make Sense Of Programs From Assembly Language Representations, Adam R. Bryant

Theses and Dissertations

This dissertation develops a theory of the conceptual and procedural aspects involved with how reverse engineers make sense of executable programs. Software reverse engineering is a complex set of tasks which require a person to understand the structure and functionality of a program from its assembly language representation, typically without having access to the program's source code. This dissertation describes the reverse engineering process as a type of sensemaking, in which a person combines reasoning and information foraging behaviors to develop a mental model of the program. The structure of knowledge elements used in making sense of executable programs are …


3-D Scene Reconstruction From Aerial Imagery, Jared M. Ekholm Mar 2012

3-D Scene Reconstruction From Aerial Imagery, Jared M. Ekholm

Theses and Dissertations

3-D scene reconstructions derived from Structure from Motion (SfM) and Multi-View Stereo (MVS) techniques were analyzed to determine the optimal reconnaissance flight characteristics suitable for target reconstruction. In support of this goal, a preliminary study of a simple 3-D geometric object facilitated the analysis of convergence angles and number of camera frames within a controlled environment. Reconstruction accuracy measurements revealed at least 3 camera frames and a 6 convergence angle were required to achieve results reminiscent of the original structure. The central investigative effort sought the applicability of certain airborne reconnaissance flight profiles to reconstructing ground targets. The data sets …


Combinational Circuit Obfuscation Through Power Signature Manipulation, Hyunchul Ko Jun 2011

Combinational Circuit Obfuscation Through Power Signature Manipulation, Hyunchul Ko

Theses and Dissertations

Today's military systems are composed of hardware and software systems, many of which are critical technologies, and must be protected to ensure our adversaries cannot gain any information from a various analysis attacks. Side Channel Analysis (SCA) attacks allow an attacker to gain the significant information from the measured signatures leaked by side-channels such as power consumption, and electro-magnetic emission. In this research the focus on detecting, characterizing, and manipulating the power signature by designing a power signature estimation and manipulation method. This research has determined that the proposed method capable of characterizing and altering the type of power signature …


Android Protection System: A Signed Code Security Mechanism For Smartphone Applications, Jonathan D. Stueckle Mar 2011

Android Protection System: A Signed Code Security Mechanism For Smartphone Applications, Jonathan D. Stueckle

Theses and Dissertations

This research develops the Android Protection System (APS), a hardware-implemented application security mechanism on Android smartphones. APS uses a hash-based white-list approach to protect mobile devices from unapproved application execution. Functional testing confirms this implementation allows approved content to execute on the mobile device while blocking unapproved content. Performance benchmarking shows system overhead during application installation increases linearly as the application package size increases. APS presents no noticeable performance degradation during application execution. The security mechanism degrades system performance only during application installation, when users expect delay. APS is implemented within the default Android application installation process. Applications are hashed …


Software And Critical Technology Protection Against Side Channel Analysis Through Dynamic Hardware Obfuscation, John R. Bochert Mar 2011

Software And Critical Technology Protection Against Side Channel Analysis Through Dynamic Hardware Obfuscation, John R. Bochert

Theses and Dissertations

Side Channel Analysis (SCA) is a method by which an adversary can gather information about a processor by examining the activity being done on a microchip though the environment surrounding the chip. Side Channel Analysis attacks use SCA to attack a microcontroller when it is processing cryptographic code, and can allow an attacker to gain secret information, like a crypto-algorithm's key. The purpose of this thesis is to test proposed dynamic hardware methods to increase the hardware security of a microprocessor such that the software code being run on the microprocessor can be made more secure without having to change …


Sub-Circuit Selection And Replacement Algorithms Modeled As Term Rewriting Systems, Eric D. Simonaire Dec 2008

Sub-Circuit Selection And Replacement Algorithms Modeled As Term Rewriting Systems, Eric D. Simonaire

Theses and Dissertations

Intent protection is a model of software obfuscation which, among other criteria, prevents an adversary from understanding the program’s function for use with contextual information. Relating this framework for obfuscation to malware detection, if a malware detector can perfectly normalize a program P and any obfuscation (variant) of the program O(P), the program is not intent protected. The problem of intent protection on programs can also be modeled as intent protection on combinational logic circuits. If a malware detector can perfectly normalize a circuit C and any obfuscation (variant) O(C) of the circuit, the circuit is not intent protected. In …


Secureqemu: Emulation-Based Software Protection Providing Encrypted Code Execution And Page Granularity Code Signing, William B. Kimball Dec 2008

Secureqemu: Emulation-Based Software Protection Providing Encrypted Code Execution And Page Granularity Code Signing, William B. Kimball

Theses and Dissertations

This research presents an original emulation-based software protection scheme providing protection from reverse code engineering (RCE) and software exploitation using encrypted code execution and page-granularity code signing, respectively. Protection mechanisms execute in trusted emulators while remaining out-of-band of untrusted systems being emulated. This protection scheme is called SecureQEMU and is based on a modified version of Quick Emulator (QEMU) [5]. RCE is a process that uncovers the internal workings of a program. It is used during vulnerability and intellectual property (IP) discovery. To protect from RCE program code may have anti-disassembly, anti-debugging, and obfuscation techniques incorporated. These techniques slow the …


Hardware, Software And Data Analysis Techniques For Sram-Based Field Programmable Gate Array Circuits, Eugene B. Hockenberry Jun 2008

Hardware, Software And Data Analysis Techniques For Sram-Based Field Programmable Gate Array Circuits, Eugene B. Hockenberry

Theses and Dissertations

This work presents a built, tested, and demonstrated test structure that is low-cost, flexible, and re-usable for robust radiation experimentation, primarily to investigate memory, in this case SRAMs and SRAM-based FPGAs. The space environment can induce many kinds of failures due to radiation effects. These failures result in a loss of money, time, intelligence, and information. In order to evaluate technologies for potential failures, a detailed test methodology and associated structure are required. In this solution, an FPGA board was used as the controller platform, with multiple VHDL circuit controllers, data collection and reporting modules. The structure was demonstrated by …


Obfuscation Framework Based On Functionally Equivalent Combinatorial Logic Families, Moses C. James Mar 2008

Obfuscation Framework Based On Functionally Equivalent Combinatorial Logic Families, Moses C. James

Theses and Dissertations

This thesis aims to be a few building blocks in the bridge between theoretical and practical software obfuscation that researchers will one day construct. We provide a method for random uniform selection of circuits based on a functional signature and specific construction specifiers. Additionally, this thesis includes the first formal definition of an algorithm that performs only static analysis on a program; that is analysis that does not rely on the input and output behavior of the analyzed program. This is analogous to some techniques used in real-world software reverse engineering. Finally, this thesis uses the equivalent circuit library to …


Software Obfuscation With Symmetric Cryptography, Alan C. Lin Mar 2008

Software Obfuscation With Symmetric Cryptography, Alan C. Lin

Theses and Dissertations

Software protection is of great interest to commercial industry. Millions of dollars and years of research are invested in the development of proprietary algorithms used in software programs. A reverse engineer that successfully reverses another company‘s proprietary algorithms can develop a competing product to market in less time and with less money. The threat is even greater in military applications where adversarial reversers can use reverse engineering on unprotected military software to compromise capabilities on the field or develop their own capabilities with significantly less resources. Thus, it is vital to protect software, especially the software’s sensitive internal algorithms, from …


Locating Encrypted Data Hidden Among Non-Encrypted Data Using Statistical Tools, Walter J. Hayden Mar 2007

Locating Encrypted Data Hidden Among Non-Encrypted Data Using Statistical Tools, Walter J. Hayden

Theses and Dissertations

This research tests the security of software protection techniques that use encryption to protect code segments containing critical algorithm implementation to prevent reverse engineering. Using the National Institute of Standards and Technology (NIST) Tests for Randomness encrypted regions hidden among non-encrypted bits of a binary executable file are located. The location of ciphertext from four encryption algorithms (AES, DES, RSA, and TEA) and three block sizes (10, 100, and 500 32-bit words) were tested during the development of the techniques described in this research. The test files were generated from the Win32 binary executable file of Adobe's Acrobat Reader version …


Software Protection Against Reverse Engineering Tools, Joshua A. Benson Mar 2007

Software Protection Against Reverse Engineering Tools, Joshua A. Benson

Theses and Dissertations

Advances in technology have led to the use of simple to use automated debugging tools which can be extremely helpful in troubleshooting problems in code. However, a malicious attacker can use these same tools. Securely designing software and keeping it secure has become extremely difficult. These same easy to use debuggers can be used to bypass security built into software. While the detection of an altered executable file is possible, it is not as easy to prevent alteration in the first place. One way to prevent alteration is through code obfuscation or hiding the true function of software so as …