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