search

riscv / riscv-cheri

This repository contains the CHERI extension specification, adding hardware capabilities to RISC-V ISA to enable fine-grained memory protection and scalable compartmentalization.
https://jira.riscv.org/browse/RVG-148
Creative Commons Attribution 4.0 International
37 stars 24 forks source link

Checks on pcc #311

Open jasonyu1996 opened 5 days ago

jasonyu1996 commented 5 days ago

According to 3.2.1:

Operations that update pcc, such as changing privilege or executing jump instructions,
unseal capabilities prior to writing. Therefore, implementations do not need to check that
 that pcc is unsealed when executing each instruction. However, this property has not yet
been formally verified and may not hold if additional CHERI extensions beyond
Zcheripurecap are implemented.

I'm wondering if this also holds for the other checks on pcc. For example, can an implementation omit checks on the tag / X permission of pcc (or even omit storing them), since it seems to me that instructions that change pcc already check them as well.

tariqkurd-repo commented 5 days ago

It's a good question - we'd need to look at all the ways a new PCC can be installed - so from JALR, Xepc, Xtvec. You can certainly check for the tag and X permission when using the PCC from those sources, as if it's missing it won't be possible to execute from the target PCC. After that point there's no reason to store X and the tag, as PC incrementing, branches and immediate offset jumps can't clear it, because they all check that the target is in bounds before jumping.

jasonyu1996 commented 5 days ago

It's a good question - we'd need to look at all the ways a new PCC can be installed - so from JALR, Xepc, Xtvec. You can certainly check for the tag and X permission when using the PCC from those sources, as if it's missing it won't be possible to execute from the target PCC. After that point there's no reason to store X and the tag, as PC incrementing, branches and immediate offset jumps can't clear it, because they all check that the target is in bounds before jumping.

Yes that's also my understanding. Hence the question.