How to verify mmio access?

[zpzigi754]

I've tried with the below code for mocking a mmio access.

const BUFFER: *mut u32 = 0xb8000 as *mut u32;
#[cfg(kani)]
#[kani::proof]
fn test_write() {
    let val = 12;
    unsafe {
        core::ptr::write_volatile(BUFFER, val);
    }
}

using the following command line invocation:

cargo kani

with Kani version: 0.3.0

It brought out the following failures.

SUMMARY:
 ** 5 of 7 failed
Failed Checks: dereference failure: pointer NULL
 File: "/rustc/c52b9c10bfb5164015eb977ff498e0597ae63eb1/library/core/src/ptr/mod.rs", line 1519, in std::ptr::write_volatile
Failed Checks: dereference failure: deallocated dynamic object
 File: "/rustc/c52b9c10bfb5164015eb977ff498e0597ae63eb1/library/core/src/ptr/mod.rs", line 1519, in std::ptr::write_volatile
Failed Checks: dereference failure: dead object
 File: "/rustc/c52b9c10bfb5164015eb977ff498e0597ae63eb1/library/core/src/ptr/mod.rs", line 1519, in std::ptr::write_volatile
Failed Checks: dereference failure: pointer outside object bounds
 File: "/rustc/c52b9c10bfb5164015eb977ff498e0597ae63eb1/library/core/src/ptr/mod.rs", line 1519, in std::ptr::write_volatile
Failed Checks: dereference failure: invalid integer address
 File: "/rustc/c52b9c10bfb5164015eb977ff498e0597ae63eb1/library/core/src/ptr/mod.rs", line 1519, in std::ptr::write_volatile

VERIFICATION:- FAILED

Why did the verification failures occur and how to pass the verification when an object of absolute address (e.g., mmio) is involved?

[danielsn]

As far as Kani knows, this is an illegal access to unallocated memory, which Kani is correctly catching.

It should be possible as a feature enhancement for Kani to allow specification of memory areas as MMIO.

changing tag to feature request.

[tedinski]

CBMC support for mmio seems to be in flux, and the "new approach" has yet to be merged:

diffblue/cbmc#6747

[danielsn]

https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/mm_io1/main.c

[danielsn]

Notes on CBMC's mmio implementation.

It doesn't havoc values.

int main()
{
  int *p=0x10;
  int *q=0x20;

  *p=42;
  assert(*p==42);
  int old = *q;
  int old2 = *q;
  assert(old == old2);
  return 0;
}

╰─$ cbmc mmio.c --pointer-check --mmio-regions 32:4,16:4                                                                                      10 ↵
CBMC version 5.53.1 (cbmc-5.53.1-9-gac2eaf3189) 64-bit x86_64 macos
Parsing mmio.c
Converting
Type-checking mmio
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.019433s
size of program expression: 47 steps
simple slicing removed 5 assignments
Generated 5 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 7.8937e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00605537s
Running propositional reduction
Post-processing
Runtime Post-process: 0.00285405s
Solving with MiniSAT 2.2.1 with simplifier
497 variables, 333 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 0.00297401s
Runtime decision procedure: 0.00923489s

** Results:
mmio.c function main
[main.pointer_dereference.1] line 8 dereference failure: invalid integer address in *p: SUCCESS
[main.assertion.1] line 9 assertion *p==42: SUCCESS
[main.pointer_dereference.2] line 9 dereference failure: invalid integer address in *p: SUCCESS
[main.pointer_dereference.3] line 12 dereference failure: invalid integer address in *q: SUCCESS
[main.assertion.2] line 14 assertion old == old2: SUCCESS

** 0 of 5 failed (1 iterations)
VERIFICATION SUCCESSFUL

[adpaco-aws]

#1328 is still blocked by CBMC's diffblue/cbmc#6747