Engineering Commons^™

Panoramas From Photons, Sacha Jungerman, Atul Ingle, Mohit Gupta

Computer Science Faculty Publications and Presentations

Scene reconstruction in the presence of high-speed motion and low illumination is important in many applications such as augmented and virtual reality, drone navigation, and autonomous robotics. Traditional motion estimation techniques fail in such conditions, suffering from too much blur in the presence of high-speed motion and strong noise in low-light conditions. Single-photon cameras have recently emerged as a promising technology capable of capturing hundreds of thousands of photon frames per second thanks to their high speed and extreme sensitivity. Unfortunately, traditional computer vision techniques are not well suited for dealing with the binary-valued photon data captured by these cameras …

Learned Compressive Representations For Single-Photon 3d Imaging, Felipe Gutierrez-Barragan, Fangzhou Mu, Andrei Ardelean, Atul Ingle, Claudio Bruschini, Edoardo Charbon, Yin Li, Mohit Gupta, Andreas Velten

Computer Science Faculty Publications and Presentations

Single-photon 3D cameras can record the time-of-arrival of billions of photons per second with picosecond accuracy. One common approach to summarize the photon data stream is to build a per-pixel timestamp histogram, resulting in a 3D histogram tensor that encodes distances along the time axis. As the spatio-temporal resolution of the histogram tensor increases, the in-pixel memory requirements and output data rates can quickly become impractical. To overcome this limitation, we propose a family of linear compressive representations of histogram tensors that can be computed efficiently, in an online fashion, as a matrix operation. We design practical lightweight compressive representations …

Sequential Frame-Interpolation And Dct-Based Video Compression Framework, Yeganeh Jalalpour, Wu-Chi Feng, Feng Liu

Computer Science Faculty Publications and Presentations

Video data is ubiquitous; capturing, transferring, and storing even compressed video data is challenging because it requires substantial resources. With the large amount of video traffic being transmitted on the internet, any improvement in compressing such data, even small, can drastically impact resource consumption. In this paper, we present a hybrid video compression framework that unites the advantages of both DCT-based and interpolation-based video compression methods in a single framework. We show that our work can deliver the same visual quality or, in some cases, improve visual quality while reducing the bandwidth by 10--20%.

The Db Community Vis-À-Vis Environmental, Health, And Societal Grand Challenges: Innovation Engine, Plumber, Or Bystander?, Anastasia Ailamaki, Leilani Battle, Johannes Gehrke, Masaru Kitsuregawa, David Maier, Christopher Re, Meihui Zhang, Magdalena Balazinska

Computer Science Faculty Publications and Presentations

This panel considers the role of the database research community in addressing humanity's greatest challenges. Are we an innovation engine, tool providers, or are we standing on the side while other research communities take the lead?

Concolic Execution Of Nmap Scripts For Honeyfarm Generation, Zhe Li, Bo Chen, Wu-Chang Feng, Fei Xie

Computer Science Faculty Publications and Presentations

Attackers rely upon a vast array of tools for automating attacksagainst vulnerable servers and services. It is often the case thatwhen vulnerabilities are disclosed, scripts for detecting and exploit-ing them in tools such asNmapandMetasploitare released soonafter, leading to the immediate identification and compromise ofvulnerable systems. Honeypots, honeynets, tarpits, and other decep-tive techniques can be used to slow attackers down, however, such approaches have difficulty keeping up with the sheer number of vulnerabilities being discovered and attacking scripts that are being released. To address this issue, this paper describes an approach for applying concolic execution on attacking scripts in Nmap in …

An Automated Ar-Based Annotation Tool For Indoor Navigation For Visually Impaired People, Pei Du, Nirupama Bulusu

Computer Science Faculty Publications and Presentations

Low vision people face many daily encumbrances. Traditional visual enhancements do not suffice to navigate indoor environments, or recognize objects efficiently. In this paper, we explore how Augmented Reality (AR) can be leveraged to design mobile applications to improve visual experience and unburden low vision persons. Specifically, we propose a novel automated AR-based annotation tool for detecting and labeling salient objects for assisted indoor navigation applications like NearbyExplorer. NearbyExplorer, which issues audio descriptions of nearby objects to the users, relies on a database populated by large teams of volunteers and map-a-thons to manually annotate salient objects in the environment like …

Towards Adaptive, Self-Configuring Networked Unmanned Aerial Vehicles, Nirupama Bulusu, Ehsan Aryafar, Feng Liu

Computer Science Faculty Publications and Presentations

Networked drones have the potential to transform various applications domains; yet their adoption particularly in indoor and forest environments has been stymied by the lack of accurate maps and autonomous navigation abilities in the absence of GPS, the lack of highly reliable, energy-efficient wireless communications, and the challenges of visually inferring and understanding an environment with resource-limited individual drones. We advocate a novel vision for the research community in the development of distributed, localized algorithms that enable the networked drones to dynamically coordinate to perform adaptive beam forming to achieve high capacity directional aerial communications, and collaborative machine learning to …

On The (Im)Practicality Of Adversarial Perturbation For Image Privacy, Arezoo Rajabi, Rakesh B. Bobba, Mike Rosulek, Charles Wright, Wu-Chi Feng

Computer Science Faculty Publications and Presentations

Image hosting platforms are a popular way to store and share images with family members and friends. However, such platforms typically have full access to images raising privacy concerns. These concerns are further exacerbated with the advent of Convolutional Neural Networks (CNNs) that can be trained on available images to automatically detect and recognize faces with high accuracy.

Recently, adversarial perturbations have been proposed as a potential defense against automated recognition and classification of images by CNNs. In this paper, we explore the practicality of adversarial perturbation based approaches as a privacy defense against automated face recognition. Specifically, we first …

Applying The Principle Of Least Privilege To System Management Interrupt Handlers With The Intel Smi Transfer Monitor, Brian Delgado, Tejaswini Vibhute, Karen L. Karavanic

Computer Science Faculty Publications and Presentations

Recent years have seen a growing concern over System Management Mode (SMM) and its broad access to platform resources. The SMI Transfer Monitor (STM) is Intel’s most powerful executing CPU context. The STM is a firmware-based hypervisor that applies the principle of least privilege to powerful System Management Interrupt (SMI) handlers that control runtime firmware. These handlers have traditionally had full access to memory as well as the register state of applications and kernel code even when their functionality did not require it. The STM has been been enabled for UEFI and, most recently, coreboot firmware, adding protection against runtime …

No-Reference Image Denoising Quality Assessment, Si Lu

Computer Science Faculty Publications and Presentations

A wide variety of image denoising methods are available now. However, the performance of a denoising algorithm often depends on individual input noisy images as well as its parameter setting. In this paper, we present a noreference image denoising quality assessment method that can be used to select for an input noisy image the right denoising algorithm with the optimal parameter setting. This is a challenging task as no ground truth is available. This paper presents a data-driven approach to learn to predict image denoising quality. Our method is based on the observation that while individual existing quality metrics and …

Good Similar Patches For Image Denoising (Poster), Si Lu

Computer Science Faculty Publications and Presentations

Patch-based denoising algorithms like BM3D have achieved outstanding performance. An important idea for the success of these methods is to exploit the recurrence of similar patches in an input image to estimate the underlying image structures....

Video Frame Interpolation Via Adaptive Separable Convolution, Simon Niklaus, Long Mai, Feng Liu

Computer Science Faculty Publications and Presentations

Standard video frame interpolation methods first estimate optical flow between input frames and then synthesize an intermediate frame guided by motion. Recent approaches merge these two steps into a single convolution process by convolving input frames with spatially adaptive kernels that account for motion and re-sampling simultaneously. These methods require large kernels to handle large motion, which limits the number of pixels whose kernels can be estimated at once due to the large memory demand. To address this problem, this paper formulates frame interpolation as local separable convolution over input frames using pairs of 1D kernels. Compared to regular 2D …

Fast On-Line Kernel Density Estimation For Active Object Localization, Anthony D. Rhodes, Max H. Quinn, Melanie Mitchell

Computer Science Faculty Publications and Presentations

A major goal of computer vision is to enable computers to interpret visual situations—abstract concepts (e.g., “a person walking a dog,” “a crowd waiting for a bus,” “a picnic”) whose image instantiations are linked more by their common spatial and semantic structure than by low-level visual similarity. In this paper, we propose a novel method for prior learning and active object localization for this kind of knowledge-driven search in static images. In our system, prior situation knowledge is captured by a set of flexible, kernel-based density estimations— a situation model—that represent the expected spatial structure of the given situation. These …

Sparse Coding On Stereo Video For Object Detection, Sheng Y. Lundquist, Melanie Mitchell, Garrett T. Kenyon

Computer Science Faculty Publications and Presentations

