Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Corner cases in bounds checking #40

Open
sorear opened this issue Jan 24, 2024 · 3 comments
Open

Corner cases in bounds checking #40

sorear opened this issue Jan 24, 2024 · 3 comments
Labels
documentation Improvements or additions to documentation

Comments

@sorear
Copy link
Contributor

sorear commented Jan 24, 2024

We don't currently have a precise definition of the tests CTESTSUBSET and CBUILDCAP perform. Are they set tests (every byte which is authorized by cap A is also authorized by cap B) or interval tests (B.base <= A.base && A.top <= B.top)?

Is it legal to construct a zero-length capability with base = top != 0 (with CSETBOUNDS, etc)? If so, are two zero-length capabilities with different bases considered equivalent by CTESTSUBSET? They represent the same set but different intervals.

Is it legal to construct a 2^XLENMAX length capability with base != 0 (using CSETBOUNDS or CBUILDCAP)? Such a capability would authorize all bytes in the address space, so it is an improper subset of Infinity but again not a subinterval.

Is it legal to construct a capability with length greater than 2^XLENMAX, thus including some bytes more than once? The malformed bounds check looks at the base but not the top, so you can do some interesting things at the maximum exponent.

Is it legal to construct a capability with length greater than zero and less than 2^XLENMAX, but with a base that causes it to wrap around 2^XLENMAX, for instance base = 2^XLENMAX-1, top = 1? (The documentation addresses representable regions that wrap around, but this is asking about the accessible region wrapping.) Such a capability is well defined as an interval, but unlikely to be useful unless memory itself wraps around, and supporting them makes interval operations much more complicated (no longer a lattice, etc).

Under RV32, any capability represented with EF=0 E=0 can also be represented using EF=1 T8=1. Should the redundant case be considered malformed?

I'd like to see a definition of subset semantics somewhere near the definition of the malformed bounds check in §2.5.

@PeterRugg
Copy link
Contributor

PeterRugg commented Jan 25, 2024

Good questions! I'll have a go:

Is it legal to construct a zero-length capability with base = top != 0 (with CSETBOUNDS, etc)?

Yes. Some codegen, e.g. structs with variable-length arrays at the end, emit setbounds of length zero. They would always trap on dereference anyway, so we have toyed with the idea of making such things untagged and reusing some other bounds encoding (e.g. encoding the top as inclusive), to mitigate these kinds of issues. Changing it raises the issue of what capability to return if somebody tries to do it, e.g. should getlen on the result always give zero. Zero-length capabilities haven't caused any major issues until now, and in fact I believe it was a design goal to allow them initially.

If so, are two zero-length capabilities with different bases considered equivalent by CTESTSUBSET? They represent the same set but different intervals.

The sail should disambiguate, and does for ISAv9, but there should be text too. It's B.base <= A.base && A.top <= B.top.

Is it legal to construct a 2^XLENMAX length capability with base != 0 (using CSETBOUNDS or CBUILDCAP)?

It isn't special-cased, but will be always be illegal because the almighty cap doesn't extend up above 2^XLENMAX. For these bounds checks, the overflow bit has to be tracked. Again, we may need text to clarify that. Same goes for lengths > 2^XLENMAX.

Is it legal to construct a capability with length greater than zero and less than 2^XLENMAX, but with a base that causes it to wrap around 2^XLENMAX, for instance base = 2^XLENMAX-1, top = 1?

Same again: the overflow means you're trying to authorise a cap outside of any existing cap.

I need to look into the RV32 case.

@jonwoodruff
Copy link
Contributor

Under RV32, any capability represented with EF=0 E=0 can also be represented using EF=1 T8=1. Should the redundant case be considered malformed?

@sorear I believe you have a point here. EF=0 E=0 would never be chosen by CSetBounds, as it could "more precisely" be represented with EF=1 T8=1. We should therefore leave EF=0 and E=0 reserved for RV32, methinks.

@tariqkurd-repo tariqkurd-repo added the documentation Improvements or additions to documentation label Jan 25, 2024
@sorear
Copy link
Contributor Author

sorear commented Jan 25, 2024

I've addressed the set vs. interval questions in #48, and expect to cover the rest.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation
Projects
None yet
Development

No branches or pull requests

4 participants