ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

TL;DR

ANOSY is a tool that uses refinement types to automatically approximate attacker knowledge, enabling safe and precise declassification of sensitive data in information flow control systems.

Contribution

It introduces ANOSY, a novel approximate knowledge synthesizer that automatically constructs over- and under-approximations for declassification policies using refinement types.

Findings

ANOSY permits up to 14 declassification queries before policy violation.

It is both precise and permissive in tracking attacker knowledge.

The prototype demonstrates effective enforcement of quantitative declassification policies.

Abstract

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 to track the attacker knowledge over multiple declassification queries and checks for violations against user-specified policies in information flow control applications. We implement a prototype of ANOSY and show that it is precise and permissive: up to 14 declassification queries are permitted before a policy violation occurs using the powerset of intervals domain.