changeset 789:d18f6f0bcf60

Describe GET/POST
author Adam Chlipala <adamc@hcoop.net>
date Tue, 05 May 2009 14:45:21 -0400
parents f5fea13a60b9
children 39bb3a830e90
files doc/manual.tex
diffstat 1 files changed, 6 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/doc/manual.tex	Tue May 05 14:36:16 2009 -0400
+++ b/doc/manual.tex	Tue May 05 14:45:21 2009 -0400
@@ -1846,6 +1846,12 @@
 
 Ur/Web programs generally mix server- and client-side code in a fairly transparent way.  The one important restriction is that mixed client-server code must encapsulate all server-side pieces within named functions.  This is because execution of such pieces will be implemented by explicit calls to the remote web server, and it is useful to get the programmer's help in designing the interface to be used.  For example, this makes it easier to allow a client running an old version of an application to continue interacting with a server that has been upgraded to a new version, if the programmer took care to keep the interfaces of all of the old remote calls the same.  The functions implementing these services are assigned names in the same way as normal web entry points, by using module structure.
 
+\medskip
+
+The HTTP standard suggests that GET requests only be used in ways that generate no side effects.  Side effecting operations should use POST requests instead.  The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis.  Any page that may have a side effect must be accessed through a form, all of which use POST requests.  A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions.  Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers.
+
+Ur/Web includes a kind of automatic protection against cross site request forgery attacks.  Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server.  Signing and signature checking are inserted automatically by the compiler.  This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect.
+
 
 \section{Compiler Phases}