4 ms·

> to prove something underwhelming, like memory safety or other similarly low-level properties. After all that hard work you'd only end up at the same point whe

> to prove something underwhelming, like memory safety or other similarly low-level properties. After all that hard work you'd only end up at the same point where most of the software world -- which is already using memory safe languages -- is today. I'm not sure why this is underwhelming. You reduce your hardware cost budget by using a low-level language while ensuring you don't suffer from the single greatest source of security vulnerabilities in real programs. These have significant real-world impact.

pron 2y ago
> I'm not sure why this is underwhelming. You reduce your hardware cost budget by using a low-level language while ensuring you don't suffer from the single greatest source of security vulnerabilities in real programs. There are two problems with your statement. First, it's unclear whether what you save pays for what you gain. Second, the participation of memory unsafety in vulnerabilities is not binary. If you can cheaply reduce memory unsafety by 95%, that doesn't mean that paying a high price for the remaining 5% is worth it. Yes, memory safety is the single greatest source of security vulnerabilities in some languages (it is not in general, but then again most software is already written in memory-safe languages), but once you've already reduced it by 95% it no longer is. (BTW, I'm not even sure that soundly eliminating the 95% is clearly worth it compared to alternatives, but that's a separate discussion). There's this obsession with soundness that is undoubtedly interesting to researchers of sound methods, but isn't actually justified by the real-world needs of software (sometimes it is and sometimes it isn't, but when and by how much is something that can only be answered empirically; it isn't something that can be simply asserted). Software correctness is at least as much art as it is a science, and ignoring the empirical aspects that make it into an art and focusing only on the aspects that are science because that's where things are clear-cut doesn't make those aspects disappear. At the end of the day someone has a budget and they need to spend it in the way that yields to most correct software; how that is best done is an empirical question. After all, you started with an empirical finding about memory safety being a leading source of some bugs, but it simply doesn't follow that total memory safety soundness is the answer to the empirical question that we need answered. Soundness is clear-cut and mathematical (and that's also why it's attractive [1]); sadly, software correctness is the very opposite. We must continue researching sound methods, but if anyone thinks -- knowing what we know now -- that this should be the main focus and the best answer to software correctness then I think they are misjudging the nature of the problem. [1]: Ironically, people who focus on soundness love proofs, yet they try to skirt around the proofs of the futility of soundness by resorting to empirical -- though untested -- claims.
- naasking 2y ago
  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).

pron 2y ago

> I'm not sure why this is underwhelming. You reduce your hardware cost budget by using a low-level language while ensuring you don't suffer from the single greatest source of security vulnerabilities in real programs. There are two problems with your statement. First, it's unclear whether what you save pays for what you gain. Second, the participation of memory unsafety in vulnerabilities is not binary. If you can cheaply reduce memory unsafety by 95%, that doesn't mean that paying a high price for the remaining 5% is worth it. Yes, memory safety is the single greatest source of security vulnerabilities in some languages (it is not in general, but then again most software is already written in memory-safe languages), but once you've already reduced it by 95% it no longer is. (BTW, I'm not even sure that soundly eliminating the 95% is clearly worth it compared to alternatives, but that's a separate discussion). There's this obsession with soundness that is undoubtedly interesting to researchers of sound methods, but isn't actually justified by the real-world needs of software (sometimes it is and sometimes it isn't, but when and by how much is something that can only be answered empirically; it isn't something that can be simply asserted). Software correctness is at least as much art as it is a science, and ignoring the empirical aspects that make it into an art and focusing only on the aspects that are science because that's where things are clear-cut doesn't make those aspects disappear. At the end of the day someone has a budget and they need to spend it in the way that yields to most correct software; how that is best done is an empirical question. After all, you started with an empirical finding about memory safety being a leading source of some bugs, but it simply doesn't follow that total memory safety soundness is the answer to the empirical question that we need answered. Soundness is clear-cut and mathematical (and that's also why it's attractive [1]); sadly, software correctness is the very opposite. We must continue researching sound methods, but if anyone thinks -- knowing what we know now -- that this should be the main focus and the best answer to software correctness then I think they are misjudging the nature of the problem. [1]: Ironically, people who focus on soundness love proofs, yet they try to skirt around the proofs of the futility of soundness by resorting to empirical -- though untested -- claims.

naasking 2y ago
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).