Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean

• URL: http://arxiv.org/abs/2609.15648v1
• Date: Mon, 14 Sep 2026 14:32:51 GMT
• Title: Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
• Abstract summary: We develop a new methodology for verifying cryptographic software written in Rust.<n> Rust's ownership discipline enables Aeneas to extract a pure model of this code in Lean.<n>Agents autonomously write formal proofs, which are independently verified by the Lean kernel.
• Score: 36.30712689467804
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification convenience. Rust's ownership discipline enables Aeneas to extract a pure model of this code in Lean, relieving us from low-level reasoning about pointer liveness and aliasing. Lean's extensibility lets us develop tactics and libraries that greatly simplify reasoning about extracted Rust code. We design and tune our toolchain to facilitate the use of AI. Agents autonomously write formal proofs, which are independently verified by the Lean kernel. Agents also assist in the formalization of cryptographic standards and platform-specific intrinsics, which still requires expert design and review. We apply our methodology to SymCrypt, Microsoft's cryptographic provider. We verify its implementations of algorithms such as SHA-3 and ML-KEM, which were ported from C to Rust. We also extend SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code. Our 237~KLOC Lean development establishes safety, panic-freedom, and functional correctness of 16.7~KLOC of Rust code supporting post-quantum cipher suites for x86-64 and ARM platforms. Our evaluation shows that verified Rust can meet SymCrypt's performance, portability, deployment, and maintainability requirements.

Related papers

• Kani: A Model Checker for Rust [3.019677299390329]
  Kani is an open-source model checker for Rust.<n>It pushes bounded model checking beyond bug-finding to provide correctness guarantees.<n>Kani operates at scale in production CI, with over 16,000 harnesses verified per code change.
  arXiv  Detail & Related papers  (2026-07-01T22:05:33Z)
• CREBench: Evaluating Large Language Models in Cryptographic Binary Reverse Engineering [12.401873262343862]
  We study the cryptographic binary reverse engineering capabilities of large language models (LLMs)<n>Our benchmark comprises 432 challenges built from 48 standard cryptographic algorithms, 3 insecure crypto key usage scenarios, and 3 difficulty levels.<n>We also establish a strong human expert baseline of 92.19 points, showing that humans maintain an advantage in cryptographic RE tasks.
  arXiv  Detail & Related papers  (2026-04-04T14:51:09Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• Targeted Fuzzing for Unsafe Rust Code: Leveraging Selective Instrumentation [3.6968220664227633]
  Rust is a promising programming language that focuses on usability and security.<n>It allows programmers to write unsafe code which is not subject to the strict Rust security policy.<n>We present an automated approach to detect unsafe and safe code components to decide which parts of the program a fuzzer should focus on.
  arXiv  Detail & Related papers  (2025-05-05T08:48:42Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases.<n>We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem.<n>The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• A Proof-Producing Compiler for Blockchain Applications [0.0873811641236639]
  CairoZero is a programming language for running decentralized applications (dApps) at scale.<n> cryptographic protocols are used to verify the results of execution efficiently on blockchain.<n>We show how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications.
  arXiv  Detail & Related papers  (2025-01-25T00:31:47Z)
• Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis [8.361424157571468]
  Syzygy is an automated approach to translate C to safe Rust.<n>This is the largest automated and test-validated C to safe Rust code translation achieved so far.
  arXiv  Detail & Related papers  (2024-12-18T18:55:46Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries.<n>We first build a binary large language model (FoC-BinLLM) to summarize the semantics of cryptographic functions in natural language.<n>We then build a binary code similarity model (FoC-Sim) upon the FoC-BinLLM to create change-sensitive representations and use it to retrieve similar implementations of unknown cryptographic functions in a database.
  arXiv  Detail & Related papers  (2024-03-27T09:45:33Z)
• CLAWSAT: Towards Both Robust and Accurate Code Models [74.57590254102311]
  We integrate contrastive learning (CL) with adversarial learning to co-optimize the robustness and accuracy of code models. To the best of our knowledge, this is the first systematic study to explore and exploit the robustness and accuracy benefits of (multi-view) code obfuscations in code models.
  arXiv  Detail & Related papers  (2022-11-21T18:32:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.