Re: Fwd: Fwd: Draft Proposed Standard SES (Secure EcmaScript)

On Sat, Mar 19, 2016 at 11:55 AM, Mark S. Miller <[email protected]> wrote:
> Forwarded with David's permission. I should mention that my responses both
> previously and here were written thinking they were going to es-discuss
> rather than cap-talk. They assume more JS and less ocaps as background than
> I would have written for this audience. If any of the JS aspects are
> mysterious, please ask. Thanks.
>
>
> ---------- Forwarded message ----------
> From: Mark S. Miller <[email protected]>
> Date: Sat, Mar 19, 2016 at 11:14 AM
> Subject: Re: [cap-talk] Fwd: Draft Proposed Standard SES (Secure EcmaScript)
> To: David Nicol <[email protected]>
>
>
> On Fri, Mar 18, 2016 at 9:46 PM, David Nicol <[email protected]> wrote:
>>
>>
>>
>> On Fri, Mar 18, 2016 at 10:44 PM, Mark S. Miller <[email protected]>
>> wrote:
>>>
>>> On Fri, Mar 18, 2016 at 6:34 PM, David Nicol <[email protected]>
>>> wrote:
>>>>
>>>> I hope the following makes sense, it is imprecise
>>>>
>>>>
>>>>
>>>>
>>>> I have a question. Does SES entirely do away with the "scope chain" and
>>>> all passing by shared visibility, trading that for explicit object members,
>>>> or are lexical scopes still available?
>>>
>>>
>>> Lexical scopes are still exactly as available as they are otherwise. SES
>>> does nothing whatsoever to change that. Historically, one of the many things
>>> that motivated me to fight so hard to get true lexical scoping into
>>> ES5/strict was that the SES-shim needed it. But now that we have it, SES
>>> does nothing to change it.
>>
>>
>> what about "variable hoisting" seeming to re-order things? I ask just
>> because it's confusing coming from Perl, where you can redeclare the same
>> local symbol repeatedly if you want, to Javascript where you can only
>> declare a symbol once per scope.
>
>
>
> SES does not change JavaScript's scoping rules at all. Everything that does
> or does not hoist in regular JavaScript does or does not hoist in the same
> way in SES. Everything that does or does not admit redeclaration in regular
> JavaScript does so identically in SES. That's why the SES document does not
> say anything about enhancing, restricting, or altering JavaScript's grammar.
> In fact it does not mention grammar at all.
>
> You can think of many languages as cleanly divided into two major relevant
> parts,
>
>   * the nature of the code: flow of control, scoping, etc
>   * the nature of the data it operates on -- primarily the behavior of
> objects in the heap.
>
> SES requires the nature of code to obey the locality we associate with
> lexical scoping but is otherwise neutral. Since ES5 and later do so, SES
> does not need to say more here or propose any changes, in order to achieve
> its fundamental properties.

Not really familiar with javascript, but to slightly modify one of
your examples from one of your talks

"use strict";

var count = 0;

function makeCounter() {
     // Moved var count = 0 from here to above
     // appears to be valid strict javascript afaict
     return def({
         incr: function() { return ++count;},
         decr: function () { return --count;}
     });
}

with the comment in the bottom of the slide:
"A tamper-proof record of lexical closures encapsulating state is a
defensive object"

