I've been a huge fan of CHERI for years, but unfortunately the hardware is super closed (huge research institutions only). Hopefully there will be a hardware option for hobbyists one of these years (the virtual machines don't interest me).
[3] has a list of publications for the rigorous engineering agenda.
1. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
3. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
I have the Rust programming language to fill the software part of this niche. The hardware part of CHERI is what makes it interesting to me.
(e.g. I've tinkered with Rust bootloaders before, and it doesn't matter too much whether the emulator is CHERI or not since Rust itself lets me express memory safety in the type system.)
You might be interested in a very timely blog post: https://cheriot.org/cheri/myths/2024/08/28/cheri-myths-safe-...
That sounds an awful lot like ensuring your code is free from memory-safety errors. A language which always traps on erroneous memory accesses is a memory safe language, so if CHERI really guarantees what that sentence says, then C on CHERI hardware is memory safe.
C is not memory-safe, even on CHERI, because it has to be trapped by CHERI; it cannot catch itself.
Safe Rust is memory-safe on its own, because memory unsafety can only be introduced by Unsafe Rust; Safe Rust has no unsafe operations. Assuming the Unsafe Rust is sound, Safe Rust cannot cause memory safety to be violated on its own. (You can do `/proc/mem` tricks on Linux, but that's a platform thing...)
1. Non-unsafe rust is memory-safe because otherwise unsafe operations (e.g. out-of-bounds accesses on arrays) are guaranteed to trap.
2. A typical C implementation on typical non-CHERI hardware is not safe because various invalid memory operations (e.g. out-of-bounds, use after free) may fail to trap.
3. A typical C implementation on CHERI hardware guarantees that all otherwise memory-unsafe operations trap.
I think we both agree on #1 and #2. Am I wrong about #3? If I'm not wrong about #3, then what makes you say that #3 is not memory-safe?
That article indeed is quite timely. I do agree with it. Slightly different angle though.
Morello boards are hard to come by, but there have been efforts to offer cloud-computing style use of them, especially now that bhyve support exists; if you're interested I can try to find out more (I'd offer you time on my cloud-computing Morello cluster from MSR, but it's offline for silly reasons). The "Big CHERI" RISC-V FPGA boards are indeed quite expensive, but CHERIoT-Ibex runs on the Arty A7 or the purpose-built Sonata board, and those are much more reasonable. (I'd still love to see it brought up on cheaper boards, too...)
I’m actually more interested in developing from the riscV branch.
Thinking about computers in the 100 year time frame I decided that processing “local” symbols is better than more sophisticated processes. The risc-V direct access to symbol development is where I want to start defining my “local” symbols.
The hope is that this line of thought will reduce the number of abstraction layers between the user and their environment.
CHERI having these concepts defined for risc-v creates a foundation for local processing Of symbols with a “good computing seal of integrity. I also see it as leading to less re-invention which should help progress.
The symbols I'm discussing were first documented by Claude Shannon. When I'm discussing symbols or large circuits I consider them interchangeable views of the same thing. They represent each other.
https://en.wikipedia.org/wiki/Claude_Shannon
I'm actually a designer so if I wanted to describe them as instructions I easily could. I'm a stickler for language so I believe that the use of the term instructions limits the conversation because it is too specific to communicate what I'm thinking about.
I would say an early example local symbol development might be libC. Our current computing environment evolved from the Personal Computing revolution and the internet. This came about through commercial interests and public adoption. I see this development as reaffirming the ideals first proposed by the "mother of all demos".
https://en.wikipedia.org/wiki/The_Mother_of_All_Demos
What I consider a "local" symbol is being demonstrated by Apple with their on device ML. The highest ideal to me is that everyone develops their own personal symbol table of digital services. I see CHERI as offering the fast track to that type of computing. I see this a integrating rather than programming.
I'm a big fan of the mother of all demos. Have you happened to have read "what the dormouse said" ? It has a great narrative of that event including all the behind the scenes action that Stewart Brand contributed, like setting up the TV broadcast truck on top of the hill to relay the video output and importantly the sounds of the mainframe back in Menlo park.
I can't believe we can watch the "mother of all demos". That alone proves its significance.
My favorite aspect of the demo is that it reveals that our human computing desires are universal and have been there from the start. It has taken generations to achieve the mass adoptions of these ideas. This realization takes the mystique away from the BigCo and their services. They are simple human desires for technology that were obvious from the beginning.