Hi Sam, since I don't know how to enforce a projection-only restriction and you are not suggesting that proxies trap ===, I'm not sure what we're arguing about. I'll just clarify some points inline.
On Sun, Dec 8, 2013 at 4:21 PM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu>wrote: > 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> > > >> 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. > I think this means we agree on the point I started with: Since JS is committed to === as a test, and since you agree proxies should not be able to trap ===, it is too late for JS or E to be a candidate for a language in which contracts can be true projections. New languages taking some of these lessons into account, like perhaps Pyret, might be able to escape the dilemma without loss of useful functionality (performance aside) by avoiding the inclusion of any equality comparison operation more precise than join. > > 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. > When I link a linear algebra package into some small program I'm writing, I may wonder "what if one of the algorithms in here doesn't terminate". But I rarely take steps to protect the parts of my code that call into it from the possibility of this non-return. My calling code is too simple anyway to know how to cope with an attempted "recovery" from such non-termination anyway. I may try to choose a linear algebra package that has a reputation for being efficient, but I certainly don't try to protect my caller from the possibility of inefficiency. When I engineer a large system consisting of many such programs, I do worry about continued efficient operation of the overall system if one of these components goes astray. However, that doesn't mean I'm fine with the linear algebra package deleting my files, even if the small program I'm linking it into is authorized to do so. Different worries make sense at different granularities. > > >> 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. > I didn't understand this. > > 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. > You are correct. That's why the actual scenario described by the paper involves five vats (Alice, Bob, Contract Host, $ Issuer, Stock Issuer). Different worries at different granularities. > > 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. > You're correct that this is a weakness of this as an example for the current argument. But I'll just note that the application itself is designed to be more robust, given the expected division into five vats. > > Sam > -- Text by me above is hereby placed in the public domain Cheers, --MarkM _______________________________________________ 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
