es-discuss Digest, Vol 43, Issue 7

Mark S. Miller erights at google.com
Fri Sep 3 20:45:50 PDT 2010


On Fri, Sep 3, 2010 at 6:04 PM, Leo Meyerovich <lmeyerov at gmail.com> wrote:

> > Although I illustrated the non-overt channel here as a covert channel in
> a possibly failed attempt at clarity, my real point and my real worry is
> about its use as a side channel. As a side channel, this ability to sense
> the collection of individual objects is much more informative than anything
> I know of in current JS. If anyone knows of any side channels that seem as
> bad, perhaps I've overlooked them, so please post. If they also seem
> unpluggable, then I would agree that my position here becomes pointless and
> we'd need to give on resisting side channels as well.
> >
>
>
> Off the top of my head:
>
> 1) Does ES5 fully freeze the global / root protos / etc. or allow a way to
> call function without them? Taint can show up through here.
>

Of course not. But it does allow these to be frozen. SES makes use of that
to freeze them (after cleaning them up) as the last step of its
initialization <
http://code.google.com/p/es-lab/source/browse/trunk/src/ses/initSES.js#557
>.



>
> 2) Even with frozen APIs, do we acknowledge timing attacks? Out-of-memory,
> non-termination, and other platform exception tricks?
>

Acknowledged.



>
> 3) Sniffing is already ubiquitous in terms of language / host API variants
>

Sure. What issue does that raise?

More generally, ES mostly has what one might call sources of "static
nondeterminism" <
http://code.google.com/p/google-caja/wiki/SourcesOfNonDeterminism>. By
"static" I mean ways implementations of the spec may differ from each other.
But these only open a non-overt channel if they may differ dynamically among
runs on the same platform in a way that can be influenced.


>
> Stepping back, I'm not even sure precisely why gc status classifies as a
> side channel. First, when passing references, defensive coders must already
> consider non-local properties to protect against memory leaks: gc state
> should, arguably,  already be carefully thought about when dealing with
> components. Second, this seems somewhat close to a transient resource
> reification pattern where it's use as explicit communication seems fine: you
> check against what the system has reclaimed, etc.**


> Lest anyone misunderstands, I actually do agree that it's suspicious if you
> do not consider coding wrt to gc as being natural. Making the intended
> threat model to protect against more precise would help me at least. For
> example, it could answer why the ability to check whether an object has been
> collected is not an overt channel that is part of getting a reference: if
> you don't want somebody to check, don't give them the object.
>


Nice. Excellent questions. The boundary between overt and non-overt is
relative to the semantics of a platform. For the same concrete platform
implementation, there can be multiple semantic accounts, and thereby
multiple notions of where the boundary is between overt and non-overt.

Similarly, we normally say that a program is correct (in a formal
correctness sense) if it would behave correctly on any platform that obeys
the semantics. If a program happens to operate correctly on a given platform
by relying on unspecified features of that platform, but would operate
incorrectly on a different possible implementation of that platform's
semantics, we would normally say the program is incorrect. Of course, given
a different semantic account of the platform, different programs for that
platform will be considered correct.

Formal models for reasoning about confidentiality that ignore non-overt
channels are generally unsound. Deterministic platforms aside, "correctly"
preserving confidentiality involves reasoning about implementations and
about multiple levels of abstraction.

A correct program must only rely on the communications provided by overt
channels. This brings us to an important realization from Fred Spiessen's
thesis <http://www.evoluware.eu/fsp_thesis.pdf>: Formal models for reasoning
about integrity that ignore non-overt channels remain sound. The correctness
of a program at preserving integrity is within conventional correctness,
which we can reason about soundly in a modular manner.

Now to your questions. My earlier statements are with regard to using a
conventional programming language semantics, in which memory allocation
mechanics are mostly ignored. At <
http://wiki.ecmascript.org/doku.php?id=strawman:gc_semantics> I captured
some notes and references to papers that explore how to extend such
conventional semantics to take account of some of these issues. At the
opposite extreme, we could reason about the semantics of the machine
instruction set, where the "program" we are reasoning about is the entire
tower of software leading up the same program. At this level of abstraction,
there is finite memory and no memory allocation. Under this perspective, we
would get very different answers about what is correct or incorrect, and
corresponding different answers about what is overt and non-overt.

Of course, the artifacts this committee produces and this list discusses are
semantics for next standard versions of JavaScript. These are programming
language semantics in the conventional sense.


>
>
> **having overidable object destructors are probably a cleaner alternative
> in most cases for this second use
>
>
>
>
> _______________________________________________
> es-discuss mailing list
> es-discuss at mozilla.org
> https://mail.mozilla.org/listinfo/es-discuss
>



-- 
    Cheers,
    --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20100903/6d74708c/attachment.html>


More information about the es-discuss mailing list