Cover Image

VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Antón, Anna Lena Duque, Müller, Johannes, Schmitz, Philipp, Jauch, Tobias, Wezel, Alex, Deutschmann, Lucas, Fadiheh, Mohammad Rahmani, Stoffel, Dominik, Kunz, Wolfgang
Format:	Preprint
Published:	2024
Subjects:	Cryptography and Security
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Scalable Formal Verification Methodology for Data-Oblivious Hardware
by: Deutschmann, Lucas, et al.
Published: (2023)

Okapi: Efficiently Safeguarding Speculative Data Accesses in Sandboxed Environments
by: Schmitz, Philipp, et al.
Published: (2023)

Biting the CHERI bullet: Blockers, Enablers and Security Implications of CHERI in Defence
by: Faily, Shamal
Published: (2025)

MCU-Wide Timing Side Channels and Their Detection
by: Müller, Johannes, et al.
Published: (2023)

Enabling Security on the Edge: A CHERI Compartmentalized Network Stack
by: Ferraro, Donato, et al.
Published: (2025)

Case Study: Securing MMU-less Linux Using CHERI
by: Almatary, Hesham, et al.
Published: (2023)

Mon CHÉRI: Mitigating Uninitialized Memory Access with Conditional Capabilities
by: Gülmez, Merve, et al.
Published: (2024)

PoisonCap: Efficient Hierarchical Temporal Safety for CHERI
by: Wang, Yuecheng, et al.
Published: (2026)

Pitfalls in VM Implementation on CHERI: Lessons from Porting CRuby
by: Liu, Hanhaotian, et al.
Published: (2026)

Not quite a piece of CHERI-cake: Are new digital security by design architectures usable?
by: Alhindi, Maysara, et al.
Published: (2025)

PICASSO: Scaling CHERI Use-After-Free Protection to Millions of Allocations using Colored Capabilities
by: Gülmez, Merve, et al.
Published: (2026)

Using LLMs to Facilitate Formal Verification of RTL
by: Orenes-Vera, Marcelo, et al.
Published: (2023)

Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
by: Liu, Jiale, et al.
Published: (2026)

FormalRTL: Verified RTL Synthesis at Scale
by: Li, Kezhi, et al.
Published: (2026)

RTL Verification for Secure Speculation Using Contract Shadow Logic
by: Tan, Qinhan, et al.
Published: (2024)

SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
by: Chang, Fu-Chieh, et al.
Published: (2026)

Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
by: Blain, Dominik, et al.
Published: (2026)

AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL
by: Bai, Yunsheng, et al.
Published: (2025)

Broken Quantum: A Systematic Formal Verification Study of Security Vulnerabilities Across the Open-Source Quantum Computing Simulator Ecosystem
by: Blain, Dominik
Published: (2026)

VeriPlan: Integrating Formal Verification and LLMs into End-User Planning
by: Lee, Christine, et al.
Published: (2025)

VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
by: Xin, Yutong, et al.
Published: (2026)

Formal Verification of Secure Encrypted Virtualization
by: Weerasena, Hansika, et al.
Published: (2026)

EXAMINING THE POWER OF MITIGATION STRATEGIES TO ADDRESS THE CLASSROOM IMPACT OF ADVERSE CHILDHOOD EXPERIENCES
by: Jauch, Jamie
Published: (2024)

Trajectory optimization based on recursive B-spline approximation for automated longitudinal control of a battery electric vehicle
by: Jauch, Jens
Published: (2024)

The Dumbed‐Down Discourse Dilemma
by: Malte Jauch
Published: (2025)

Attracting foreign investment at all costs?: the case of export processing zones (EPZs) and Ramatex in Namibia
by: Herbert Jauch
Published: (2009)

¿Atraer inversiones extranjeras a cualquier precio?: el caso de las zonas francas industriales y Ramatex en Namibia
by: Herbert Jauch
Published: (2009)

Attirer à tout prix les investissements étrangers?: le cas des zones franches d'exportation (ZFE) et de Ramatex en Namibie
by: Herbert Jauch
Published: (2009)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
by: Yubeaton, Patrick, et al.
Published: (2025)

RTL2M$μ$PATH: Multi-$μ$PATH Synthesis with Applications to Hardware Security Verification
by: Hsiao, Yao, et al.
Published: (2024)

AIvril: AI-Driven RTL Generation With Verification In-The-Loop
by: Islam, Mubashir ul, et al.
Published: (2024)

The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
by: Tihanyi, Norbert, et al.
Published: (2023)

Fully Automatic Neural Network Reduction for Formal Verification
by: Ladner, Tobias, et al.
Published: (2023)

VeriRAG: A Retrieval-Augmented Framework for Automated RTL Testability Repair
by: Qi, Haomin, et al.
Published: (2025)

Formal Verification of Probing Security via Conditional Independence
by: Kura, Satoshi, et al.
Published: (2026)

QTFlow: Quantitative Timing-Sensitive Information Flow for Security-Aware Hardware Design on RTL
by: Reimann, Lennart M., et al.
Published: (2024)

Maps between standard and principal flag orders
by: Jauch, Erich C.
Published: (2022)

Exhaustive Search for Quantum Circuit Optimization using ZX Calculus
by: Fischbach, Tobias, et al.
Published: (2025)

Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification
by: Strauch, Tobias
Published: (2025)

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
by: Reinhard, Tobias
Published: (2024)