3 ms·

Here's the problem with this argument: the long history of security vulnerabilities demonstrates that people are complete shite at estimating both the likelihoo

Here's the problem with this argument: the long history of security vulnerabilities demonstrates that people are complete shite at estimating both the likelihood of security problems, and the severity and scope of any unaddressed security problems. So the only empirical data that we know to be absolutely reliable is this long history of colossal human failure on estimating this risk. That's why I don't trust your argument one bit, and thus, that's why soundness properties are important, because they take flawed human judgment completely out of the equation. Which isn't to say that I want soundness proven for all properties no matter the cost, but I do take issue with your outright dismissal of soundness. There are low-hanging fruit like memory safety that handle the vast majority of these problems, and so unquestionably have a great bang for your buck.

pron 2y ago
But you are again trying to make a non-binary problem into a binary one. We will never be able to soundly verify all the properties we need. That dream is just getting further and further away. 100% correctness is unattainable. So given that, let's say we could only ever hope for 99%. In that case it doesn't matter whether we get rid of 99% of problems using unsound methods or soundly get rid of the cause of 99% of the problems -- the end result is the same. What matters is the cost of getting to that 99% correctness, not the technique. My choice of technique -- sound or otherwise -- is driven by its cost-effectiveness, not principle. I don't care if you're using a sound technique or an unsound one; I only care about how much it costs to give me the most correctness I need and can get within my budget. > I do take issue with your outright dismissal of soundness I don't dismiss soundness. I dismiss the focus on soundness out of principle rather than effectiveness. That myopic focus is grounded in the preferences of researchers of sound methods; it is not grounded in the study of software correctness.
- naasking 2y ago
  > But you are again trying to make a non-binary problem into a binary one. We will never be able to soundly verify all the properties we need. I literally said I did not want soundness for all properties no matter the cost, but that soundness for some critical properties is absolutely warranted. The binary for some properties is absolutely there and completely justifiable based on the reasoning I laid out (memory safety in particular).
  - foldr 2y ago
    >The binary for some properties is absolutely there and completely justifiable based on the reasoning I laid out As a spectator in this thread, I do not see an argument for this conclusion in any of your posts. You're just insisting on it rather than arguing based on data.
    - naasking 2y ago
      > You're just insisting on it rather than arguing based on data. So the unbelievably long history of memory safety vulnerabilities is not an argument for distrusting human judgment on the prevalence or scope of possible unsafety in one's program, and thus an argument for memory soundness. This is literally the argument I presented here [1]. In your mind, this is not an argument based on data? [1] https://news.ycombinator.com/item?id=40378315 https://news.ycombinator.com/item?id=40378315
      - foldr 2y ago
        It's not an argument for always insisting on eliminating 100% of memory safety bugs via sound methods regardless of budget. That requires a more elaborate argument than just "memory safety bugs are really bad and therefore we should eliminate all of them with certainty".
        naasking 2y ago
        > It's not an argument for always insisting on eliminating 100% of memory safety bugs via sound methods regardless of budget. Firstly, I never said sound methods ought to be used. Secondly, I also never said that memory safety bugs always must be eliminated without qualification, I specifically couched this in a context of security. In that context, ensuring memory safety is absolutely critical. For instance, scientific simulations of the weather or something don't have such considerations. The whole problem of memory unsoundness is that you cannot predict the scope or severity of unsoundness. They are simply not like other "bugs", so the heuristic arguments the OP presented simply don't work. All other desirable properties derive from memory soundness, so if you cannot rely on it then your system effectively has no guarantees of any kind. So yes, any system with any kind of attack surface should absolutely ensure memory safety by any means necessary. If you need to use an unsafe language for performance reasons, as per my initial reply, then isolate the unsafety to trusted kernels (like checked arrays) that can be verified by model checking or other proof techniques.

pron 2y ago

But you are again trying to make a non-binary problem into a binary one. We will never be able to soundly verify all the properties we need. That dream is just getting further and further away. 100% correctness is unattainable. So given that, let's say we could only ever hope for 99%. In that case it doesn't matter whether we get rid of 99% of problems using unsound methods or soundly get rid of the cause of 99% of the problems -- the end result is the same. What matters is the cost of getting to that 99% correctness, not the technique. My choice of technique -- sound or otherwise -- is driven by its cost-effectiveness, not principle. I don't care if you're using a sound technique or an unsound one; I only care about how much it costs to give me the most correctness I need and can get within my budget. > I do take issue with your outright dismissal of soundness I don't dismiss soundness. I dismiss the focus on soundness out of principle rather than effectiveness. That myopic focus is grounded in the preferences of researchers of sound methods; it is not grounded in the study of software correctness.

naasking 2y ago
> But you are again trying to make a non-binary problem into a binary one. We will never be able to soundly verify all the properties we need. I literally said I did not want soundness for all properties no matter the cost, but that soundness for some critical properties is absolutely warranted. The binary for some properties is absolutely there and completely justifiable based on the reasoning I laid out (memory safety in particular).
- foldr 2y ago
  >The binary for some properties is absolutely there and completely justifiable based on the reasoning I laid out As a spectator in this thread, I do not see an argument for this conclusion in any of your posts. You're just insisting on it rather than arguing based on data.
  - naasking 2y ago
    > You're just insisting on it rather than arguing based on data. So the unbelievably long history of memory safety vulnerabilities is not an argument for distrusting human judgment on the prevalence or scope of possible unsafety in one's program, and thus an argument for memory soundness. This is literally the argument I presented here [1]. In your mind, this is not an argument based on data? [1] https://news.ycombinator.com/item?id=40378315 https://news.ycombinator.com/item?id=40378315
    - foldr 2y ago
      It's not an argument for always insisting on eliminating 100% of memory safety bugs via sound methods regardless of budget. That requires a more elaborate argument than just "memory safety bugs are really bad and therefore we should eliminate all of them with certainty".
      - naasking 2y ago
        > It's not an argument for always insisting on eliminating 100% of memory safety bugs via sound methods regardless of budget. Firstly, I never said sound methods ought to be used. Secondly, I also never said that memory safety bugs always must be eliminated without qualification, I specifically couched this in a context of security. In that context, ensuring memory safety is absolutely critical. For instance, scientific simulations of the weather or something don't have such considerations. The whole problem of memory unsoundness is that you cannot predict the scope or severity of unsoundness. They are simply not like other "bugs", so the heuristic arguments the OP presented simply don't work. All other desirable properties derive from memory soundness, so if you cannot rely on it then your system effectively has no guarantees of any kind. So yes, any system with any kind of attack surface should absolutely ensure memory safety by any means necessary. If you need to use an unsafe language for performance reasons, as per my initial reply, then isolate the unsafety to trusted kernels (like checked arrays) that can be verified by model checking or other proof techniques.