29 citations · 30 across the 6 of their papers we have counts for
11 papers
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
Sankha Narayan Guria, Niki Vazou, Marco Guarnieri +1
Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but bre…
REST: Integrating Term Rewriting with Program Verification (Extended Version)
Zachary Grannan, Niki Vazou, Eva Darulova +1
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables fl…
Refinement Types: A Tutorial
Ranjit Jhala, Niki Vazou
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable…
LIO*: Low Level Information Flow Control in F*
Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin +1
We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired…
Type-Level Computations for Ruby Libraries
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou +2
Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often aris…
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, Michael Hicks
This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enfor…