summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-05 14:45:21 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-05 14:45:21 -0400
commitbb11d221d430a04da3214229cd6f1792f70b6cb8 (patch)
treef47c57f7cab56d58b08fe34265791a470b514525
parent331a548a72381bb798611ac8cd5e8397699bf17d (diff)
Describe GET/POST
-rw-r--r--doc/manual.tex6
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index b822b7a2..52403a7e 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1846,6 +1846,12 @@ For both links and actions, direct arguments and local variables mentioned impli
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}