Cover Image

Automated Formal Verification of a Software Fault Isolation System

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Sotoudeh, Matthew, Yedidia, Zachary
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Cryptography and Security
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalizing Stack Safety as a Security Property
by: Anderson, Sean Noble, et al.
Published: (2021)

Protocols to Code: Formal Verification of a Next-Generation Internet Router
by: Pereira, João C., et al.
Published: (2024)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
by: Thibault, Jérémy, et al.
Published: (2024)

Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts
by: Cho, Hyunhum, et al.
Published: (2026)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
by: Huyghebaert, Sander, et al.
Published: (2023)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
by: Baumann, Jonathan, et al.
Published: (2026)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
by: Reitz, Antonin, et al.
Published: (2024)

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
by: Lindner, Andreas, et al.
Published: (2023)

Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
by: Ball, Thomas, et al.
Published: (2024)

Friend or Foe Inside? Exploring In-Process Isolation to Maintain Memory Safety for Unsafe Rust
by: Gülmez, Merve, et al.
Published: (2023)

Automated Repeatable Adversary Threat Emulation with Effects Language (EL)
by: Damodaran, Suresh K., et al.
Published: (2025)

LockForge: Automating Paper-to-Code for Logic Locking with Multi-Agent Reasoning LLMs
by: Saha, Akashdeep, et al.
Published: (2025)

Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics
by: Chen, Haobin Hiroki, et al.
Published: (2025)

Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset
by: Menon, Anand, et al.
Published: (2025)

Verification of Neural Networks' Global Robustness
by: Kabaha, Anan, et al.
Published: (2024)

PermRust: A Token-based Permission System for Rust
by: Gehring, Lukas, et al.
Published: (2025)

A Type System to Ensure Non-Interference in ReScript
by: Bennetzen, Benjamin, et al.
Published: (2024)

Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
by: Tempel, Sören, et al.
Published: (2024)

Gradual Verification for Smart Contracts
by: Sun, Haojia, et al.
Published: (2023)

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
by: Arquint, Linard, et al.
Published: (2025)

A Broad Comparative Evaluation of Software Debloating Tools
by: Brown, Michael D., et al.
Published: (2023)

DALC-CT: Dynamic Analysis of Low-Level Code Traces for Constant-Time Verification
by: Njungle, Nges Brian, et al.
Published: (2026)

Securing Cryptographic Software via Typed Assembly Language (Extended Version)
by: Song, Shixin, et al.
Published: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
by: Sotoudeh, Matthew
Published: (2025)

Smart Contract Languages: a comparative analysis
by: Bartoletti, Massimo, et al.
Published: (2024)

Empirical Security Analysis of Software-based Fault Isolation through Controlled Fault Injection
by: Bars, Nils, et al.
Published: (2025)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
by: Thibault, Jérémy, et al.
Published: (2025)

Constraint-Level Design of zkEVMs: Architectures, Trade-offs, and Evolution
by: Hassanzadeh-Nazarabadi, Yahya, et al.
Published: (2025)

FSLH: Flexible Mechanized Speculative Load Hardening
by: Baumann, Jonathan, et al.
Published: (2025)

Censor Resistant Instruction Independent Obfuscation for Multiple Programs
by: Ajorian, Ali
Published: (2025)

Program Analysis for High-Value Smart Contract Vulnerabilities: Techniques and Insights
by: Smaragdakis, Yannis, et al.
Published: (2025)

ILA: Correctness via Type Checking for Fully Homomorphic Encryption
by: Gollamudi, Tarakaram, et al.
Published: (2025)

Code Generation for Cryptographic Kernels using Multi-word Modular Arithmetic on GPU
by: Zhang, Naifeng, et al.
Published: (2025)

Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach
by: Li, Fang, et al.
Published: (2025)

Dynamic Graph-based Fingerprinting of In-browser Cryptomining
by: Sermchaiwong, Tanapoom, et al.
Published: (2025)

zkStruDul: Programming zkSNARKs with Structural Duality
by: Krishnan, Rahul, et al.
Published: (2025)

TYPEPULSE: Detecting Type Confusion Bugs in Rust Programs
by: Chen, Hung-Mao, et al.
Published: (2025)

SMT-Boosted Security Types for Low-Level MPC
by: Skalka, Christian, et al.
Published: (2025)

SafeFFI: Efficient Sanitization at the Boundary Between Safe and Unsafe Code in Rust and Mixed-Language Applications
by: Braunsdorf, Oliver, et al.
Published: (2025)