5 ms·

Therein lies hubris. I like C as well, but I never kid myself into thinking that discipline and documentation can replace compiler restrictions. I've written l

Therein lies hubris. I like C as well, but I never kid myself into thinking that discipline and documentation can replace compiler restrictions. I've written large codebases in C, sometimes alone, sometimes in a team, and despite DECADES of experience and meticulous attention to detail, I STILL find the same old memory errors in my own code. C cannot be made safe because you are not a god.

throwawaymaths 4y ago
> C cannot be made safe because you are not a god I mean this is demonstrably untrue: SEL4 is written by mere mortals, in C. It's safer than rust, there are formally verified security guarantees that include and go beyond the memory safety of rust. It is the case though that c is an incredibly shitty language to do this sort of static analysis on because for example it's easy to do shenanigans like lexical macros that make the static analyzers job much much harder.
- vore 4y ago
  seL4 also has the whole Isabelle/HOL theorem prover to verify its properties, so it's not quite right to claim it's written in C. If you can claim seL4 is "written in C", you could equally claim that if the Rust compiler emitted C, you're writing a C program -- after all, a static type checker is just a shittier theorem prover.
  - throwawaymaths 4y ago
    This is like saying <insert language with docstrings> is not actually writing in <lang> because you need whatever engine's target language (md, XML, whatever) to compile the docs.
    - avgcorrection 4y ago
      That comparison is nonsensical and you know it. You can delete all the comments and have the same guarantees about what the code does (none). You can’t write a kernel without some formal verification tool and then claim that it adheres to the specification.
      - throwawaymaths 4y ago
        No, but if you change none of the code and only delete the annotations, it will still adhere to the spec.
        avgcorrection 4y ago
        Oh, I see. You said that it is “written in C”, and then later denied the claim that it is also written with that formal verification language. If you delete those annotations it will still adhere to the specification,[1] but it’s still false that it was purely written in C—your statement that “there are formally verified security guarantees” in fact relies on the existence of that proof code. But fine. With that kind of dishonesty I could claim that the Linux kernel is written in nothing: I have compiled it and deleted the source code. Look ma, it’s no-code kernel. [1] Kind of a bummer though that you cannot change any of the C code any more now that the verification code is gone.
        throwawaymaths 4y ago
        Jesus Christ. It's not like most c programs arent already written in another language like make or cmake. By your standards none but the most trivial of hello world a.out c programs are c programs.
- renox 4y ago
  And C is also AFAIK the only language with a formally proven compiler CompCert C. If you used something else, you'd need to trust a lot more code.
  - vore 4y ago
    CompCert doesn't stop you from writing memory unsafe C, of course, just that it won't miscompile your maybe memory unsafe C.
  - aw1621107 4y ago
    > And C is also AFAIK the only language with a formally proven compiler CompCert C. There's CakeML, which is a formally verified subset of Standard ML [0] [0]: https://cakeml.org/popl14.pdf https://cakeml.org/popl14.pdf
  - kobebrookskC3 4y ago
    curiously, seL4 doesn't need to trust the compiler: the assembly is verified to satisfy the abstract specification
- yaantc 4y ago
  Macros are not such a big deal: static analyzers do not work on the source code directly, they work on some intermediate representation usually (often the LLVM IR, for Ikos and Clang SA for example) or parsed source code. Either way, the pre-processing has been done when the analysis starts. Funky macros can still make static analysis more complex by introducing layer(s) of indirection of course.
- kstenerud 4y ago
  You can make any code in any language "safe" when you throw enough resources at it. That's not an argument for safety, nor a rebuttal (unless your goal is to prove someone wrong on the internet).
  - throwawaymaths 4y ago
    Ok but please acknowledge that this comment is explicitly the opposite of "you cannot make c safe ever"
    - kstenerud 4y ago
      It's the exact opposite of "you cannot make language X safer", only if you define that as "given enough time and resources, you could make a proof that your program is correct". But that's not a safe language; that's a safe work. ANY programming work - regardless of language - can be made safe via such expensive means, which puts this square into the space of "argument ad absurdum". You could argue that brainfuck or assembler can be made safe via these means, but everyone would rightly ridicule you for it.
      - throwawaymaths 4y ago
        Maybe I'm crazy but "being a god" is much higher bar than "given enough time and resources, you could make a proof that your program is correct". Moreover, unlike your bf analogy: Sel4 exists, and is in use, and is used in safety-critical applications such as military drones.
