Defense Notices

The Trusted Platform Module (TPM) serves as the root-of-trust in a trusted computing environment, and therefore warrants formal specification and verification. This thesis presents results of an effort to specify and verify an abstract TPM 1.2 model using PVS that is useful for understanding the TPM and verifying protocols that use it. TPM commands are specified as state transformations and sequenced to represent protocols using a state monad. Preconditions, postconditions, and invariants are specified for individual commands and validated. All specifications are written and verified automatically using the PVS decision procedures and rewriting system.

Software use is an inescapable reality. Computer systems are embedded into devices from the mundane to the complex and significantly impact daily life. Increased use expands the opportunity for malicious use which threatens security and privacy. Factors such as high profile data breaches, rising cost due to security incidents, competitive advantage and pending legislation are driving software developers to integrate security into software development rather than adding security after a product has been developed. Security requirements must be elicited, modeled, analyzed, documented and validated beginning at the initial phases of the software engineering process rather than being added at later stages. However, approaches to developing security requirements have been lacking which presents barriers to security requirements integration during the requirements phase of software development. In particular, software development organizations working within short development lifecycles (often characterized as agile lifecyle) and minimal resources need a light and practical approach to security requirements engineering that can be easily integrated into existing agile processes. 
In this thesis, we present an approach for eliciting, analyzing, prioritizing and developing security requirements which can be integrated into existing software development lifecycles for small, agile organizations. The approach is based on identifying candidate security goals, categorizing security goals based on security perspectives, understanding the stakeholder goals to develop preliminary security requirements and prioritizing preliminary security requirements. The identification activity implements part of speech tagging to scan requirements artifacts for security terminology to discover candidate security goals. The categorization activity applies a general security perspective to candidate goals. Elicitation activities are undertaken to gain a deeper understanding of the security goals from stakeholders. Elicited goals are prioritized using risk management techniques and security requirements are developed from validated goals. Security goals may fail the validation activity, requiring further iterations of analysis, elicitation, and prioritization activities until stakeholders are satisfied with or have eliminated the security requirement. Finally, candidate security requirements are output which can be further modeled, defined and validated using other approaches. A security requirements repository is integrated into our proposed approach for future security requirements refinement and reuse. We validate the framework through an industrial case study with a small, agile software development organization.

The design of a two-way active splitter requires background knowledge of discrete RF amplifier design and 3-port power divider design. These two design topics will sufficiently showcase the knowledge acquired thus far from previous graduate courses and show the ability to research/acquire the needed information to combine these two general topics into one design. The completed design will consist of a gain stage at the input of a 3-port power divider, and a gain stage at each output of the 3-port power divider. Matching networks will be required at the input/outputs of the design and also between the gain stages and 3-port power divider. The most important design considerations are: Bandwidth, Noise and Stability. The next critical design considerations are: Gain, DC requirements, S parameter flatness return loss and Group Delay. Once the NF, BW and Stability specifications are met, the amplifier will be adjusted to increase gain until the previous specs become violated. Gain is not as critical; the minimum gain required will only need to be greater than the insertion loss of the 3-port power divider and matching networks. The matching networks will be tuned to minimize NF; maximizing gain is not as important as minimizing NF. At this point the less important parameters will be verified/optimized. ADS will be used to simulate the design. The gain stage will be simulated and optimized first. Then the optimized gain stage will be added to the 3-port power divider input/outputs, along with the matching networks, to create the finalized simulation. Once the simulation of the entire design has been optimized it will be implemented similar to the simulation steps. Start with a milled PCB to test/optimize the gain stage. Then mill a PCB of the entire design and test/optimize it also. Throughout the simulation and implementation testing/optimizing the main design lessons learned/take aways will be presented and discussed. The main goal is to present the major design tradeoffs discovered throughout the design process.

