SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations

• URL: http://arxiv.org/abs/2407.15080v3
• Date: Thu, 21 Nov 2024 09:33:54 GMT
• Title: SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
• Abstract summary: We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs.
• Score: 0.15800607910450126
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs. The basis of our proof method is a new form of simulation relation. It operates over directives that model the attacker's control over the micro-architectural state, and it accounts for the fact that the compiler transformation may change the influence of the micro-architectural state on the execution (and hence the directives). Using our proof method, we show the correctness of dead code elimination. When we tried to prove register allocation correct, we identified a previously unknown weakness that introduces violations to non-interference. We have confirmed the weakness for a mainstream compiler on code from the libsodium cryptographic library. To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated program. Using the analysis, we present an automated fix to existing register allocation implementations. We prove the correctness of the fixed register allocations with our proof method.

Related papers

• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• Independent Patch Verification for Coding Agents with a Bidirectional Reconstruct-and-Verify Framework [49.16055123488827]
  coding agents powered by large language models can now generate code patches directly from bug reports.<n>No mechanism independently verifies whether it truly resolves the reported problem.<n>We propose RETRACE, a training-free post-generation verification framework.
  arXiv  Detail & Related papers  (2026-08-09T22:59:13Z)
• From C to Idiomatic Rust: A Ship-of-Theseus Agentic Translation [0.13537117504260618]
  C underpins operating systems, embedded platforms, and network infrastructure because its abstractions map directly to machine behaviour.<n> Rust eliminates most of failure modes through a static ownership and borrowing model that enforces memory safety and aliasing constraints at compile time.<n>This paper presents a migration methodology that first generates a semantics-preserving, non-idiomatic Rust baseline and then incrementally rewrites it into idiomatic Rust using agentic AI.
  arXiv  Detail & Related papers  (2026-07-30T21:00:27Z)
• On the Inseparability of Instructions and Data in Shared-Embedding Sequence Models [0.0]
  We formalize prompted systems as Prompted Action Models with control-authoritative actions.<n>We prove Semantic-Faithful Control (SFC) is unachievable within the shared pipeline.<n>We identify the root cause and the class of solution it demands.
  arXiv  Detail & Related papers  (2026-06-25T21:52:29Z)
• Verifying the Rust Standard Library [3.303009078327922]
  Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code.<n>We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library.
  arXiv  Detail & Related papers  (2026-06-16T00:11:04Z)
• Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence [2.124730017640531]
  We introduce Protocol-Driven Development (PDD), where the primary software artifact is a machine-enforceable protocol rather than code.<n>PDD defines a governance model for automated software engineering.
  arXiv  Detail & Related papers  (2026-05-13T04:23:14Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDul is a language that unifies input transformations and predicate definitions into a single combined abstraction.<n>We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.
  arXiv  Detail & Related papers  (2025-11-13T18:06:21Z)
• Context-Guided Decompilation: A Step Towards Re-executability [50.71992919223209]
  Binary decompilation plays an important role in software security analysis, reverse engineering and malware understanding.<n>Recent advances in large language models (LLMs) have enabled neural decompilation, but the generated code is typically only semantically plausible.<n>We propose ICL4Decomp, a hybrid decompilation framework that leverages in-context learning (ICL) to guide LLMs toward generating re-executable source code.
  arXiv  Detail & Related papers  (2025-11-03T17:21:39Z)
• Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics [0.0]
  We construct All-Path Reachability Proofs through symbolic execution and compiling their graph structure.<n>We consolidate many semantic rewrites into single rules while preserving correctness by construction.<n>We implement this as a language-agnostic extension to the K framework.
  arXiv  Detail & Related papers  (2025-09-26T02:49:08Z)
• Search-Based Correction of Reasoning Chains for Language Models [72.61861891295302]
  Chain-of-Thought (CoT) reasoning has advanced the capabilities and transparency of language models (LMs)<n>We introduce a new self-correction framework that augments each reasoning step in a CoT with a latent variable indicating its veracity.<n>We also introduce Search Corrector, a discrete search algorithm over-valued veracity assignments.
  arXiv  Detail & Related papers  (2025-05-17T04:16:36Z)
• A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset [0.0]
  We present a method based on program analysis and formal verification to identify conditionally relevant variables (CRVs)<n>CRVs could lead to violation of safety properties in control software when affected by single event upsets (SEUs)
  arXiv  Detail & Related papers  (2025-05-10T13:56:02Z)
• MIB: A Mechanistic Interpretability Benchmark [77.35046700898326]
  We propose MIB, a Mechanistic Interpretability Benchmark, with two tracks spanning four tasks and five models.<n>Using MIB, we find that attribution and mask optimization methods perform best on circuit localization.<n>For causal variable localization, we find that the supervised DAS method performs best, while SAE features are not better than neurons.
  arXiv  Detail & Related papers  (2025-04-17T17:55:45Z)
• Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs [0.07499722271664144]
  Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program. For any attack a target context mounts against the compiled program one has to exhibit a source context mounting the same attack against the source program. We describe a novel back-translation technique, which results in simpler proofs that can be more easily mechanized in a proof assistant.
  arXiv  Detail & Related papers  (2025-03-25T12:50:35Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages. This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a novel framework that overcomes the lack of human-written proof to enable automated proof generation of Rust code. We demonstrate superior efficiency and precision compared to GPT-4o. This advancement leads to a significant improvement in performance, achieving a 70.50% accuracy rate in a benchmark crafted by human experts.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Breaking Bad: How Compilers Break Constant-Time~Implementations [12.486727810118497]
  We investigate how compilers break protections introduced by defensive programming techniques. We run a large-scale experiment to see if such compiler-induced issues manifest in state-of-the-art cryptographic libraries. Our study reveals that several compiler-induced secret-dependent operations occur within some of the most highly regarded cryptographic libraries.
  arXiv  Detail & Related papers  (2024-10-17T12:34:02Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  We present miniCodeProps, a benchmark of 201 program specifications in the Lean proof assistant. Despite its simplicity, miniCodeProps is sufficient to break current LLM-based provers.
  arXiv  Detail & Related papers  (2024-06-16T21:11:23Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries. We first build a binary large language model (FoC-BinLLM) to summarize the semantics of cryptographic functions in natural language. 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)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  Undefined behavior in C often causes devastating security vulnerabilities. We introduce SECOMP, a compiler for compartmentalized C code with machine-checked proofs. This is the first time such a strong criterion is proven for a mainstream programming language.
  arXiv  Detail & Related papers  (2024-01-29T16:32:36Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  Large Language Models (LLMs) have shown success in code analysis and synthesis. We present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis.
  arXiv  Detail & Related papers  (2023-11-07T05:47:47Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• Formalizing Stack Safety as a Security Property [0.6466206145151128]
  We propose a new formal characterization of stack safety using concepts from language-based security. This formulation is motivated by a particular class of enforcement mechanisms, the "lazy" stack safety micro-policies studied by Roessler and DeHon. We validate the properties by using them to distinguish between correct and incorrect implementations of Roessler and DeHon's micro-policies.
  arXiv  Detail & Related papers  (2021-05-02T08:18:34Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)
• Towards a Theoretical Understanding of the Robustness of Variational Autoencoders [82.68133908421792]
  We make inroads into understanding the robustness of Variational Autoencoders (VAEs) to adversarial attacks and other input perturbations. We develop a novel criterion for robustness in probabilistic models: $r$-robustness. We show that VAEs trained using disentangling methods score well under our robustness metrics.
  arXiv  Detail & Related papers  (2020-07-14T21:22:29Z)

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.