- kobebrookskC3 4y ago
  it's also a very limited version of C, without concurrency, dynamic memory allocation, or goto, and you can't even take the address of local variables!
tsimionescu 4y ago
To be fair, religiously running Valgrind, Helgrind, Asan plus a static analyzer will probably do more than most compilers to ensure you don't have memory issues. Probably more than Rust, at least if you find yourself needing some unsafe blocks in your own code or dependencies.
- camel-cdr 4y ago
  If you add to that the discipline of fuzzing, then you've actually got a pretty reasonable workflow. Fuzzing wasn't mentioned in the article but the author does at least to some extended in their project, from what I could tell at a glance.
  - dopidopHN 4y ago
    Sorry. I’m a JVM slob, what is fuzzing in that context of testing code rubustness?
    - aw1621107 4y ago
      Broadly speaking, it's automated generation of test inputs to try to find bugs. For example, fuzzing a parser might involve feeding it random inputs and watching for crashes, hangs, etc. Fuzzers frequently also use instrumentation to try to figure out inputs that will hit more code paths in a more intelligent manner.
      - andai 4y ago
        Here's a fun one: a fuzzer will generate valid JPEGs by starting with random input and mutating it to maximize code coverage. https://news.ycombinator.com/item?id=8571879 https://news.ycombinator.com/item?id=8571879
  - gavinhoward 4y ago
    Author here. I fuzz religiously. I use it to generate lots of my test suite. I love fuzzing. I've added a note about it to the post.
deleted 4y ago
[deleted]
deleted 4y ago
[deleted]
sonofhans 4y ago
> C cannot be made safe because you are not a god. Oh god yes. That should be tattooed on everyone who thinks otherwise. “Ha! Unlike all those other people, who are clearly not as attentive as myself, _I_ never make this type of mistake.”
alpaca128 4y ago
The author doesn't seem to disagree with your view: > The final reason is the only one that justifies my decision: my code will be rewritten in a memory-safe language. [...] It’s my own language. It’s called Yao. > This is the only reason I could justify that decision. All of the other reasons above are excuses. This is the real reason. > You can bet that I do not want to accept liability for a project written in C. It will be rewritten as soon as possible.

throwawaymaths 4y ago

> C cannot be made safe because you are not a god I mean this is demonstrably untrue: SEL4 is written by mere mortals, in C. It's safer than rust, there are formally verified security guarantees that include and go beyond the memory safety of rust. It is the case though that c is an incredibly shitty language to do this sort of static analysis on because for example it's easy to do shenanigans like lexical macros that make the static analyzers job much much harder.

vore 4y ago
seL4 also has the whole Isabelle/HOL theorem prover to verify its properties, so it's not quite right to claim it's written in C. If you can claim seL4 is "written in C", you could equally claim that if the Rust compiler emitted C, you're writing a C program -- after all, a static type checker is just a shittier theorem prover.
- throwawaymaths 4y ago
  This is like saying <insert language with docstrings> is not actually writing in <lang> because you need whatever engine's target language (md, XML, whatever) to compile the docs.
  - avgcorrection 4y ago
    That comparison is nonsensical and you know it. You can delete all the comments and have the same guarantees about what the code does (none). You can’t write a kernel without some formal verification tool and then claim that it adheres to the specification.
    - throwawaymaths 4y ago
      No, but if you change none of the code and only delete the annotations, it will still adhere to the spec.
      - avgcorrection 4y ago
        Oh, I see. You said that it is “written in C”, and then later denied the claim that it is also written with that formal verification language. If you delete those annotations it will still adhere to the specification,[1] but it’s still false that it was purely written in C—your statement that “there are formally verified security guarantees” in fact relies on the existence of that proof code. But fine. With that kind of dishonesty I could claim that the Linux kernel is written in nothing: I have compiled it and deleted the source code. Look ma, it’s no-code kernel. [1] Kind of a bummer though that you cannot change any of the C code any more now that the verification code is gone.
        throwawaymaths 4y ago
        Jesus Christ. It's not like most c programs arent already written in another language like make or cmake. By your standards none but the most trivial of hello world a.out c programs are c programs.
