ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESB...
summary
ESBMC is extended to accept CHERI-enabled clang output, translate it to its goto IR, and symbolically execute programs while modeling CHERI intrinsics, tag memory, capability compression and hybrid/pure cap modes. Directly encoding the compression in SMT causes a symbolic compression explosion, so either aggressively reduce compressions or assume CHERI semantics (treat hardware guarantees as given). Proving absence of CHERI exceptions is often orders of magnitude slower; assuming semantics speeds verification and permits reasoning about external libraries without source. Work is WIP; stack tag provenance and some examples (malloc reuse, ARM RMM pointer provenance) remain challenging.
AI-written summary · about
chapters (8)
- 0:00ESBMC-CHERI introduction
- 1:04ESBMC symbolic execution
- 3:53Adapting ESBMC for CHERI C
- 6:02CHERI memory compression issues
- 8:29Real-world Providence examples
- 13:07Providence and undefined behavior
- 17:48CHERI pointer arithmetic
- 18:53Verification scope and complexity
related talks
20mNegative/Positive Verification for WorldGuard, CHERI and Other RISC-V Security Models-
23mCORE-V Verification Test Bench – Commercial Qualit...
14mSVM: A Synthesizable Approach to Efficient RISC-V CPU Verification
24mRISC V Processor Verification based on Open source Framework
12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate Rollback
23mUnlocking Open Source RISC-V SoC Verification
47mTutorial: Choosing Appropriate Verification Techniques for Desired RISC...
23mOpen Source Verification Platform for RISC V Processors