Unstructured casting considered harmful to security

Unstructured casting (e.g. Java, C#, C++, etc.) can be harmful to security.

Structured casting consists of the following:

1: Casting self to an interface implemented by this Actor
2: Upcasting
  a) an Actor of an implementation type to the interface type of the implementation
  b) an Actor of an interface type to the interface type that was extended 
3: Conditional downcasting of an Actor of an interface type to an extension interface type.  (An implementation type cannot be downcast because there is nothing to which to downcast.)

Claim: All other casting is unstructured and should be prohibited.
Note that this means that an implementation cannot be subtyped although an implementation can use other implementations for modularity.

Edit: The above was clarified as a result of a perceptive FriAM comment by Marc Stiegler

Actor DepositOnlyAccount[initialBalance:Euro] uses SimpleAccount[initialBalance]｡ 
 implements Account using
     deposit[anAmount] →
        ⍠Account_⨀SimpleAccount.deposit[anAmount]¶
          // use deposit message handler from SimpleAccount (see below)
     getBalance[ ] → ⦻¶      // always throw exception
     withdraw[anAmount:Euro] → ⦻§▮   // always throw exception

As a result of the above definition, DepositOnlyAccount⊒Account and
DepositOnlyAccount has message handlers with the following signatures:


        getBalance[ ] ↦ ⦻,   //  always throws exception
        withdraw[ ] ↦ ⦻,     //  always throws exception
        deposit[Euro] ↦ Void▮

The above makes use of the following:

Interface Account with
       getBalance[ ]↦Euro, 
       deposit[Euro]↦Void,
       withdraw[Euro]↦Void▮ 

Actor SimpleAccount[startingBalance:Euro]
  myBalance ≔ startingBalance｡
      // myBalance is an assignable variable
         // initialized with startingBalance
  implements Account using
     getBalance[ ] →   myBalance¶
     deposit[anAmount] → 
       Void                    // return Void
          afterward  myBalance ≔ myBalance+anAmount¶   
               // the next  message is processed with
                        //  myBalance reflecting the deposit
     withdraw[anAmount:Euro]:Void →
       (amount > myBalance) � 
          True ⦂ Throw  Overdrawn[ ] ⍌
          False ⦂ Void           //  return Void
                    afterward myBalance ≔ myBalance–anAmount ⍰§▮
                 //  the next  message is processed with updated myBalance

Please don't feed the troll

LtU Policies

At the risk of violating the "Civility" policy (#3) I'd like to point out that this post (and other recent posts from Hewitt) violates the following policies:

4A) Avoid design discussions
4B) Avoid ungrounded discussion
4C) Strong claims require strong evidence
6D) Language advocacy
7) Mentioning your own work

By Brandon Bloom at Sat, 2015-08-22 23:33 | login or register to post comments

Please don't mind the attempted censorship.

This is an important topic for discussion.

