If you don't wish to defend the claim that types do not carry permissions, then leave it. I'm personally interested in the answer since I've never heard this position before. Since types encode program properties, they can represent and enforce any discretionary or mandatory policy we'd like, in principle. There are plenty of papers using types to enforce high-level security policies [1]. Even Java's simple generics can enforce read/write policies on file paths [2].
I do agree with Jonathan that ocap shouldn't necessarily be a goal for BitC, although it certainly would be nice. If your language is good enough to use in low-level applications, people will use it in high-level applications. Sandro [1] http://www.dsi.unive.it/~michele/Papers/concur04.pdf [2] I've done this in C#, apologies if the Java is incorrect: interface Permission {} interface R extends Permission {} interface W extends Permission {} interface RW extends R,W {} final class Path<? extends Permission> { internal string path; } class File { public static <T extends R> Stream OpenRead(Path<T> file) { ... } public static <T extends W> Stream OpenWrite(Path<T> file) { ... } } On 08/07/2014 12:59 AM, Matt Oliveri wrote: > Sandro, I have to ask how important it is to you that I continue > responding to your points and questions. It seems like you at least > understand what I'm saying, although you clearly have a very different > opinion about it. I don't need to convince you and I'd really rather > stop discussing it now. All this back and forth doesn't seem to be > changing anyone's minds. It may be that I'm still abusing a few terms, > but that's not the heart of it. I think if we really want to fully > explain ourselves at this point, the best way would be to go through a > number of examples in detail. But I don't see why that's worth the > trouble, since this issue is not an issue for BitC in the near term, > or maybe ever. > > On Tue, Jul 8, 2014 at 12:05 AM, Sandro Magi <[email protected]> wrote: >> On 07/07/2014 9:16 PM, Matt Oliveri wrote: >>> It's rights amplification only when we consider static types to >>> provide information about permissions or authority. >> In an object-oriented language, you are permitted to send objects >> messages. In a typed object oriented language, you are permitted to send >> messages only to objects that can receive those messages (as defined by >> some criteria). Types must carry permissions, in principle. >> >>> 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. >> My view yields strictly more precise information at every point in the >> program, so I disagree that neither view subsumes the other. >> >> Certainly they have inconsistent ontologies, but your view doesn't >> capture the subjective experience of programming in Java. Dynamic >> message sends don't look anything like native static message sends for >> one, so Java is not like any other dynamically typed language in >> existence. And to argue that some operations are disallowed, but they >> aren't disallowed by some system of "permissions" seems bizarre >> (consider refinements of Java's type system like adding typestate where >> the state of a file handle is in the type -- now types suddenly do >> define permissions?). >> >>> Indeed, it is because downcast would otherwise provide uncontrolled rights >>> amplification that we must not consider static types as limiting authority. >>> [...] My position allows static types, ambient reflection and downcast, and >>> the object-capability model to coexist. >> I don't understand. Nothing about my perspective forbids a capability >> secure language from having some forms of rights amplification, as long >> as they are "sufficiently benign". For instance, some capability >> languages include rights amplification in the form of EQ. >> >> Language security is not necessarily all or nothing, but often a sliding >> scale, ie. less rights amplification = more secure by default. No one >> ever said "any rights amplification = insecure". Java isn't capability >> insecure simply because some forms of rights amplification are >> available, it's insecure because it violates the connectivity postulate, >> and the encapsulation postulate given unrestricted reflection. >> >> We can still recognize that Joe-E is capability secure, even though it >> includes rights amplification in the form of downcasts and (restricted) >> reflection. This isn't inconsistent with my view in any way, we simply >> recognize the rights amplification for what it is. >> >> Sandro > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
