# HG changeset patch # User Adam Chlipala # Date 1241379529 14400 # Node ID 7394368a5cadc7bac9ff07028e44e1a701513fb2 # Parent 7b47fc964a0f5becc294079c9a1ec2c407f3efa9 cookieSec demo diff -r 7b47fc964a0f -r 7394368a5cad demo/cookieSec.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/cookieSec.ur Sun May 03 15:38:49 2009 -0400 @@ -0,0 +1,39 @@ +cookie username : string + +table lastVisit : { User : string, When : time } + PRIMARY KEY User + +fun main () = + userO <- getCookie username; + + list <- queryX (SELECT * FROM lastVisit) + (fn r => {[r.LastVisit.User]} {[r.LastVisit.When]}); + + return + Cookie: {[userO]}
+ + + + {list} +

User	Last Visit

+ +

Set cookie value

+ + +and set r = + setCookie username r.User; + main () + +and imHere () = + userO <- getCookie username; + case userO of + None => return You don't have a cookie set! + | Some user => + dml (DELETE FROM lastVisit WHERE User = {[user]}); + dml (INSERT INTO lastVisit (User, When) VALUES ({[user]}, CURRENT_TIMESTAMP)); + main () + diff -r 7b47fc964a0f -r 7394368a5cad demo/cookieSec.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/cookieSec.urp Sun May 03 15:38:49 2009 -0400 @@ -0,0 +1,4 @@ +database dbname=test +sql cookieSec.sql + +cookieSec diff -r 7b47fc964a0f -r 7394368a5cad demo/cookieSec.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/cookieSec.urs Sun May 03 15:38:49 2009 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page diff -r 7b47fc964a0f -r 7394368a5cad demo/prose --- a/demo/prose Sun May 03 15:13:00 2009 -0400 +++ b/demo/prose Sun May 03 15:38:49 2009 -0400 @@ -143,6 +143,12 @@

SQL views are also supported with a special declaration form, analogous to table. A multi-parameter type class fieldsOf is used to characterize places where both tables and views are allowed. For instance, the polymorphic function list shown here lists the contents of any table or view containing just a single int column named A.

+cookieSec.urp + +

Ur/Web guarantees that compiled applications are immune to certain kinds of cross site request forgery. 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.

+ +

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.

+ sum.urp

Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.

diff -r 7b47fc964a0f -r 7394368a5cad src/cjr_print.sml --- a/src/cjr_print.sml Sun May 03 15:13:00 2009 -0400 +++ b/src/cjr_print.sml Sun May 03 15:38:49 2009 -0400 @@ -2421,20 +2421,20 @@ E.declBinds env d)) env ds - fun flatFields (t : typ) = + fun flatFields always (t : typ) = case #1 t of TRecord i => let val xts = E.lookupStruct env i in - SOME (map #1 xts :: List.concat (List.mapPartial (flatFields o #2) xts)) + SOME ((always @ map #1 xts) :: List.concat (List.mapPartial (flatFields [] o #2) xts)) end | TList (_, i) => let val ts = E.lookupStruct env i in case ts of - [("1", t'), ("2", _)] => flatFields t' + [("1", t'), ("2", _)] => flatFields [] t' | _ => raise Fail "CjrPrint: Bad struct for TList" end | _ => NONE @@ -2448,12 +2448,11 @@ (TRecord i, loc) => let val xts = E.lookupStruct env i - val xts = case eff of - ReadCookieWrite => - (sigName xts, (TRecord 0, ErrorMsg.dummySpan)) :: xts - | _ => xts + val extra = case eff of + ReadCookieWrite => [sigName xts] + | _ => [] in - case flatFields (TRecord i, loc) of + case flatFields extra (TRecord i, loc) of NONE => raise Fail "CjrPrint: flatFields impossible" | SOME fields' => List.revAppend (fields', fields) end diff -r 7b47fc964a0f -r 7394368a5cad src/settings.sml --- a/src/settings.sml Sun May 03 15:13:00 2009 -0400 +++ b/src/settings.sml Sun May 03 15:38:49 2009 -0400 @@ -77,7 +77,9 @@ fun setClientToServer ls = clientToServer := S.addList (clientToServerBase, ls) fun mayClientToServer x = S.member (!clientToServer, x) -val effectfulBase = basis ["set_cookie", +val effectfulBase = basis ["dml", + "nextval", + "set_cookie", "new_client_source", "get_client_source", "set_client_source",

Set cookie value

Record your visit