[Ur] Ur's Browser Based Crypto Benefits?

[Adam Chlipala]

On 12/03/2013 12:04 PM, Burton Samograd wrote:
> Would Ur with it's native JS security features (protection from xss code injection, etc) help or eliminate any of the problems outlined in the following papers?
>
>      http://rdist.root.org/2010/11/29/final-post-on-javascript-crypto/
>
>      http://blog.cryptographyengineering.com/2012/12/the-anatomy-of-bad-idea.html
>    

These posts, especially the second, focus on issues orthogonal to 
programming languages and compilers, where Ur/Web wouldn't have much to 
offer.  These issues include bad API design (focus of 2nd post), 
processes whereby the wrong code is sent to clients, bad library 
implementation or general programmer incompetence, bad sources of 
pseudorandomness in browsers, and the consequences of browser 
implementation bugs.

HOWEVER, I think Ur/Web offers some substantial advantages for 
implementing and reasoning about crypto libraries, which should 
naturally be runnable both server-side and client-side.  Ur/Web includes 
a foreign function interface that allows all sorts of circumvention of 
the suggested interfaces, but, if you don't use it, then you're 
guaranteed (modulo compiler bugs) that you can think of your application 
in terms of a much-simplified behavioral model.

The DOM isn't exposed directly.  I'd call it a /security bug/ in Ur/Web 
if it were possible to write a .ur file that somehow managed to access 
the DOM directly!  The more functional model in Ur/Web makes it easier 
to reason about components separately and derive guarantees about their 
composition.  Of course, there's also no eval() in Ur/Web, and it would 
be a bug if there turned out to be any way to trigger similar behavior 
in a .ur file.

Same-origin policy?  Write your whole program in Ur/Web and there's no 
need to think about that kind of stuff.  Language-level guarantees 
provide all the protection you need between components.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20131203/94917efd/attachment.html>