renox 4y ago
And C is also AFAIK the only language with a formally proven compiler CompCert C. If you used something else, you'd need to trust a lot more code.
- vore 4y ago
  CompCert doesn't stop you from writing memory unsafe C, of course, just that it won't miscompile your maybe memory unsafe C.
- aw1621107 4y ago
  > And C is also AFAIK the only language with a formally proven compiler CompCert C. There's CakeML, which is a formally verified subset of Standard ML [0] [0]: https://cakeml.org/popl14.pdf https://cakeml.org/popl14.pdf
- kobebrookskC3 4y ago
  curiously, seL4 doesn't need to trust the compiler: the assembly is verified to satisfy the abstract specification
yaantc 4y ago
Macros are not such a big deal: static analyzers do not work on the source code directly, they work on some intermediate representation usually (often the LLVM IR, for Ikos and Clang SA for example) or parsed source code. Either way, the pre-processing has been done when the analysis starts. Funky macros can still make static analysis more complex by introducing layer(s) of indirection of course.
kstenerud 4y ago
You can make any code in any language "safe" when you throw enough resources at it. That's not an argument for safety, nor a rebuttal (unless your goal is to prove someone wrong on the internet).
- throwawaymaths 4y ago
  Ok but please acknowledge that this comment is explicitly the opposite of "you cannot make c safe ever"
  - kstenerud 4y ago
    It's the exact opposite of "you cannot make language X safer", only if you define that as "given enough time and resources, you could make a proof that your program is correct". But that's not a safe language; that's a safe work. ANY programming work - regardless of language - can be made safe via such expensive means, which puts this square into the space of "argument ad absurdum". You could argue that brainfuck or assembler can be made safe via these means, but everyone would rightly ridicule you for it.
    - throwawaymaths 4y ago
      Maybe I'm crazy but "being a god" is much higher bar than "given enough time and resources, you could make a proof that your program is correct". Moreover, unlike your bf analogy: Sel4 exists, and is in use, and is used in safety-critical applications such as military drones.
kobebrookskC3 4y ago
it's also a very limited version of C, without concurrency, dynamic memory allocation, or goto, and you can't even take the address of local variables!

tsimionescu 4y ago

To be fair, religiously running Valgrind, Helgrind, Asan plus a static analyzer will probably do more than most compilers to ensure you don't have memory issues. Probably more than Rust, at least if you find yourself needing some unsafe blocks in your own code or dependencies.

camel-cdr 4y ago
If you add to that the discipline of fuzzing, then you've actually got a pretty reasonable workflow. Fuzzing wasn't mentioned in the article but the author does at least to some extended in their project, from what I could tell at a glance.
- dopidopHN 4y ago
  Sorry. I’m a JVM slob, what is fuzzing in that context of testing code rubustness?
  - aw1621107 4y ago
    Broadly speaking, it's automated generation of test inputs to try to find bugs. For example, fuzzing a parser might involve feeding it random inputs and watching for crashes, hangs, etc. Fuzzers frequently also use instrumentation to try to figure out inputs that will hit more code paths in a more intelligent manner.
    - andai 4y ago
      Here's a fun one: a fuzzer will generate valid JPEGs by starting with random input and mutating it to maximize code coverage. https://news.ycombinator.com/item?id=8571879 https://news.ycombinator.com/item?id=8571879
- gavinhoward 4y ago
  Author here. I fuzz religiously. I use it to generate lots of my test suite. I love fuzzing. I've added a note about it to the post.

deleted 4y ago

[deleted]

deleted 4y ago

[deleted]

sonofhans 4y ago

> C cannot be made safe because you are not a god. Oh god yes. That should be tattooed on everyone who thinks otherwise. “Ha! Unlike all those other people, who are clearly not as attentive as myself, _I_ never make this type of mistake.”

alpaca128 4y ago

The author doesn't seem to disagree with your view: > The final reason is the only one that justifies my decision: my code will be rewritten in a memory-safe language. [...] It’s my own language. It’s called Yao. > This is the only reason I could justify that decision. All of the other reasons above are excuses. This is the real reason. > You can bet that I do not want to accept liability for a project written in C. It will be rewritten as soon as possible.