Deep Convolutional Neural Networks (DCNN) require millions of labeled training examples for image classification and object detection tasks, which restrict these models to domains where such a dataset is available. We explore the use of unsupervised sparse coding applied to stereo-video data to help alleviate the need for large amounts of labeled data. In this paper, we show that unsupervised sparse coding is able to learn disparity and motion sensitive basis functions when exposed to unlabeled stereo-video data. Additionally, we show that a DCNN that incorporates unsupervised learning exhibits better performance than fully supervised networks. Furthermore, finding a sparse representation …

Video Frame Interpolation Via Adaptive Convolution, Simon Niklaus, Long Mai, Feng Liu

Computer Science Faculty Publications and Presentations

Video frame interpolation typically involves two steps: motion estimation and pixel synthesis. Such a two-step approach heavily depends on the quality of motion estimation. This paper presents a robust video frame interpolation method that combines these two steps into a single process. Specifically, our method considers pixel synthesis for the interpolated frame as local convolution over two input frames. The convolution kernel captures both the local motion between the input frames and the coefficients for pixel synthesis. Our method employs a deep fully convolu- tional neural network to estimate a spatially-adaptive con- volution kernel for each pixel. This deep neural …

Bayesian Optimization For Refining Object Proposals, Anthony D. Rhodes, Jordan Witte, Melanie Mitchell, Bruno Jedynak

Computer Science Faculty Publications and Presentations

We develop a general-purpose algorithm using a Bayesian optimization framework for the efficient refinement of object proposals. While recent research has achieved substantial progress for object localization and related objectives in computer vision, current state-of-the-art object localization procedures are nevertheless encumbered by inefficiency and inaccuracy. We present a novel, computationally efficient method for refining inaccurate bounding-box proposals for a target object using Bayesian optimization. Offline, image features from a convolutional neural network are used to train a model to predict an object proposal’s offset distance from a target object. Online, this model is used in a Bayesian active search to …

Proving Non-Deterministic Computations In Agda, Sergio Antoy, Michael Hanus, Steven Libby

Computer Science Faculty Publications and Presentations

We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. The first approach eliminates non-determinism by considering the set of all non-deterministic values produced by an application. The second approach encodes every non-deterministic choice that the application could perform. We consider our initial experiment a success. Although proving properties of programs is a notoriously difficult task, the functional logic …

Incorporating Priors For Medical Image Segmentation Using A Genetic Algorithm, Payel Ghosh, Melanie Mitchell, James A. Tanyi, Arthur Y. Hung

Computer Science Faculty Publications and Presentations

Medical image segmentation is typically performed manually by a physician to delineate gross tumor volumes for treatment planning and diagnosis. Manual segmentation is performed by medical experts using prior knowledge of organ shapes and locations but is prone to reader subjectivity and inconsistency. Automating the process is challenging due to poor tissue contrast and ill-defined organ/tissue boundaries in medical images. This paper presents a genetic algorithm for combining representations of learned information such as known shapes, regional properties and relative position of objects into a single framework to perform automated three-dimensional segmentation. The algorithm has been tested for prostate segmentation …

Sparse Encoding Of Binocular Images For Depth Inference, Sheng Y. Lundquist, Dylan M. Paiton, Peter F. Schultz, Garrett T. Kenyon

Computer Science Faculty Publications and Presentations

Sparse coding models have been widely used to decompose monocular images into linear combinations of small numbers of basis vectors drawn from an overcomplete set. However, little work has examined sparse coding in the context of stereopsis. In this paper, we demonstrate that sparse coding facilitates better depth inference with sparse activations than comparable feed-forward networks of the same size. This is likely due to the noise and redundancy of feed-forward activations, whereas sparse coding utilizes lateral competition to selectively encode image features within a narrow band of depths.

A Verified Information-Flow Architecture, Arthur Azevedo De Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach

Computer Science Faculty Publications and Presentations

SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE and an end-to-end proof of noninterference for this model. We …

From Boolean Equalities To Constraints, Sergio Antoy, Michael Hanus

Computer Science Faculty Publications and Presentations

Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction …

A Constraint Language For Static Semantic Analysis Based On Scope Graphs, Hendrik Van Antwerpen, Pierre Néron, Andrew Tolmach, Eelco Visser, Guido Wachsmuth

Computer Science Faculty Publications and Presentations

In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs—such as record field access—for which binding and typing are mutually dependent.We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for …

A Scaffolded, Metamorphic Ctf For Reverse Engineering, Wu-Chang Feng

Computer Science Faculty Publications and Presentations

