4 ms·

Even if that were the case, you'd be working very hard, wasting your assurance budget, to prove something underwhelming, like memory safety or other similarly l

by pron 2y ago

Even if that were the case, you'd be working very hard, wasting your assurance budget, 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. On the other hand, if you were to spend your budget how they do (rather, should do) with modern unsound methods, you would likely end up not noticeably worse than if you did both. Remember, the goal isn't to prove some technical property, but to find the greatest number of bugs that matter to you -- those you believe are most dangerous for your particular program or library -- within budget. Researchers are often interested in discovering what properties they can verify, but practitioners care about the functional properties they need to verify. Deductive methods (including type systems) are particularly myopic in that regard precisely because they're so limited in their effectiveness to begin with. People interested in those particular techniques are rightfully very excited when they discover they can do a little bit more than they previously could, even if what they can do is still so far behind what practitioners need (and are getting elsewhere with more practical methods). In general, the gap between research and what practitioners think it might mean for their industry work is large in this field and greatly misunderstood by practitioners.

naasking 2y ago
> 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).
zozbot234 2y ago
> to prove something underwhelming, like memory safety or other similarly low-level properties. Memory safety is table stakes. If you can't even prove memory safety, your program doesn't really have any well-defined semantics after all. > you'd only end up at the same point where most of the software world -- which is already using memory safe languages -- is today. Which is another way of saying that the modern software world is already using lightweight formal methods in an end-to-end fashion. Type checking is one such use of lightweight formal methods. Unsound methods can be useful to surface possible bugs quickly and efficiently, much like fuzzing does. But they're not a kind of verification - they provide no guarantee of correctness.
- pron 2y ago
  > Which is another way of saying that the modern software world is already using lightweight formal methods in an end-to-end fashion. Sure, but only for specific properties that are inductive. Most properties that programmers care about aren't. It is precisely this kind of extrapolation from one property to another that doesn't work. > But they're not a kind of verification - they provide no guarantee of correctness. Correct 1. nothing else does either (again, sound formal verification only works in very limited situations -- either in the property they guarantee or the program they can guarantee it in -- and is falling further and further behind what the software world needs) and 2. unlike for algorithms, a "guarantee" is not and cannot be the bar for real software running on physical hardware, as you cannot guarantee the real behaviour of a software system even if the algorithm is guaranteed to be correct. Unlike an algorithm, a software system is ultimately a physical object, not a mathematical one. To crudely oversimplify, you don't care about any confidence beyond the probability of a bit flip. In other words, you're pointing out that the current state-of-the-art in the field is not as good as something we don't (perhaps can't) have and don't need to begin with.
  - zozbot234 2y ago
    > Sure, but only for specific properties that are inductive. Most properties that programmers care about aren't. Yes but in practice, we keep finding ways of making more such interesting properties "inductive" by placing appropriate restrictions on how the program can be designed. This is how the Rust borrow checker works, at a high level.
roca 2y ago
As a practitioner but also a small-time CS researcher, I don't expect verifying that small Rust libraries use 'unsafe' correctly will "waste my assurance budget". On the cost side: we don't know yet how hard it will be to formally verify small Rust libraries that wrap unsafe code in safe abstractions. That's partly because we don't even know exactly what the specification is that unsafe Rust code has to satisfy. But once we've settled on that and built good proof assistant tools, I think the work will usually be pretty easy, because most of these libraries are fundamentally quite simple and small, even including all their dependencies. You correctly identified compositionality as a key issue. Fortunately, verifying correct use of 'unsafe' is inherently compositional: knowing nothing but the code of the library and its dependencies, we must prove that the necessary safety properties hold in all possible contexts. On the benefit side: proving that libraries do not undermine Rust's safety guarantees is important, and the importance grows with the popularity of the library. And of course those guarantees aren't just "memory safety" but data-race-freedom and the general "mutable-xor-shared" property --- the importance of which is the subject of the OP here!
- pron 2y ago
  > You correctly identified compositionality as a key issue. Fortunately, verifying correct use of 'unsafe' is inherently compositional Yes, it is an inductive property. Sadly, not a very powerful one. > On the benefit side: proving that libraries do not undermine Rust's safety guarantees is important, and the importance grows with the popularity of the library. It is only important if you take it as an axiom that all programs must be proven to be memory-safe. That may be an axiom accepted by some Rust fans, but it is obviously not an axiom of software. What software needs are methods that reduce dangerous bugs (where "dangerous" means different things for different programs) in the most cost-effective way. It may well be the case that, say, soundly eliminating 95% of bugs caused by memory unsafety and using the rest of the budget on unsound methods is more effective than spending it on eliminating the last 5% of those particular bugs. Software's needs do not currently justify complete sound memory safety at all costs, so the question of cost is still the most relevant one. There is no justification to focus on one cause of bugs just because it can be soundly eliminated. > And of course those guarantees aren't just "memory safety" but data-race-freedom and the general "mutable-xor-shared" property --- the importance of which is the subject of the OP here! Neither of these are worthwhile enough to move the needle. This is precisely what I mean by the myopic focus on what can be done as opposed to what needs to be done. If the gap is 10 orders of magnitude, narrowing it by 1 doesn't have a big impact, unless it were completely free, which it isn't.
tialaramex 2y ago
> Remember, the goal isn't to prove some technical property, but to find the greatest number of bugs that matter to you No. And this has been a particular challenge for poor C++. If we prove a property then the property holds, but if we just found and meticulously fixed 846 of the crucial holes in our system, the bad guys exploit #847 to break in just the same. Is there a #848? #849? Maybe. We as an industry are significantly under-delivering and we ought to take responsibility for that. I think you're correct about the gap but wrong about what the gap is. WUFFS exists today. Lots of people on HN have written or even are writing codecs in a general purpose programming language and don't even realise that's a terrible idea. "I'm pretty careful" substitutes for a machine checked proof and the results can be seen easily.
- pron 2y ago
  > And this has been a particular challenge for poor C++. If we prove a property then the property holds, but if we just found and meticulously fixed 846 of the crucial holes in our system, the bad guys exploit #847 to break in just the same. Is there a #848? #849? Maybe. That is an unattainable goal for most properties we care about, particularly if they're as complex as "an unauthorised user cannot obtain some information". Even a complete and total elimination of all memory safety bugs and all concurrency bugs won't get you anywhere near that goal (and you can verify that for yourself by looking at common server vulnerabilities). I should have said that the attainable goal is etc..
  - naasking 2y ago
    > particularly if they're as complex as "an unauthorised user cannot obtain some information". Even a complete and total elimination of all memory safety bugs and all concurrency bugs won't get you anywhere near that goal Actually that's not really true. If you take that as a base and remove ambient authority, then you have capability security which does get you as close to fulfilling that property as is possible to achieve. I'd say that's pretty near that goal.
    - pron 2y ago
      I disagree, for multiple reasons: 1. You need to verify that all the sensitive data is indeed guarded with the appropriate capabilities. 2. You need to verify that the capability objects are created only after proper authorisation. 3. You need to verify that the capability objects cannot escape their relevant context. 4. You need to verify that the data is not accessible by "extra-program" means, e.g. the file containing the data may be read via a dumb directory-injection attack. Some simple sound techniques by the programming language can help with 3 and a part of 2, but not the rest. Indeed the current #1 top vulnerability [1] is a misconfigured or incorrect access control. [1]: https://owasp.org/www-project-top-ten/ https://owasp.org/www-project-top-ten/
deleted 2y ago
[deleted]

by pron 2y ago

naasking 2y ago

> 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).