Current programming languages (e.g. Java, C#, C++) are seriously deficient in security as a result of unstructured casting.

Attempting to suppress discussions of security in Programming Languages does our community a great disservice.

Some of you may be interested in our on-line Silicon Valley FriAM discussion group where such security issues are addressed.
Visit this group at http://groups.google.com/group/friam

By Hewitt at Mon, 2015-08-24 06:06 | login or register to post comments

Please learn how to communicate

With all (serious) due respect, you continue to fail to communicate well. Hence the first response to your post. Calling that censorship seems to me to indicate that you still seriously fail to recognize your own failure to communicate on LtU. Which is, of course, sad, because it leads to all these sturm und drang wastes of time.

By raould at Mon, 2015-08-24 20:04 | login or register to post comments

Blog communication is difficult; but miscommunication easy :-(

Blog communication is difficult; but miscommunication is all too easy.

Unfortunately, Brandon Bloom was calling for censorship :-(

By Hewitt at Mon, 2015-08-24 20:13 | login or register to post comments

re please learn how to communicate

Raould, I'm confused. What don't you understand?

By Thomas Lord at Mon, 2015-08-24 20:32 | login or register to post comments

not understanding is sort of a default start condition

Hewitt does (primarily) two things impeding communication, which he could change and get a better yield in fruitful results. (And I would like that, because he seems to have ideas worth exploring, although "downcasts are bad" in this case seems small fry and uncontroversial to practitioners, and as such slightly weird when offered out of the blue without motivating context.)

Replies to puzzled queries can be short and cryptic instead of longer prose explanation.
Points are made in code examples, instead of prose explaining the examples.

Both have lack of explanation in common, which might be coincidence, or could be curse-of-knowledge (lack of empathy towards a state of not already knowing something). The OP above has more code than prose in plain language. Imagine a book composed entirely of figures, but without any prose explanations. This would puzzle or infuriate readers if they could not ignore the book.

Especially when not many folks know a language syntax involved, code might be offered to concretely illustrate something stated in natural language, first in common simple terms before any technical jargon, if the latter is necessary. A good amount of prose is "some", on the order of as many details as are presented in code figures. While OP has a bit of prose, the amount of detail in code is bigger.

I get a reaction that negative feedback is censorship, which I don't like, so I sympathize and offer constructive advice. It's not so much length in prose that people like as situating things in context, relating specific detail and general pattern. A schematic example follows. You might have noticed odd thing T. This is a specific instance of general problem P. A pattern with P looks like this, and when applied specifically to T you get this, except with reservation R. See also related concept C.

Imagine you are Rod Serling easing a viewer into a weird story. The new informational part has entropy new to readers, and counts as weird when they don't know it already. If there's a header saying "this is going to sound weird, but..." as part of the frame to outline new parts, it's much easier to digest. There's only so much exposition Serling can offer before a bored viewer changes channels, but none at all is a little skimpy.

I have a coworker who used to make elaborate figures illustrating dynamic system behavior. Then, he'd post them in a wiki page, without any prose explanation at all. I tried to explain why this was hard on someone trying to figure out his diagram, which wasn't as self-evident as he supposed. What does each line connecting two elements mean? When does this happen? Which part is old and obvious and which part is new and informative?

By Rys McCusker at Mon, 2015-08-24 22:32 | login or register to post comments

re not understanding is sort of a default start condition

Uh.. OK, Rys. I'm confused. What doesn't raould understand?

Also:

Both have lack of explanation in common

There is always an option to put some work into formulating a concise, clarifying question. Nearly nobody who rants at Hewitt ever bothers to do so. Instead, they often write at great length about their own beliefs and experience.

By Thomas Lord at Mon, 2015-08-24 22:50 | login or register to post comments

kibitzing

I'm guessing, since I don't have raould right here, but the list of things he doesn't understand might include: 1) why it was posted, 2) what code examples mean, 3) how casting relates to other things affecting security, 4) whether casting in ActorScript resembles casting in other languages, 5) where casting appears in the examples, 6) implied alternatives to casting, 7) what characterizes scenarios in real world manifestations, and other answers to the five w's.

(I realize I wasn't asked for my advice, but I thought I should offer it at least once. I don't mind a dismissive reaction. I assumed a goal was not to be deliberately obscure, so I suggested a presentation improvement. I didn't ask a clarifying question, because I don't have a question. Just kibitzing.)

By Rys McCusker at Mon, 2015-08-24 23:05 | login or register to post comments

Formulating good questions doesn't scale

I managed to ask a clarifying question in the thread on Nullable, because the post is about something very simple: an alternative to Haskell's Maybe. Now the OP is clear enough for me. In this context, that's an outstandingly successful interaction, compared to most others.
And that was already hard: I wouldn't describe it as concise, and while trying to understand that post, I already came up with 2-3 different hypotheses that didn't make sense. This wouldn't scale.

That's why we demand that Hewitt communicates better, as we demand it out of all other (PL) scientists. Not out of spite or politics.
That's also why (PL) researchers are taught to discuss one non-standard idea at a time, in the context of standard ideas: the result might seem more boring, but it's easier to discuss the merit of that one idea.

By Blaisorblade at Mon, 2015-08-24 23:19 | login or register to post comments

re formulating good questions

That's also why (PL) researchers are taught to discuss one non-standard idea at a time, in the context of standard ideas: the result might seem more boring, but it's easier to discuss the merit of that one idea.

Aside: It seems to me that the posts about Nullable and casting do just that.

I managed to ask a clarifying question in the thread on Nullable, because the post is about something very simple: an alternative to Haskell's Maybe.

Comparisons to Haskell seem to be a source of persistent confusion (not just on this narrow topic).

The ActorScript type system contains no universal quantification over types; types are a partially ordered set but not a lattice or semi-lattice (hence no "Nothing" but yes Null Integer). ActorScript types are categorically constructed, including message types. No noteworthy type inference is needed.

ActorScript uses an Actor model of computation, not a lambda or combinator model, neither a RAM-machine model. Functional and procedural concepts are easy to express in ActorScript but ActorScript in generality is not easy to express in those other models (and doing so would shed more heat than light).

The Unicode-laden notation doesn't seem that hard to figure out well enough to get the point of the posts, at least after a few skims of the main body of the ActorScript paper on HAL.

It seems to me a really, really simple language that opens up a vast new frontier in response to the question "What kind of abstractions does it make sense to build with this?" It doesn't seem trivial to implement well but neither do I see any huge obstacle.

I'm increasingly confused by other people's bafflement at it.

By Thomas Lord at Tue, 2015-08-25 01:51 | login or register to post comments

A major intended application area is IoT

Thanks Thomas!

A major intended application area for ActorScript is IoT which acts as an inspiration and design challenge.

Comments and suggestions for improvement are greatly appreciated.

By Hewitt at Tue, 2015-08-25 02:40 | login or register to post comments

re IoT?

A major intended application area for ActorScript is IoT which acts as an inspiration and design challenge.

Whose "IoT"? I mean: what market structure? Hence what commodity forms?

By Thomas Lord at Tue, 2015-08-25 04:37 | login or register to post comments

Actors for IoT

There is some description of Actors for IoT here

By Hewitt at Tue, 2015-08-25 14:11 | login or register to post comments

+1

Thanks, Brandon.

By Ehud Lamm at Mon, 2015-08-24 08:09 | login or register to post comments

"Stone Casting" by Mark Miller

From Static Types vs Dynamic Capabilities

Stone Casting (from Communities.com)

In Original-E http://www.communities.com/products/tools/e/e_white_paper.html
, an Java variant attempting to fix Java's security problems, we also felt,
like Jonathan, that thinning was a useful authority reduction pattern, and
that Java interface types & interface type inheritance was a useful way to
express the thinnings you want to be possible. However, we made thinning
into an operation distinct from static type loss -- "stone casting" as in
"cast in stone". With the proxies of Java 1.3
http://java.sun.com/j2se/1.3/docs/guide/reflection/proxy.html , we can now
express this in Java itself without building a new language. Contrast the
above

Thin p2 = p1;

with

Thin p2 = (Thin)StoneCast.new(p1, Thin.class);

This latter returns a new object that implements the Thin interface but not
Thick, and forward any This message on to the object it wraps -- the object
designated by p1. An attempt to recover the authority absent from p2:

Thick p3 = (Thick)p2;

will fail, as p2 is not a kind of Thick. Jonathan knows about the Stone
Casting alternative, writing:

Therefore,
>there needs to be some form of interface-like abstraction in which the
>downcast is disallowed. In Java, this requires the introduction of proxy
>objects. Proxy objects in turn break representation identity.

It indeed has an effect on object identity. Whereas previously "p1 == p2"
would and should succeed, since they dynamically designate the same object,
in the stone-casting case "p1 == p2" would fail, since they designate
different objects. I believe this is the only correct answer. Whether two
objects are forseen facets on the same state, or whether they share state
through other means is their business, not the business of their clients.

Cast in Steele

Why is this the only stance in the spirit of Java's semantics? To anyone
who still feels confused about the relationship of static and dynamic types
in Java, I highly recommend Chapter 4 of Guy Steele's "The Java Language
Specification". It's first few pages make clear that the type of a variable
is simply a static constraint on the possible values the variable may have,
and that a variable of type T may hold a (reference to) an object of a
subtype of T. The type of the variable has no effect on the object it
designates.

I know Jonathan knows all this. He's just proposing a Java variant that
doesn't work according to this description. I simply want to say that this
wouldn't be a minor semantic tweak -- it would be an earthquake -- even if
only three lines of code need to be changed in the implementation and three
lines of text in the tutorial. But the proof of the pudding and all that.
Should there come to be a serious secure language proposal along
the lines Jonathan suggests, I'm sure we'd all learn a great deal. In the
meantime, I will continue to approach the relationship between capabilities
and types in the traditional way -- according to the dynamic perspective.

Cheers,
--MarkM

By Hewitt at Mon, 2015-08-24 16:08 | login or register to post comments

Can keep this one brief

I agree, unstructured casting is bad. In C++ I only use virtual methods, hence using things like the visitor pattern. In functional languages type-classes form a kind of type-case. It seems all safe casting methods are a form of type case. Virtual methods scatter the type case into the various classes of a hierarchy, but essentially you want:

type-case a of
    Int -> -- do something with Int
    otherwise -> -- all options must be covered

Virtual methods check for completeness in the same way but do the type matching on dispatch.

You can view type-case as locally declaring a new interface of which all the option types are then extended by, with each case being the implementation of the single method interface for the respective type.

Of course type-case requires runtime type information, which type-classes do not (in general), which may not be what you want.

By Keean Schupke at Mon, 2015-08-24 06:20 | login or register to post comments

re "conditional downcasting"

What does this mean:

3: Conditional downcasting of an Actor of an interface type to an extension interface type.

Under what condition is such down-casting permitted?

By Thomas Lord at Mon, 2015-08-24 22:32 | login or register to post comments

Downcasting of an interface type: to an extension interface

Excellent question!

Downcasting of an interface type I is allowed only to an extension of I. For example, if x is of interface type I, then either

1. E is an extension of I and there is some y of type E such that x=y↑I and therefore x↓E=y
2. x↓E throws an exception because E is not an extension of I or there is no y of type E such that x=y↑I

By Hewitt at Tue, 2015-08-25 00:28 | login or register to post comments

re downcasting of an interfasce type: to an extension interface

Cool. Point (1) stood to reason but I wasn't sure if there was a run-time check so (2) wasn't obvious. (I couldn't think of useful enough downcasting w/out a run-time check but I didn't rule it out, either.)

By Thomas Lord at Tue, 2015-08-25 01:55 | login or register to post comments

Extension type does the heavy lifting in downcasting

Thanks Thomas!

The extension type does the heavy lifting in downcasting (and upcasting).

By Hewitt at Tue, 2015-08-25 02:14 | login or register to post comments

Lambda the Ultimate

User login

Navigation