4 ms·

I've been really impressed with what you're doing with Fil-C, but: > Here's the difference with Fil-C: It's totally memory safe and fanatically compatible with

I've been really impressed with what you're doing with Fil-C, but: > Here's the difference with Fil-C: It's totally memory safe and fanatically compatible with C/C++, no B.S. Is this true on both counts? If I'm reading your docs right, you're essentially adding hidden capabilities to pointers. This is a great technique that gives you almost perfect machine-level compatibility by default, but it comes with the standard caveats: 1. Your type safety/confusion guards are essentially tied to pointer "color," and colors are finite. In other words, in a sufficiently large program, an attacker can still perform type confusion by finding types with overlapping colors. Not an issue in small codebases, but maybe in browser- or kernel-sized ones. 2. In terms of compatibility, I'm pretty sure this doesn't allow a handful of pretty common pointer-integer roundtrip operations, at least not without having the user/programmer reassign the capability to the pointer that's been created out of "thin air." You could argue correctly that this is a bad thing that programmers shouldn't be doing, but it's well-defined and common enough IME. (You also cited my blog's writeup of `totally_safe_transmute` as an example of something that Fil-C would prevent, but I'm not sure I agree: the I/O effect in that example means that the program could thwart the runtime checks themselves. Of course, it's fair to say that /proc/self/mem is a stunt anyways.)

pizlonator 2y ago
My type safety and confusion guards have nothing to do with colors of any kind. There are no finite colors to run out of. Fil-C totally allows pointer to integer round tripping in many cases, if the compiler can see it’s safe. I’m citing unsafe transmute as something that Fil-C doesn’t prevent. It’s not something that memory safety prevents.
- woodruffw 2y ago
  > My type safety and confusion guards have nothing to do with colors of any kind. There are no finite colors to run out of. I'm having trouble seeing where the type confusion protection properties come from, then. I read through your earlier (I think?) design that involved isoheaps and it made sense in that context, but the newer stuff (in `gimso_semantics.md` and `invisicap.txt`) seems to mostly be around bounds checking instead. Apologies if I'm missing something obvious. > I’m citing unsafe transmute as something that Fil-C doesn’t prevent. It’s not something that memory safety prevents. I think the phrasing is confusing, because this is what the manifesto says: > No program accepted by the Fil-C compiler can possibly go on to escape out of the Fil-C type system. This to me suggests that Fil-C's type system detects I/O effects, but I take it that wasn't the intended suggestion.
  - pizlonator 2y ago
    Here’s a write up that goes into more detail: https://github.com/pizlonator/llvm-project-deluge/blob/deluge/gimso_semantics.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
    - woodruffw 2y ago
      I read that, but I'm not seeing where the type is encoded in the capability.
      - pizlonator 2y ago
        Short answer: if you know how CHERI and SoftBound do it, then Fil-C is basically like that. Long answer: let's assume 64-bit (8 byte pointers) without loss of generality. Each capability knows, for each 8 bytes in its allocation, whether those 8 bytes are a pointer, and if so, what that pointer's capability is. Example: char* p = malloc(64); This will allocate 64 bytes. p's capability will know, for each of the 8 8-byte slots, if that slot is a pointer and if so, what it's capability is. Since you just allocated the object, none of them have capabilities. Then if you do: *(int**)(p + 8) = malloc(sizeof(int)); Then p's capability will know that at offset 8, there is a pointer, and it will know that the capability is whatever came out of the malloc. Hence, each capability is dynamically tracking where the pointers are. So it's not a static type but rather something that can change over time. There's a bunch of engineering that goes into this being safe under races (it is) and for supporting pointer atomics (they just work).
      - pizlonator 2y ago
        BTW I wrote another doc to try to explain what's happening. Hope this helps. https://github.com/pizlonator/llvm-project-deluge/blob/deluge/invisicaps_by_example.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
        woodruffw 2y ago
        Thank you, I found this very helpful!

pizlonator 2y ago

My type safety and confusion guards have nothing to do with colors of any kind. There are no finite colors to run out of. Fil-C totally allows pointer to integer round tripping in many cases, if the compiler can see it’s safe. I’m citing unsafe transmute as something that Fil-C doesn’t prevent. It’s not something that memory safety prevents.

woodruffw 2y ago
> My type safety and confusion guards have nothing to do with colors of any kind. There are no finite colors to run out of. I'm having trouble seeing where the type confusion protection properties come from, then. I read through your earlier (I think?) design that involved isoheaps and it made sense in that context, but the newer stuff (in `gimso_semantics.md` and `invisicap.txt`) seems to mostly be around bounds checking instead. Apologies if I'm missing something obvious. > I’m citing unsafe transmute as something that Fil-C doesn’t prevent. It’s not something that memory safety prevents. I think the phrasing is confusing, because this is what the manifesto says: > No program accepted by the Fil-C compiler can possibly go on to escape out of the Fil-C type system. This to me suggests that Fil-C's type system detects I/O effects, but I take it that wasn't the intended suggestion.
- pizlonator 2y ago
  Here’s a write up that goes into more detail: https://github.com/pizlonator/llvm-project-deluge/blob/deluge/gimso_semantics.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
  - woodruffw 2y ago
    I read that, but I'm not seeing where the type is encoded in the capability.
    - pizlonator 2y ago
      Short answer: if you know how CHERI and SoftBound do it, then Fil-C is basically like that. Long answer: let's assume 64-bit (8 byte pointers) without loss of generality. Each capability knows, for each 8 bytes in its allocation, whether those 8 bytes are a pointer, and if so, what that pointer's capability is. Example: char* p = malloc(64); This will allocate 64 bytes. p's capability will know, for each of the 8 8-byte slots, if that slot is a pointer and if so, what it's capability is. Since you just allocated the object, none of them have capabilities. Then if you do: *(int**)(p + 8) = malloc(sizeof(int)); Then p's capability will know that at offset 8, there is a pointer, and it will know that the capability is whatever came out of the malloc. Hence, each capability is dynamically tracking where the pointers are. So it's not a static type but rather something that can change over time. There's a bunch of engineering that goes into this being safe under races (it is) and for supporting pointer atomics (they just work).
    - pizlonator 2y ago
      BTW I wrote another doc to try to explain what's happening. Hope this helps. https://github.com/pizlonator/llvm-project-deluge/blob/deluge/invisicaps_by_example.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
      - woodruffw 2y ago
        Thank you, I found this very helpful!