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. ; ; (, 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
  4. (, 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
  5. ; ; ; ; ; ; ; ; ; ; et al (, Genome Research)
    The epithelial and interstitial stem cells of the freshwater polyp Hydra are the best-characterized stem cell systems in any cnidarian, providing valuable insight into cell type evolution and the origin of stemness in animals. However, little is known about the transcriptional regulatory mechanisms that determine how these stem cells are maintained and how they give rise to their diverse differentiated progeny. To address such questions, a thorough understanding of transcriptional regulation in Hydra is needed. To this end, we generated extensive new resources for characterizing transcriptional regulation in Hydra , including new genome assemblies for Hydra oligactis and the AEP strain of Hydra vulgaris , an updated whole-animal single-cell RNA-seq atlas, and genome-wide maps of chromatin interactions, chromatin accessibility, sequence conservation, and histone modifications. These data revealed the existence of large kilobase-scale chromatin interaction domains in the Hydra genome that contain transcriptionally coregulated genes. We also uncovered the transcriptomic profiles of two previously molecularly uncharacterized cell types: isorhiza-type nematocytes and somatic gonad ectoderm. Finally, we identified novel candidate regulators of cell type–specific transcription, several of which have likely been conserved at least since the divergence of Hydra and the jellyfish Clytia hemisphaerica more than 400 million years ago. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email