[Ur] Supporting 'style' attribute securely

[Alexei Golovko]

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? Because compiler does not check external style files.
Moreover, as user may set minimal font size and maximum page width, you can't guarantee there are no overflows.
And this means, 'width' is blacklisted; this is too srtict, I think.

I would be glad to see invariants you wrote about. But implementation seems too hard and too browser-specific. Maybe better way is to provide important guarantees (no url injection) at the compiler level and let controlling of rectangles will be in some library code (e.g. let in urp file may be declared handler for "style=..." syntax sugar as ordinary urweb function for filtering).

>  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.