Firewalls, network devices, and the access control lists that manage traffic are very important components of modern networking from a security and regulatory perspective. They provide the protection between networks that only wish to communicate over an explicit set of channels, expressed through the protocols, traveling over the network. 
In small test environments and networks, firewall policies may be easy to comprehend and understand; however, in real world organizations these devices and policies must be capable of handling large amounts of traffic traversing hundreds or thousands of rules in a particular policy. Therefore, the need for an organization to unerringly and deterministically understand what traffic is allowed through a firewall, while being presented with hundreds or thousands of rules and routes, is imperative. This dissertation investigates the comprehension of traffic flow through these complex devices by focusing on the following research 
topics: 
- Expands on how a security policy may be processed by decoupling the original rules from the policy, and instead allow a holistic understanding of the solution space being represented. 
- Introduces a new set of data structures and algorithms collectively referred to as a Firewall Policy Diagram (FPD). A structure that is capable of modeling Internet Protocol version 4 packet (IPv4) solution space in memory efficient, mathematically set-based entities. 
- Presents a concise, precise, and descriptive language called Firewall Policy Query Language (FPQL) as a mechanism to explore the space. FPQL is a Backus Normal Form (Backus-Naur Form) (BNF) compatible notation for a query language to do just that sort of exploration. It looks to translate concise representations of what the end user needs to know about the solution space, and extract the information from the underlying data structures. 
- Finally, this dissertation presents a behavioral model of the capabilities found in firewall type devices and a process for taking vendor-specific nuances to a common implementation. This includes understanding interfaces, routes, rules, translation, and policies; and modeling them in a consistent manner such that the many different vendor implementations may be compared to each other.

A mobile Ad Hoc network commonly referred to as a MANET is made up of many nodes that can communicate to each other directly without the need of an access point or a central coordinator. Essentially all the nodes in the network can act either as an end system or an intermediate system. The nodes are also mobile and their movements and speed can be random thus making its network topology very dynamic due to constant link breakages and formations leading to deterioration of the performance of the MANET routing protocols. MANETs are not widely deployed and therefore mobility models are used in simulation environments to test network performance. I plan to use four of the mobility models supported in the ns-3 network simulator to show the impact of mobility on MANET routing protocols. The attributes of the nodes that will be changing are velocity and node density and the performance parameters that will be evaluated are throughput, end-to-end delay and overhead. The analysis will seek to answer the following questions: how does mobility and node density affect the performance of the different protocols? Does mobility model used affect protocol performance? Is there a superior protocol that performs better overall? And is there a mobility model that seems to offer better performance to all the protocols?

A receiver monopole antenna array is designed for use in a sense-and-avoid radar for use in the Cessna C-172 and small Unmanned Aerial Vehicles (UAVs). This three element array is used for range, radial velocity and azimuthal angle calculations. After modeling and simulating it, the array is designed, implemented and finally tested in an anechoic chamber. These results are compared to both simulation and theoretical results. Since this array was designed to face harsh weather conditions, a protective dome made with ABS plastic is designed to cover it. The effects of this dome on the array’s radiation pattern are analyzed and compared to the array’s pattern without the dome. 
This array has a center frequency of 1.4454 GHz and has good reflection coefficient and coupling levels for the range of frequencies tested (1.35 to 1.5 GHz). The maximum gain of its elements varies between 0 and 2.2 dB for this frequency range.

State-of-the-art General-Purpose computing on Graphics Processing Unit (GPGPU) is facing severe power challenge due to the increasing number of cores placed on a chip with decreasing feature size. In order to hide the long latency operations, GPGPU employs the fine-grained multi-threading among numerous active threads, leading to the sizeable register files with massive power consumption. Exploring the optimal power savings in register files becomes the critical and first step towards the energy-efficient GPGPU design. The conventional method to reduce dynamic power consumption is the supply voltage scaling, and the inter-bank tunneling FETs (TFETs) are the promising candidates compared to CMOS for low voltage operations regarding to both leakage and performance. However, always executing at the low voltage (so that low frequency) will result in significant performance degradation. In this study, we propose the hybrid CMOS-TFET based register files. To optimize the register power consumption, we allocate TFET-based registers to threads whose execution progress can be delayed to some degree to avoid the memory contentions with other threads, and the CMOS-based registers are still used for threads requiring normal execution speed. Our experimental results show that the proposed technique achieves 30% energy (including both dynamic and leakage) reduction in register files with little performance degradation compared to the baseline case equipped with naive power optimization technique.

