Re:Unsoundness in Pin
by staticassertion on Friday November 29, 2019 @08:57PM
(#21668022)
I don't get how that's ever possible, regardless of soundness issues. Can you not simply use unsafe in a capsule, and violate this constraint? The only way isolates in V8 manage to provide any isolation is because the runtime/ language forbid such things entirely.
I suspect it is not so simple as "Rust's safety ensures malicious rust code can't access data".
Capsules aren't allowed to use unsafe. The target of tock is not generally going to be out of order, so spectre things shouldn't occur
Re:Unsoundness in Pin
by staticassertion on Friday November 29, 2019 @10:14PM
(#21668291)
Is there a doc about that? Can they also not use external crates? Very curious.
There's a blog post https://www.tockos.org/blog/2017/crates-are-not-safe
Lots of example code https://github.com/tock/tock/tree/master/capsules
Re:Unsoundness in Pin
by staticassertion on Saturday November 30, 2019 @04:42PM
(#21672294)
Thank you.
> A capsule is a Rust struct and associated functions. Capsules interact with each other directly, accessing exposed fields and calling functions in other capsules. Trusted platform configuration code initializes them, giving them access to any other capsules or kernel resources they need. Capsules can protect internal state by not exporting certain functions or fields.
> ...
> Rust’s language protection offers strong safety guarantees. Unless a capsule is able to subvert the Rust type system, it can only access resources explicitly granted to it, and only in ways permitted by the interfaces those resources expose. However, because capsules are cooperatively scheduled in the same single-threaded event loop as the kernel, they must be trusted for system liveness. If a capsule panics, or does not yield back to the event handler, the system can only recover by restarting.
I take it from the present discussion that that might not be as good of an idea as they think.
Worth noting that they also have process isolation on top, but it doesn’t seem to be motivated by any potential insecurity of the type system.