[HN Gopher] Formal CHERI: design-time proof of full-scale archit...
___________________________________________________________________
Formal CHERI: design-time proof of full-scale architecture security
properties (2022)
Author : fanf2
Score : 91 points
Date : 2024-08-28 11:42 UTC (11 hours ago)
(HTM) web link (www.lightbluetouchpaper.org)
(TXT) w3m dump (www.lightbluetouchpaper.org)
| anotherhue wrote:
| I'd take this over incremental clock speed improvements any day.
| LoganDark wrote:
| 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).
| detourdog wrote:
| This project shares so many foundational computing ideals
| this represents the best aspects of "the many eyes surfacing
| not just bugs but assumptions".
|
| 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.
| gnufx wrote:
| See the references I just posted, crossing with that, for
| CHERI-RISC-V if others are interested.
| jazzyjackson wrote:
| Hi, sorry, this is all quite a bit above my head but I am
| interested in alternate architectures, would you mind
| expanding on what kinds of symbols you're talking about? My
| mind jumps to the members of an instruction set, but I
| assume you would have called them instructions in that
| case, what's the alternative to a local symbol?
| detourdog wrote:
| Sorry I'm always trying to keep it simple.
|
| 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.
| jazzyjackson wrote:
| Intriguing, thanks, I'll have to marinate on that.
|
| 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.
|
| https://en.m.wikipedia.org/wiki/What_the_Dormouse_Said
| detourdog wrote:
| I haven't read that book yet. I have been meaning to but
| just haven't gotten to it.
|
| 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.
| gnufx wrote:
| I wonder why emulators aren't interesting for a hobbyist.
| However, there are FPGA implementations [1], and micro-
| controller-type systems on FPGA available commercially [2].
|
| [3] has a list of publications for the rigorous engineering
| agenda.
|
| 1. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/che
| ri...
|
| 2. https://cheriot.org/
|
| 3. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/che
| ri...
| LoganDark wrote:
| > I wonder why emulators aren't interesting for a hobbyist.
|
| 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.)
| c-c-c-c-c wrote:
| CHERIoT chips will be available early next year from SCI
| Semiconductor iirc. I have heard of some samples floating
| around
| timhh wrote:
| (2022)
| pizlonator wrote:
| Fil-C is now best case 2x slower than normal C, worst case about
| 6x, and I haven't even finished implementing the obvious
| optimizations.
|
| I bet that the Intel chip I'm on is more than 6x faster than any
| of the CHERI hardware.
|
| Fil-C has a more deterministic and safer handling of use-after-
| free and it's flexible enough to run CPython (pretty sure CPython
| was too much for CHERI's capabilities).
|
| If you consider that:
|
| - Fil-C will get faster even without architecture help
|
| - Fil-C runs on normal HW
|
| - it probably only takes a small extension to the HW to eliminate
| any remaining Fil-C overhead (a much smaller extension than
| CHERI).
|
| - Fil-C is just a thing I pulled out of my ass in the last 10
| months or so and is a totally solo spare-time project (I.e. if a
| real compiler team did this full time they'd probably make it
| even better than where I'm at)
|
| Then it sure does seem like CHERI is going to be doomed long
| term.
| IshKebab wrote:
| A big application of CHERI is embedded where you can't just
| spend 6x more area/power on software.
|
| Also CHERI isn't just about memory safety. It also supports
| software isolation & capabilities.
|
| See CherIoT for an example of both of these.
| pizlonator wrote:
| Fil-C is capability based and its capabilities offer stronger
| guarantees than CHERI's.
|
| My point is that if a single dude working solo for 10 months
| gets to 6x overhead in the bad case then the overhead of the
| software capability approach (either exactly Fil-C or
| something vaguely like it) is likely to be much much less
| than 6x in the limit. Fil-C was 200x slower just six months
| ago and I'm not even done optimizing. That should give you an
| idea of where it's heading.
| yosefk wrote:
| it would be interesting if you shared more details
| pizlonator wrote:
| https://github.com/pizlonator/llvm-project-
| deluge/blob/delug...
|
| https://m.youtube.com/watch?v=JRoX9_lXJFg
|
| Note that both that doc and the video have old perf
| numbers. I'm landing optimizations all the time.
| pitaj wrote:
| It's an interesting approach. A hybrid software with limited
| hardware change is interesting.
|
| > Fil-C will get faster even without architecture help
|
| Only to a point. You'll plateau eventually since you have
| checks on every dereference.
| pizlonator wrote:
| No, I won't have checks on every dereference. The
| monotonicity of Fil-C's capabilities makes it possible to do
| a lot of redundant check elimination.
|
| That's what I'm working on now. Should have some early
| results soon.
| pitaj wrote:
| Obviously, removing repeated/redundant bounds checks is a
| basic optimization. That's not what I meant. My point still
| stands.
| pizlonator wrote:
| I think that check on every access is a lot different
| than check on some accesses.
|
| That plateau might not be any different than the CHERI
| plateau, since at the microarch level, CHERI will have
| more checks since it cannot benefit from a compiler's
| static reasoning about redundant check elimination.
| gchadwick wrote:
| Improved hardware based abstractions to provide stronger
| security and better ways to isolate software components just
| seems like a good idea. Yes you can certainly do plenty in
| software (in particular using language like Rust) but
| presumably we still want hardware enforced security properties?
| So why not improve those as well as software?
|
| To put it another way why not remove existing hardware security
| abstractions we do have? Ditch virtualization (or hugely strip
| it back), get rid of different privilege levels, loose page-
| table enforced permissions. After all you can just build safe
| software why bother with these things?
|
| I for one don't think this is a sensible line of argument,
| defence in depth is a good idea, build your software to be as
| secure as possible then build your hardware such that if there
| is some flaw in your software's defences you can keep things
| contained though hardware abstractions.
|
| Even with improved languages there's a giant body of existing
| code you need to work with, with compartmentalization in CHERI
| you can keep this stuff safely contained. Plus how do you
| guarantee everything running on the system has been built in
| your safe language and compiled with your blessed known good
| compiler? Feasible in some places (like embedded systems) far
| less feasible in others.
| pizlonator wrote:
| Fil-C is not ABI compatible with regular C, so there's no way
| to accidentally forget to compile some part of your stack
| with Fil-C.
|
| If changing all the HW we use was as easy as waving a wand,
| then your argument would be sound. Unfortunately, it's super
| hard to get folks to use different HW. And because of how
| silicon economics work out, a new upstart architecture with
| limited users is sure to experience slower perf scaling than
| the mainstream HW. That strongly disincentivizes anyone from
| being an early adopter of exotic new HW. I think that's why
| CHERI isn't mainstream yet despite a decade of investment.
|
| Hence why even ignoring Fil-C, it's probably more realistic
| to rewrite stuff in Rust than it is to switch to CHERI. Fil-C
| adds a third option where you pay some perf but you don't
| have to rewrite your code or switch what HW you use. CHERI
| also costs perf - practically speaking, available CHERI HW is
| more than 6x slower than the HW Fil-C can run on. That's
| fundamental, due to silicon economics.
|
| Finally, I think you're overselling the CHERI defense in
| depth. My understanding is that CHERIoT doesn't use virtual
| memory and that there are subtle reasons why virtual memory
| and CHERI put together gets weird, especially if you want to
| support capability revocation. On the other hand, Fil-C works
| on top of virtual memory so you get both virtual memory
| protection and capability protection, hence more defense in
| depth.
| pitaj wrote:
| Recompiling everything is a non-starter in many cases.
| pizlonator wrote:
| If recompiling is a nonstarter then a new HW arch like CHERI
| is even more of a nonstarter.
___________________________________________________________________
(page generated 2024-08-28 23:00 UTC)