On Sun, Dec 8, 2013 at 10:15 PM, Mark Miller <erig...@gmail.com> wrote: > 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.
I didn't say that proxies shouldn't trap `===`, just that we often also want a pointer equality operation. Of course, making `===` run fast on current web programs is an additional constraint, but not one that we're considering here. > 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. It's not obvious to me how `join` helps here, especially since (a) your paper defines `join` only as an operation on promises, and (b) `join` itself uses `===` (really Object.is). Perhaps Pyret as a language aimed at teaching can make a different compromise here, but even Haskell has eventually needed to use pointer equality in some places (such as compare-and-swap). >> > 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. I genuinely don't understand the point you're trying to make here. I've described in this thread a genuine issue where we needed, in Racket, to constrain the use of proxies because the handlers might use too many resources during a critical section. There are two scenarios we might be considering -- one in which we (in principle) know the code that we're linked with, and one in which we don't. In the former, we're in situation you describe with a linear algebra package, but in that scenario we can do many other things, such as expect our clients to use a restricted sublanguage to write proxy handlers with. The other scenario, which is what your ESOP paper is about, for example, is the interesting one, where genuinely unknown code cannot be trusted to use such a sublanguage. My point is that in this second scenario, if we can't trust the code to write in a projection-only sublanguage, we also can't trust the code to not use too many resources and thus result in some other important invariant violation. >> >> 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. My claim is if two objects compare as equal under the system Andreas proposed to start this thread, where one is a proxy for the other, then the proxy cannot in fact cheat the exchange (unless there's some underlying vulnerability, or a vulnerability that a projection-only proxy would also expose). If you're still unsure what I mean, perhaps you can just write what you think the dishonest proxy would look like. >> 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. I'm not sure what you're saying I'm correct about, but it looks to me like the contract host runs unknown code in its vat. In particular, `Object.is` a local operation, so we must be comparing two local values in `join`, which are untrusted (otherwise we wouldn't need to compare them). Is that not the case? And if not, how would any proxy issues make any difference whatsoever to this example? >> >> >> 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. I contend that _all_ examples will have a similar form -- if you have untrusted code that might misbehave, then you must be prepared for that code to fail to meet its obligations (if it can't actually fail, then you could have trusted it). But then you need error handling, meaning that error behavior from projections that aborts the entire computation is inappropriate. Note that even if we defer the error handling to a separate vat, we've just pushed the problem somewhere else. 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
