You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When Tock 2.0 was released, capsules had the ability to refuse to return Allow buffers as well as the ability to return buffers other than the most recently provided buffer. This was reflected in TRD 104, as well as the design of the fake::Driver trait:
However, that is changing in upstream Tock: tock/tock#2906. Now, libtock_platform can rely on the Allow system call to always return the last successfully-Allowed buffer. The Allow APIs I am designing for libtock-rs (e.g. #348) rely on this.
As a result, libtock_platform and libtock_unittest are currently unsound when combined: libtock_unittest allows a safe fake::Driver implementation to handle buffers in a way that libtock_platform assumes is impossible. To resolve this, we need to update libtock_unittest to match the new behavior of the Tock kernel (and the new TRD 104 wording).
The text was updated successfully, but these errors were encountered:
jrvanwhy
changed the title
Allow unsoundness due to TRD change (capsule behavior limits)
Update libtock_unittest to disallow non-swapping Allow behavior.
Dec 12, 2021
When Tock 2.0 was released, capsules had the ability to refuse to return Allow buffers as well as the ability to return buffers other than the most recently provided buffer. This was reflected in TRD 104, as well as the design of the
fake::Driver
trait:However, that is changing in upstream Tock: tock/tock#2906. Now,
libtock_platform
can rely on the Allow system call to always return the last successfully-Allowed buffer. The Allow APIs I am designing forlibtock-rs
(e.g. #348) rely on this.As a result,
libtock_platform
andlibtock_unittest
are currently unsound when combined:libtock_unittest
allows a safefake::Driver
implementation to handle buffers in a way thatlibtock_platform
assumes is impossible. To resolve this, we need to updatelibtock_unittest
to match the new behavior of the Tock kernel (and the new TRD 104 wording).The text was updated successfully, but these errors were encountered: