Cheri + Rust

[Alan Karp]

https://nw0.github.io/cheri-rust.pdf

I've only read the abstract so far, but it's intriguing.

--------------
Alan Karp

[Mark S. Miller]

Nice find. From the abstract I expect to be surprised. My current belief is that the kind of language-safety provided by Rust subsumes the safety that Cheri would provide, such that Rust-on-CHERI is needless overhead beyond Rust by itself, with no appreciable increase in safety. Would be happy to find I'm wrong. I am intrigued. Thanks.

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CANpA1Z2K%2BpT0%2BKHguSbGuL%3DXTV8G0CN7FcnBTr4Ypbd4Gre5Zw%40mail.gmail.com.

[William ML Leslie]

On Fri, 27 Nov 2020 at 15:49, Mark S. Miller <ma...@agoric.com> wrote:
>
> Nice find. From the abstract I expect to be surprised. My current belief is that the kind of language-safety provided by Rust subsumes the safety that Cheri would provide, such that Rust-on-CHERI is needless overhead beyond Rust by itself, with no appreciable increase in safety. Would be happy to find I'm wrong. I am intrigued. Thanks.
>

Thanks Alan - it's a really interesting exploration. Not only is
CHERI good for Rust because it subsumes compiler bugs and works for
unsafe code, but Rust is good for CHERI because it can enforce certain
types of safe resource management. Looking forward to getting into it
in detail tomorrow.

>
> On Thu, Nov 26, 2020 at 8:34 PM Alan Karp <alan...@gmail.com> wrote:
>>
>> https://nw0.github.io/cheri-rust.pdf
>>
>> I've only read the abstract so far, but it's intriguing.
>>
>> --------------
>> Alan Karp
>>
>> --
>> You received this message because you are subscribed to the Google Groups "friam" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CANpA1Z2K%2BpT0%2BKHguSbGuL%3DXTV8G0CN7FcnBTr4Ypbd4Gre5Zw%40mail.gmail.com.
>
> --
> You received this message because you are subscribed to the Google Groups "friam" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CAK-_AD6t%2BTRBciRQLJn70VB1jnehKq%3Dp%3D0pz_5MoLz%2BmPhDzcA%40mail.gmail.com.



--
William Leslie

Q: What is your boss's password?
A: "Authentication", clearly

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law. You absolutely MAY reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without
prior contractual agreement.

[Ben Laurie]

On Fri, 27 Nov 2020 at 04:34, Alan Karp <alan...@gmail.com> wrote:

https://nw0.github.io/cheri-rust.pdf

I've only read the abstract so far, but it's intriguing.

Aha. A topic of great interest to me! More in thread...

[Ben Laurie]

On Fri, 27 Nov 2020 at 05:09, William ML Leslie <william.l...@gmail.com> wrote:

On Fri, 27 Nov 2020 at 15:49, Mark S. Miller <ma...@agoric.com> wrote:
>
> Nice find. From the abstract I expect to be surprised. My current belief is that the kind of language-safety provided by Rust subsumes the safety that Cheri would provide, such that Rust-on-CHERI is needless overhead beyond Rust by itself, with no appreciable increase in safety. Would be happy to find I'm wrong. I am intrigued. Thanks.
>

Thanks Alan - it's a really interesting exploration.  Not only is
CHERI good for Rust because it subsumes compiler bugs

Exactly - Mark's theory would be nice if we knew how to write perfect compilers. And also bear in mind that Rust's safety is ad hoc currently - there's no theory of it that can be formally proved.

 

and works for
unsafe code,

There is also this. There's a lot of unsafe code in Rust.

 

but Rust is good for CHERI because it can enforce certain
types of safe resource management.

One thing that is hard (or, at least, painful) at the h/w level is linear (or affine) capabilities - Rust adds those through properties of the language. I believe unsafe code can subvert them, though, so....

 

  Looking forward to getting into it
in detail tomorrow.

A final point is that people are increasingly writing OSes and hypervisors in Rust, and using CHERI for compartmentalisation has *substantial* performance benefits, so having Rust understand CHERI is also useful.

BTW, I don't know if this group has also noticed Morello, which is Arm's experimental CPU with CHERI support: https://www.lightbluetouchpaper.org/2020/10/29/sri-and-cambridge-release-cheri-software-stack-for-arm-morello/ contains links to many useful and interesting things.

 

To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CAHgd1hEB%3D0m_6M%2B2Ewc_1DTvTCkV7TxEZMqFjjDwrdSi-_xBSw%40mail.gmail.com.

[Matt Rice]

On Fri, Nov 27, 2020 at 4:34 AM Alan Karp <alan...@gmail.com> wrote:
>
> https://nw0.github.io/cheri-rust.pdf
>
> I've only read the abstract so far, but it's intriguing.

haven't gotten very far either, but noticed this (quoting the link)

>> Others are not mitigated by capabilities:
>> Compiler plugin: documentation plugin allowed arbitrary code execution by a different user while running the compiler, CVE-2018-1000622 [1, 38].
...

This really seems to me like the *classic* confused deputy with
different permissions to me.
In a cap system you'd be sending a capability to a third party
controlled plugin, rather than an ambiently third party writable
location, at which point it becomes intent...

[Ben Laurie]

In the context of CHERI "capabilities" refers to chunks of memory - it can be used to implement a broader capability system, but itself is only capable of speaking about RAM...

 

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CACTLOFra%2BSnk8mE3xhcAFNMATCjr--TX8tWkY3ENU1o_ukNcgg%40mail.gmail.com.

[Matt Rice]

I understand that, in the cross-compilation terminology they are
entirely speaking of 'target' issues.
The bug in question is a 'build' issue, Its just the generality of the
statement that bothers me when capabilities at the 'build' phase,
absolutely mitigate the vulnerability.

> To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CABrd9SSwZcSMqiOsDrYsmh3VFU4KFXM%2BM32W%3DKZO1wHQ7t417A%40mail.gmail.com.

[Ben Laurie]

On Fri, 27 Nov 2020 at 15:20, Matt Rice <rat...@gmail.com> wrote:

I understand that, in the cross-compilation terminology they are
entirely speaking of 'target' issues.
The bug in question is a 'build' issue, Its just the generality of the
statement that bothers me when capabilities at the 'build' phase,
absolutely mitigate the vulnerability.

Sure. If only we had a capability OS etc to do the build on...

 

To view this discussion on the web visit https://groups.google.com/d/msgid/friam/CACTLOFof0GoP3H067o2kmX3ot7kkduuwau-JPx%3Dao8wfihra8A%40mail.gmail.com.

[Kevin Reid]

On Thu, Nov 26, 2020 at 8:49 PM Mark S. Miller <ma...@agoric.com> wrote:

Nice find. From the abstract I expect to be surprised. My current belief is that the kind of language-safety provided by Rust subsumes the safety that Cheri would provide, such that Rust-on-CHERI is needless overhead beyond Rust by itself, with no appreciable increase in safety. Would be happy to find I'm wrong. I am intrigued. Thanks.

The primary consideration is adding capability checks to Rust's unsafe code blocks. In fact, section 5.8 discusses compiling safe Rust to machine code which does not use CHERI capabilities, for reduced memory usage (64-bit pointers instead of 128-bit capabilities). The problem is that many standard library algorithms use unsafe code to skip bounds checks based on higher-level reasoning, and any reference which might at some point be used by such code needs to be a capability.

[Pierre Thierry]

Scribit 'Ben Laurie' via friam dies 27/11/2020 hora 10:02:

> And also bear in mind that Rust's safety is ad hoc currently -
> there's no theory of it that can be formally proved.

OK, this surprises me. IIUC, Simon Peyton-Jones said linear logic
inspired Rust's ownership typing when talking about Linear Haskell.

Curiously,
Pierre Thierry
--
pie...@nothos.net
OpenPGP 0xD9D50D8A

[Tony Arcieri]

On Fri, Nov 27, 2020 at 2:02 AM 'Ben Laurie' via friam <fr...@googlegroups.com> wrote:

And also bear in mind that Rust's safety is ad hoc currently - there's no theory of it that can be formally proved.

Note there’s a work-in-progress for this: stacked borrows

https://plv.mpi-sws.org/rustbelt/stacked-borrows/

--

Tony Arcieri