On Mon, Jul 7, 2014 at 7:10 PM, Sandro Magi <[email protected]> wrote: > On 07/07/2014 3:26 PM, Matt Oliveri wrote: >> Using Haskell as an imperative language with >> frequent calls to unsafePerformIO would be very annoying and >> unnatural. Using Java in the way I describe is not at all unnatural. > > You're changing the goalposts. You said that Java's type system does not > guarantee that you can't call a method if it doesn't belong to a type. > In fact, the only way to attempt to call a method that doesn't belong to > the type is via reflection,
In general, yes. You need reflection when the method to call is not statically known. But otherwise downcast suffices, which is part of the reason why the style in question is often not as annoying in practice as it theoretically can be. > and contrary to what you just claimed, > method invocation via reflection is quite unnatural in Java. Well the syntax is bad, so it is quite annoying. I'm not sure that makes it unnatural though. I think of it as finishing the job that checked downcast started, for those cases when the method to call is not statically known. If our disagreement ultimately just boils down to opinions about sensible ways to use Java though, then let's just agree to disagree. >> As far as I can tell, no one has >> given evidence that my way of looking at Java is unequivocally wrong. > > What is wrong are the specific claims that downcasting is not rights > amplification, and that an object's dynamic type defines the permission > set (and not the static type in scope). No other claims were disputed > other than these security claims. Yes. Those are precisely the claims I'm talking about. > Your claim that "downcast should not be considered rights > amplification", at least in Java, is simply wrong. The definition of > rights amplification is intensional: the combination of two or more > authorities yields a new authority greater than can be achieved via any > combination of its individual parts. For downcast, we combine an object > instance of type Foo and an ambient type descriptor of type Bar <: Foo, > to yield an instance of Bar which exposes more permissions than either > Foo or the Bar type descriptor provide individually in the given scope. > That's a clear rights amplification. Ditto for reflection. It's rights amplification only when we consider static types to provide information about permissions or authority. When we do not, an instance of the subtyping relation cannot be viewed as a source of authority, so one cannot say a downcast is combining that authority with an object. Indeed, it is because downcast would otherwise provide uncontrolled rights amplification that we must not consider static types as limiting authority. My point of view is simply "OK. That's still consistent." > Your position on permission sets is also perfectly clear, namely that > the dynamic type of a Java object defines its permission set because, > like dynamically typed languages, we can invoke methods dynamically via > reflection (or by downcasting) instead of being constrained to the type > in scope at the time; thus, the capability patterns used in such > dynamically typed languages are needed for unrestricted Java. No one > disagreed with this last point. Our disagreement has been over > classifying Java using capability terminology: > > You: in Java, objects are dynamic types which define permissions sets. > Me: in Java, scoped static types define permission sets, and two > rights amplification primitives are > available, downcasting and reflection. I'm very happy to see that we are at least understanding each other. I was getting worried. > Is the latter not a more precise and useful conceptualization? Technically you can't say which of the two is more precise. Because they contradict each other, neither can be a refinement of the other. (So I guess I should ensure you realize that I'm also saying static types _do not_ define permission sets.) I think they're both useful conceptualizations. I agree that thinking of static types as defining permissions is more useful for BitC. My reason is that with BitC, reflection is unwanted baggage anyway. > We know > immediately that writing a class loader that forbids programs that call > reflection APIs or use downcasting instructions yields a typed > capability secure runtime. That's an interesting point. Has this actually been done? (I accept the point as valid either way though.) > We also know that the presence of these > rights amplification primitives are what necessitates the use of > dynamically typed capability patterns. Yes. And I fully acknowledge that their presence makes secure programming more error-prone, and more of a pain in the butt. But equipped only with your point of view, the primitives would seem outright unacceptable. That's the key difference I wanted to communicate. > What utility does your position provide that is not captured by my > position? I've already asked this, but you never answered that I can recall. My position allows static types, ambient reflection and downcast, and the object-capability model to coexist. Waterken used this combination. I said that, and I thought it was implicit that I consider it a useful combination. Sorry. But more generally, I think my position is helpful _whenever_ runtime type checks are found to be inevitable in most or all cases, such as Waterken unmarshaling data and method calls from a network connection. This is because when static types are required to provide an upper bound on permissions, any dynamic checks you could use to discover the dynamic type must be explicitly permitted by the static type. This perspective seems more appropriate when implementing or extending the reflection system itself, not when using it as part of the ambient system. If you need runtime checks all over the place, putting that in the types is just noise. I suppose in the long run what you'd want is a Shap/Sandro-style system expressive enough to model a Java-style system, and then use it without a syntax nightmare. But is BitC going to be that expressive? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
