Skip to content

Store capability PTE traps don't actually trap #95

Open
@PeterRugg

Description

@PeterRugg

let ptw_sc = if e.CapWrite() == 0b1 then PTW_SC_OK else PTW_SC_TRAP;
let (succ, ext_ptw') : (bool, ext_ptw) =
match (base_succ, ac) {
/* Base translation exceptions take priority over CHERI exceptions */
(false, _) => (false, init_ext_ptw),
(true, Read(Cap)) => (true, ext_ptw_lc_join(ext_ptw, ptw_lc)),
(true, Write(Cap)) => (true, ext_ptw_sc_join(ext_ptw, ptw_sc)),
(true, ReadWrite(Data, Cap)) => (true, ext_ptw_sc_join(ext_ptw, ptw_sc)),
(true, ReadWrite(Cap, Data)) => (true, ext_ptw_lc_join(ext_ptw, ptw_lc)),
(true, ReadWrite(Cap, Cap)) => (true, ext_ptw_sc_join(ext_ptw_lc_join(ext_ptw, ptw_lc), ptw_sc)),
(true, Read(Data)) => (true, ext_ptw),
(true, Write(Data)) => (true, ext_ptw),
(true, ReadWrite(Data, Data)) => (true, ext_ptw),
(true, Execute()) => (true, ext_ptw)
};
if succ
then PTE_Check_Success(ext_ptw')
else PTE_Check_Failure(ext_ptw', if ext_ptw'.ptw_sc == PTW_SC_TRAP then EPTWF_CAP_ERR else EPTWF_NO_PERM)

The ptw_sc value has no way of influencing succ, meaning no exception gets thrown.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions