I was never trying to say that Java is a good object-capability language. Just that it can technically be used as one, and that when doing so, downcast should not be considered rights amplification. I completely agree that the BitC point of view is superior for secure coding in most cases.
There is something to be said for type systems that let you say something about code without changing the semantics of that code. Maybe not in Java's case, but in general. Subtyping where types give you partial information about an object without changing its semantics is useful. Abstract types which restrict the interface of objects thereby changing its semantics are also useful. I'm just trying to make darn sure we understand the right way to think about both. On Sun, Jul 6, 2014 at 12:56 AM, Sandro Magi <[email protected]> wrote: > What is Java's type system if not a security analysis enforcing the > methods one is permitted to invoke on a reference in a given context? > How is this permissions analysis really that different from runtime > permission checks based on file handle state? Java's type system guarantees that you can call a method if it belongs to the type. It doesn't guarantee that you can't call a method if it doesn't belong to a type. So I wouldn't call it security analysis, except to the extent that MethodNotFoundException is considered a vulnerability. It's not a very interesting one. Again, this is just the way it is; I'm not defending it. >> Assuming all those methods are public, this is technically incorrect, >> because reflection would allow calling the RWFile's Write method >> regardless of the static type. >> Without reflection or downcast, you're right. In OCaml, you're right. >> Taking away reflection results in an object system with a very different >> feel. > > Why? The number of Java/C# programs that actually use reflection is > small. Joe-E still feels like Java. Waterken used reflection a lot. Maybe if it weren't for that they _would've_ gone Shap's way, tamed away reflection, and restricted downcast. Anyway I think a BitC-style type system is better for most things, so it's OK to focus on that for now. But sooner or later, someone's gonna want a more dynamic feeling system with reflection, and Java shows that this doesn't rule out useful types, as long as you understand the difference. >> In your example in the presence of ambient downcast, clearly something >> is wrong if you didn't mean to grant write permission. You and Shap >> say allowing downcast was wrong. I'm saying passing a RWFile was >> wrong. > > I'm saying the idea that types should *not* be exploited to reason about > security properties is counterproductive. If we acknowledge that types > enhance reasoning about program properties, then security properties are > simply a particular subset of those properties. Yes I agree. But a type system shouldn't be considered defective just because it doesn't enforce your favorite kind of property. And if enforcing that property with types gets in the way of something you want to do, then it can reasonably be considered the wrong trade off. It kind of seems like you guys are thinking "Using types for security is always better than using types along with reflection, so who cares about Java? Nobody needs something like Java's types!" Because Shap, and now you keep misunderstanding what I'm saying, which is merely that something like Java is a reasonable alternative. Not the right alternative for your case, but an alternative worth understanding. > We want tools that enhance our dismal security reasoning, but I don't > see how your position advances this agenda. What purpose does your > approach serve? How would you declare and check the security policy > that's violated by passing in a RWFile, as above? It seems you would > need a completely different static analysis. In what way would such a > language be superior to the Joe-E-like language Shap and I are thinking > about, in which the type visible in scope fully defines the security > context of every operation, and which simply uses standard type theory? I hope it's now clear that I am not proposing a type system like Java's to improve the state of security. And I don't think BitC is Joe-E-like, because what I've been saying about types being lower bounds applies to Joe-E too for most types. Joe-E added some marker interfaces which give you useful security-relevant information, but there's a fixed set of those. Like you said, Joe-E still feels like Java. BitC is totally different. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
