[Ur] Supporting 'style' attribute securely

[Adam Chlipala]

Marc Weber wrote:
> Excerpts from Adam Chlipala's message of Sun Apr 15 20:12:00 +0200 2012:
>> It's just like using eval() in an unsafe way, but Ur/Web rules out
>> eval()!
> Can't you just use it as 'external' function and write a binding for
> it in .urp files?
>
> So the point is that all problems are known by reading the .urp file?

Correct on both counts.  Whether a project uses FFI code is decidable, 
while whether, e.g., a PHP script has code injection vulnerabilities is 
undecidable.

> So this discussion is about both: The urweb compiler and the HTML parser
> you wrote to sanitize / verify that user typed well formed HTML?
> Thus if a user wants to design his newsletter for a shop he should be
> prevented from using<div style="something using a milicious url">  or
> the like?

Right, though I think of the HTML parser as part of the Ur/Web 
compiler.  It should be possible by looking at .urp files alone to 
guarantee certain invariants of program execution.  Allowing arbitrary 
JavaScript execution makes it possible to break all invariants, but 
arbitrary JavaScript execution can be ruled out with appropriate URL 
policies and lack of FFI use.