From db6451caad44785887bb9c9a1781bd861a3a46ce Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 23 Oct 2018 15:51:29 -0400 Subject: Fix a manual typo --- doc/manual.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/manual.tex b/doc/manual.tex index 857539db..d2db4816 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -2453,7 +2453,7 @@ It is most convenient to encapsulate an FFI binding with a new \texttt{.urp} fil \item \texttt{clientOnly Module.ident} registers a value as being allowed only in client-side code. \item \texttt{clientToServer Module.ident} declares a type as OK to marshal between clients and servers. By default, abstract FFI types are not allowed to be marshalled, since your library might be maintaining invariants that the simple serialization code doesn't check. \item \texttt{effectful Module.ident} registers a function that can have side effects. This is the default for \texttt{transaction}-based types, and, actually, this directive is mostly present for legacy compatibility reasons, since it used to be required explicitly for each \texttt{transaction}al function. -\item \texttt{ffi FILE.urs} names the file giving your library's signature. You can include multiple such files in a single \texttt{.urp} file, and each file \texttt{mod.urp} defines an FFI module \texttt{Mod}. +\item \texttt{ffi FILE.urs} names the file giving your library's signature. You can include multiple such files in a single \texttt{.urp} file, and each file \texttt{mod.urs} defines an FFI module \texttt{Mod}. \item \texttt{include FILE} requests inclusion of a C header file. \item \texttt{jsFile FILE} requests inclusion of a JavaScript source file. \item \texttt{jsFunc Module.ident=name} gives a mapping from an Ur name for a value to a JavaScript name. -- cgit v1.2.3 From c1932084390aca19c748da024b7b168c160a3aea Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 14 Dec 2018 15:42:59 -0500 Subject: New .urp option: safeGetDefault --- doc/manual.tex | 1 + src/compiler.sig | 1 + src/compiler.sml | 7 +++++++ src/demo.sml | 1 + src/settings.sig | 1 + src/settings.sml | 4 +++- 6 files changed, 14 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/manual.tex b/doc/manual.tex index d2db4816..e064e59e 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -190,6 +190,7 @@ Here is the complete list of directive forms. ``FFI'' stands for ``foreign func \item \texttt{profile} generates an executable that may be used with gprof. \item \texttt{rewrite KIND FROM TO} gives a rule for rewriting canonical module paths. For instance, the canonical path of a page may be \texttt{Mod1.Mod2.mypage}, while you would rather the page were accessed via a URL containing only \texttt{page}. The directive \texttt{rewrite url Mod1/Mod2/mypage page} would accomplish that. The possible values of \texttt{KIND} determine which kinds of objects are affected. The kind \texttt{all} matches any object, and \texttt{url} matches page URLs. The kinds \texttt{table}, \texttt{sequence}, and \texttt{view} match those sorts of SQL entities, and \texttt{relation} matches any of those three. \texttt{cookie} matches HTTP cookies, and \texttt{style} matches CSS class names. If \texttt{FROM} ends in \texttt{/*}, it is interpreted as a prefix matching rule, and rewriting occurs by replacing only the appropriate prefix of a path with \texttt{TO}. The \texttt{TO} field may be left empty to express the idea of deleting a prefix. For instance, \texttt{rewrite url Main/*} will strip all \texttt{Main/} prefixes from URLs. While the actual external names of relations and styles have parts separated by underscores instead of slashes, all rewrite rules must be written in terms of slashes. An optional suffix of \cd{[-]} for a \cd{rewrite} directive asks to additionally replace all \cd{\_} characters with \cd{-} characters, which can be handy for, e.g., interfacing with an off-the-shelf CSS library that prefers hyphens over underscores. \item \texttt{safeGet URI} asks to allow the page handler assigned this canonical URI prefix to cause persistent side effects, even if accessed via an HTTP \cd{GET} request. +\item \texttt{safeGetDefault} asks to allow \emph{any} page handler to cause side effects, even if accessed via an HTTP \cd{GET} request. \item \texttt{script URL} adds \texttt{URL} to the list of extra JavaScript files to be included at the beginning of any page that uses JavaScript. This is most useful for importing JavaScript versions of functions found in new FFI modules. \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server. \item \texttt{sigfile PATH} sets a path where your application should look for a key to use in cryptographic signing. This is used to prevent cross-site request forgery attacks for any form handler that both reads a cookie and creates side effects. If the referenced file doesn't exist, an application will create it and read its saved data on future invocations. You can also initialize the file manually with any contents at least 16 bytes long; the first 16 bytes will be treated as the key. diff --git a/src/compiler.sig b/src/compiler.sig index bcf69fd4..7922393d 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -61,6 +61,7 @@ signature COMPILER = sig dbms : string option, sigFile : string option, fileCache : string option, + safeGetDefault : bool, safeGets : string list, onError : (string * string list * string) option, minHeap : int, diff --git a/src/compiler.sml b/src/compiler.sml index f724bf56..271cf2f1 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -65,6 +65,7 @@ type job = { dbms : string option, sigFile : string option, fileCache : string option, + safeGetDefault : bool, safeGets : string list, onError : (string * string list * string) option, minHeap : int, @@ -385,6 +386,7 @@ fun institutionalizeJob (job : job) = Settings.setMetaRules (#filterMeta job); Option.app Settings.setProtocol (#protocol job); Option.app Settings.setDbms (#dbms job); + Settings.setSafeGetDefault (#safeGetDefault job); Settings.setSafeGets (#safeGets job); Settings.setOnError (#onError job); Settings.setMinHeap (#minHeap job); @@ -470,6 +472,7 @@ fun parseUrp' accLibs fname = dbms = NONE, sigFile = NONE, fileCache = NONE, + safeGetDefault = false, safeGets = [], onError = NONE, minHeap = 0, @@ -605,6 +608,7 @@ fun parseUrp' accLibs fname = val dbms = ref NONE val sigFile = ref (Settings.getSigFile ()) val fileCache = ref (Settings.getFileCache ()) + val safeGetDefault = ref false val safeGets = ref [] val onError = ref NONE val minHeap = ref 0 @@ -645,6 +649,7 @@ fun parseUrp' accLibs fname = dbms = !dbms, sigFile = !sigFile, fileCache = !fileCache, + safeGetDefault = !safeGetDefault, safeGets = rev (!safeGets), onError = !onError, minHeap = !minHeap, @@ -708,6 +713,7 @@ fun parseUrp' accLibs fname = dbms = mergeO #2 (#dbms old, #dbms new), sigFile = mergeO #2 (#sigFile old, #sigFile new), fileCache = mergeO #2 (#fileCache old, #fileCache new), + safeGetDefault = #safeGetDefault old orelse #safeGetDefault new, safeGets = #safeGets old @ #safeGets new, onError = mergeO #2 (#onError old, #onError new), minHeap = Int.max (#minHeap old, #minHeap new), @@ -829,6 +835,7 @@ fun parseUrp' accLibs fname = | "include" => headers := relifyA arg :: !headers | "script" => scripts := arg :: !scripts | "clientToServer" => clientToServer := ffiS () :: !clientToServer + | "safeGetDefault" => safeGetDefault := true | "safeGet" => safeGets := arg :: !safeGets | "effectful" => effectful := ffiS () :: !effectful | "benignEffectful" => benignEffectful := ffiS () :: !benignEffectful diff --git a/src/demo.sml b/src/demo.sml index 1e58e2f8..eaec38bb 100644 --- a/src/demo.sml +++ b/src/demo.sml @@ -124,6 +124,7 @@ fun make' {prefix, dirname, guided} = dbms = mergeWith #2 (#dbms combined, #dbms urp), sigFile = mergeWith #2 (#sigFile combined, #sigFile urp), fileCache = mergeWith #2 (#fileCache combined, #fileCache urp), + safeGetDefault = #safeGetDefault combined orelse #safeGetDefault urp, safeGets = #safeGets combined @ #safeGets urp, onError = NONE, minHeap = 0, diff --git a/src/settings.sig b/src/settings.sig index 986d6ed7..6ba7e96a 100644 --- a/src/settings.sig +++ b/src/settings.sig @@ -258,6 +258,7 @@ signature SETTINGS = sig val getFileCache : unit -> string option (* Which GET-able functions should be allowed to have side effects? *) + val setSafeGetDefault : bool -> unit val setSafeGets : string list -> unit val isSafeGet : string -> bool diff --git a/src/settings.sml b/src/settings.sml index cfbe98a5..3772fc04 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -740,9 +740,11 @@ structure SS = BinarySetFn(struct val compare = String.compare end) +val safeGetDefault = ref false val safeGet = ref SS.empty +fun setSafeGetDefault b = safeGetDefault := b fun setSafeGets ls = safeGet := SS.addList (SS.empty, ls) -fun isSafeGet x = SS.member (!safeGet, x) +fun isSafeGet x = !safeGetDefault orelse SS.member (!safeGet, x) val onError = ref (NONE : (string * string list * string) option) fun setOnError x = onError := x -- cgit v1.2.3 From ffcf765623b2da7ca330916eda404ac210eb513e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 19 Dec 2018 11:38:46 -0500 Subject: Follow-up to #146: update documentation --- demo/prose | 3 ++- doc/manual.tex | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/demo/prose b/demo/prose index ce12aba1..75c80169 100644 --- a/demo/prose +++ b/demo/prose @@ -5,12 +5,13 @@
Install System Dependencies

-

sudo apt-get install build-essential \
+
sudo apt install build-essential \
   emacs-goodies-el \
   libgmp-dev \
   libssl-dev \
   libpq-dev \
   libsqlite3-dev \
+  libicu-dev \
   mlton \
   sqlite3

diff --git a/doc/manual.tex b/doc/manual.tex index e064e59e..59727099 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -59,9 +59,9 @@ make sudo make install \end{verbatim} -Some other packages must be installed for the above to work. At a minimum, you need a standard UNIX shell, with standard UNIX tools like sed and GCC (or an alternate C compiler) in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the development files for the OpenSSL C library. As of this writing, in the ``testing'' version of Debian Linux, this command will install the more uncommon of these dependencies: +Some other packages must be installed for the above to work. At a minimum, you need a standard UNIX shell, with standard UNIX tools like sed and GCC (or an alternate C compiler) in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the development files for the OpenSSL C library and the ICU C library. As of this writing, in the ``testing'' version of Debian Linux, this command will install the more uncommon of these dependencies: \begin{verbatim} -apt-get install mlton libssl-dev +apt-get install mlton libssl-dev libicu-dev \end{verbatim} Note that, like the Ur/Web compiler, MLton is a whole-program optimizing compiler, so it frequently requires much more memory than old-fashioned compilers do. Expect building Ur/Web with MLton to require not much less than a gigabyte of RAM. If a \texttt{mlton} invocation ends suspiciously, the most likely explanation is that it has exhausted available memory. -- cgit v1.2.3 From 15105e3e62d595fe620d019a7ef9aeeb0197d24d Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 26 Jan 2019 14:24:48 -0500 Subject: Clarifying security model in the manual --- doc/manual.tex | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) (limited to 'doc') 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{} 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{} 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} -- cgit v1.2.3 From b8b2375819b2ac9fefb3299dcbb1e04f51cb71a6 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 27 Jan 2019 10:00:38 -0500 Subject: Manual entry for '-endpoints' --- doc/manual.tex | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc') diff --git a/doc/manual.tex b/doc/manual.tex index 8f7787fc..ba53f5d8 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -278,6 +278,8 @@ sqlite3 path/to/database/file Date: Wed, 17 Jul 2019 14:28:46 -0400 Subject: New JavaScript FFI function 'listen' --- doc/manual.tex | 1 + lib/js/urweb.js | 10 ++++++++++ 2 files changed, 11 insertions(+) (limited to 'doc') diff --git a/doc/manual.tex b/doc/manual.tex index ba53f5d8..62b322ae 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -2573,6 +2573,7 @@ It is possible to write JavaScript FFI code that interacts with the functional-r \item \cd{sr(v)} and \cd{sb(s, f)}, the ``return'' and ``bind'' monad operators, respectively \item \cd{ss(s)}, to produce the signal corresponding to source \cd{s} \item \cd{scur(s)}, to get the current value of signal \cd{s} + \item \cd{listen(s, f)}, to ask that function \cd{f} be called with the current value of \cd{s}, every time it changes, including immediately upon establishing this listener \end{itemize} \item The behavior of the \cd{} pseudo-tag may be mimicked by following the right convention in a piece of HTML source code with a type like $\mt{xbody}$. Such a piece of source code may be encoded with a JavaScript string. To insert a dynamic section, include a \cd{