Separation Logic(cacm.acm.org)
cacm.acm.org
Separation Logic
https://cacm.acm.org/magazines/2019/2/234356-separation-logic/fulltext
26 comments
Sorry, cannot read articles with horrible type setting like that. Unsharp code examples, missing symbols in the text, ...
Just for you buddy https://dl.acm.org/doi/pdf/10.1145/3211968
Much better now.
Wake me when they prove Chrome is correct.
A recent (and in a lot of cases more useful) trend is showing that programs are incorrect (buggy) rather than correct.
Specifically, there is a recent an analogue of SL, called incorrectness separation logic (ISL) that i designed to prove the presence of bugs, i.e. detect bugs:
https://link.springer.com/chapter/10.1007/978-3-030-53291-8_...
The main advantage of ISL is that it uses under-approximation, unlike original SL which uses over-approximation. That is to say, SL is used to show ALL program behaviours are correct, and in the process of doing so we may over-approximate the set of program behaviours. By contrast, ISL is used to show there are SOME incorrect (buggy) program behaviours.
ISL was implemented in a tool called PulseX at Facebook and shown to be a very scalable approach (comparable with and in some cases better than the state-of-the art Infer tool):
https://dl.acm.org/doi/abs/10.1145/3527325
Specifically, there is a recent an analogue of SL, called incorrectness separation logic (ISL) that i designed to prove the presence of bugs, i.e. detect bugs:
https://link.springer.com/chapter/10.1007/978-3-030-53291-8_...
The main advantage of ISL is that it uses under-approximation, unlike original SL which uses over-approximation. That is to say, SL is used to show ALL program behaviours are correct, and in the process of doing so we may over-approximate the set of program behaviours. By contrast, ISL is used to show there are SOME incorrect (buggy) program behaviours.
ISL was implemented in a tool called PulseX at Facebook and shown to be a very scalable approach (comparable with and in some cases better than the state-of-the art Infer tool):
https://dl.acm.org/doi/abs/10.1145/3527325
That's a ridiculously high bar to set before you recognize any progress being made.
What? Are you saying that me literally sleeping until an impossible thing happens is too high a bar? I should say so!
I probably meant it figuratively, huh? What I am saying after having keynoted at a Microsoft formal methods conference (as a critic) and after playing with TLS+ (which was educational) is that formal verification will make little impact on commercial systems because such systems are obliged to be built with inherently buggy components.
I am happy to acknowledge that progress is happening, yet the ultimate source of trouble is human ambition and impatience. How do you solve that?
I probably meant it figuratively, huh? What I am saying after having keynoted at a Microsoft formal methods conference (as a critic) and after playing with TLS+ (which was educational) is that formal verification will make little impact on commercial systems because such systems are obliged to be built with inherently buggy components.
I am happy to acknowledge that progress is happening, yet the ultimate source of trouble is human ambition and impatience. How do you solve that?
Not going to happen; Chrome is such a huge pile of code that it's pretty much guaranteed to be incorrect.
Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we're told which assumptions/preconditions need to be proved first)
Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we're told which assumptions/preconditions need to be proved first)
Great to see this discussion here. Concerning
"pretty much guaranteed to be incorrect"
... as it happens, SL (and infer) can be used to prove this too :) though that is more recent.
https://dl.acm.org/doi/pdf/10.1145/3527325
"pretty much guaranteed to be incorrect"
... as it happens, SL (and infer) can be used to prove this too :) though that is more recent.
https://dl.acm.org/doi/pdf/10.1145/3527325
> Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we're told which assumptions/preconditions need to be proved first)
That's not what constructive logic means.
That's not what constructive logic means.
The last part about preconditions/assumptions isn't specific to constructive logic; it's about backwards-chaining proof tactics; for example, applying the `ring` tactic in Coq will tell us to prove that the given structure is a ring (see the Errors section of https://coq.inria.fr/refman/addendum/ring.html#concrete-usag... )
The reason constructive logic is nice for this is the first part: we'll be given a counterexample, or a total algorithm for generating counterexamples, etc. (depending on the nature of the statement and its quantifiers). This is preferable to classical logics, where an automated prover might tell us "false", but we have no idea why.
The reason constructive logic is nice for this is the first part: we'll be given a counterexample, or a total algorithm for generating counterexamples, etc. (depending on the nature of the statement and its quantifiers). This is preferable to classical logics, where an automated prover might tell us "false", but we have no idea why.
Yes - to elaborate, a constructive logic is a logic without P or not P. This doesn't have much to do with whether a tool can tell you what obligations you haven't proven. The separation logic based provers I've used have all had excluded middle.
You'd better wake up sooner: "Static analysis with SL has matured to the point where it has been applied industrially in the Facebook Infer program analyzer, an open source tool used at Facebook, Mozilla, Spotify, Amazon Web Services, and other companies (www.fbinfer.com)."
Facebook Infer is now just an ordinary unsound static analysis tool where some of the original analyses are inspired by separation logic. It doesn't actually prove any facts about the program being analyzed using separation logic.
It's a common trend in industry. Here is this brilliant logical tool for reasoning about programs, in this case Hoare triples' descendent separation logic. Now let's figure out how we can keep our programmers from having to learn how to use it!
A logical description of what a piece of code does is evidently too much to ask of a working programmer. Instead, the prevailing dream is to just write code and then have some other code figure out what the first code actually does. Surely the sufficiently smart compiler is almost at hand.
This used to frustrate me and I suppose to some minor extent it still does. However, most of my frustration was relieved by Dijkstra's distinction between program correctness and program pleasantness. With vanishingly rare exceptions, revealed preferences show that industry could not care less about correctness. After all, it's pleasantness that determines success in the marketplace. Plenty of critically incorrect code nevertheless makes its owners billions. Sure, maybe all your private medical data and credit history got leaked, but here have a voucher for $10 a month worth of dark web monitoring for a year. I don't like this model, but at least it's in some sense rational.
A logical description of what a piece of code does is evidently too much to ask of a working programmer. Instead, the prevailing dream is to just write code and then have some other code figure out what the first code actually does. Surely the sufficiently smart compiler is almost at hand.
This used to frustrate me and I suppose to some minor extent it still does. However, most of my frustration was relieved by Dijkstra's distinction between program correctness and program pleasantness. With vanishingly rare exceptions, revealed preferences show that industry could not care less about correctness. After all, it's pleasantness that determines success in the marketplace. Plenty of critically incorrect code nevertheless makes its owners billions. Sure, maybe all your private medical data and credit history got leaked, but here have a voucher for $10 a month worth of dark web monitoring for a year. I don't like this model, but at least it's in some sense rational.
I think it's that most, or nearly every code, is actually not critical and failure is ok. I would argue that code for every part of facebook is actually not critical. Of course it's bad if there's an error or the feed of instagram is actually not correct, or you can't send a message right now. But it's not critical, facebook will survive and the cost of eliminating those bugs is just not worth it. After all, unit tests only reduce the possibility of failure to an acceptable level. Amazons cloud had outages and amazon survived. It just about economics. The cost of hiring the right developers, writing and maintaining the code etc.
Writing code is not about solving a problem perfectly but delivering solutions under economic constraints.
Writing code is not about solving a problem perfectly but delivering solutions under economic constraints.
> Here is this brilliant logical tool for reasoning about programs, in this case Hoare triples' descendent separation logic. Now let's figure out how we can keep our programmers from having to learn how to use it!
That's a good description of the Rust borrow checker, which is intended to be a sound analysis but a lot more restrictive than full separation logic.
That's a good description of the Rust borrow checker, which is intended to be a sound analysis but a lot more restrictive than full separation logic.
Yes I think we need less abstraction. Best illustrated with RPC, when we try to treat it the same as local call we lose so much information. We want to reason about latency and failure so we need our language to represent this information and allow us to apply our logic to it.
It, like so many things, is a balancing act. How much does the working programmer need to know about binaries, symbol tables, platform calling conventions etc etc to use a debugger well? The author of a debugger absolutely has to, the user less so except in specialized circumstances. Allowing users to get at the inside-baseball bits of a tool without disenfranchising people that are focused on other areas of work seems ideal to me. RPC is unreasonable in that it makes unfair assumptions about the nature of the network. Seems to me insisting that programmers learn a good chunk of separation logic before knowing if a tool that uses the same internally is unreasonable in a like way. But a tool that _allows_ users that get some utility from it to learn separation logic if they need, now that's a well-designed tool.
If you can't use a tool without being an expert in it, the only people that will use that tool are experts and the techniques die out as the experts do.
If you can't use a tool without being an expert in it, the only people that will use that tool are experts and the techniques die out as the experts do.
I agree. Experience has taught me to hesitate to speak in absolutes absent a hard proof, but until I see a counter-example I'll believe that all abstractions are more or less leaky. Even pure functional programs have the observable side effect of using CPU time.
It's a difficult problem that I believe has no globally optimal solution. However, I think there's fruitful research to be done in better recognizing what ought to be abstracted and what ought not to be in some domain specific sort of way. Informally we do this already. For example it's relatively common knowledge that one shouldn't leak username validity via timing attacks, so in that case the processing time cannot be abstracted away.
It's a difficult problem that I believe has no globally optimal solution. However, I think there's fruitful research to be done in better recognizing what ought to be abstracted and what ought not to be in some domain specific sort of way. Informally we do this already. For example it's relatively common knowledge that one shouldn't leak username validity via timing attacks, so in that case the processing time cannot be abstracted away.
1. This "unsoundness" was the subject of extensive (endless) discussions on the Infer team (as you can imagine). This spurred some theory and there are some precise theorems associated with how parts of Infer work. E.g., racerd has some theorems and over a period of a year saw no observed false negatives, so I'm not sure it's accurate to say that it's "just an ordinary unsound static analysis" (see https://dl.acm.org/doi/10.1145/3290370 and references).
2. Apart from that, to me, if logic inspires (part of) the design of an analyzer, that's perhaps more valuable than using logic to judge it after the fact, as analysis design is hard; and this is true even if analyzer ends up following part of the spirit if not the letter of the logic.
I believe I get where you care coming from, though, and appreciate your perspective. :)
2. Apart from that, to me, if logic inspires (part of) the design of an analyzer, that's perhaps more valuable than using logic to judge it after the fact, as analysis design is hard; and this is true even if analyzer ends up following part of the spirit if not the letter of the logic.
I believe I get where you care coming from, though, and appreciate your perspective. :)
Oh wow, this thread has attracted some notable participants. Much respect for your work. While you're here I've been wondering about applying all this stuff to the problem of having an unknown computing environment and bootstrapping a sane workspace on top of it. That might not make sense. I'm at a loss for how to explore the literature. Something like ubiquitous/pervasive computing with service discovery combined with foundational proof carrying code, certified compilers, verified stacks, etc.
Wow nice to bump into you here sir. Keep fighting the good fight.
It's possible but yes that would be a waste of an individual or group's time given the current techniques. It could be crowd sourced or automated with machine learning.
https://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.a...
This special topics course was held shortly before John Reynolds passed away.
(If you're bored, you can also see other things we have hosted on the same platform, including Deep Reinforcement Learning, Intro to ML, and the Computer Science Department holiday party :)