Defense Notices

With the increasing frequency of natural disasters and intentional attacks that challenge the optical network, vulnerability to cascading and regional-correlated challenges is escalating. Given the high complexity and large traffic load of the optical networks, the correlated challenges pose great damage to reliable network communication. We start our research by proposing a critical regional identification mechanism and study different vulnerability scales using real-world physical network topologies. We further propose geographical diversity and incorporate it into a new graph resilience metric cTGGD (compensated Total Geographical Graph Diversity), which is capable of characterizing and differentiating resiliency level from different physical networks. We propose path geodiverse problem (PGD) and two heuristics for solving the problem with less complexity compared to the optimal algorithm. The geodiverse paths are optimized with a delay-skew optimization formulation for optimal traffic allocation. We implement GeoDivRP in ns-3 to employ the optimized paths and demonstrate their effectiveness compared to OSPF Equal-Cost Multi-Path routing (ECMP) in terms of both throughput and overall link utilization. As from the attackers perspective, we have analyzed the mechanism by which the attackers could use to maximize the attack impact with a limited budget and demonstrate the effectiveness of different network restoration plans.

With the increasing number of devices being connected to the network, efficient connection of those devices to the network is very important. The routing protocols have evolved through time. I have used Mininet and Quagga to implement the routing protocols in a topology with ten routers and eleven host machines. Initially the basic configuration of the routers is done to bring its interfaces administratively up and the IP addresses are assigned. Static routes are configured on the routers using Quagga zebra daemons. With the amount of overhead observed, static protocol is replaced with RIPv2 using the Quagga ripd daemon and the features of RIPv2 are implemented like MD5 authentication and split horizon. RIPv2 is replaced with OSPF routing protocol. The differences between static and dynamic protocol are observed. Complex OSPF applications are implemented using the Quagga ospfd daemon. The best route to the neighboring routers is changed using the OSPF cost attribute. Next the networks in the lab are 
assumed to belong to different autonomous systems and BGP is implemented using the Quagga bgpd daemon. The routing updates are filtered using the access list attributes. The path to the neighboring routers is changed using BGP metrics such as MED, weight, AS_PATH and local_pref. Load balancing is also implemented and the results are verified using traceroute and routing tables.

Single-fiber-laser-based coherent Raman scattering (CRS) spectroscopy and microscopy system can automatically maintain frequency synchronization between pump and Stokes beam, which dramatically simplifies the setup configuration. The Stokes frequency shift is generated by soliton self-frequency shift (SSFS) through a photonic crystal fiber. The impact of pulse chirping on the signal power reduction of coherent anti-Stokes Raman scattering (CARS) and stimulated Raman scattering (SRS) have been investigate through theoretical analysis and experiment. The strategies of system optimization is discussed. 
Our multimodal system provides measurement diversity among CARS, SRS and photothermal, which can be used for comparison and offering complementary information. Distribution of hemoglobin in human red blood cells and lipids in sliced mouse brain sample have been imaged. Frequency and power dependency of photothermal signal is characterized. 
Instead of using intensity modulated pump, the polarization switched SRS method is applied to our system by changing the polarization of the pump. Based on the polarization dependency of the third-order susceptibility of the material, this method is able to eliminate the nonresonant photothermal signal from the resonant SRS signal. Red blood cells and sliced mouse brain samples were imaged to demonstrate the capability of the proposed technique. The result shows that polarization switched SRS removes most of the photothermal signal. 

Rapid development in technologies and database systems result in producing and storing large amounts of data. With such an enormous increase in data over the last few decades, data mining became a useful tool to discover the knowledge hidden in large data. Domain experts often use machine learning algorithms for finding theories that would explain their data. 
In this project we compare Weka implementation of CART and C4.5 with their original implementation on different datasets from University of California Irvine (UCI). Comparisons of these implementations has been carried in terms of accuracy, decision tree complexity and area under ROC curve (AUC). Results from our experiments show that the decision tree complexity of C4.5 is much higher than CART and that the original implementation of these algorithms perform slightly better than their corresponding Weka implementation in terms of accuracy and AUC. 

Logging system information and its metrics provides us with a valuable resource to monitor the system for unusual activity and understand the various factors affecting its performance. Though there are several tools that are available to log and analyze the system locally, it is inefficient to individually analyze every system and is seldom effective in case of hardware failure. Having centralized access to this information aids the system administrators in performing their operational tasks. Here we present a centralized logging solution for system logs and metrics by using Time Series Databases (TSDB). We provide reliable storage and efficient access to system information by storing the parsed system logs and metrics in a TSDB. In this project, we develop a solution to store the system’s default log storage - syslog as well as the system metrics like CPU load, disk load, and network traffic load into a TSDB. We further extend our ability to monitor and analyze the data in our TSDB by using an open source graphing tool. 

Property-directed verification of functional programs tends to take one of two paths. 
First, is the traditional testing approach, where properties are expressed in the original programming language and checked with a collection of test data. 
Alternatively, for those desiring a more rigorous approach, properties can be written and checked with a formal tool; typically, an external proof system. 
This dissertation details a hybrid approach that captures the best of both worlds: the formality of a proof system paired with the native integration of an embedded, domain specific language (EDSL) for testing. 

