[Ur] Supporting 'style' attribute securely

[Adam Chlipala]

Sorry for the late reply; been working on a few modest compiler 
improvements, and now I'm ready to think about this again!

Edward Z. Yang wrote:
> I can give a few examples, and we can patch them up, but perhaps
> the bigger question is how adversarial we consider our users.
> In an adversarial setting, the only secure policy is a whitelist
> policy, and given the complexity of CSS you really need more
> types than URLs and strings.

Do you think it should be possible to partition CSS properties into 
those that are always safe to apply locally, and those that aren't?  
Then the compiler could have two modes, to control whether the "unsafe" 
properties are included.

Perhaps a simpler policy, more in line with the current support for URL 
policies, would be to allow whitelisting of properties by name, in .urp 
files.  This has the advantage of supporting new or browser-specific 
properties without hardcoding them in the Ur/Web implementation.

>    - A trivial example: background-color:expression(...) causes JavaScript execution
>      in Internet Explorer.

Hm... so perhaps we also want a whitelist of "functions" that have 
parens after them, and not allow parens in "text" property values?  
Perhaps then a property value is a _list_ of items, each of which is 
either paren-free text or a call to a whitelisted "function," with 
special handling for the "url" "function"?

>    - The background CSS property takes an embedded URL, so it is neither pure URL
>      nor pure text.

Does my proposal above deal adequately with this one?

>    - User provided styles can be used to implement phishing; via absolute
>      positioning user-controlled links on top of normal ones.

Perhaps it's worth including a special case for the "position" property, 
with an explicit whitelist of choices?

>    - The innerHTML attack: foo.innerHTML = foo.innerHTML is not an idempotent
>      operation; if applied multiple times you "lose" levels of backslash escaping.

This one I'm not sure applies to Ur/Web.  Are you thinking of a case 
where a problem could arise from this property, outside of 
project-specific JavaScript code accessed with the FFI?

>    - Treatment of escape sequences is inconsistent across browsers; for example,
>      numeric escapes don't work in many contexts.  You have to very carefully
>      pick the escaping function you want.

So perhaps we just disallow (in CSS style code) all characters that need 
escaping?

>    - Font-families are another can of worms, because they're "unrestricted" but
>      subject to the above problems.

Can you give an example of some funny business with font families?