tock icon indicating copy to clipboard operation
tock copied to clipboard

kernel: make ReadableProcessBuffer an unsafe trait

Open lschuermann opened this issue 1 year ago • 6 comments

Pull Request Overview

As raised in https://github.com/tock/tock/issues/3757, users of this trait will need to rely on the implementations of ptr to be correct for their own safety guarantees.

Fixes #3757. Cc @kupiakos

Testing Strategy

This pull request was tested by make prepush.

TODO or Help Wanted

N/A

Documentation Updated

  • [x] Updated the relevant files in /docs, or no updates are required.

Formatting

  • [x] Ran make prepush.

lschuermann avatar Nov 10 '24 19:11 lschuermann

I don't the link to the issue is enough context as I don't think I understand what this is protecting.

With this PR we would have an implementation of an unsafe trait that does return ptr::null(). Any user of ReadableProcessBuffer would have to check for that whether the trait is safe or not.

bradjc avatar Nov 15 '24 18:11 bradjc

I don't the link to the issue is enough context as I don't think I understand what this is protecting.

With this PR we would have an implementation of an unsafe trait that does return ptr::null(). Any user of ReadableProcessBuffer would have to check for that whether the trait is safe or not.

I approved because this is objectively a soundness fix, but I agree the documentation could improve further.

On a cursory glance, I think the main requirement is that each ReadableProcessBuffer represents a valid slice, and len() and ptr() can be relied upon by unsafe code to return the length and data pointer of that slice. That probably calls for docs on len and ptr as well as the trait.

jrvanwhy avatar Nov 16 '24 23:11 jrvanwhy

Sorry letting this linger, I am working towards a deadline and will try to get back to this after that. I agree with all the concerns raised above.

lschuermann avatar Dec 05 '24 19:12 lschuermann

Leon will resume working on this.

bradjc avatar Sep 06 '25 18:09 bradjc

@ppannuto I have clarified the semantics of the ReadableProcessBuffer::ptr method, and how it relates to the value returned by the len method.

For that method to be useful to consumers of this type, we also have to make statements about how and when the pointer to the underlying memory is dereferenceable, and what types of operations are legal (read+write or read-only). Because ReadableProcessBuffer::ptr returns a pointer to memory that may or may not be writeable, we want to have another mut_ptr method on WriteableProcessBuffer that explicitly permits writes to its underlying memory.

This should take care of ambiguity around how exactly legal, sound implementations of ptr and mut_ptr must behave.


Now, I believe your other concern is that we should document that our current implementations of these traits conforms to these soundness requirements (i.e., we should document the safety of the unsafe impl lines).

I don't know of a good way to do this. It seems like stating the exact soundness conditions on the implementations of the trait would be redundant at best, and risk them going out of sync in the worst case.

What we want is to state that the implementation of ReadableProcessBuffer is sound, because our implementation complies with the ReadableProcessBuffer::ptr API contract. This is because our implementation does the length-check and returns a null-pointer for zero-length buffers, and relies on the guarantees concerning pointer validity provided on calls to new / new_external.

Is that sufficient, or do you want more extensive, redundant docs?

lschuermann avatar Sep 08 '25 01:09 lschuermann

@ppannuto Does this manage to address your concerns?

lschuermann avatar Oct 28 '25 15:10 lschuermann