Dependent Information Flow Types

Example: Multi-tenant Dropbox service

The example illustrates a mutable object store (objects encoded using records of closures), modeling a toy drop box service, featuring disjoint dynamically generated security compartments, ensuring that no interference may occur between tenants.
typedef 
  intf_type = 
     Sigma[ uid:int^BOT, 
            drop: (int^U(uid) => cmd^BOT)^BOT, 
            fetch: (cmd^BOT => int^U(uid))^BOT ]^BOT ;;

typedef 
  store_type = { ref (intf_type)^BOT };;

let 
  store =  ref ( { } : store_type )
in let user_code = ref [int^BOT] 0
in let new_box = 
  fun x:cmd^BOT => 
    (
    user_code := (! user_code)+1 ; 
    let u = ! user_code in
    let refr = ref [ int^U(u) ] 0
    in
    let stub =  [ uid:int^BOT=u, 
                  drop: (int^U(u) => cmd^BOT)^BOT = (fun d:int^U(u) => ( refr := d + !refr )  ), 
                  fetch: (cmd^BOT => int^U(u))^BOT  = (fun x:cmd^BOT =>  !refr ) ]
    in
    let obj = [ intf_type ] stub
    in
    let elt = ref obj
    in 
      ( store :=  ( elt ::  !store) ; obj  )
    )
in let open_box =
  (fun u:int^BOT => 
    let drops = !store
       in let r = (foreach (dr in drops) with acum = {}:{
                    Sigma[ uid:int^BOT, 
                           drop: (int^U(u) => cmd^BOT)^BOT, 
                           fetch: (cmd^BOT => int^U(u))^BOT ]^BOT} do 
                         let d = !dr
                         in if (d.uid == u) then
                              d::acum 
                             else acum)
          in first(r)
         )
in 
let usage_box =
  (fun c:cmd^BOT => 
    let drops = !store
       in foreach (dr in drops) with acum = 0 do 
             let d = !dr  in ( (  (  ( [ Sigma[ uid:int^BOT, 
                                drop: (int^U(BOT) => cmd^BOT)^BOT, 
                                fetch: (cmd^BOT => int^U(TOP))^BOT ]^BOT ] d).fetch ) ( skip) ) + acum )
  )
in
(
let d = new_box ( skip ) in
(
   let myusr = d.uid
   in
   let h = open_box (myusr)
   in (
         h.drop ([int^U(myusr)] 10);
         let v = h.fetch (skip) in h.drop (v);
         usage_box (skip)
      )
))
;;

/* negative case */

typedef 
  intf_type = 
     Sigma[ uid:int^BOT, 
            drop: (int^U(uid) => cmd^BOT)^BOT, 
            fetch: (cmd^BOT => int^U(uid))^BOT ]^BOT 
in typedef 
  store_type = { ref (intf_type)^BOT }
in let 
  store =  ref ( { } : store_type )
in let user_code = ref [int^BOT] 0
in let new_box = 
  fun x:cmd^BOT => 
    (
    user_code := (! user_code)+1 ; 
    let u = ! user_code in
    let refr = ref [ int^U(u) ] 0
    in
    let stub =  [ uid:int^BOT=u, 
                  drop: (int^U(u) => cmd^BOT)^BOT = (fun d:int^U(u) => ( refr := d + !refr )  ), 
                  fetch: (cmd^BOT => int^U(u))^BOT  = (fun x:cmd^BOT =>  !refr ) ]
    in
    let obj = [ intf_type ] stub
    in
    let elt = ref obj
    in 
      ( store :=  ( elt ::  !store) ; obj  )
    )
in let open_box =
  (fun u:int^BOT => 
    let drops = !store
       in let r = (foreach (dr in drops) with acum = {}:{
                    Sigma[ uid:int^BOT, 
                           drop: (int^U(u) => cmd^BOT)^BOT, 
                           fetch: (cmd^BOT => int^U(u))^BOT ]^BOT} do 
                         let d = !dr
                         in if (d.uid == u) then
                              d::acum 
                             else acum)
          in first(r)
         )
in 
let usage_box =
  (fun c:cmd^BOT => 
    let drops = !store
       in foreach (dr in drops) with acum = 0 do 
             let d = !dr  in ( (  (  ( [ Sigma[ uid:int^BOT, 
                                drop: (int^U(BOT) => cmd^BOT)^BOT, 
                                fetch: (cmd^BOT => int^U(TOP))^BOT ]^BOT ] d).fetch ) ( skip) ) + acum )
  )
in
(
let d = new_box ( skip ) in
let c = new_box ( skip ) in
(
   let myusr = d.uid
   in
   let h = open_box (myusr)
   in
   let yousr = c.uid 
   in
   let g = open_box (yousr)
   in (
         h.drop ([int^U(myusr)] 10);
         let v = h.fetch (skip) in g.drop ( v );
         usage_box (skip)
      )
))
;;