We describe a framework for specifying, merging and analyzing modular policies. We present policy automata, a formal model of computations that grant or deny access to a resource. This model combines defeasible logic with state machines, representing complex policies as combinations of simpler modular policies. We demonstrate this framework by applying it to a concrete application: a programmable payment card that can accept new policies dynamically. We present Polaris, a tool which analyzes policy automata to reveal potential conflicts or redundant policies, and compiles automata into Java Card applets.