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
• Authors: Sören van der Wall, Roland Meyer,
• 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:
• 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

• 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)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL is a formal verified EL++ reasoner equipped with machine-checkable correctness proofs. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.
  arXiv  Detail & Related papers  (2024-12-11T19:17:28Z)
• 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)
• 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)
• 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.