Information Flow Security























LIFTY* (Liquid Information Flow TYpes)


Use Liquid Types to encode (and repair) information flow.


Policy Agnostic Programming

  • Programmer only cares about functionality.
  • Policies are encoded as liquid types.
  • Vefirier automatically insert checks to enforce policies.



*Type-Driven Repair for Information Flow Security by Polikarpova et. al.












Example: Conference Managment System


showPaper :: PaperId -> IO () showPaper pid = print getCurrentUser $ do title <- getTitle pid authors <- getAuthors pid return (title ++ ":_" ++ show authors)


Blind Review Policy: Only Chair can see Authors.
Policy Violation: Look at the type error!

















Policies as Refinement Types


Blind Review Policy: Only Chair can see Authors. 

getAuthors :: PaperId -> Tagged <{\u -> u == Chair}> [User]


where the Tagged monad is policy parametric 

data Tagged <p :: User -> Bool> a




















Policy Propagation: The Tagged Monad


(>>=)  :: forall <p :: User -> Bool>. 
          Tagged <p> a
       -> (a -> Tagged <p> b)
       -> Tagged <p> b

return :: forall <p :: User -> Bool>. 
          a -> Tagged <p> a 

print  :: forall <p :: User -> Bool>. 
          viewer:Tagged <p> (User<p>) 
       -> msg:Tagged <p> String 
       -> IO ()
















The Chair can see more...


{-@ whenUserIsChair :: forall <p :: User -> Bool>.  
     Tagged <{\v -> v == Chair}>[a] 
  -> Tagged <p> [a] 
   @-}
whenUserIsChair t = do 
  u <- getCurrentUser 
  if u == Chair then t else return []

















Program Repair


Using the whenUserIsChair conditional


showPaperFixed :: PaperId -> IO () showPaperFixed pid = print getCurrentUser $ do title <- getTitle pid authors <- {- whenUserIsChair $ -} getAuthors pid return (title ++ ":_" ++ show authors)




















More complex policies



  • Viewer should have same privilages as the user (bug in HotCRP).

  • Only print paper status after notification date (bug in EDAS).




















Recap



  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Specify Properties of Data
  4. Termination: Semantic Termination Checking
  5. Reflection: Allow Haskell functions in Logic
  6. Case Study: Prove Program Equivalence
  7. Information Flow Security Policies