2 comments

  • snvzz 13 days ago
    >CHERI was first prototyped as extensions of MIPS and RISC-V; it is currently being evaluated by Arm...

    Note there's also a RISC-V effort[0][1] to write an extension specification proper.

    0. https://jira.riscv.org/browse/RVS-2141?src=confmacro

    1. https://wiki.riscv.org/display/HOME/RISC-V+Specification+Sta...

  • teleforce 13 days ago
    Does this CHERI platform enable memory safety for programming languages and all the facilities provided by borrow checking language like Rust is not necessary?
    • CJefferson 12 days ago
      No, there are actually quite a few things CHERI does that aren't the borrow checker's job, and some things the borrow checker does that CHERI doesn't help with.

      In C and C++, if you write x[4] for an array with only 2 members, you get undefined behaviour. In Rust this causes a 'panic', but that isn't a 'borrow checker' thing, that's because in Rust all array accesses are bounds checked by default.

      You can do un-bounds checked array accesses in Rust, you can do bounds-checked accesses in C++ (for std::vector at least), it's just that the languages chose different defaults.

      One thing the borrow checker does is help write parallel code by stopping multiple threads writing to the same memory at the same time. CHERI doesn't stop that at all.

    • nextaccountic 13 days ago
      No. CHERI doesn't help with data races, for example. Also it doesn't help with compiler optimizations that exploit UB to make code faster.

      Unfortunately low level languages are kind of addicted to optimizations that only work for languages with UB. There's too much performance being left at the table if you create a programming language entirely without UB.

      There's no law of nature, however, that says this must be the case forever. You could have a theorem prover prove useful properties about programs (and them feed them to the optimizer) and refrain from "optimizing" if you can't 100% prove that this will not break.

    • Peter_Sewell 12 days ago
      CHERI enables a rather high level of memory safety. It uses dynamic hardware checks rather than the safe-Rust static checks, which means that existing C/C++ code can often be ported to CHERI C/C++ with minor changes. Of course, as others note, "memory safety" is not a simple single thing, and there are certainly some cases that CHERI C/C++ don't depend on (as noted in this paper by Vadim Zaliva and others in our group). But in examples like this one from another comment:

          struct buffer {
                char *data;
                size_t capacity;
                size_t length;
              }
      
      the pointer 'data' will in CHERI have to be a valid capability, not just a virtual address, to permit access. It should normally have been instantiated with the correct bounds from the appropriate allocation, separately from the 'length' field, so the hardware will do the right check.
    • PhilipRoman 12 days ago
      EDIT: Apparently CHERI can handle this scenario, please ignore the rest of the comment

      Memory safety is not a binary choice. Consider this typical structure:

          struct buffer {
            char *data;
            size_t capacity;
            size_t length;
          }
      
      In fact it doesn't even have to be C, you could write it in Java, Python, etc. Lets say you decide to reuse such a buffer multiple times. From the C semantics point of view, there is nothing wrong with accessing elements past length. But it can easily lead to a heartbleed style vulnerability. There is probably some escape hatch for CHERI to mark memory as uninitialized, but I'm not very familiar with it. In Rust you can probably give out slices which will ensure bounds checking (or eliminate it if possible). The only correct way towards safety is languages which enable the programmer to add additional restrictions, like Rust or Frama-C.

      Anyway, this is mostly just theoretical musing, in practice CHERI will catch lots of issues. But I don't think it is correct to call it "memory safety".

      • vzaliva 12 days ago
        In CHERI, the `data` pointer in your example is not merely a 64-bit pointer (assuming ARM Morello architecture) but a special 128-bit data structure called a `capability`, which encodes within it the bounds of the memory block allocated to it. The hardware will prevent any out-of-bounds access, even if you manage to bypass any C language type checks, for example, by using inline assembly. So, this offers a pretty strong level of memory protection.
        • PhilipRoman 12 days ago
          Yes, but the capability will be enforcing the bound w.r.t "capacity", not "length" as that is the allocated size. From CHERI's point of view "length" is just some random user defined variable with no effect on bounds checks.
          • Peter_Sewell 12 days ago
            If you want to narrow the bounds of `data` on reuse, you can do easily do that in CHERI C (you'd need to also keep the larger capability somewhere to rederive the `data` capability from, either in this struct or elsewhere, depending where the allocation come from).
            • PhilipRoman 12 days ago
              Oh that is great news, I was not aware that CHERI was this powerful. Interesting if this could be abused by JIT compilers to provide free runtime bounds checks, kind of like the free null pointer checks done by catching SEGV.
    • Vecr 13 days ago
      Not in the near future, because compilers will still emit weird code in the presence of UB. The hardware enforces more stuff, and it makes it more likely you'll get a crash instead of the program continuing in a bad state, but it absolutely does not eliminate the general UB or "implementation defined" problems.
    • kryptiskt 12 days ago
      It's different. Borrow checking is statically enforced at compile time. CHERI applies at runtime, so it can't provide peace of mind that the code is safe, just that it will fail if it tries to do unsafe stuff.
    • saagarjha 12 days ago
      No. CHERI does not have a straightforward way of protecting against UAF.