[Ur] Supporting 'style' attribute securely

[Adam Chlipala]

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.  The extreme case is security concerns of running code 
contributed by others who aren't trustworthy, while retaining the 
ability to reason about invariants of the modules that you write 
yourself; but even with a single programmer, modularity with strong 
guarantees is useful for program understanding.