Dependent Information Flow Types

Simple examples

(fun x: Sigma[u: int^BOT, n: int^U(u)]^BOT => if x.u == 1 then x.n else [int^U(1)] 0);;

/* Type: (Pi(x: Sigma[u: int^BOT, n: int^U(u)]^BOT).BOT; int^U(1))^BOT */


(fun x:Sigma[u:int^BOT, n:int^U(u)]^BOT => if x.u == 1 then x.n else [int^U(2)] 0);;

/* Type: (Pi(x: Sigma[u: int^BOT, n: int^U(u)]^BOT).BOT; int^U(TOP))^BOT */


(fun x:Sigma[u:int^BOT, n:int^U(u)]^BOT => if x.u == 1 then x.n else [int^A(TOP,TOP)] 0);;

/* Type: (Pi(x: Sigma[u: int^BOT, n: int^U(u)]^BOT).BOT; int^A(TOP, TOP))^BOT */


(fun x:int^BOT => [Sigma[u:int^BOT, n:int^U(u)]^BOT] [u:int^BOT = x, n:int^U(x) = 2]);;

/* Type: (Pi(x: int^BOT).BOT; Sigma[u: int^BOT, n: int^U(u)]^BOT)^BOT */


(fun x:int^BOT => [Sigma[u:int^BOT, n:int^U(x)]^BOT] [u:int^BOT = x, n:int^U(x) = 2]);;

/* Type: (Pi(x: int^BOT).BOT; Sigma[u: int^BOT, n: int^U(x)]^BOT)^BOT */


(fun x:int^BOT => [Sigma[u:int^BOT, n:int^U(u)]^BOT] [u:int^BOT = 1, n:int^U(x) = 2]);;

/* Wrong type: Expected declared type Sigma[u: int^BOT, n: int^U(u)]^BOT but found type Sigma[u: int^BOT, n: int^U(x)]^BOT */


let f = (fun x:int^BOT => [int^U(x)] x)
in f;;

/* Type: (Pi(x: int^BOT).BOT; int^U(x))^BOT */


let f = (fun x:int^BOT => [int^U(x)] x)
in f(1);;

/* Type: int^U(1) */


let f = (fun x:int^BOT => [int^U(x)] x)
in f(1) + f(2);;

/* Type: int^U(TOP) */


let f = (fun x:int^BOT => [int^U(x)] x)
in foreach(x in {1,3,4})
    with y = [int^U(1)] 0 
     do f(x) + y ;;

/* Type: int^U(TOP) */


foreach(x in {1,3,4})
  with y = [int^U(1)] 0 
    do x + y ;;

/* Type: int^U(1) */


let l = [{int^TOP}] {1,2,3} in
  foreach (x in l) with c = 0 do c+1;;

/* Type: int^TOP */


let b = { [s:int^TOP = 0], [s:int^TOP = 1], [s:int^TOP = 2]}
  in foreach (x in b) 
      with c = 0 
        do c+1 ;;

/* Type: int^TOP */


let b = { [s:ref(int^TOP)^BOT = ref [int^TOP] 0], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 1], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 2]}
  in foreach (x in b) 
       with c = 0 
         do c + !(x.s) ;;

/* Type: int^TOP */

let b = { [s:ref(int^TOP)^BOT = ref [int^TOP] 0], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 1], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 2]}
  in 
    foreach (x in b) 
      with c = 0 
        do ( (x.s) := !(x.s) + 1 ; !(x.s) ) ;;

/* Type: int^TOP */

let b = { [s:ref(int^TOP)^BOT = ref [int^TOP] 0], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 1], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 2]}
  in 
    foreach (x in b) 
      with c = 0 
        do ( (x.s) := !(x.s) + 1 ; c + 1 ) ;;

/* Type: int^BOT */


let b = { [s:ref(int^TOP)^BOT = ref [int^TOP] 0], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 1], 
          [s:ref(int^TOP)^BOT = ref [int^TOP] 2]}
  in 
    foreach (x in b) 
      with c = 0 
        do c + 1 ;;

/* Type: int^BOT */


let r = ref [int ^ U(BOT)] 1 in
let v = ref [int ^ U(BOT)] 2
  in (
    r := [ int ^ U(1) ] 1 ;
    if (!r == 0) then v := [ int ^ U(BOT) ] 1
  );;

/* Insecure flow detected from label U(1) to label U(BOT)! */


let r = ref [int ^ U(BOT)] 1 in
let v = ref [int ^ U(BOT)] 2
  in (
    r := [ int ^ U(BOT) ] 1 ;
    if (!r == 0) then v := [ int ^ U(BOT) ] 1
  );;
  
/* Type: cmd^U(BOT) */

let low = ref 0 in
  let f = (fun r: ref(int^BOT)^BOT, x:int^BOT => r := x)
   in  if [bool^TOP] true  then 
                f(low,1) ;;

/* Insecure flow detected from label TOP to label BOT! */

let high = ref [int ^ TOP ]0 in 
  let f = ( ]TOP[ (fun r: ref(int^TOP)^BOT, x:int^BOT => r := x ) )
    in if [bool^TOP] true then f(high,1)  ;;

/* Type: cmd^TOP */

let high = ref [int ^ TOP ]0 in 
  let f = ( ]TOP[ (fun r: ref(int^TOP)^BOT, x:int^BOT => r := x ) )
    in f  ;;

/* Type: (Pi(r: ref(int^TOP)^BOT, x: int^BOT).TOP; cmd^BOT)^BOT */

 let topSecrets = (
   let h = (let tmp = [h : int^TOP = 0] in tmp.h == 0) in
   if h then ({} : { int^TOP }) else ({} : { int^TOP })
 ) ;;

 foreach (x in topSecrets) with count = 0 do count + 1 ;;

/* Type: int^TOP */