diff options
author | Adam Chlipala <adam@chlipala.net> | 2018-03-30 18:01:44 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2018-03-30 18:01:44 -0400 |
commit | 7d4a7a7f92095edfea1cb55a11e037667c2c21da (patch) | |
tree | 6d646efc50754526afbb58b15487f03f81678a66 | |
parent | de2d8358dda08bfaf491d815df91d0c1ba33e7c9 (diff) |
Demo links escape frames
-rw-r--r-- | demo/more/prose | 4 | ||||
-rw-r--r-- | demo/prose | 12 |
2 files changed, 8 insertions, 8 deletions
diff --git a/demo/more/prose b/demo/more/prose index 9c267ca0..1f1d5a49 100644 --- a/demo/more/prose +++ b/demo/more/prose @@ -1,8 +1,8 @@ -<p>These are some extra demo applications written in <a href="http://www.impredicative.com/ur/">Ur/Web</a>. See <a href="http://www.impredicative.com/ur/demo/">the main demo</a> for a more tutorial-like progression through language and library features.</p> +<p>These are some extra demo applications written in <a target="_top" href="http://www.impredicative.com/ur/">Ur/Web</a>. See <a target="_top" href="http://www.impredicative.com/ur/demo/">the main demo</a> for a more tutorial-like progression through language and library features.</p> dragList.urp -<p>This is an Ur/Web version of the "draggable lists" <a href="http://groups.inf.ed.ac.uk/links/examples/">demo program from Links</a>.</p> +<p>This is an Ur/Web version of the "draggable lists" <a target="_top" href="http://groups.inf.ed.ac.uk/links/examples/">demo program from Links</a>.</p> grid1.urp @@ -1,6 +1,6 @@ -<p><b>Ur/Web</b> is a domain-specific language for programming web applications backed by SQL databases. It is (strongly) statically typed (like ML and Haskell) and purely functional (like Haskell). <b>Ur</b> is the base language, and the web-specific features of Ur/Web (mostly) come only in the form of special rules for parsing and optimization. The Ur core looks a lot like <a href="http://sml.sourceforge.net/">Standard ML</a>, with a few <a href="http://www.haskell.org/">Haskell</a>-isms added, and kinder, gentler versions added of many features from dependently typed languages like the logic behind <a href="http://coq.inria.fr/">Coq</a>. The type system is much more expressive than in ML and Haskell, such that well-typed web applications cannot "go wrong," not just in handling single HTTP requests, but across their entire lifetimes of interacting with HTTP clients. Beyond that, Ur is unusual in using ideas from dependent typing to enable very effective metaprogramming, or programming with explicit analysis of type structure. Many common web application components can be built by Ur/Web functions that operate on types, where it seems impossible to achieve similar code re-use in more established statically typed languages.</p> +<p><b>Ur/Web</b> is a domain-specific language for programming web applications backed by SQL databases. It is (strongly) statically typed (like ML and Haskell) and purely functional (like Haskell). <b>Ur</b> is the base language, and the web-specific features of Ur/Web (mostly) come only in the form of special rules for parsing and optimization. The Ur core looks a lot like <a target="_top" href="http://sml.sourceforge.net/">Standard ML</a>, with a few <a target="_top" href="http://www.haskell.org/">Haskell</a>-isms added, and kinder, gentler versions added of many features from dependently typed languages like the logic behind <a target="_top" href="http://coq.inria.fr/">Coq</a>. The type system is much more expressive than in ML and Haskell, such that well-typed web applications cannot "go wrong," not just in handling single HTTP requests, but across their entire lifetimes of interacting with HTTP clients. Beyond that, Ur is unusual in using ideas from dependent typing to enable very effective metaprogramming, or programming with explicit analysis of type structure. Many common web application components can be built by Ur/Web functions that operate on types, where it seems impossible to achieve similar code re-use in more established statically typed languages.</p> -<p>The page you are currently reading is a part of the demo included with the Ur/Web sources and supporting files available from <a href="https://github.com/urweb/urweb">GitHub</a>. The following steps will build a local instance of the demo if you're lucky (and running a Debian-based Linux OS, which actually tend to have Ur/Web packages built in these days). If you're not lucky, you can consult the beginning of <a href="http://www.impredicative.com/ur/manual.pdf">the manual</a> for more detailed instructions.</p> +<p>The page you are currently reading is a part of the demo included with the Ur/Web sources and supporting files available from <a target="_top" href="https://github.com/urweb/urweb">GitHub</a>. The following steps will build a local instance of the demo if you're lucky (and running a Debian-based Linux OS, which actually tend to have Ur/Web packages built in these days). If you're not lucky, you can consult the beginning of <a target="_top" href="http://www.impredicative.com/ur/manual.pdf">the manual</a> for more detailed instructions.</p> <h6>Install System Dependencies</h6> @@ -26,7 +26,7 @@ sudo make install <p><blockquote><pre>$ urweb -dbms sqlite -db /path_to_db.sqlite -demo /Demo -noEmacs demo </blockquote></pre></p> -<p>The <tt>-dbms sqlite</tt> flag indicates that instead of using the default database management system (<a href="https://www.postgresql.org/">PostgreSQL</a>), we wish to use <a href="https://sqlite.org/">SQLite</a> (usually unsuited for production). The <tt>-db</tt> flag allows us to specify the file-system path to our SQLite database. The <tt>-demo /Demo</tt> parameter indicates that we want to build a demo application that expects its URIs to begin with <tt>/Demo</tt>, while the <tt>-noEmacs</tt> parameter disables invocation of Emacs to syntax-highlight source files for HTML rendering. The final argument <tt>demo</tt> gives the path to a directory housing Ur/Web source files (<tt>.ur</tt>, <tt>.urp</tt>, <tt>.urs</tt>, etc.). +<p>The <tt>-dbms sqlite</tt> flag indicates that instead of using the default database management system (<a target="_top" href="https://www.postgresql.org/">PostgreSQL</a>), we wish to use <a target="_top" href="https://sqlite.org/">SQLite</a> (usually unsuited for production). The <tt>-db</tt> flag allows us to specify the file-system path to our SQLite database. The <tt>-demo /Demo</tt> parameter indicates that we want to build a demo application that expects its URIs to begin with <tt>/Demo</tt>, while the <tt>-noEmacs</tt> parameter disables invocation of Emacs to syntax-highlight source files for HTML rendering. The final argument <tt>demo</tt> gives the path to a directory housing Ur/Web source files (<tt>.ur</tt>, <tt>.urp</tt>, <tt>.urs</tt>, etc.). </p> <p> @@ -88,7 +88,7 @@ hello.urp <p>We must, of course, begin with "Hello World."</p> -<p>The project file justs list one filename prefix, <tt>hello</tt>. This causes both <tt>hello.urs</tt> and <tt>hello.ur</tt> to be pulled into the project. <tt>.urs</tt> files are like <a href="http://caml.inria.fr/ocaml/">OCaml</a> <tt>.mli</tt> files, and <tt>.ur</tt> files are like OCaml <tt>.ml</tt> files. That is, <tt>.urs</tt> files provide interfaces, and <tt>.ur</tt> files provide implementations. <tt>.urs</tt> files may be omitted for <tt>.ur</tt> files, in which case most permissive interfaces are inferred.</p> +<p>The project file justs list one filename prefix, <tt>hello</tt>. This causes both <tt>hello.urs</tt> and <tt>hello.ur</tt> to be pulled into the project. <tt>.urs</tt> files are like <a target="_top" href="http://caml.inria.fr/ocaml/">OCaml</a> <tt>.mli</tt> files, and <tt>.ur</tt> files are like OCaml <tt>.ml</tt> files. That is, <tt>.urs</tt> files provide interfaces, and <tt>.ur</tt> files provide implementations. <tt>.urs</tt> files may be omitted for <tt>.ur</tt> files, in which case most permissive interfaces are inferred.</p> <p>Ur/Web features a module system very similar to those found in SML and OCaml. Like in OCaml, interface files are treated as module system signatures, and they are ascribed to structures built from implementation files. <tt>hello.urs</tt> tells us that we only export a function named <tt>main</tt>, taking no arguments and running a transaction that results in an HTML page. <tt>transaction</tt> is a monad in the spirit of the Haskell IO monad, with the intent that every operation performable in <tt>transaction</tt> can be undone. By design, Ur/Web does not provide a less constrained way of running side-effecting actions. This particular example application will employ no side effects, but the compiler requires that all pages be generated by transactions.</p> @@ -114,7 +114,7 @@ form.urp nested.urp -<p>Here is an implementation of the tiny challenge problem from <a href="http://www.accursoft.co.uk/web/">this web framework comparison</a>. Using nested function definitions, it is easy to persist state across clicks.</p> +<p>Here is an implementation of the tiny challenge problem from <a target="_top" href="http://www.accursoft.co.uk/web/">this web framework comparison</a>. Using nested function definitions, it is easy to persist state across clicks.</p> cookie.urp @@ -207,7 +207,7 @@ view.urp cookieSec.urp -<p>Ur/Web guarantees that compiled applications are immune to certain kinds of <a href="http://www.owasp.org/index.php/Top_10_2007-A5">cross site request forgery</a>. For instance, a "phisher" might send many e-mails linking to a form that he has set up to look like your web site. The form is connected to your web site, where it might, say, transfer money from your bank account to the phisher's account. The phisher doesn't know your username, but, if that username is stored in a cookie, it will be sent automatically by your browser. Ur/Web automatically signs cookie values cryptographically, with the signature included as a POST parameter and not part of a cookie, to prevent such attacks.</p> +<p>Ur/Web guarantees that compiled applications are immune to certain kinds of <a target="_top" href="http://www.owasp.org/index.php/Top_10_2007-A5">cross site request forgery</a>. For instance, a "phisher" might send many e-mails linking to a form that he has set up to look like your web site. The form is connected to your web site, where it might, say, transfer money from your bank account to the phisher's account. The phisher doesn't know your username, but, if that username is stored in a cookie, it will be sent automatically by your browser. Ur/Web automatically signs cookie values cryptographically, with the signature included as a POST parameter and not part of a cookie, to prevent such attacks.</p> <p>This demo shows a simple mock-up of a situation where such an attack is often possible with traditional web frameworks. You can set an arbitrary username for yourself in a cookie, and you can modify the database in a way that depends on the current cookie value. Try getting the latter action to succeed without first setting your desired username in the cookie. This should be roughly as impossible as cracking the particular cryptographic hash function that is used.</p> |