At the heart of this hybridization is the titular concept -- \emph{a theorem prover as a library}. 
The verification capabilities of this prover, HaskHOL, are introduced to a Haskell development environment as a GHC compiler plugin. 
Operating at the compiler level provides for a comparatively simpler integration and allows verification to co-exist with the numerous other passes that stand between source code and program. 

The logical connection between language and proof library is formalized, and the open problems related to this connection are documented. 
Additionally, the resultant, novel verification workflow is applied to two major classes of problems, type class laws and polymorphic test cases, to judge the real-world feasibility of compiler-directed verification. 
These applications and formalization serve to position this work relative to existing work and to highlight potential, future extensions.

Ice shelves are sensitive indicators of climate change and play a critical role in the stability of ice sheets and oceanic currents. Basal melting of ice shelves plays an important role in both the mass balance of the ice sheet and the global climate system. Airborne- and satellite based remote sensing systems can perform thickness measurements of ice shelves. Time separated repeat flight tracks over ice shelves of interest generate data sets that can be used to derive basal melt rates using traditional glaciological techniques. Many previous melt rate studies have relied on surface elevation data gathered by airborne- and satellite based altimeters. These systems infer melt rates by assuming hydrostatic equilibrium, an assumption that may not be accurate, especially near an ice shelf’s grounding line. Moderate bandwidth, VHF, ice penetrating radar has been used to measure ice shelf profiles with relatively coarse resolution. This study presents the application of an ultra wide bandwidth (UWB), UHF, ice penetrating radar to obtain finer resolution data on the ice shelves. These data reveal significant details about the basal interface, including the locations and depth of bottom crevasses and deviations from hydrostatic equilibrium. While our single channel radar provides new insight into ice shelf structure, it only images a small swatch of the shelf, which is assumed to be an average of the total shelf behavior. This study takes an additional step by investigating the application of a 3 D imaging technique to a data set collected using a ground based multi channel version of the UWB radar. The intent is to show that the UWB radar could be capable of providing a wider swath 3 D image of an ice shelf. The 3 D images can then be used to obtain a more complete estimate of bottom melt rates of ice shelves.

A mobile ad-hoc network (MANET) routing algorithm defines the path packets take to reach their destination using measurements of attributes such as adjacency and distance. Graph theory is increasingly applied in many fields of research today to model the properties of data on a graph plane. Graph theory is applied to in networking to form structures from patterns of nodes. Conventional MANET protocols are often based on path measurements from wired network algorithms and do not implement mechanisms to mitigate route entropy, defined as the procession of a converged path to a path loss state as a result of increasing random movement. Graph isomorphism measures equality beginning in the individual node and in sets of nodes and edges. The measurement of isomorphism is applied in this research to form paths from an aggregate set of route inputs, such as adjacency, cardinality to impending nodes in a path, and network width. A routing protocol based on the presence of isomorphism in a MANET topology is then tested to measure the performance of the proposed routing protocol.

The problem of outdoor positioning has been largely solved via the use of GPS. This thesis addresses the problem of determining position in areas where GPS is unavailable. No clear solution exists for indoor localization and all approximation methods offer unique drawbacks. To mitigate the drawbacks, robust systems combine multiple complementary approaches. In this thesis, fusion of wireless internet access points and inertial sensors was used to allow indoor positioning without the need for prior information regarding surroundings. Implementation of the algorithm involved development of three separate systems. The first system simply combines inertial sensors on the Android Nexus 7 to form a step counter capable of providing marginally accurate initial measurements. Having achieved reliable initial measurements, the second system receives signal strength from nearby wireless internet access points, augmenting the sensor data in order to generate half-planes. The half-planes partition the available space and bound the possible region in which each access point can exist. Lastly, the third system addresses the tendency of the step counter to lose accuracy over time by using the recently established positions of the access points to correct flawed values. The resulting process forms a simple feedback loop.

It is difficult to write programs which are both correct and fast. A promising approach, functional programming, is based on the idea of using pure, mathematical functions to construct programs. With effort, it is possible to establish a connection between a specification written in a functional language, which has been proven correct, and a fast implementation, via program transformation. 

When practiced in the functional programming community, this style of reasoning is still typically performed by hand, by either modifying the source code or using pen-and-paper. Unfortunately, performing such semi-formal reasoning by directly modifying the source code often obfuscates the program, and pen-and-paper reasoning becomes outdated as the program changes over time. Even so, this semi-formal reasoning prevails because formal reasoning is time-consuming, and requires considerable expertise. Formal reasoning tools often only work for a subset of the target language, or require programs to be implemented in a custom language for reasoning. 

This dissertation investigates a solution, called HERMIT, which mechanizes reasoning during compilation. HERMIT can be used to prove properties about programs written in the Haskell functional programming language, or transform them to improve their performance. 
Reasoning in HERMIT proceeds in a style familiar to practitioners of pen-and-paper reasoning, and mechanization allows these techniques to be applied to real-world programs with greater confidence. HERMIT can also re-check recorded reasoning steps on subsequent compilations, enforcing a connection with the program as the program is developed. 

HERMIT is the first system capable of directly reasoning about the full Haskell language. The design and implementation of HERMIT, motivated both by typical reasoning tasks and HERMIT's place in the Haskell ecosystem, is presented in detail. Three case studies investigate HERMIT's capability to reason in practice. These case studies demonstrate that semi-formal reasoning with HERMIT lowers the barrier to writing programs which are both correct and fast.