zozbot234 2y ago

> to prove something underwhelming, like memory safety or other similarly low-level properties. Memory safety is table stakes. If you can't even prove memory safety, your program doesn't really have any well-defined semantics after all. > you'd only end up at the same point where most of the software world -- which is already using memory safe languages -- is today. Which is another way of saying that the modern software world is already using lightweight formal methods in an end-to-end fashion. Type checking is one such use of lightweight formal methods. Unsound methods can be useful to surface possible bugs quickly and efficiently, much like fuzzing does. But they're not a kind of verification - they provide no guarantee of correctness.

pron 2y ago
> Which is another way of saying that the modern software world is already using lightweight formal methods in an end-to-end fashion. Sure, but only for specific properties that are inductive. Most properties that programmers care about aren't. It is precisely this kind of extrapolation from one property to another that doesn't work. > But they're not a kind of verification - they provide no guarantee of correctness. Correct 1. nothing else does either (again, sound formal verification only works in very limited situations -- either in the property they guarantee or the program they can guarantee it in -- and is falling further and further behind what the software world needs) and 2. unlike for algorithms, a "guarantee" is not and cannot be the bar for real software running on physical hardware, as you cannot guarantee the real behaviour of a software system even if the algorithm is guaranteed to be correct. Unlike an algorithm, a software system is ultimately a physical object, not a mathematical one. To crudely oversimplify, you don't care about any confidence beyond the probability of a bit flip. In other words, you're pointing out that the current state-of-the-art in the field is not as good as something we don't (perhaps can't) have and don't need to begin with.
- zozbot234 2y ago
  > Sure, but only for specific properties that are inductive. Most properties that programmers care about aren't. Yes but in practice, we keep finding ways of making more such interesting properties "inductive" by placing appropriate restrictions on how the program can be designed. This is how the Rust borrow checker works, at a high level.

roca 2y ago

As a practitioner but also a small-time CS researcher, I don't expect verifying that small Rust libraries use 'unsafe' correctly will "waste my assurance budget". On the cost side: we don't know yet how hard it will be to formally verify small Rust libraries that wrap unsafe code in safe abstractions. That's partly because we don't even know exactly what the specification is that unsafe Rust code has to satisfy. But once we've settled on that and built good proof assistant tools, I think the work will usually be pretty easy, because most of these libraries are fundamentally quite simple and small, even including all their dependencies. You correctly identified compositionality as a key issue. Fortunately, verifying correct use of 'unsafe' is inherently compositional: knowing nothing but the code of the library and its dependencies, we must prove that the necessary safety properties hold in all possible contexts. On the benefit side: proving that libraries do not undermine Rust's safety guarantees is important, and the importance grows with the popularity of the library. And of course those guarantees aren't just "memory safety" but data-race-freedom and the general "mutable-xor-shared" property --- the importance of which is the subject of the OP here!

pron 2y ago
> You correctly identified compositionality as a key issue. Fortunately, verifying correct use of 'unsafe' is inherently compositional Yes, it is an inductive property. Sadly, not a very powerful one. > On the benefit side: proving that libraries do not undermine Rust's safety guarantees is important, and the importance grows with the popularity of the library. It is only important if you take it as an axiom that all programs must be proven to be memory-safe. That may be an axiom accepted by some Rust fans, but it is obviously not an axiom of software. What software needs are methods that reduce dangerous bugs (where "dangerous" means different things for different programs) in the most cost-effective way. It may well be the case that, say, soundly eliminating 95% of bugs caused by memory unsafety and using the rest of the budget on unsound methods is more effective than spending it on eliminating the last 5% of those particular bugs. Software's needs do not currently justify complete sound memory safety at all costs, so the question of cost is still the most relevant one. There is no justification to focus on one cause of bugs just because it can be soundly eliminated. > And of course those guarantees aren't just "memory safety" but data-race-freedom and the general "mutable-xor-shared" property --- the importance of which is the subject of the OP here! Neither of these are worthwhile enough to move the needle. This is precisely what I mean by the myopic focus on what can be done as opposed to what needs to be done. If the gap is 10 orders of magnitude, narrowing it by 1 doesn't have a big impact, unless it were completely free, which it isn't.

tialaramex 2y ago

> Remember, the goal isn't to prove some technical property, but to find the greatest number of bugs that matter to you No. And this has been a particular challenge for poor C++. If we prove a property then the property holds, but if we just found and meticulously fixed 846 of the crucial holes in our system, the bad guys exploit #847 to break in just the same. Is there a #848? #849? Maybe. We as an industry are significantly under-delivering and we ought to take responsibility for that. I think you're correct about the gap but wrong about what the gap is. WUFFS exists today. Lots of people on HN have written or even are writing codecs in a general purpose programming language and don't even realise that's a terrible idea. "I'm pretty careful" substitutes for a machine checked proof and the results can be seen easily.

pron 2y ago
> And this has been a particular challenge for poor C++. If we prove a property then the property holds, but if we just found and meticulously fixed 846 of the crucial holes in our system, the bad guys exploit #847 to break in just the same. Is there a #848? #849? Maybe. That is an unattainable goal for most properties we care about, particularly if they're as complex as "an unauthorised user cannot obtain some information". Even a complete and total elimination of all memory safety bugs and all concurrency bugs won't get you anywhere near that goal (and you can verify that for yourself by looking at common server vulnerabilities). I should have said that the attainable goal is etc..
- naasking 2y ago
  > particularly if they're as complex as "an unauthorised user cannot obtain some information". Even a complete and total elimination of all memory safety bugs and all concurrency bugs won't get you anywhere near that goal Actually that's not really true. If you take that as a base and remove ambient authority, then you have capability security which does get you as close to fulfilling that property as is possible to achieve. I'd say that's pretty near that goal.
  - pron 2y ago
    I disagree, for multiple reasons: 1. You need to verify that all the sensitive data is indeed guarded with the appropriate capabilities. 2. You need to verify that the capability objects are created only after proper authorisation. 3. You need to verify that the capability objects cannot escape their relevant context. 4. You need to verify that the data is not accessible by "extra-program" means, e.g. the file containing the data may be read via a dumb directory-injection attack. Some simple sound techniques by the programming language can help with 3 and a part of 2, but not the rest. Indeed the current #1 top vulnerability [1] is a misconfigured or incorrect access control. [1]: https://owasp.org/www-project-top-ten/ https://owasp.org/www-project-top-ten/

deleted 2y ago

[deleted]