skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Hydra: Effective Runtime Network Verification
It is notoriously difficult to verify that a network is behaving as intended, especially at scale. This paper presents Hydra, a system that uses ideas from runtime verification to check that every packet is correctly processed with respect to a specification in real time. We propose a domain-specific language for writing properties, called Indus, and we develop a compiler that turns properties thus specified into executable P4 code that runs alongside the forwarding code at line rate. To evaluate our approach, we used Indus to model a range of properties, showing that it is expressive enough to capture examples studied in prior work. We also deployed Hydra checkers for validating paths in source routing and for enforcing slice isolation in Aether, an open-source cellular platform. We confirmed a subtle bug in Aether's 5G mobile core that would have been hard to detect using static techniques. We also evaluated the overheads of Hydra on hardware, finding that it does not significantly increase latency and often does not require additional pipeline stages.  more » « less
Award ID(s):
1918396
PAR ID:
10467227
Author(s) / Creator(s):
; ; ; ; ; ; ; ;
Publisher / Repository:
ACM
Date Published:
ISBN:
9798400702365
Page Range / eLocation ID:
182 to 194
Subject(s) / Keyword(s):
Programmable networks, runtime verification, P4.
Format(s):
Medium: X
Location:
New York NY USA
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; (, 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE))
    null (Ed.)
    We propose HYDRA-C, a design-time evaluation framework for integrating monitoring mechanisms in multicore real-time systems (RTS). Our goal is to ensure that security (or other monitoring) mechanisms execute in a "continuous" manner - i.e., as often as possible, across cores. This is to ensure that any such mechanisms run with few interruptions, if any. HYDRA-C is intended to allow designers of RTS to integrate monitoring mechanisms without perturbing existing timing properties or execution orders. We demonstrate the framework using a proofof-concept implementation with intrusion detection mechanisms as security tasks. We develop and use both, (a) a custom intrusion detection system (IDS) as well as (b) Tripwire - an open source data integrity checking tool. We compare the performance of HYDRA-C with a state-of-the-art multicore RT security integration approach and find that our method does not impact the schedulability and, on average, can detect intrusions 19.05% faster without impacting the performance of RT tasks. 
    more » « less
  2. ; ; ; ; (, Frontiers in Earth Science)
    Pakistan is the most glaciated country on the planet but faces increasing water scarcity due to the vulnerability of its primary water source, the Indus River, to changes in climate and demand. Glacier melt constitutes over one-third of the Indus River’s discharge, but the impacts of glacier shrinkage from anthropogenic climate change are not equal across all eleven subbasins of the Upper Indus. We present an exploration of glacier melt contribution to Indus River flow at the subbasin scale using a distributed surface energy and mass balance model run 2001–2013 and calibrated with geodetic mass balance data. We find that the northern subbasins, the three in the Karakoram Range, contribute more glacier meltwater than the other basins combined. While glacier melt discharge tends to be large where there are more glaciers, our modeling study reveals that glacier melt does not scale directly with glaciated area. The largest volume of glacier melt comes from the Gilgit/Hunza subbasin, whose glaciers are at lower elevations than the other Karakoram subbasins. Regional application of the model allows an assessment of the dominant drivers of melt and their spatial distributions. Melt energy in the Nubra/Shyok and neighboring Zaskar subbasins is dominated by radiative fluxes, while turbulent fluxes dominate the melt signal in the west and south. This study provides a theoretical exploration of the spatial patterns to glacier melt in the Upper Indus Basin, a critical foundation for understanding when glaciers melt, information that can inform projections of water supply and scarcity in Pakistan. 
    more » « less
  3. ; (, Proceedings of the ACM on Programming Languages)
    Optimizing compilers rely on peephole optimizations to simplify combinations of instructions and remove redundant instructions. Typically, a new peephole optimization is added when a compiler developer notices an optimization opportunity---a collection of dependent instructions that can be improved---and manually derives a more general rewrite rule that optimizes not only the original code, but also other, similar collections of instructions. In this paper, we present Hydra, a tool that automates the process of generalizing peephole optimizations using a collection of techniques centered on program synthesis. One of the most important problems we have solved is finding a version of each optimization that is independent of the bitwidths of the optimization's inputs (when this version exists). We show that Hydra can generalize 75% of the ungeneralized missed peephole optimizations that LLVM developers have posted to the LLVM project's issue tracker. All of Hydra's generalized peephole optimizations have been formally verified, and furthermore we can automatically turn them into C++ code that is suitable for inclusion in an LLVM pass. 
    more » « less
  4. ; ; (, ICSE '20: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Companion Proceedings)
    null (Ed.)
    Recent research in empirical software engineering is applying techniques from neurocognitive science and breaking new grounds in the ways that researchers can model and analyze the cognitive processes of developers as they interact with software artifacts. However, given the novelty of this line of research, only one tool exists to help researchers represent and analyze this kind of multi-modal biometric data. While this tool does help with visualizing temporal eyetracking and physiological data, it does not allow for the mapping of physiological data to source code elements, instead projecting information over images of code. One drawback of this is that researchers are still unable to meaningfully combine and map physiological and eye tracking data to source code artifacts. The use of images also bars the support of long or multiple code files, which prevents researchers from analyzing data from experiments conducted in realistic settings. To address these drawbacks, we propose VITALSE, a tool for the interactive visualization of combined multi-modal biometric data for software engineering tasks. VITALSE provides interactive and customizable temporal heatmaps created with synchronized eyetracking and biometric data. The tool supports analysis on multiple files, user defined annotations for points of interest over source code elements, and high level customizable metric summaries for the provided dataset. VITALSE, a video demonstration, and sample data to demonstrate its capabilities can be found at http://www.vitalse.app. 
    more » « less
  5. (, IEEE)
    Feature-rich software programs typically provide many configuration options for users to enable and disable features, or tune feature behaviors. Given the values of configuration options, certain code blocks in a program will become redundant code and never be used. However, the redundant code is still present in the program and thus unnecessarily increases a program's attack surface by allowing attackers to use it as return-oriented programming (ROP) gadgets. Existing code debloating techniques have several limitations: not targeting this type of redundant code, requiring access to program source code or user-provided test inputs. In this paper, we propose a practical code debloating approach, called BinDebloat, to address these limitations. BinDebloat identifies and removes redundant code caused by configuration option values. It does not require user-provided test inputs, or support from program developers, and is designed to work on closed-source programs. It uses static program analysis to identify code blocks that are control-dependent on configuration option values. Given a set of configuration option values, it automatically determines which of such code blocks become redundant and uses static binary rewriting to neutralize these code blocks so that they are removed from the attack surface. We evaluated BinDebloat on closed-source Windows programs and the results show that BinDebloat can effectively reduce a program's attack surface. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email