[Ur] Supporting 'style' attribute securely

[Adam Chlipala]

Alexei Golovko wrote:
> 24.04.2012, 16:15, "Adam Chlipala"<adamc at impredicative.com>:
>> Alexei Golovko wrote:
>>
>>>   And I disagree that compiler should prevent things like phishing through absolute positioning etc. Compiler should be safe with respect to _programmer's_ errors; this also means that user data can't appear in unsafe place unintentionally, without explicit parsing of this data. But if programmer do explicit parsing, compiler can not check correctness --- for example, if I use plain text design of forum, for safe input I need check alignments (that is leading spaces), compiler can't help me in this question.
>> You are assuming the programmer only wants the compiler's help in
>> reasoning about whole-program invariants.  In contrast, I want the
>> compiler to help in reasoning about invariants of modules, such that we
>> can compose modules and get certain guarantees for free.  For instance,
>> I want to be able to use a module that I can think of as controlling a
>> certain rectangle of the page display.  If the module can use CSS to
>> escape out of its box and draw content elsewhere, then the invariant is
>> violated.
> But this invariant is already violated: module can include any custom stylesheet by adding its URL to whitelist, can't it?

Yes.  I'm talking about invariants that can be guaranteed within Ur/Web 
code; .urp directives don't count, since such files are easy to audit.  
Without explicit whitelisting, Ur/Web code is very limited in which 
stylesheets it can reference.

Your suggestion to focus just on avoiding code injection is a reasonable 
point in the design space, and I'm not ruling it out.