allow() is unsound #129
Comments
|
I'm not sure about that. The buffer is private and is never exposed directly. Instead, the only way to obtain data from the buffer is to copy data from/to it. When |
|
It is undefined behavior whenever all of the following occur simultaneously:
In this case, |
|
Maybe I am missing a point here, but from my naive point of view this would imply that MMIO and DMA is undefined behavior in general. Maybe you need some non-atomicity assumption here? |
|
If I'm reading the nomicon correctly, MMIO works if you use shared references to types containing UnsafeCell (and use volatile reads/writes). |
|
Yes, it would probably be more correct to store an |
|
I'm not suggesting we mark |
|
Ah, I see I put "unsafe" rather than "unsound" in the title. It should have been "unsound". |
|
This issue is actually worse than my original description states: it is not currently possible to un-allow a buffer shared with the kernel. See tock/tock#1831 for background. Note that Tock's design here may change in the future to make un-allow work reliably: tock/tock#1905 |
Allowed is the type that will be returned by Platform::allow() in the successful case. It represents a memory buffer shared with the kernel. It uses raw pointers and volatile writes to perform read/write accesses to the memory to avoid encountering undefined behavior. This is the first step towards fixing tock#129 and tock#143.
Allowed is the type that will be returned by Platform::allow() in the successful case. It represents a memory buffer shared with the kernel. It uses raw pointers and volatile writes to perform read/write accesses to the memory to avoid encountering undefined behavior. This is the first step towards fixing tock#129 and tock#143.
222: Add the Allowed type to libtock_platform. r=hudson-ayers a=jrvanwhy Allowed is the type that will be returned by `Platform::allow()` in the successful case. It represents a memory buffer shared with the kernel. It uses raw pointers and volatile writes to perform read/write accesses to the memory to avoid encountering undefined behavior. This is the first step towards fixing #129 and #143. Co-authored-by: Johnathan Van Why <jrvanwhy@google.com>
|
Solved in the Tock 2.0 ABI design and |
SharedMemoryinstances returned byallow()contain a reference to a buffer that may be mutated by the kernel. This is undefined behavior in Rust.It's probably not possible to expose a safe API that allows an application to access an
allow()-ed buffer until that buffer has been taken back from the kernel (i.e. overwritten with anotherallow()call).The text was updated successfully, but these errors were encountered: