4 ms·

Checked C isn’t C. I’ve yet to see a convincing reason to use it instead of, say, Go. Or Rust, if you want real safety.

by Filligree 5y ago

naasking 5y ago
Transitioning an existing C codebase to checked C has to be easier than transitioning to Rust.
- Diggsey 5y ago
  Maybe / maybe not. It's relatively easy to translate C to unsafe Rust, which is a mostly automatic process. The hard part is taking that unsafe C/Rust and turning it into checked/safe code. For this part, Rust has many benefits over C: - As a language it is easier to refactor. This is due to a more hygenic macro system, a lack of header files, etc. - The safe subset of Rust is much larger and more expressive than the subset of checked C. This provides more options for the unsafe -> safe translation effort. - The safe subset of Rust is more powerful than the subset of checked C. This means that it's more likely that a piece of code can be translated 1:1 into safe Rust, compared to a more complex transformation. For example, code which returns a pointer into one of its arguments is not uncommon in C, and this can be directly translated into Rust lifetime annotations.
  - miffy900 5y ago
    > Maybe / maybe not. It's relatively easy to translate C to unsafe Rust, which is a mostly automatic process. This makes no sense; extending C code with Checked-C would still be easier as with Checked-C you wouldn't do any translation at all; it's a superset of C, in the same way that TypeScript is to JavaScript.
    - Diggsey 5y ago
      First, we're talking about "Transitioning an existing C codebase to checked C". If you're just adding new checked C code, then you're not doing that. Second, you can't just add checked C to a codebase, because you have to actually interop with the unchecked C code, which uses different pointer types. My argument is that it may be easier to do an automatic migration to unsafe Rust, and then incrementally convert to safe Rust, than it would be to leave the codebase as C and try to incrementally convert it to checked C, because the "incremental conversion to checked C" is extremely difficult.
      - naasking 5y ago
        If you read the abstract of the linked paper, you'd see they assert that the annotated pointers can be safely erased, thus making them ordinary pointers again.
- opnitro 5y ago
  Much easier. It doesn't change the runtime representation of types at all. It also supports a gradual typing-esque system for adding more precise types onto existing languages without changing the source code.
- ck45 5y ago
  Yes, it reminds me of this project, using Checked C for the FreeBSD kernel: http://secdev.ieee.org/wp-content/uploads/2020/11/s1-02-Duan.pdf http://secdev.ieee.org/wp-content/uploads/2020/11/s1-02-Duan...
- roca 5y ago
  Yes, but without temporal safety, it's not that valuable.
  - naasking 5y ago
    Spatial errors still account for almost 30% of yearly security vulnerabilities via buffer overflows alone, which is only one subclass. I think solving those makes it plenty useful. Then add the fact that exist transformations that turn temporal errors into spatial errors, and you'll see it's not necessarily much of a limitation even then: https://onlinelibrary.wiley.com/doi/full/10.1002/spe.2105 https://onlinelibrary.wiley.com/doi/full/10.1002/spe.2105
    - roca 5y ago
      Wow, that paper is extremely wrong. > Memory deallocation can be modeled as an assignment. For example, the statement free(p) can be represented by the statement p=invalid, where invalid is a special untyped pointer to a temporally ‘invalid’ range of memory. Absolutely not. That works for memory accesses through 'p'. It doesn't help you at all for memory accesses through other pointer aliases to the same memory block. I mean, it's trivial to replace "free(p)" with a macro that also nulls out 'p', but no-one claims that that solves UAF bugs.
      - naasking 5y ago
        You can't quote a paragraph out of context and simply claim it's wrong. Whether their claim is wrong depends entirely on the global invariants their analysis ensures.
        roca 5y ago
        I skimmed the entire paper before making that comment. I'm pretty sure I understand it. BTW I have a PhD in static program analysis. If you think the paper is right, just explain how it detects use-after-free in the following code fragment: int* p = (int*)malloc(sizeof(int)); int* q = p; free(p); *q = 1;