Hands-on Capture-the-Flag (CTF) challenges tap into and cultivate the intrinsic motivation within people to solve puzzles, much in the same way Sudoku and crossword puzzles do. While the format has been successful in security competitions, there have been a limited number of attempts to integrate them into a classroom environment. This paper describes MetaCTF, a metamorphic set of CTF challenges for teaching reverse code engineering. MetaCTF is 1) scaffolded in a way that allows students to make incremental progress, 2) integrated with the course material so that students can immediately apply knowledge gained in class, 3) polymorphic and metamorphic so …

Compiling Collapsing Rules In Certain Constructor Systems, Sergio Antoy, Andy Jost

Computer Science Faculty Publications and Presentations

The implementation of functional logic languages by means of graph rewriting requires a special handling of collapsing rules. Recent advances about the notion of a needed step in some constructor systems offer a new approach to this problem. We present two results: a transformation of a certain class of constructor-based rewrite systems that eliminates collapsing rules, and a rewrite-like relation that takes advantage of the absence of collapsing rules. We formally state and prove the correctness of these results. When used together, these results simplify without any loss of efficiency an implementation of graph rewriting and consequently of functional logic …

Automatic Fault Injection For Driver Robustness Testing, Kai Cong, Li Lei, Zhenkun Yang, Fei Xie

Computer Science Faculty Publications and Presentations

Robustness testing is a crucial stage in the device driver development cycle. To accelerate driver robustness testing, effective fault scenarios need to be generated and injected without requiring much time and human effort. In this pa- per, we present a practical approach to automatic runtime generation and injection of fault scenarios for driver robust- ness testing. We identify target functions that can fail from runtime execution traces, generate effective fault scenarios on these target functions using a bounded trace-based it- erative strategy, and inject the generated fault scenarios at runtime to test driver robustness using a permutation-based injection mechanism. We …

Naturalized Communication And Testing, Marly Roncken, Swetha Mettala Gilla, Hoon Park, Navaneeth Prasannakumar Jamadagni, Christopher Cowan, Ivan Sutherland

Computer Science Faculty Publications and Presentations

We ”naturalize” the handshake communication links of a self-timed system by assigning the capabilities of filling and draining a link and of storing its full or empty status to the link itself. This contrasts with assigning these capabilities to the joints, the modules connected by the links, as was previously done. Under naturalized communication, the differences between Micropipeline, GasP, Mousetrap, and Click circuits are seen only in the links — the joints become identical; past, present, and future link and joint designs become interchangeable. We also “naturalize” the actions of a self-timed system, giving actions status equal to states — …

Micro-Policies: Formally Verified, Tag-Based Security Monitors, Arthur Azevedo De Amorim, Maxime Denes, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach

Computer Science Faculty Publications and Presentations

Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level “symbolic machine,” and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy’s rules embodies a high-level …

Static Conflict Detection For A Policy Language, Alix Trou, Robert Dockins, Andrew Tolmach

Computer Science Faculty Publications and Presentations

We present a static control flow analysis used in the Simple Unified Policy Programming Language (SUPPL) compiler to detect internally inconsistent policies. For example, an access control policy can decide to both “allow” and “deny” access for a user; such an inconsistency is called a conflict. Policies in Suppl. follow the Event-Condition-Action paradigm; predicates are used to model conditions and event handlers are written in an imperative way. The analysis is twofold; it first computes a superset of all conflicts by looking for a combination of actions in the event handlers that might violate a user-supplied definition of conflicts. SMT …

Desiderata For A Big Data Language, David Maier

Computer Science Faculty Publications and Presentations

Data management and analytics systems for big data have proliferated, including column stores, array databases, graphanalysis environments and linear-algebra packages. This burgeoning of systems has lead to a surfeit of language and APIs. It is time to consider a new framework that can span these systems and simplify the programming and maintenance of Big Data applications. There are two key goals for such a framework:

Portability: It should be relatively easy to move an application or tool developed on one platform to operate against another. As a corollary, back-end data and analytics services should be swappable in a particular …

Needed Computations Shortcutting Needed Steps, Sergio Antoy, Jacob Johannsen, Steven Libby

Computer Science Faculty Publications and Presentations

We define a compilation scheme for a constructor-based, strongly-sequential, graph rewriting system which shortcuts some needed steps. The object code is another constructor-based graph rewriting system. This system is normalizing for the original system when using an innermost strategy. Consequently, the object code can be easily implemented by eager functions in a variety of programming languages. We modify this object code in a way that avoids total or partial construction of the contracta of some needed steps of a computation. When computing normal forms in this way, both memory consumption and execution time are reduced compared to ordinary rewriting computations …