On 05/07/2014 1:10 PM, Matt Oliveri wrote: > It may be alarming that a static type system would > essentially tell you nothing about security, but that was not the goal > of Java's type system.
That it was not the goal of Java's type system is not to say that aligning security reasoning with type reasoning *should not* be the goal of a type system (or a programming language). That's the point whole of equating downcasting with rights amplification: we recognize grant/revoke/amplify operations happening at the type level like what happens at the value level. Of course it's not strictly necessary given the Turing tarpit, but we already knew that given E, Joule, etc. That other languages have no type enforcement like typed languages isn't relevant either. The question is, given type checking, does the type system impede or assist reasoning about the flow of permissions? With ambient downcasting, the answer is unquestionably "impede". > No, casts do not change an object. The set of methods it implements > stays the same. The permissions it provides stays the same. Whether casting mutates the object isn't relevant to whether the full set of permissions are usable in a given context. When a file handle is closed, you no longer have permission to read/write to it. Why should we consider a change in context at the type level, eg. casting, to not modify permissions, but changes at the value level, eg. file.Close(), to modify permissions? 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? > 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. > 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. 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? Sandro _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
