Program synthesis in administration of higher-order permissions.

In "administrative" access control, policy controls permissions not just on application actions, but also on actions to modify permissions, on actions to modify permissions on those actions, and so on. One context of work in administrative policy is "administrative RBAC", in which policy controls the permissions of roles, the membership of roles, and other elements of RBAC access-control state. Here we study and extend the UARBAC model for administrative RBAC from the perspective of usability and expressiveness. Using tools from logic and program verification, we formulate UARBAC logically and develop an algorithm that produces "administrative plans" that achieve specified permissions through permitted actions. This work is closely related to work on the safety problem in administrative access control, but is intended to aid legitimate users in understanding how to achieve a desired access-control state. We then show how this machinery can be used so that administrative actions at any desired depth, and so plans as well, can be uniformly simulated in the existing UARBAC model.