thesuperbigfrog 5y ago
>> Checked C isn’t C. According to the paper, it is: "Checked C is backward compatible with legacy C in the sense that all legacy code will type-check and compile. However, only code that appears in checked regions, which we call checked code, is spatially safe. Checked regions can be designated at the level of files, functions, or individual code blocks, the first with a #pragma and the latter two using the checked keyword. Within checked regions, both legacy pointers and certain unsafe idioms (e.g., variadic function calls) are disallowed." >> I’ve yet to see a convincing reason to use it instead of, say, Go. Or Rust, if you want real safety. What if you have a legacy codebase with hundreds of thousands of lines of C you want to maintain and improve? What if Go, Rust, etc. are not supported on your target platform?
- tialaramex 5y ago
  > What if you have a legacy codebase with hundreds of thousands of lines of C you want to maintain and improve? We know that smaller projects have successfully gone on the journey of moving from C to Rust, and they did so the same way you a whale right? One bite at a time. So that might absolutely be a reasonable choice. Things that could make it especially attractive: * There's existing Rust skill set in your team and not checked C * You intend to do other new work in Rust, so this is a skill set you'll be needing anyway. * There is relevant existing work in Rust e.g. today you use a popular C library for processing radar data. You know an equivalent library (or a port of the C library) is available as a Rust crate, if you went with Checked C, either the library isn't checked (partly undoing the good work) or you have to also translate the third party library to checked C. * The main benefit you were looking for is something checked C doesn't care about e.g. freedom from data races is a pretty big deal for concurrent software, and checked C doesn't do that today, and has no plans to do it in future but such races aren't possible in (safe) Rust. Or you wish you had nice built-in features like iterators. * Or the opposite side of the same coin, the main thing you dislike about C is still present in checked C. Maybe you don't like C's silent wrapping overflow, in checked C it's still there, but in Rust you can switch it off. Maybe you don't want the integer fifteen to be silently considered boolean "true" because you thought this programming language was supposed to have type checking, Rust is with you on that, Checked C of course is not.
junon 5y ago
> real safety Spoken by someone who clearly doesn't understand software safety. Neither Rust nor Go are "safe", formally.
- rurban 5y ago
  Practically neither
- RealityVoid 5y ago
  What does "formally safe" mean for you here? Are you talking about something like SEL4 that is formally verified? If yes, I wonder how many SW's are out that that are actually formally verified. Also, the problem of formal verification lies not in the language but in the code itself, right? So what would the problem be with Rust or Go?
- MaxBarraclough 5y ago
  It's true that Rust isn't safe, but the Safe Rust subset is.

Checked C isn’t C. I’ve yet to see a convincing reason to use it instead of, say, Go. Or Rust, if you want real safety.

naasking 5y ago

Transitioning an existing C codebase to checked C has to be easier than transitioning to Rust.

Diggsey 5y ago
Maybe / maybe not. It's relatively easy to translate C to unsafe Rust, which is a mostly automatic process. The hard part is taking that unsafe C/Rust and turning it into checked/safe code. For this part, Rust has many benefits over C: - As a language it is easier to refactor. This is due to a more hygenic macro system, a lack of header files, etc. - The safe subset of Rust is much larger and more expressive than the subset of checked C. This provides more options for the unsafe -> safe translation effort. - The safe subset of Rust is more powerful than the subset of checked C. This means that it's more likely that a piece of code can be translated 1:1 into safe Rust, compared to a more complex transformation. For example, code which returns a pointer into one of its arguments is not uncommon in C, and this can be directly translated into Rust lifetime annotations.
- miffy900 5y ago
  > Maybe / maybe not. It's relatively easy to translate C to unsafe Rust, which is a mostly automatic process. This makes no sense; extending C code with Checked-C would still be easier as with Checked-C you wouldn't do any translation at all; it's a superset of C, in the same way that TypeScript is to JavaScript.
  - Diggsey 5y ago
    First, we're talking about "Transitioning an existing C codebase to checked C". If you're just adding new checked C code, then you're not doing that. Second, you can't just add checked C to a codebase, because you have to actually interop with the unchecked C code, which uses different pointer types. My argument is that it may be easier to do an automatic migration to unsafe Rust, and then incrementally convert to safe Rust, than it would be to leave the codebase as C and try to incrementally convert it to checked C, because the "incremental conversion to checked C" is extremely difficult.
    - naasking 5y ago
      If you read the abstract of the linked paper, you'd see they assert that the annotated pointers can be safely erased, thus making them ordinary pointers again.
