Refinement-based Design of a Group-centric Secure Information Sharing Model

This paper presents a formal, state machine-based specification (stateful specification) of a high assurance, secure information-sharing policy. The policy is group-centric; users join and leave groups, objects are added and removed (group operations). Users gain access to objects via membership relationships they have or have had with groups that contain or have contained those objects. The stateful specification given here is a refinement of a prior specification that is given in first-order linear temporal logic (FOTL). The prior FOTL specification defines authorization based solely on event histories, but gives little guidance regarding implementation. The current specification is the result of a second step in a multi-step design process that separates concerns and provides multiple opportunities to detect unintended policy characteristics. We show that our stateful specification is consistent with the prior FOTL specification with respect to the action sequences it permits and the authorization decisions it renders. For verification purposes we use a combination of model-checking and manual techniques.