Defense Notices

Coq's extraction plugin is used to produce code of a general purpose

  programming language from a specification written in the Calculus of Inductive

  Constructions (CIC). Currently, this mechanism is trusted, since there is no

  formal connection between the synthesized code and the CIC terms it originated

  from. This comes from a lack of formal specifications for the target

  languages: OCaml, Haskell, and Scheme. We intend to use the formally specified

  CakeML language as an extraction target, and generate a theorem in Coq that

  relates the generated CakeML abstract syntax to the CIC terms it is generated

  from. This work expands on the techniques used in the HOL4 translator from

  Higher Order Logic to CakeML. The HOL4 translator also allows for the

  generation of stateful code from the state and exception monad. We expand on

  their techniques by extracting terms with dependent types, and generating

  stateful code for other kinds of monads, like the reader monad, depending on

  what kind of computation the monad intends to represent.

Remote attestation is a process where one digital system gathers and provides evidence of its state and identity to an external system. For this process to be successful, the external system must find the evidence convincingly trustworthy within that context. Remote attestation is difficult to make trustworthy due to the external system’s limited access to the attestation target. In contrast to local attestation, the appraising system is unable to directly observe and oversee the attestation target. In this work, we present a system architecture design and prototype implementation that we claim enables trustworthy remote attestation. Furthermore, we formally model the system within a temporal logic embedded in the Coq theorem prover and present key theorems that strengthen this trust argument.

Recent years have seen tremendous developments in the field of computer vision and its extensive applications. The fundamental task, image classification, benefiting from deep convolutional neural networks (CNN)'s extraordinary ability to extract deep semantic information from input data, has become the backbone for many other computer vision tasks, like object detection and segmentation. A modern detection usually has bounding-box regression and class prediction with a pre-trained classification model as the backbone. The architecture is proven to produce good results, however, improvements can be made with closer inspections. A detector takes a pre-trained CNN from the classification task and selects the final bounding boxes from multiple proposed regional candidates by a process called non-maximum suppression (NMS), which picks the best candidates by ranking their classification confidence scores. The localization evaluation is absent in the entire process. Another issue is the classification uses one-hot encoding to label the ground truth, resulting in an equal penalty for misclassifications between any two classes without considering the inherent relations between the classes.

My research aims to address the following issues. (1) We proposed the first location-aware detection framework for single-shot detectors that can be integrated into any single-shot detectors. It boosts detection performance by calibrating the ranking process in NMS with localization scores. (2) To more effectively back-propagate gradients, we designed a super-class guided architecture that consists of a superclass branch (SCB) and a finer class branch (FCB). To further increase the effectiveness, the features from SCB with high-level information are fed to FCB to guide finer class predictions. (3) Recent works have shown 3D point cloud models are extremely vulnerable under adversarial attacks, which poses a serious threat to many critical applications like autonomous driving and robotic controls. To increase the robustness of CNN models on 3D point cloud models, we propose a family of robust structured declarative classifiers for point cloud classification, where the internal constrained optimization mechanism can effectively defend adversarial attacks through implicit gradients.

Intelligent Reflecting Surfaces (IRSs) grant the ability to control what was once considered the uncontrollable part of wireless communications, the channel. These smart signal mirrors show promise to significantly improve the effective signal-to-noise-ratio (SNR) of cell-users when the line-of-sight (LOS) channel between the base station (BS) and user is blocked. IRSs use implementable optimized phase shifts that beamform a reflected signal around channel blockages, and because they are passive devices, they have the benefit of having low cost and low power consumption. Previous works have concluded that IRSs need several hundred elements to outperform relays. Unfortunately, overhead and complexity costs related to optimizing these devices limit their scope to single-input single-output (SISO) systems. With multiple-input multiple-output (MIMO) and Massive MIMO becoming crucial components to modern 5G and beyond networks, a way to mitigate these overhead costs and integrate IRS technology with the promising MIMO techniques is paramount for these devices to have a place within modern cell technologies. This thesis proposes an IRS element grouping scheme that greatly reduces the number of unique IRS phases that need to be calculated and sent to the IRS controller via the limited rate feedback channel and allows for the ideal number of groups to be obtained at the BS before data transmission. Three methods are proposed to design the phase shifts and element partitioning within our scheme to improve effective SNR in an IRS-aided system. In our simulations, it is shown that our best performing method is one that dynamically partitions the IRS elements into non- uniform groups based on information gathered from the reflected channel and then optimizes its phase shifts. This method successfully handles the overhead trade-off problem, and shows significant achievable rate improvement from previous works.