opnitro 5y ago
Much easier. It doesn't change the runtime representation of types at all. It also supports a gradual typing-esque system for adding more precise types onto existing languages without changing the source code.
ck45 5y ago
Yes, it reminds me of this project, using Checked C for the FreeBSD kernel: http://secdev.ieee.org/wp-content/uploads/2020/11/s1-02-Duan.pdf http://secdev.ieee.org/wp-content/uploads/2020/11/s1-02-Duan...
roca 5y ago
Yes, but without temporal safety, it's not that valuable.
- naasking 5y ago
  Spatial errors still account for almost 30% of yearly security vulnerabilities via buffer overflows alone, which is only one subclass. I think solving those makes it plenty useful. Then add the fact that exist transformations that turn temporal errors into spatial errors, and you'll see it's not necessarily much of a limitation even then: https://onlinelibrary.wiley.com/doi/full/10.1002/spe.2105 https://onlinelibrary.wiley.com/doi/full/10.1002/spe.2105
  - roca 5y ago
    Wow, that paper is extremely wrong. > Memory deallocation can be modeled as an assignment. For example, the statement free(p) can be represented by the statement p=invalid, where invalid is a special untyped pointer to a temporally ‘invalid’ range of memory. Absolutely not. That works for memory accesses through 'p'. It doesn't help you at all for memory accesses through other pointer aliases to the same memory block. I mean, it's trivial to replace "free(p)" with a macro that also nulls out 'p', but no-one claims that that solves UAF bugs.
    - naasking 5y ago
      You can't quote a paragraph out of context and simply claim it's wrong. Whether their claim is wrong depends entirely on the global invariants their analysis ensures.
      - roca 5y ago
        I skimmed the entire paper before making that comment. I'm pretty sure I understand it. BTW I have a PhD in static program analysis. If you think the paper is right, just explain how it detects use-after-free in the following code fragment: int* p = (int*)malloc(sizeof(int)); int* q = p; free(p); *q = 1;

thesuperbigfrog 5y ago

>> Checked C isn’t C. According to the paper, it is: "Checked C is backward compatible with legacy C in the sense that all legacy code will type-check and compile. However, only code that appears in checked regions, which we call checked code, is spatially safe. Checked regions can be designated at the level of files, functions, or individual code blocks, the first with a #pragma and the latter two using the checked keyword. Within checked regions, both legacy pointers and certain unsafe idioms (e.g., variadic function calls) are disallowed." >> I’ve yet to see a convincing reason to use it instead of, say, Go. Or Rust, if you want real safety. What if you have a legacy codebase with hundreds of thousands of lines of C you want to maintain and improve? What if Go, Rust, etc. are not supported on your target platform?

tialaramex 5y ago
> What if you have a legacy codebase with hundreds of thousands of lines of C you want to maintain and improve? We know that smaller projects have successfully gone on the journey of moving from C to Rust, and they did so the same way you a whale right? One bite at a time. So that might absolutely be a reasonable choice. Things that could make it especially attractive: * There's existing Rust skill set in your team and not checked C * You intend to do other new work in Rust, so this is a skill set you'll be needing anyway. * There is relevant existing work in Rust e.g. today you use a popular C library for processing radar data. You know an equivalent library (or a port of the C library) is available as a Rust crate, if you went with Checked C, either the library isn't checked (partly undoing the good work) or you have to also translate the third party library to checked C. * The main benefit you were looking for is something checked C doesn't care about e.g. freedom from data races is a pretty big deal for concurrent software, and checked C doesn't do that today, and has no plans to do it in future but such races aren't possible in (safe) Rust. Or you wish you had nice built-in features like iterators. * Or the opposite side of the same coin, the main thing you dislike about C is still present in checked C. Maybe you don't like C's silent wrapping overflow, in checked C it's still there, but in Rust you can switch it off. Maybe you don't want the integer fifteen to be silently considered boolean "true" because you thought this programming language was supposed to have type checking, Rust is with you on that, Checked C of course is not.

junon 5y ago

> real safety Spoken by someone who clearly doesn't understand software safety. Neither Rust nor Go are "safe", formally.

rurban 5y ago
Practically neither
RealityVoid 5y ago
What does "formally safe" mean for you here? Are you talking about something like SEL4 that is formally verified? If yes, I wonder how many SW's are out that that are actually formally verified. Also, the problem of formal verification lies not in the language but in the code itself, right? So what would the problem be with Rust or Go?
MaxBarraclough 5y ago
It's true that Rust isn't safe, but the Safe Rust subset is.