Image de couverture de livre

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Thibault, Jérémy, Lenormand, Joseph, Hritcu, Catalin
Format:	Preprint
Publié:	2025
Sujets:	Programming Languages Cryptography and Security
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
par: Thibault, Jérémy, et autres
Publié: (2024)

FSLH: Flexible Mechanized Speculative Load Hardening
par: Baumann, Jonathan, et autres
Publié: (2025)

Misquoted No More: Securely Extracting F* Programs with IO
par: Andrici, Cezar-Constantin, et autres
Publié: (2026)

SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
par: Andrici, Cezar-Constantin, et autres
Publié: (2025)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
par: Baumann, Jonathan, et autres
Publié: (2026)

Dynamic IFC Theorems for Free!
par: Algehed, Maximilian, et autres
Publié: (2020)

A Proof-Producing Compiler for Blockchain Applications
par: Avigad, Jeremy, et autres
Publié: (2025)

The Jasmin Compiler Preserves Cryptographic Security
par: Arranz-Olmos, Santiago, et autres
Publié: (2025)

Secure Composition of Robust and Optimising Compilers
par: Kruse, Matthis, et autres
Publié: (2023)

Computationally Bounded Robust Compilation and Universally Composable Security
par: Künnemann, Robert, et autres
Publié: (2024)

Language-Based Security for Low-Level MPC
par: Skalka, Christian, et autres
Publié: (2024)

SMT-Boosted Security Types for Low-Level MPC
par: Skalka, Christian, et autres
Publié: (2025)

Adding Compilation Metadata To Binaries To Make Disassembly Decidable
par: Engel, Daniel, et autres
Publié: (2026)

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
par: van der Wall, Sören, et autres
Publié: (2024)

SplittingSecrets: A Compiler-Based Defense for Preventing Data Memory-Dependent Prefetcher Side-Channels
par: Sharma, Reshabh K, et autres
Publié: (2026)

Lightweight Yet Secure: Secure Scripting Language Generation via Lightweight LLMs
par: Zhang, Keyang, et autres
Publié: (2026)

Deterministic Fully-Static Whole-Binary Translation without Heuristics
par: Chen, Hongyu, et autres
Publié: (2026)

Formalizing Stack Safety as a Security Property
par: Anderson, Sean Noble, et autres
Publié: (2021)

Secure Synthesis of Distributed Cryptographic Applications (Technical Report)
par: Acay, Coşku, et autres
Publié: (2024)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
par: Huyghebaert, Sander, et autres
Publié: (2023)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
par: Ramananandro, Tahina, et autres
Publié: (2025)

A Language for Smart Contracts with Secure Control Flow (Technical Report)
par: Yao, Siqiu, et autres
Publié: (2024)

Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
par: Amorim, Arthur, et autres
Publié: (2025)

OblivIO: Securing reactive programs by oblivious execution with bounded traffic overheads
par: Blaabjerg, Jeppe Fredsgaard, et autres
Publié: (2023)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
par: Reitz, Antonin, et autres
Publié: (2024)

OpenAPI Specification Extended Security Scheme: A method to reduce the prevalence of Broken Object Level Authorization
par: Haddad, Rami, et autres
Publié: (2022)

Compile-time Security Analysis and Optimization of Sensitive String Producers
par: Samuel, Mike, et autres
Publié: (2026)

CrypTorch: PyTorch-based Auto-tuning Compiler for Machine Learning with Multi-party Computation
par: Liu, Jinyu, et autres
Publié: (2025)

Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics
par: Chen, Haobin Hiroki, et autres
Publié: (2025)

Beyond Imprecise Distance Metrics: Trace-Guided Directed Greybox Fuzzing via LLM-Predicted Call Stacks
par: Zhang, Yifan, et autres
Publié: (2025)

iResolveX: Multi-Layered Indirect Call Resolution via Static Reasoning and Learning-Augmented Refinement
par: Santra, Monika, et autres
Publié: (2026)

A Deductive System for Contract Satisfaction Proofs
par: Correnson, Arthur, et autres
Publié: (2026)

Enabling AI ASICs for Zero Knowledge Proof
par: Tong, Jianming, et autres
Publié: (2026)

Translating C To Rust: Lessons from a User Study
par: Li, Ruishi, et autres
Publié: (2024)

Demystifying Invariant Effectiveness for Securing Smart Contracts
par: Chen, Zhiyang, et autres
Publié: (2024)

QLCoder: A Query Synthesizer For Static Analysis of Security Vulnerabilities
par: Wang, Claire, et autres
Publié: (2025)

IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities
par: Li, Ziyang, et autres
Publié: (2024)

Understanding the Effectiveness of Large Language Models in Detecting Security Vulnerabilities
par: Khare, Avishree, et autres
Publié: (2023)

Securing Cryptographic Software via Typed Assembly Language (Extended Version)
par: Song, Shixin, et autres
Publié: (2025)

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
par: Arquint, Linard, et autres
Publié: (2025)