RBS+dsb-tlbiis-dsb

Description

forbidThis ‘read-broken-secret’ (RBS) test is a fundamental test for the security guarantees ‘break’ gives you. Thread 0 unmaps a VA before writing to the original PA (for example, here, through an alias). Thread 1 attempts to read that VA.It is allowed for Thread 1 to see the translation-fault, or to translate the VA using the old mapping and see the old write, but it is forbidden to translate the VA to the PA and see the new write.This ensures that, once a mapping to a location is ‘broken’, later writes to that location are ‘secret’ for any cores that were using that VA.

Source

[download toml source]
Page table setup Code
physical pa1; x |-> pa1; x ?-> invalid; y |-> pa1; *pa1 = 0; identity 0x1000 with code;
Thread 0
{R0=extz(0b0, 64), R1=pte3(x, page_table_base), R5=extz(page(x), 64), R2=extz(0x2, 64), R3=y, PSTATE.EL=0b01}
STR X0,[X1] DSB SY TLBI VAE1IS,X5 DSB SY STR X2,[X3]
Thread 1
{R1=x, VBAR_EL1=extz(0x1000, 64)}
LDR X0,[X1]
thread1_el1_handler
MOV X0,#1 MRS X13,ELR_EL1 ADD X13,X13,#4 MSR ELR_EL1,X13 ERET
Final State
1:X0 = 2

Execution Diagrams

Results

ETS RBS+dsb-tlbiis-dsb forbidden (0 of 2) 12912ms
strong RBS+dsb-tlbiis-dsb forbidden (0 of 2) 4158ms

Command-line invocation

isla-axiomatic --arch=/path/to/rems-project/isla-snapshots/aarch64.ir --config=/path/to/rems-project/isla/configs/aarch64_mmu_on.toml --footprint-config=/path/to/rems-project/isla/configs/aarch64.toml --model=/path/to/rems-project/systems-isla-tests/models/aarch64_mmu_strong_ETS.cat --armv8-page-tables --check-sat-using "(then dt2bv qe simplify solve-eqs bv)" --remove-uninteresting safe --dot . -t /path/to/litmus-tests/litmus-tests-armv8a-system-vmsa/tests/pgtable/HAND/RBS+dsb-tlbiis-dsb.litmus.toml

To generate diagrams we use model aarch64_mmu_no_axioms.cat to get diagrams of forbidden executions. To generate LaTeX sources of each test, pass --latex=.