arXiv subjects

Daniel Engel

Publications and source records attributed to Daniel Engel.

6 recordsLinked to original sources

arXiv2026

Adding Compilation Metadata To Binaries To Make Disassembly Decidable

The binary executable format is the standard method for distributing and executing software. Yet, it is also as opaque a representation of software as can be. If the binary format were augmented with metadata that provides security-relevant information, such as which data is intended by the compiler to be executable instructions, or how memory regions are expected to be bounded, that would dramatically improve the safety and maintainability of software. In this paper, we propose a binary format that is a middle ground between a stripped black-box binary and open source. We provide a tool that generates metadata capturing the compiler's intent and inserts it into the binary. This metadata enables lifting to a correct and recompilable higher-level representation and makes analysis and instrumentation more reliable. Our evaluation shows that adding metadata does not affect runtime behavior or performance. Compared to DWARF, our metadata is roughly 17% of its size. We validate correctness by compiling a comprehensive set of real-world C and C++ binaries and demonstrating that they can be lifted, instrumented, and recompiled without altering their behavior.

cs.CR↗

arXiv2025

Formally Verified Binary-level Pointer Analysis

Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the result is trustworthy, i.e., it can be formally established that the pointer designations are overapproximative. This paper presents an approach to formally proven correct binary-level pointer analysis. A salient property of our approach is that it first generically considers what proof obligations a generic abstract domain for pointer analysis must satisfy. This allows easy instantiation of different domains, varying in precision, while preserving the correctness of the analysis. In the trade-off between scalability and precision, such customization allows "meaningful" precision (sufficiently precise to ensure basic sanity properties, such as that relevant parts of the stack frame are not overwritten during function execution) while also allowing coarse analysis when pointer computations have become too obfuscated during compilation for sound and accurate bounds analysis. We experiment with three different abstract domains with high, medium, and low precision. Evaluation shows that our approach is able to derive designations for memory writes soundly in COTS binaries, in a context-sensitive interprocedural fashion.

cs.SE↗

arXiv2022

Transferable Cross-Chain Options

An option is a financial agreement between two parties to trade two assets. One party is given the right, but not the obligation, to complete the swap before a specified termination time. In todays financial markets, an option is considered an asset which can itself be transferred: while an option is active, one party can sell its rights (or obligations) to another. Todays blockchains support simple options in the form of cross-chain atomic swap protocols where one party has the choice whether to complete the swap. The options implemented by these cross-chain protocols, are not, however, transferable. This paper proposes novel distributed protocols for transferable cross-chain options, where both option owners and providers can sell their positions to third parties. The protocol ensures that none of the parties can be cheated, that no unauthorized party can interfere, and that the transfer succeeds if the buyer and seller faithfully follow the protocol.

cs.CR↗

arXiv2021

Presentation and Publication: Loss and Slippage in Networks of Automated Market Makers

Automated market makers (AMMs) are smart contracts that automatically trade electronic assets according to a mathematical formula. This paper investigates how an AMM's formula affects the interests of liquidity providers, who endow the AMM with assets, and traders, who exchange one asset for another at the AMM's rates. *Linear slippage* measures how a trade's size affects the trader's return, *angular slippage* measures how a trade's size affects the subsequent market price, *divergence loss* measures the opportunity cost of providers' investments, and *load* balances the costs to traders and providers. We give formal definitions for these costs, show that they obey certain conservation laws: these costs can be shifted around but never fully eliminated. We analyze how these costs behave under *composition*, when simple individual AMMs are linked to form more complex networks of AMMs.

cs.OH↗

arXiv2021

Invited Paper: Failure is (literally) an Option: Atomic Commitment vs Optionality in Decentralized Finance

Many aspects of blockchain-based decentralized finance can be understood as an extension of classical distributed computing. In this paper, we trace the evolution of two interrelated notions: failure and fault-tolerance. In classical distributed computing, a failure to complete a multi-party protocol is typically attributed to hardware malfunctions. A fault-tolerant protocol is one that responds to such failures by rolling the system back to an earlier consistent state. In the presence of Byzantine failures, a failure may be the result of an attack, and a fault-tolerant protocol is one that ensures that attackers will be punished and victims compensated. In modern decentralized finance however, failure to complete a protocol can be considered a legitimate option, not a transgression. A fault-tolerant protocol is one that ensures that the party offering the option cannot renege, and the party purchasing the option provides fair compensation (in the form of a fee) to the offering party. We sketch the evolution of such protocols, starting with two-phase commit, and finishing with timed hashlocked smart contracts.

cs.DC↗

arXiv2021

Composing Networks of Automated Market Makers

Automated market makers (AMMs) are automata that trade electronic assets at rates set by mathematical formulas. AMMs are usually implemented by smart contracts on blockchains. In practice, AMMs are often composed: and outputs from AMMs can be directed into other compatible AMMs. This paper proposes a mathematical model for AMM composition. We define sequential and parallel composition operators for AMMs in a way that ensures that AMMs are closed under composition, in a way that works for "higher-dimensional" AMMs that manage more than two asset classes, and so the composition of AMMs in "stable" states remains stable.

cs.DC↗