Crux, a Precise Verifier for Rust and Other Languages
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913561604784128 |
|---|---|
| author | Pernsteiner, Stuart Diatchki, Iavor S. Dockins, Robert Dodds, Mike Hendrix, Joe Ravich, Tristan Redmond, Patrick Scott, Ryan Tomb, Aaron |
| author_facet | Pernsteiner, Stuart Diatchki, Iavor S. Dockins, Robert Dodds, Mike Hendrix, Joe Ravich, Tristan Redmond, Patrick Scott, Ryan Tomb, Aaron |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_18280 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Crux, a Precise Verifier for Rust and Other Languages Pernsteiner, Stuart Diatchki, Iavor S. Dockins, Robert Dodds, Mike Hendrix, Joe Ravich, Tristan Redmond, Patrick Scott, Ryan Tomb, Aaron Programming Languages 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. |
| title | Crux, a Precise Verifier for Rust and Other Languages |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2410.18280 |