so this is 'defensive' rather than 'confined', confinement then
happens through multiple evaluations of the source code (rather than
the evaluator causing error due to the evaluation of the function
makeCounter being called in a context where the 'count' variable does
not exist, did I get that correct?

so say if I wanted a Diary object which contains alice/bob/carols
secrets, and ensures the separation of those secrets, you need to
evaluate this source multiple times?

> SES requires the nature of objects on the heap to obey the locality we
> associate with memory safety and object oriented programming (which is the
> locality of applicative order lambda calculus with local side effects
> <http://mumble.net/~jar/pubs/secureos/>). SES requires that objects be able
> to truly encapsulate their state and present a tamper-proof api surface that
> can defend their invariants from hostile clients. Again, at the
> object-to-object level ES5 and later do so.
>
> Finally, there is the nature of the objects that other objects have implicit
> (ungranted) access to, either by scoping or by binding to intrinsics. Beyond
> ES5, locking down the primordials and removing powerful host globals is
> almost all that additionally needs to be said! I hope the document makes
> that clear. Nothing in ES2015, ES2016, or draft ES2017 as of March 17
> changes any of these fundamentals. Some ES2015 changes, notably the Proxies
> and WeakMaps that support membranes, are fundamental improvements to the
> expressiveness of SES. Other post ES5 changes, including syntactic changes
> like proposed private state, help support the kinds of programming SES is
> meant to support. But all such changes help support abstraction and
> modularity generally, and so are, in that sense, independent of SES.
>
> Likewise, SES is a great boon to abstraction and modularity, even when
> security per se is not a concern. In an important way, ocaps are midway
> between memory safety and pure functional programming. All three limit side
> effects in order to aid local reasoning about the meaning of programs. When
> mere memory safety is not enough but pure functional programming is too
> much, ocaps may be just right ;).
>
> WASM and SES
>
> SES's independence from syntactic issues is clearest by considering how WASM
> (WebAssembly) and SES interact. WASM gives us a new form of code with a
> somewhat different nature, but still limited to the locality properties of
> lexical scoping. WASM brings in some new primitive data types like various
> sizes of integer. But because these are immutable SES need not care. WASM
> does not introduce now objects or API, but rather, operates on the same heap
> of objects that JavaScript operates on. All the rules about what JavaScript
> code can and cannot do with these objects applies equally to WASM. Thus, the
> small set of changes that SES proposes, to turn JavaScript into an ocap
> language, are already sufficient to turn WASM, executing in those same
> realms, into an ocap language.
>
>
>
>>
>>
>>
>>
>>>>
>>>> If lexical scopes are still available, can the global symbols, that
>>>> represent immutables, get assigned new representations? That is, can core
>>>> features get turned off after we're done using them, like
>>>>
>>>>       function = function(x){ throw }; // we have all the functions we
>>>> need, further attempts to compile more will fail.
>>>
>>>
>>> I don't understand the question. "function" is a keyword. It cannot be
>>> used as a variable name.
>>
>>
>> I should have written
>>
>>       function function(){throw};
>>
>> or
>>
>>       var function = function(x){ throw };
>>
>> as if the keywords are plain symbols like coder-declared ones.
>
>
> This is just as illegal and meaningless in SES as it is in normal
> JavaScript.
>
>
>
>>>
>>>
>>>>
>>>>
>>>> Can the immutables be lexically hidden?
>>>
>>>
>>> Good question. Yes and no.
>>>
>>> You can hide the original global name bindings by several means. The
>>> fresh global of a new ses realm is a plain mutable object. It initially
>>> inherits from the proto-global, but you can change that. To have full
>>> control, you can put what you want on the global and then do
>>> "freshGlobal.__proto__ = null" (or use Reflect.setPrototypeOf). By wrapping
>>> any code you execute in a prelude and postlude that shadows globals and
>>> hides the global object itself, you can also change the bindings of these
>>> names.
>>>
>>> However, this does not enable you to deny access to the intrinsics that
>>> can be reached by syntax. For example, the expression "[]" in any SES realm
>>> will create an array that initially inherits from the proto-SES realm's
>>> Array.prototype, independent of the scoping environment in which that code
>>> executes. That's why we require everything in the proto-SES realm to be
>>> transitively immutable and powerless. We assume these objects cannot be
>>> denied.
>>>
>>> Of course, a code rewriting strategy can change what is reachable by
>>> syntax. But SES does nothing to either help or hurt rewrite-based
>>> enforcement.
>>
>>
>> so allowing unlimited external access to eval() may become safe from side
>> effects, but not from resource-starving DOS attacks; it still isn't
>> recommended.
>
>
> Yes, that is true and important. For each type of protection we may ask "at
> what granularity"? We can partition most (not all) security concerns into
>
>   * integrity -- loosely, only authorized actions happen
>   * availability -- loosely, authorized actions continue to happen
>   * confidentiality -- loosely, only authorized secrets are learned.
>
> The browser's same origin policy defends only integrity. Because code from
> mutually suspicious origins share an event loop, they are fully vulnerable
> to each other regarding availability. Among things sharing an event loop,
> and infinite loop by one blocks all. Finally, browsers don't claim to defend
> confidentiality against side channels and covert channels.
>
> SES, operating within the browser's event loop, cannot do anything about
> availability and is not in a position to try. However, JavaScript in a
> non-browser environment like a Node server is in a position to try to defend
> availability to an important and practical degree. I agree that we need to
> revise the mobile code example to explain the availability cost in making
> remote eval available. I was clearer about that in the earlier
> <http://wiki.ecmascript.org/doku.php?id=strawman:concurrency#open_vat> where
> the permission to access that remote eval power was explicit and clear.
> Thanks for pointing this out!
>
> SES makes a contribution to the less valuable side of the confidentiality
> issue: SES helps suppress reading non-overt channels under very restrictive
> conditions -- where no timing channels are granted -- but does not prevent
> signaling on these channels. Preventing signaling would be more valuable,
> but no one has any practical idea how to do that by any means.
>
> The big difference is in integrity -- as you say, limiting side effects.
> Conventional OSes do privilege separation only at the granularity of
> user/account. The browser same origin policy added another epicycle,
> extending privilege separation one level, to user-at-origin. But neither was
> compositional. SES extends privilege separation within an origin. But it
> does not add yet another level of epicycle. It enables privileges to be
> separated and composed effectively down to very fine grain.
>
>
>
>>
>>
>>>>
>>>> By allowing hiding, you might be able to avoid having to construct a new
>>>> eval function with each realm unless you really need one. That is,
>>>> leave "eval" out of the core language, and put in its place
>>>> evalFactory(topRealm)
>>>
>>>
>>> I'm sorry, I don't understand the suggestion. What does evalFactory do?
>>
>>
>> evalFactory is supposed to generate an eval function whose scope chain
>> stops at the argument, which is expected to be a scope, if the with
>> statement caused new vars declared within its block to go in the scope
>> (which it doesn't) it would be like so
>>
>>
>>          function evalFactory(S){
>>                return function ( src ) {
>>                      fancyWritingWith(S) { eval(src) }
>>                };
>>          };
>>
>> http://www.2ality.com/2011/06/with-statement.html
>
>
> This has some similarity to the internal technique used by the SES-shim to
> control global scoping, but it is very different from SES.
>
>
>>
>>
>> SES still isn't about creating little languages that are invoked with a
>> near-native eval keyword, and that isn't a criticism of it.
>
>
> Correct and thanks.
>
>
>>
>>
>> Thanks
>>
>>
>>>>
>>>>
>>>>>
>>>>> It is now ready for comments at https://github.com/FUDCo/ses-realm
>
>
>
>
>
> --
>     Cheers,
>     --MarkM
>
> _______________________________________________
> cap-talk mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/cap-talk
>