arXiv subjects

Caleb Helbling

Publications and source records attributed to Caleb Helbling.

5 recordsLinked to original sources

arXiv2026

Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution

Modern high-assurance software systems development favors memory safe languages such as SPARK (ADA) or Rust. However, developers often encounter non-memory safe code (e.g., C) in legacy systems and libraries which would be prohibitively expensive or risky to re-write. In response, developers have begun turning to machine learning/AI systems and other automated code translators. Automated translation comes with its own risks, however. The original and ported code are not precisely the same, semantically - otherwise there would be no point in performing the translation. To reduce these risks, we have developed cozy, a comparative binary analysis tool that simultaneously analyzes a binary compiled from "unsafe" source code and a binary compiled from a translation of the source code to a memory safe language. cozy walks the developer through differences in the behavior of the two binaries, presenting each difference and asking the user to assess whether the difference is intentional (good) or erroneous. Outside of the flagged differences, the binaries are formally verified to be equivalent. Consequently, the review process guarantees equivalence modulo changes approved by the developer. cozy has applications to automated translation, bug correction, code reviews, operation authorization, and automatic translation.

cs.SE↗

arXiv2025

cozy: Comparative Symbolic Execution for Binary Programs

This paper introduces cozy, a tool for analyzing and visualizing differences between two versions of a software binary. The primary use case for cozy is validating "micropatches": small binary or assembly-level patches inserted into existing compiled binaries. To perform this task, cozy leverages the Python-based angr symbolic execution framework. Our tool analyzes the output of symbolic execution to find end states for the pre- and post-patched binaries that are compatible (reachable from the same input). The tool then compares compatible states for observable differences in registers, memory, and side effects. To aid in usability, cozy comes with a web-based visual interface for viewing comparison results. This interface provides a rich set of operations for pruning, filtering, and exploring different types of program data.

cs.SE↗

arXiv2021

Solving the Funarg Problem with Static Types

The difficulty associated with storing closures in a stack-based environment is known as the funarg problem. The funarg problem was first identified with the development of Lisp in the 1970s and hasn't received much attention since then. The modern solution taken by most languages is to allocate closures on the heap, or to apply static analysis to determine when closures can be stack allocated. This is not a problem for most computing systems as there is an abundance of memory. However, embedded systems often have limited memory resources where heap allocation may cause memory fragmentation. We present a simple extension to the prenex fragment of System F that allows closures to be stack-allocated. We demonstrate a concrete implementation of this system in the Juniper functional reactive programming language, which is designed to run on extremely resource limited Arduino devices. We also discuss other solutions present in other programming languages that solve the funarg problem but haven't been formally discussed in the literature.

cs.PL↗

arXiv2020

Directed Graph Hashing

This paper presents several algorithms for hashing directed graphs. The algorithms given are capable of hashing entire graphs as well as assigning hash values to specific nodes in a given graph. The notion of node symmetry is made precise via computation of vertex orbits and the graph automorphism group, and nodes that are symmetrically identical are assigned equal hashes. We also present a novel Merkle-style hashing algorithm that seeks to fulfill the recursive principle that a hash of a node should depend only on the hash of its neighbors. This algorithm works even in the presence of cycles, which would not be possible with a naive approach. Structurally hashing trees has seen widespread use in blockchain, source code version control, and web applications. Despite the popularity of tree hashing, directed graph hashing remains unstudied in the literature. Our algorithms open new possibilities to hashing both directed graphs and more complex data structures that can be reduced to directed graphs such as hypergraphs.

cs.DM↗

arXiv2019

Juniper: A Functional Reactive Programming Language for the Arduino

This paper presents the design and implementation of Juniper: a functional reactive programming language (FRP) targeting the Arduino and related microcontroller systems. Juniper provides a number of high level features, including parametric polymorphic functions, anonymous functions, automatic memory management, and immutable data structures. Also included is a standard library which offers many useful FRP signal processing functions. Juniper is translated to standard C++ and compiled with the existing Arduino development tools, allowing Juniper programs to fit on resource-constrained devices, and enabling seamless interoperability with existing C++ libraries for these devices.

cs.PL↗