diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2019-01-26 14:24:48 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2019-01-26 14:24:48 -0500 |
| commit | 15105e3e62d595fe620d019a7ef9aeeb0197d24d (patch) | |
| tree | 01ad9faa8663c992f08248fd76bc9e8f2ae3a947 | |
| parent | 0602c8c8b3f0b09a033f393e3d8af8310edff634 (diff) | |
Clarifying security model in the manual
| -rw-r--r-- | doc/manual.tex | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/doc/manual.tex b/doc/manual.tex index 59727099..8f7787fc 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -2400,7 +2400,7 @@ A web application is built from a series of modules, with one module, the last o Elements of modules beside the main module, including page handlers, will only be included in the final application if they are transitive dependencies of the handlers in the main module. -Normal links are accessible via HTTP \texttt{GET}, which the relevant standard says should never cause side effects. To export a page which may cause side effects, accessible only via HTTP \texttt{POST}, include one argument of the page handler of type $\mt{Basis.postBody}$. When the handler is called, this argument will receive a value that can be deconstructed into a MIME type (with $\mt{Basis.postType}$) and payload (with $\mt{Basis.postData}$). This kind of handler should not be used with forms that exist solely within Ur/Web apps; for these, use Ur/Web's built-in support, as described below. It may still be useful to use $\mt{Basis.postBody}$ with form requests submitted by code outside an Ur/Web app. For such cases, the function $\mt{Top.postFields} : \mt{postBody} \to \mt{list} \; (\mt{string} \times \mt{string})$ may be useful, breaking a \texttt{POST} body of type \texttt{application/x-www-form-urlencoded} into its name-value pairs. +Normal links are accessible via HTTP \texttt{GET}, which the relevant standard says should never cause side effects. To export a page that may cause side effects, accessible only via HTTP \texttt{POST}, include one argument of the page handler of type $\mt{Basis.postBody}$. When the handler is called, this argument will receive a value that can be deconstructed into a MIME type (with $\mt{Basis.postType}$) and payload (with $\mt{Basis.postData}$). This kind of handler should not be used with forms that exist solely within Ur/Web apps; for these, use Ur/Web's built-in support, as described below. It may still be useful to use $\mt{Basis.postBody}$ with form requests submitted by code outside an Ur/Web app. For such cases, the function $\mt{Top.postFields} : \mt{postBody} \to \mt{list} \; (\mt{string} \times \mt{string})$ may be useful, breaking a \texttt{POST} body of type \texttt{application/x-www-form-urlencoded} into its name-value pairs. Any normal page handler may also include arguments of type $\mt{option \; Basis.queryString}$, which will be handled specially. Rather than being deserialized from the current URI, such an argument is passed the whole query string that the handler received. The string may be analyzed by calling $\mt{Basis.show}$ on it. A handler of this kind may be passed as an argument to $\mt{Basis.effectfulUrl}$ to generate a URL to a page that may be used as a ``callback'' by an external service, such that the handler is allowed to cause side effects. @@ -2419,9 +2419,7 @@ Ur/Web programs generally mix server- and client-side code in a fairly transpare \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, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$. 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. +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, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$. 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. \subsection{Tasks} @@ -2443,6 +2441,19 @@ The currently supported task kinds are: \item $\mt{periodic} \; n$: Code that is run when the application starts up and then every $n$ seconds thereafter. \end{itemize} +\subsection{Security Model} + +Ur/Web follows a pragmatic security model that, nonetheless, isn't magic. The warranty can be voided using the foreign function interface (FFI; see next section), but it is easy to check if that interface is being used, solely by inspecting \texttt{.urp} files. If such inspection shows no use of the FFI, then a number of classic security problems are precluded (modulo bugs in the implementation of Ur/Web itself, of course): +\begin{itemize} +\item There can be no \textbf{code-injection attacks}. That is, strings are never implicitly interpreted as programs and run, which can be particularly problematic for strings coming from unconstrained user input. In the case of SQL code, the specialized name for such vulnerabilities is \emph{SQL injections}. In the case of HTML or JavaScript code, the specialized name is \emph{cross-site scripting}. Ur/Web programmers need not worry about the difference, because the Ur/Web implementation promises that you will know if a string is being interpreted as a program! +\item Ur/Web includes a kind of automatic protection against \textbf{cross-site request forgery (CSRF) 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 that the attacker couldn't cause directly due to lack of knowledge. +\item Quite a lot of other insecure monkey business can go in web applications. Ur/Web contains a pretty locked-down standard library, so that, for instance, it is not possible for Ur/Web code to access the file system directly... ergo it is not possible to leak secret file contents or overwrite files insecurely! The FFI must be used to summon such rights explicitly. +\end{itemize} + +However, Ur/Web doesn't guarantee ``any code that compiles is secure.'' The right model is that \emph{any HTTP endpoint exposed by the application can be called at any time with any argument values and any cookie values}. Ur/Web does nothing to guarantee that all function calls experienced by the application are possible according to legit traversal of links and forms! In particular, the cryptographic signing mentioned above is \emph{not} used to prevent users from making up whatever cookie values they like. It is just used to make sure an application only takes action based on cookie values when the user has explicitly submitted a form (and presumably the application author takes care to make all forms sufficiently intuitive, so none have surprising side effects that defy security or privacy expectations). + +Another philosophical assumption is that \emph{there is no hope of protecting a user against an attacker with access to the legit user's browser}. For instance, any attacker who can observe the HTML code of one page with CSRF protection is now able to trick the user into running arbitrary handler functions, since a cookie signature is not specific to the destination handler. Sure, we would improve security slightly (at the expense of Ur/Web implementation complexity) by making signatures handler-specific or even handler-argument-specific, but the idea is that you have already lost if an attacker has that kind of access to your browser. (And he needs browser access to see the page because of course your security-critical app is accessed only via TLS, right?) + \section{\label{ffi}The Foreign Function Interface} |