Radar instruments can be used to provide information on the internal and basal conditions of large and small ice masses. Radars operating in the lower part of the high frequency (HF) spectrum are required for sounding glaciers with large inclusions. Also, low-frequency sounders are useful for measuring thickness of fast-flowing glaciers in Greenland and Antarctica. This is due to the composition, attenuation, and backscattering from large pockets of water (inclusions) present in ice profile. 
To radio-echo sound (RES) glaciers while providing compatibility between lightweight/portability (mass and volume) with low power consumption, we have designed, built, tested and deployed a radar for sounding glaciers requiring the trade-offs between science requirements and performance. The attenuation factors for an electromagnetic (EM) wave traveling through ice such as the extinction coefficient (Ke), the target surface scattering due to the rms height and correlation length, and the external EM noise sources, have been estimated for the design of the radar. 
The HF radar used is a man-portable, dual-frequency radio-echo sounder, optimized to work in the lower half of the HF spectrum using electrically-small antennas (ESA). The radar is powered by 24 VDC provided by the use of batteries, solar panels or a portable generator capable of at least 50 W. 
On July 31, 2009, the HF sounder successfully collected ice thickness data when operated at 8.75 MHz and 14.2 MHz at Jakobshavn, Greenland glacier. The present work represents the first successful survey for ice thickness using a dual-frequency technique for enhancing range accuracy. Indeed, with a single frequency time of arrival (TOA) backscattered signal the ice thickness was estimated to be 957.1 m with an estimated accuracy of 22 m. By using a second frequency TOA and the phase information at the previously estimated range at both frequencies, the target range has been re-estimated to be 952.2 m with an estimated accuracy of 8.8 m.

Synchronization is a critical operation in digital communication systems which establishes and maintains an operational link between the transmitter and the receiver. As the advancement of digital modulation and coding schemes continues, the synchronization task becomes more and more challenging since the new standards require high-throughput functionality at low signal-to-noise ratios (SNRs). Consequently, well-established synchronization methods have to be revised and improved in order to meet the new requirements. In this research effort, we study the synchronization of continuous phase modulations (CPMs) in burst-mode communications which allow transmission of data packets to multiple users efficiently in terms of consumed power and bandwidth. Despite the attractive characteristics of CPM, its synchronization in burst-mode transmissions has not been studied well because it is a rather complex modulation with memory. In this work, we resort to data-aided techniques where a known training sequence is embedded in the burst to assist the synchronization algorithms. Therefore, the first phase of this effort is to derive the optimum training sequence for which the estimation error is minimized. The second phase consists of designing practical synchronization algorithms to resolve frequency offset, carrier phase and symbol timing ambiguities based on the observed training sequence. Finally, a hardware implementation is proposed in order to test the theoretical results in a real-world environment.

Power line communication (PLC) has received steady interest over recent decades because of its economic use of existing power lines, and is one of the communication technologies envisaged for Smart Grid (SG) applications. However, since the power lines are not initially designed for data communication, the power line medium exhibits unique challanges for data communication. In particular for broadband (BB) PLC, the PLC channel shows linear periodically time varying (LPTV) behavior synchronous to the AC mains cycle, due to the time varying impedances of electrical devices that are connected to the power grid. In this research proposal, we focus on BB PLC LPTV channels, and investigate two major aspects for an orthogonal frequency division multiplexing (OFDM) system. First, we investigate the problem of optimal bit and power allocation, in order to increase throughput and improve energy e?ciency. We also provide reduced complexity mechanisms for the proposed bit loading scheme. This part constitutes the initial phase of our research. Second, we plan to tackle the problem of channel estimation for BB PLC LPTV channels and try to come up with low overhead and reduced complexity solutions, which is part of our future work that is in progress.