-
Crux, a Precise Verifier for Rust and Other Languages
Authors:
Stuart Pernsteiner,
Iavor S. Diatchki,
Robert Dockins,
Mike Dodds,
Joe Hendrix,
Tristan Ravich,
Patrick Redmond,
Ryan Scott,
Aaron Tomb
Abstract:
We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cryptographic modules and serializer / deserializer pairs. Crux builds on the same framework as the mature SAW-Cryptol toolchain, but Crux provides an interface where proofs are phrased as symbolic unit tests. Crux is desig…
▽ More
We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cryptographic modules and serializer / deserializer pairs. Crux builds on the same framework as the mature SAW-Cryptol toolchain, but Crux provides an interface where proofs are phrased as symbolic unit tests. Crux is designed for use in production environments, and has already seen use in industry.
In this paper, we focus on Crux-MIR, our verification tool for Rust. Crux-MIR provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust. Notably, Crux-MIR supports compositional reasoning, which is necessary to scale to even moderately complex proofs. We demonstrate Crux-MIR by verifying the Ring library implementations of SHA1 and SHA2 against pre-existing functional specifications.
Crux is available at https://crux.galois.com.
△ Less
Submitted 23 October, 2024;
originally announced October 2024.
-
Macaw: A Machine Code Toolbox for the Busy Binary Analyst
Authors:
Ryan G. Scott,
Brett Boston,
Benjamin Davis,
Iavor Diatchki,
Mike Dodds,
Joe Hendrix,
Daniel Matichuk,
Kevin Quick,
Tristan Ravitch,
Valentin Robert,
Benjamin Selfridge,
Andrei Stefănescu,
Daniel Wagner,
Simon Winwood
Abstract:
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 a…
▽ More
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.
△ Less
Submitted 18 February, 2025; v1 submitted 8 July, 2024;
originally announced July 2024.
-
Using a neural network approach to accelerate disequilibrium chemistry calculations in exoplanet atmospheres
Authors:
Julius L. A. M. Hendrix,
Amy J. Louca,
Yamila Miguel
Abstract:
In this era of exoplanet characterisation with JWST, the need for a fast implementation of classical forward models to understand the chemical and physical processes in exoplanet atmospheres is more important than ever. Notably, the time-dependent ordinary differential equations to be solved by chemical kinetics codes are very time-consuming to compute. In this study, we focus on the implementatio…
▽ More
In this era of exoplanet characterisation with JWST, the need for a fast implementation of classical forward models to understand the chemical and physical processes in exoplanet atmospheres is more important than ever. Notably, the time-dependent ordinary differential equations to be solved by chemical kinetics codes are very time-consuming to compute. In this study, we focus on the implementation of neural networks to replace mathematical frameworks in one-dimensional chemical kinetics codes. Using the gravity profile, temperature-pressure profiles, initial mixing ratios, and stellar flux of a sample of hot-Jupiters atmospheres as free parameters, the neural network is built to predict the mixing ratio outputs in steady state. The architecture of the network is composed of individual autoencoders for each input variable to reduce the input dimensionality, which is then used as the input training data for an LSTM-like neural network. Results show that the autoencoders for the mixing ratios, stellar spectra, and pressure profiles are exceedingly successful in encoding and decoding the data. Our results show that in 90% of the cases, the fully trained model is able to predict the evolved mixing ratios of the species in the hot-Jupiter atmosphere simulations. The fully trained model is ~1000 times faster than the simulations done with the forward, chemical kinetics model while making accurate predictions.
△ Less
Submitted 12 June, 2023;
originally announced June 2023.
