arXiv subjects

Daniel Wagner

Publications and source records attributed to Daniel Wagner.

7 recordsLinked to original sources

arXiv2024

Macaw: A Machine Code Toolbox for the Busy Binary Analyst

When attempting to understand the behavior of an executable, a binary analyst can make use of many different techniques. These include program slicing, dynamic instrumentation, binary-level rewriting, symbolic execution, and formal verification, all of which can uncover insights into how a piece of machine code behaves. As a result, there is no one-size-fits-all binary analysis tool, so a binary analysis researcher will often combine several different tools. Sometimes, a researcher will even need to design new tools to study problems that existing frameworks are not well equipped to handle. Designing such tools from complete scratch is rarely time- or cost-effective, however, given the scale and complexity of modern ISAs. We present Macaw, a modular framework that makes it possible to rapidly build reliable binary analysis tools across a range of use cases. Statically typed functional programming techniques are used pervasively throughout Macaw -- these range from using functional optimization passes to encoding tricky architectural invariants at the type level to statically check correctness properties. The level of assurance that functional programming ideas afford us allow us to iterate rapidly on Macaw while still having confidence that the underlying semantics are correct. Over a decade of development, we have used Macaw to support an industrial research team in building tools for machine code-related tasks. As such, the name 'Macaw' refers not just to the framework, but also a suite of tools that are built on top of it. We describe Macaw in depth and describe the different static and dynamic analyses that it performs, many powered by an SMT-based symbolic execution engine. We put a particular focus on interoperability between machine code and higher-level languages, including binary lifting from x86 to LLVM, as well verifying the correctness of mixed C and assembly code.

cs.PL↗

arXiv2022

Coherence of Rabi oscillations with spin exchange

Rabi measurements in atomic vapor cells are of current interest in a range of microwave imaging and sensing experiments, but are increasingly in a parameter space outside of theoretical studies of coherence defined by spin-exchange collisions. Here, we study the coherence of Rabi oscillations in vapor cells by employing continuous non-destructive readout of the hyperfine manifold of $^{87}$Rb using Faraday rotation. We develop a full model for spin-exchange (SE) coherence for hyperfine transitions that takes into account a non-static population distribution. In this regime, Rabi oscillations exhibit nontrivial time-domain signals that allow verification of vapor-cell parameters. We find excellent agreement between theory and experiment, which will aid in benchmarking sensitivities of Rabi measurement applications.

physics.atom-ph↗

arXiv2022

BASALISC: Programmable Hardware Accelerator for BGV Fully Homomorphic Encryption

Fully Homomorphic Encryption (FHE) allows for secure computation on encrypted data. Unfortunately, huge memory size, computational cost and bandwidth requirements limit its practicality. We present BASALISC, an architecture family of hardware accelerators that aims to substantially accelerate FHE computations in the cloud. BASALISC is the first to implement the BGV scheme with fully-packed bootstrapping -- the noise removal capability necessary for arbitrary-depth computation. It supports a customized version of bootstrapping that can be instantiated with hardware multipliers optimized for area and power. BASALISC is a three-abstraction-layer RISC architecture, designed for a 1 GHz ASIC implementation and underway toward 150mm2 die tape-out in a 12nm GF process. BASALISC's four-layer memory hierarchy includes a two-dimensional conflict-free inner memory layer that enables 32 Tb/s radix-256 NTT computations without pipeline stalls. Its conflict-resolution permutation hardware is generalized and re-used to compute BGV automorphisms without throughput penalty. BASALISC also has a custom multiply-accumulate unit to accelerate BGV key switching. The BASALISC toolchain comprises a custom compiler and a joint performance and correctness simulator. To evaluate BASALISC, we study its physical realizability, emulate and formally verify its core functional units, and we study its performance on a set of benchmarks. Simulation results show a speedup of more than 5,000 times over HElib -- a popular software FHE library.

cs.CR↗

arXiv2020

The Lockdown Effect: Implications of the COVID-19 Pandemic on Internet Traffic

Due to the COVID-19 pandemic, many governments imposed lock downs that forced hundreds of millions of citizens to stay at home. The implementation of confinement measures increased Internet traffic demands of residential users, in particular, for remote working, entertainment, commerce, and education, which, as a result, caused traffic shifts in the Internet core. In this paper, using data from a diverse set of vantage points (one ISP, three IXPs, and one metropolitan educational network), we examine the effect of these lockdowns on traffic shifts. We find that the traffic volume increased by 15-20% almost within a week--while overall still modest, this constitutes a large increase within this short time period. However, despite this surge, we observe that the Internet infrastructure is able to handle the new volume, as most traffic shifts occur outside of traditional peak hours. When looking directly at the traffic sources, it turns out that, while hypergiants still contribute a significant fraction of traffic, we see (1) a higher increase in traffic of non-hypergiants, and (2) traffic increases in applications that people use when at home, such as Web conferencing, VPN, and gaming. While many networks see increased traffic demands, in particular, those providing services to residential users, academic networks experience major overall decreases. Yet, in these networks, we can observe substantial increases when considering applications associated to remote working and lecturing.

cs.NI↗

arXiv2020

Measures and LMIs for Adaptive Control Validation

Occupation measures and linear matrix inequality (LMI) relax-ations (called the moment sums of squares or Lasserre hierarchy) have been used previously as a means for solving control law verification and validation (VV) problems. However, these methods have been restricted to relatively simple control laws and a limited number of states. In this document, we extend these methods to model reference adaptive control (MRAC) configurations typical of the aircraft industry. The main contribution is a validation scheme that exploits the specific nonlinearities and structure of MRAC. A nonlinear F-16 plant is used for illustration. LMI relaxations solved by off-the-shelf-software are compared to traditional Monte-Carlo simulations.

eess.SY↗

arXiv2020

Measures and LMIs for Lateral F-16 MRAC Validation

Occupation measures and linear matrix inequality (LMI) relax-ations (called the moment sums of squares or Lasserre hierarchy) are state-of-the-art methods for verification and validation (VV) in aerospace. In this document, we extend these results to a full F-16 closed-loop nonlinear dutch roll polynomial model complete with model reference adaptive control (MRAC). This is done through a new technique of approximating the reference trajectory by exploiting sparse ordinary differential equations (ODEs) with parsimony. The VV problem is then solved directly using moment LMI relaxations and off-the-shelf-software. The main results are then compared to their numerical counterparts obtained using traditional Monte-Carlo simulations.

eess.SY↗

arXiv2015

The History of Mobile Augmented Reality

This document summarizes the major milestones in mobile Augmented Reality between 1968 and 2014. Major parts of the list were compiled by the member of the Christian Doppler Laboratory for Handheld Augmented Reality in 2010 (author list in alphabetical order) for the ISMAR society. Later in 2013 it was updated, and more recent work was added during preparation of this report. Permission is granted to copy and modify.

cs.HC↗