3 ms·

> so there is no plausible reason for you to infer that I was talking about Heartbleed. Except that Heartbleed is the only OpenSSL bug I've heard of :) Also, I

by pron 7y ago

> so there is no plausible reason for you to infer that I was talking about Heartbleed. Except that Heartbleed is the only OpenSSL bug I've heard of :) Also, I don't know who Kurt Roeckx is. > there's a lot of evidence from software project metrics that the cost of modifying software can easily exceed the cost of rewriting it But we're not talking about arbitrary modification, but about, at worst, fixing undefined behavior, which requires only local modifications (or Rust wouldn't be able to prevent that either). As an ultimate reduction, you could choose to rewrite the software in C and still use sound static analysis to show lack of undefined behavior. > which means that the cost of reproducing its existing behavior in well-understood code is unbounded. Yes, but that still doesn't mean that a rewrite is cheaper. Also, while your conclusion is correct, your statement of Rice's theorem is inaccurate: it's impossible to always tell what ever piece of software would do. It's certainly possible to tell what some software would do, at least in some cases, or writing software would be impossible to begin with. BTW, if you're interested in the theory of software correctness, you might be interested in this blog post of mine, that lists relevant results: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity

kragen 7y ago
I appreciate your clarification! Indeed, I didn't mean it was impossible to tell what any software would do in any situation, only some software (in practice, nearly all) in some situations. The contrary would imply that not only writing software but also running it would be impossible. Your blog post looks very interesting indeed! I will read it with care. I do think there's a subtle point about modifying software. Not just any modification of the software that lacks undefined behavior will do; we want a modification that preserves the important aspects of the original software’s behavior. Not only is this easy to get wrong—as shown spectacularly by the OpenSSL bug (which you've presumably looked up by now), but also, for example, by the destruction of the first Ariane 5—but there is no guarantee that it can be done with purely local modifications, even if the final safety property you wanted to establish can be established with chains of local reasoning. I do agree that sound static analysis of C that is written to make that analysis tractable is just as effective as rewriting in Rust. Not only can such analysis show the absence of undefined behavior, it can show arbitrary correctness properties, including those beyond the reach of Rust’s type system. Probably the strongest example of this kind of analysis is seL4, although now its proofs verify not only the C but also the machine code, thus eliminating the compiler from the TCB.
- pron 7y ago
  Yes, I looked up the OpenSSL bug you referred to, and I think it's quite unusual. I'm not sure what those lines were exactly, but from the description it seems like it was intended to read uninitialized memory, something that (safe) Rust won't let you do, either. Also, it's probably wrong even in C, but it worked. So yeah, touching code in any way is not always 100% safe, but my point was just that sound static analysis is still cheaper than a rewrite, as it requires far less modification. As to seL4, it isn't exactly similar to sound static analysis, as the work was extremely costly. All of seL4 is 1/5 the size of jQuery and it's taken years of work. But it also includes functional verification, not just memory safety. In fact, it is among the largest programs ever functionally verified to that extent, and yet it was about 3 orders of magnitude smaller than oridnary business software, roughly the same verification gap we've had for decades. We don't yet know how to functionally verify software (end-to-end, like seL4) of any size that's not very small. Anyway, Rust offers a much more limited form of assurance, and sound static analysis tools offer the same, and at a lower cost for existing codebases.

by pron 7y ago

kragen 7y ago

I appreciate your clarification! Indeed, I didn't mean it was impossible to tell what any software would do in any situation, only some software (in practice, nearly all) in some situations. The contrary would imply that not only writing software but also running it would be impossible. Your blog post looks very interesting indeed! I will read it with care. I do think there's a subtle point about modifying software. Not just any modification of the software that lacks undefined behavior will do; we want a modification that preserves the important aspects of the original software’s behavior. Not only is this easy to get wrong—as shown spectacularly by the OpenSSL bug (which you've presumably looked up by now), but also, for example, by the destruction of the first Ariane 5—but there is no guarantee that it can be done with purely local modifications, even if the final safety property you wanted to establish can be established with chains of local reasoning. I do agree that sound static analysis of C that is written to make that analysis tractable is just as effective as rewriting in Rust. Not only can such analysis show the absence of undefined behavior, it can show arbitrary correctness properties, including those beyond the reach of Rust’s type system. Probably the strongest example of this kind of analysis is seL4, although now its proofs verify not only the C but also the machine code, thus eliminating the compiler from the TCB.

pron 7y ago
Yes, I looked up the OpenSSL bug you referred to, and I think it's quite unusual. I'm not sure what those lines were exactly, but from the description it seems like it was intended to read uninitialized memory, something that (safe) Rust won't let you do, either. Also, it's probably wrong even in C, but it worked. So yeah, touching code in any way is not always 100% safe, but my point was just that sound static analysis is still cheaper than a rewrite, as it requires far less modification. As to seL4, it isn't exactly similar to sound static analysis, as the work was extremely costly. All of seL4 is 1/5 the size of jQuery and it's taken years of work. But it also includes functional verification, not just memory safety. In fact, it is among the largest programs ever functionally verified to that extent, and yet it was about 3 orders of magnitude smaller than oridnary business software, roughly the same verification gap we've had for decades. We don't yet know how to functionally verify software (end-to-end, like seL4) of any size that's not very small. Anyway, Rust offers a much more limited form of assurance, and sound static analysis tools offer the same, and at a lower cost for existing codebases.