Multichannel synthetic aperture radar (SAR) ice sounders rely on parametric angle estimators in tomography to resolve elevation angle beyond the Rayleigh resolution limit of their cross-track arrays. The potential super resolution capability of these techniques is predicated on perfect knowledge of the array’s response to directional sources, referred to as the array manifold. Array manifold calibration improves angle estimator performance by reducing the mismatch between the model of the array’s transfer function and truth; its study straddles the fields of both signal processing and antenna theory, yet associated literature reveals dichotomous methodologies that perpetuate fragmented interpretations of the manifold calibration problem. This dissertation addresses calibration for SAR ice sounders that three dimensionally image ice sheet and glacier beds with tomographic techniques. The approach is rooted in array signal processing first but seeks a more unifying perspective of the manifold calibration problem by leveraging commercial computational electromagnetics software to understand error mechanisms and algorithm performance with a deterministic model of an electromagnetic manifold. The research outlined here proposes creation of large snapshot databases that aid in identifying calibration targets in SAR pixels with known arrival angles. The signal processing methodology taxonomizes manifold calibration into parametric and nonparametric forms and advances both in the context of SAR sounders. A parametric estimator of nonlinear manifold parameters that are common across disjoint sets is derived. The algorithm framework capitalizes on a snapshot database to aggregate many angularly diverse observations in estimating unknown model parameters. The technique, which handles multitarget calibration, is desirable in the SAR sounder problem but requires a parametric model of the angle-dependent manifold. Nonparametric calibration techniques characterize the array response over the field of view but require many observations of single sources over dense calibration grids. A subspace clustering technique is proposed to identify snapshots with a single dominant source, thereby enabling a principal components-based characterization of the sounder manifold. The measured manifold leads to significant performance improvements over the traditional array response model in tomography. These results indicate that manifold calibration will reduce uncertainty in sounder-derived maps of the subsurface, leading to more accurate estimates of total fresh ice volume.

Over the last few years, one of the primary focuses in engineering development has been system packaging and miniaturization. This is apparent in various areas such as the rise of Internet of Things (IoT), CubeSats, and Unmanned Aerial Systems (UAS). The simultaneous miniaturization in multiple industries has enabled advancements in remote sensing instrument development. Sensors such as radars, lidars, and cameras are used on UAS to characterize various aspects of the Earth System like ice, soil, and vegetation, thereby improving our understanding. In this work, an Ultra-wideband (UWB) radar system design for the Vapor 55 UAS rotorcraft is investigated. A compact, lightweight 2 – 18 GHz Frequency Modulated Continuous Wave (FMCW) radar with two channels on transmit and receive is designed to characterize extended targets like soil and snow. This thesis reports initial proof-of-concept field measurements performed with soil as the target to identify backscatter signatures that are indicative of moisture content. The thesis also describes the exploratory design, development, and laboratory test results of the miniaturized radar electronics and compact antenna front-end.

In research there exists a need to constantly test and develop systems. Testing a radar system requires costly resources in terms of equipment and spectrum. These challenges relegate most testing to simulations, which are a poor approximation of reality. An alternative to over-the-air radar testing is presented here in the form of an over-the-air ultrasonic detection and ranging (SODAR) system. This system takes advantage of the similar wave-like propagation properties of acoustic and electromagnetic waves. With a SODAR testbed, radar waveform design can quickly move out of simulation and into the real world with minimal overhead. In this thesis, basic and advanced radar sensing techniques are demonstrated with a SODAR setup. Range detection, Doppler sensing, and pulse compression are shown as examples of basic radar concepts. For advanced sensing applications, array-based direction finding and synthetic aperture radar (SAR) are shown.

