NETRA: Seeing Through Access Control

We present netra, a tool for systematically analyzing and detecting explicit information-flow vulnerabilities in access control configurations. Our tool takes a snapshot of the access-control metadata, and performs static analysis on this snapshot. We devise an augmented relational calculus that naturally models both access control mechanisms and information-flow policies uniformly. This calculus is interpreted as a logic program, with a fixpoint semantics similar to Datalog, and produces all access tuples in a given configuration that violate properties of interest. Our analysis framework is programmable both at the model level and at the property level, effectively separating mechanism from policy. We demonstrate the effectiveness of this modularity by analyzing two systems with very different mechanisms for access control—Windows XP and SELinux—with the same specification of information-flow vulnerabilities. netra finds vulnerabilities in default configurations of both systems.