[Ur] Supporting 'style' attribute securely

[Adam Chlipala]

Edward Z. Yang wrote:
> The obvious thing to do is to create a new datatype representing styles. There are a lot of things to worry about, e.g. colors and lengths and all of those types, which means it'd need a bit of engineering effort. But you want this because there are a lot of non-canonical representations and Javascript injection vectors to worry about. (This is speaking from my experience with HTML Purifier)

The strawman I had in mind was that a style would be a list of key-value 
pairs, with pretty standard escaping applied to keys.  Values would be 
either URL's or text, with suitable escaping applied to each, so that 
"text" values can never contain URL's.

Do you have a few examples showing inadequacy of the strawman?

> Adam Chlipala<adamc at impredicative.com>  wrote:
>
>> A number of folks have asked to be able to use the HTML 'style'
>> attribute in Ur/Web.  It's easy enough to add the attribute with type
>> [string], but this seems likely to allow for some sort of code
>> injection
>> attack.  At a minimum, URL's can appear in styles and be interpreted as
>>
>> URL's, which seems to function as a "universal interpreter" for
>> whatever
>> programming languages browsers want to support via URL's!  (At a
>> minimum, there are "javascript:" URL's.)
>>
>> So, any suggestions on "the right way" to support 'style' in Ur/Web?
>> I'm unlikely to accept an idea that leaves open code injection
>> vulnerabilities; one important global guarantee of Ur/Web is that code
>> injection attacks are impossible.  But I don't have such a clear idea
>> of
>> (a) what the attack possibilities are in CSS style code and (b) what
>> the
>> appropriate countermeasures are, including how they should be
>> represented with typed combinators in Ur/Web.
>>