Crowd estimation is a vital component of crowd analysis. It finds many applications in real-world scenarios, e.g., huge gatherings management like Hajj, sporting and musical events, or political rallies. Automated crowd counting facilitates better and effective management of such events and consequently prevents any undesired situation. This is a very challenging problem in practice since there exists a significant difference in the crowd number in and across different images, varying image resolution, large perspective, severe occlusions, and dense crowd-like cluttered background regions. Current approaches do not handle huge crowd diversity well and thus perform poorly in cases ranging from extreme low to high crowd-density, thus, yielding huge crowd underestimation or overestimation. Also, manual crowd counting proves to be infeasible due to very slow and inaccurate results. To address these major crowd counting issues and challenges, we investigate two different types of input data: uni-modal (image) and multi-modal (image and audio). 

In the uni-modal setting, we propose and analyze four novel end-to-end crowd counting networks, ranging from multi-scale fusion-based models to uni-scale one-pass and two-pass multi-task networks. The multi-scale networks employ the attention mechanism to enhance the model efficacy. On the other hand, the uni-scale models are well-equipped with novel and simple-yet-effective patch re-scaling module (PRM) that functions identical but is more lightweight than multi-scale approaches. Experimental evaluation demonstrates that the proposed networks outperform the state-of-the-art in majority cases on four different benchmark datasets with up to 12.6% improvement for the RMSE evaluation metric. Better cross-dataset performance also validates the better generalization ability of our schemes. For the multi-modal input, effective feature-extraction (FE) and strong information fusion between two modalities remain a big challenge. Thus, the multi-modal novel network design focuses on investigating different features fusion techniques amid improving the FE. Based on the comprehensive experimental evaluation, the proposed multi-modal network increases the performance under all standard evaluation criteria with up to 33.8% improvement in comparison to the state-of-the-art. The application of multi-scale uni-modal attention networks also proves more effective in other deep learning domains, as demonstrated successfully on seven different scene-text recognition task datasets with better performance.

Catalysts are an essential and ubiquitous component of our modern life, from empowering our agriculture to reducing toxic emissions. There is a constant need for more and better catalysts.  The catalysis research literature is immense, growing, and scattered.   Natural Language Processing (NLP), a sub-field of Machine Learning (ML), offers a potential solution to automatically make full use of all this valuable information and speed innovation. Even though NLP has made much progress in the analysis of everyday text, its application in more technical text has not been as successful.  Specifically, there are even a dearth of tools that can appropriately extract text from the PDF files of research articles, which are the most common format used in the catalyst field. Therefore, this project aims to define a tool that can extract text out PDF files of catalysis science articles, which is prerequisite to applying NLP and ML tools.  We also explore the first stage of the NLP pipeline, tokenization, by objectively comparing different tokenizers for catalysis science articles.

Photo sharing and photo storage services like to have location data for each photo that is uploaded. With the location data, these services can build advanced features, such as automatic suggestion of relevant tags or automatic photo organization, which help provide a compelling user experience. Although a photo's location can often be obtained by looking at the photo's metadata, many photos uploaded to these services will not have location metadata available. This can happen when, for example, the camera capturing the picture does not have GPS or if a photo's metadata is scrubbed due to privacy concerns.

If no location metadata for an image is available, one way to infer the location is to detect and classify a discernible landmark in the image.  Given the large number of landmarks across the world and the immense volume of images that are uploaded to photo sharing services, using human judgement to classify these landmarks would not be feasible. In this project, we aim to address this problem by building models to automatically predict the location of the image based on any landmarks depicted in the image. We will go through the machine learning design process end-to-end: performing data preprocessing, designing and training CNNs, comparing the accuracy of different CNNs, and using some own images to heuristically evaluate the best CNN.