3 ms·

As far as I see the bug primarily lies within this function here... resolv/res_send.c https://github.com/bminor/glibc/blob/master/resolv/res_send.c#L952 https:/

by cnvogel 11y ago

As far as I see the bug primarily lies within this function here... resolv/res_send.c https://github.com/bminor/glibc/blob/master/resolv/res_send.c#L952 https://github.com/bminor/glibc/blob/master/resolv/res_send.... Lines 952 ... 1389 [=~450 lines of code], with more than a dozen of variables holding random state. Think about the complexity you have with all the conditionals and loops, often copying and pasting similar conditions with (xx1 && xx2) variants. While discusions about the relative merits of Rust, C, Ocaml, Intercal are fun, with enough dedication you can write unauditable/unreviewable code in any language. Even though you might avoid memory corruption, you still can't prove that such kind of code does anything correct.

cmrx64 11y ago
You sure can prove that any correct code does something correct, but you can never prove something about a program outside of a machine-checked formal proof.
- nly 11y ago
  The problem is that it's far more difficult to prove what code doesn't do than what it does. I can write a function to do X, Y and Z, and I can show, through observation and aggressive testing, that it does indeed do X,Y and Z....but its a lot harder to prove that it only does X,Y and Z and nothing else. Memory safety is just one expression of this problem.
  - cmrx64 11y ago
    In the typical framework (refinement), if you prove your function does X, Y, and Z, then it does exactly X, Y, and Z. Please don't take my comment out of the context of formal, machine-checked proofs. It is hard, and that's my point.
sbov 11y ago
Sure. But not doing something correct is far different from a security vulnerability.
chillingeffect 11y ago
Gah! As a medical device programmer, that code is a horrors how! Ifdefs, gotos, 400 lines long, scarce comments, so many arguments passed, single letter variable name, stack declarations all over the place, etc. I could go on about the helper functions in that file, lack of argument descriptions, lack of references to standards. It all reeks of a lack of structure. I'm surprised to see the Internet runs on that. Thank you for sharing that. It's really nothing to do with C, I agree. Just a drastic lack of coding standards. Don't people refactor key code after functionality is proven and tests developed?!

by cnvogel 11y ago

cmrx64 11y ago

You sure can prove that any correct code does something correct, but you can never prove something about a program outside of a machine-checked formal proof.

nly 11y ago
The problem is that it's far more difficult to prove what code doesn't do than what it does. I can write a function to do X, Y and Z, and I can show, through observation and aggressive testing, that it does indeed do X,Y and Z....but its a lot harder to prove that it only does X,Y and Z and nothing else. Memory safety is just one expression of this problem.
- cmrx64 11y ago
  In the typical framework (refinement), if you prove your function does X, Y, and Z, then it does exactly X, Y, and Z. Please don't take my comment out of the context of formal, machine-checked proofs. It is hard, and that's my point.

sbov 11y ago

Sure. But not doing something correct is far different from a security vulnerability.

chillingeffect 11y ago

Gah! As a medical device programmer, that code is a horrors how! Ifdefs, gotos, 400 lines long, scarce comments, so many arguments passed, single letter variable name, stack declarations all over the place, etc. I could go on about the helper functions in that file, lack of argument descriptions, lack of references to standards. It all reeks of a lack of structure. I'm surprised to see the Internet runs on that. Thank you for sharing that. It's really nothing to do with C, I agree. Just a drastic lack of coding standards. Don't people refactor key code after functionality is proven and tests developed?!