On Sun, Dec 8, 2013 at 5:58 PM, Mark Miller <erig...@gmail.com> wrote: > On Fri, Dec 6, 2013 at 5:00 PM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> > wrote: >> >> On Wed, Dec 4, 2013 at 5:59 PM, Mark Miller <erig...@gmail.com> wrote: >> > Good, I think we're converging on what the important sub-problem is: >> > building an abstraction mechanism that enables the open-ended expression >> > of >> > projections, but not the expression of non-projections. My previous >> > statements about join were premised on such a projection-only >> > abstraction. >> > But I mistakenly thought that we could build it by adapting the E and >> > Joe-E >> > auditor logic. Sam is right that we can't. Some of Cormac's work on >> > trace-monitoring temporal contracts might be the answer, or at least a >> > place >> > to start. >> > >> > Once we have such an open-ended projection-only abstraction, then all >> > these >> > questions about equality become interesting and pressing. >> >> I'm unconvinced that this is genuinely a problem that needs solving. >> In particular, I don't think that given such a projection-only >> abstraction, any of the questions about equality are easier. > > > In a system in which behavioral contracts are necessarily projections, then > turning a contract on cannot change observed behavior up to contract-check > failure, resource exhaustion, or non-termination. Modulo "necessarily", Phil > stated this goal earlier in this thread. My understanding is that the > behavioral contract folks generally share this goal, but you would probably > know better than I. In any case, I also think this goal is valuable. I think > the remaining argument is about "necessarily".
The problem is that (a) "up to contract-check failure, resource exhaustion, or non-termination", is much too weak for many contexts, and (b) that in real systems (such a ES6 as deployed in Node or browsers) all three of those qualifications can be observed by code that then proceeds to behave arbitrarily differently. Behavioral contracts in practice generally treat projections as a design idea, not a requirement on final implementations, precisely for this reason. > Since one interposes contracts in order to find bugs, we don't need to > assume malice (about which more below) in order for the "necessarily" to be > valuable. Contracts can be buggy as well. Indeed, invariants in software are useful for many things other than avoiding malice. I've even published on the possibility of bugs in contracts. But this doesn't mean that more invariants are always the right choice. >> For example, if we had one, that wouldn't reduce our desire to have a >> pointer-equality predicate for performance, given which none of the >> invariants about programs that you think you have in the presence of >> projection-only abstractions are actually invariants. > > > Actually, the invariants I'm worried about cannot be violated by such a high > performance pointer equality comparison, whether or not we have a > projection-only abstraction mechanism. The high performance pointer > comparison cannot be trapped by proxies anyway, and so cannot be misled by > non-projecting proxies. Indeed. My point is that if you want to have such an operation in your language, then any behavioral invariants given by a projections-only restriction are lost anyway. >> Additionally, I'm still unconvinced that "is a projection" is a useful >> heuristic for "I should be willing to trust this unknown code". > > > Whenever you hear yourself saying "trust" without qualifying it what you > trust it with, you should be suspicious. In this case, given a > projection-enforcing mechanism I believe works (again, up to contract > failure, resource exhaustion, or non-termination), then I would be willing > to trust code constrained to run under this mechanism to be a projection. But this is just begging the question. In particular, what we want to know is whether I'd be ok with replacing one object with a projection of that object. Being sure that it's a projection doesn't answer that question. > > >> >> In >> particular, termination and resources are both real concerns. When >> the question is "should I synchronously invoke this unknown untrusted >> code in my heap and address space", I'd want a lot stronger guarantee >> than "is a projection". > > > Also, whenever you hear yourself drawing a dichotomy between full trust and > no trust, with no middle ground, you should again be suspicious. I have > never met a piece of code I fully trust, in the sense of being 100% > confident that it will execute in ways that I expect and in service of my > interests, even when I have written the code and even when it has been > subject to automated formal verification. > > For most code I invoke, my confidence is even lower. Virtually every bit of > library code I routinely call is code I did not write or vet, and which has > been subject to no formal verification. I wish to run as much of such code > as possible under POLA, the principle of least authority, in order to limit > the damage it can do if its is malicious, buggy, or subvertable. It is not > even close to feasible to run every separately written or partially trusted > bit of code in separate processes only asynchronously coupled. If I compose > together such separately trusted bits of code so that one synchronously > calls another, as I do all the bloody time as does everyone else, I am not > primarily worried about resource exhaustion or lack of termination. Those > kinds of misbehavior are readily apparent, and people would rapidly report > those bugs and stop using those libraries until those bugs are fixed. First, "resource use" and "resource exhaustion" are not at all the same. Second, we've seen so many security vulnerabilities that boil down to denial of service via unexpected resource consumption that I find your statement quite remarkable. >> Third, the ability to handle failure is a genuine semantic problem. > > Out of context, sure. In context, I either do not understand what you mean > or I do not understand the relevance. Can you expand? Thanks. The idea of projections is that they map certain behavior to \bottom. However, this usually means "raises an exception" in actual software. But exceptions and other forms of failure can be handled in JS, Racket, and every other software system we might consider (even if we have to do something drastic with multiple threads or processes, or async failure handling, etc). This means, of course, that what seemed like a projection from a local point of view becomes just another change in behavior from a higher-level point of view. The alternatives here seem to be giving up the idea that projections are a useful semantic categorization, or giving up failure handling in a fundamental way. All practical contract systems that I'm familiar with have taken the first option. >> Finally, if the expression of non-projections in proxies that produce >> true when compared to the underlying object is a problem, then there >> ought to be some some program that demonstrates this problem; some >> attack that can be demonstrated. But I don't think we've seen one yet >> in this discussion. > > > > On lines 2, 3, and 4 of Figure 2 of > <http://research.google.com/pubs/pub40673.html> is the code > > var makeEscrowPurseP = Q.join(srcPurseP ! makePurse, dstPurseP ! > makePurse); > var escrowPurseP = makeEscrowPurseP ! (); > > If we instead used here an equality operation with the behavior you explain, > say SAQ for Sam's EQ, to write > > var mep1 = srcPurseP ! makePurse; > var mep2 = dstPurseP ! makePurse; > if (SEQ(mep1, mep2)) { > var escrowPurseP = mep1 ! (); > > then we would be vulnerable to "Alice could return a dishonest purse that > acknowledges deposit without transferring anything. Alice would then obtain > Bob’s stock for free." If instead that last line above used mep2, "then Bob > could steal Alice’s money during phase 1." (Quotes here from page 17) I don't think this is the case for any proxies writable under the original proposal as described by Andreas, and it certainly isn't the case if we implemented these proxies using Racket's proxying system, which implements a version of this equality system. If we assume that the `deposit` fields of purses are immutable, then a proxy for a purse must produce a value which is equal to the underlying value (this is already the semantics of ES6 proxies). If we extend this equailty as Andreas proposes, all we have now is a proxy for the underlying function. So now we aren't be able to cheat the exchange, unless the projection-only variant can as well. Further, it looks to me like a proxy that implements the projection-only restriction you describe could still break the invariants here, by simply causing resource exhaustion after one transfer, but before the other transfer, has happened. I'm not an expert on how this code is supposed to work, though, so I might well be wrong. Finally, I'll note that this program demonstrates precisely the tension with error handling I pointed out above. If we genuinely had projections in proxies, then one of the parties could cause the whole application to fail. But this application depends, fundamentally, on failure handling to re-deposit funds if the transaction fails. Genuine projections would invalidate a crucial assumption of your code. Sam _______________________________________________ dev-tech-js-engine-internals mailing list dev-tech-js-engine-internals@lists.mozilla.org https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
