4 ms·

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

by 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.
        foldr 2y ago
        >Firstly, I never said sound methods ought to be used. You kind of did say this: "soundness for some critical properties is absolutely warranted". It seemed clear that you were taking memory safety to be one of the "critical properties". >if you cannot rely on it then your system effectively has no guarantees of any kind. In the real world you cannot rely on anything absolutely. All guarantees are probabilistic. Rust, for example, does not have a formally verified compiler, so you cannot be absolutely sure that your provably memory safe code will actually compile down to memory safe machine code (or indeed to machine code that does what it's supposed to do in any other respect). Does that mean we need to go off and formally verify the Rust compiler because otherwise none of our systems will have guarantees of any kind? If it doesn't, then note that you are making exactly the same kind of cost/benefit analysis that pron is talking about. It's easy to list lots of things that systems 'should' do. In a realistic scenario there is a budget of time/effort/attention/money.
- pron 2y ago
  > but that soundness for some critical properties is absolutely warranted A particular technique can only be warranted for practical use by its cost effectiveness, not on principle. If you justify soundness for a property because that property is at the root of 90% of bugs then you should still prefer another technique that reduces 90% of bugs more cheaply. It doesn't matter what technique is used to reduce that amount of bugs. I understand the argument that nothing but soundness covers the full gamut of mistakes people make in practice around memory safety, but at the end of the day of those mistakes amount to 800 bugs in your program out of 1000, then you should still prefer a technique that reduces 800 bugs -- the same or different ones of equal severity -- for cheaper. Indeed, there are situations where sound methods are cost-effective, and that is where they tend to be popular.
  - naasking 2y ago
    > If you justify soundness for a property because that property is at the root of 90% of bugs then you should still prefer another technique that reduces 90% of bugs more cheaply. It doesn't matter what technique is used to reduce that amount of bugs. This is a false equivalence, as not all bugs are the same and so cannot be trivially equated in this fashion. Memory safety violations permit classes of bugs of significantly higher severity than other types of bugs. Your off-hand disclaimer of "the same or different ones of equal severity" doesn't mean anything, because you cannot predict the severity or scope of even trivial memory unsoundness, so your heuristic arguments of preferring lower cost methods simply don't work. A memory safety bug can range from something as simple as "a process crashed" in the best case, to "we lost control of all our servers worldwide and all of our customer data was compromised". So I would summarize my dispute with your position as follows: 1. Memory safety is NOT an underwhelming property. Arguably, all other properties of your program derive from memory safety. 2. If you have to use an unsafe language that permits violating memory safety, say for performance reasons, and you have any kind of attack surface, then ensuring memory safety is important. Probably more important than most other properties you otherwise think are important due to #1. 3. Heuristic approaches to memory safety do not necessarily entail a reduction in the severity of bugs and/or security vulnerabilities. Arguments that you eliminated 80% of trivial memory unsoundness is simply not compelling if it leaves all of the subtle, more dangerous ones in place. 4. The long history of security vulnerabilities is a main driver in the interest in soundness among researchers, contra your claims that that this obsession has no association with real-world needs. I think I'll just leave it at that.

by pron 2y ago

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.
      - foldr 2y ago
        >Firstly, I never said sound methods ought to be used. You kind of did say this: "soundness for some critical properties is absolutely warranted". It seemed clear that you were taking memory safety to be one of the "critical properties". >if you cannot rely on it then your system effectively has no guarantees of any kind. In the real world you cannot rely on anything absolutely. All guarantees are probabilistic. Rust, for example, does not have a formally verified compiler, so you cannot be absolutely sure that your provably memory safe code will actually compile down to memory safe machine code (or indeed to machine code that does what it's supposed to do in any other respect). Does that mean we need to go off and formally verify the Rust compiler because otherwise none of our systems will have guarantees of any kind? If it doesn't, then note that you are making exactly the same kind of cost/benefit analysis that pron is talking about. It's easy to list lots of things that systems 'should' do. In a realistic scenario there is a budget of time/effort/attention/money.
pron 2y ago
> but that soundness for some critical properties is absolutely warranted A particular technique can only be warranted for practical use by its cost effectiveness, not on principle. If you justify soundness for a property because that property is at the root of 90% of bugs then you should still prefer another technique that reduces 90% of bugs more cheaply. It doesn't matter what technique is used to reduce that amount of bugs. I understand the argument that nothing but soundness covers the full gamut of mistakes people make in practice around memory safety, but at the end of the day of those mistakes amount to 800 bugs in your program out of 1000, then you should still prefer a technique that reduces 800 bugs -- the same or different ones of equal severity -- for cheaper. Indeed, there are situations where sound methods are cost-effective, and that is where they tend to be popular.
- naasking 2y ago
  > If you justify soundness for a property because that property is at the root of 90% of bugs then you should still prefer another technique that reduces 90% of bugs more cheaply. It doesn't matter what technique is used to reduce that amount of bugs. This is a false equivalence, as not all bugs are the same and so cannot be trivially equated in this fashion. Memory safety violations permit classes of bugs of significantly higher severity than other types of bugs. Your off-hand disclaimer of "the same or different ones of equal severity" doesn't mean anything, because you cannot predict the severity or scope of even trivial memory unsoundness, so your heuristic arguments of preferring lower cost methods simply don't work. A memory safety bug can range from something as simple as "a process crashed" in the best case, to "we lost control of all our servers worldwide and all of our customer data was compromised". So I would summarize my dispute with your position as follows: 1. Memory safety is NOT an underwhelming property. Arguably, all other properties of your program derive from memory safety. 2. If you have to use an unsafe language that permits violating memory safety, say for performance reasons, and you have any kind of attack surface, then ensuring memory safety is important. Probably more important than most other properties you otherwise think are important due to #1. 3. Heuristic approaches to memory safety do not necessarily entail a reduction in the severity of bugs and/or security vulnerabilities. Arguments that you eliminated 80% of trivial memory unsoundness is simply not compelling if it leaves all of the subtle, more dangerous ones in place. 4. The long history of security vulnerabilities is a main driver in the interest in soundness among researchers, contra your claims that that this obsession has no association with real-world needs. I think I'll just leave it at that.