1. A method comprising: retrieving, from a storage location, a storage and privacy service (SPS) program expressing one or more access control rules; generating, using a processor, a verification representation of the SPS program based on one or more assertions; submitting the verification representation to a constraint solver to generate a set of access control outputs; and determining if the set of access control outputs returned from the constraint solver satisfy a desired set of privacy constraints.