Niki Vazou

Liquid Haskell Developer

Niki is a research assistant professor at IMDEA Software Institute in Madrid.

Before that, she did a PhD at University of California, San Diego and a postdoc at University of Maryland.  She developed and maintains Liquid Haskell, a refinement type checker for Haskell programs that aims to make verification as easy as programming in Haskell. Liquid Haskell has been used to verify a variety of properties, ranging from metatheory to enforcement of sophisticated security.

Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but breaks non-interference. We present ANOSY, an approximate knowledge synthesizer for quantitative declassification policies. ANOSY uses refinement types to automatically construct machine checked over- and under-approximations of attacker knowledge for boolean queries on multi-integer secrets. It also provides an AnosyT monad transformer to track the attacker knowledge over multiple declassification queries, and checks for violations against the user-specified policies on information flow control applications. We implemented a prototype of ANOSY and showed that it is precise and permissive: up to 14 declassification queries were permitted before policy violation using the powersets of interval domain.