System configuration verification

This service performs the analysis of a networked system and verifies if its configuration is correct with respect to a Security Policy (based on Access Control List). The service relies on 3 input models:

(i.) the system model, including details about the physical environments, the devices included, the services provided and the physical and logical interconnections among all these elements; (ii.) the policy model (Access Control List) that specifies who can access to which resource; (iii.) the model of the agents operating in the systems (that is their initial location and initial knowledge).

This service provides an exhaustive analysis exploring all the possible states in which the agents can evolve leveraging sequences of changes of locations and accesses to resources (physical and logical). This kind of analysis builds up the complete set of all the actions the users can perform leveraging the particular configuration of the analyzed system. Based on this exploration, the service can compare this result with the security policy and can assess its correctness. As output results, this service builds a table in which the violations of the policy are highlighted. A violation can be of two kinds: a user that can access a resource against the rules in the security policy, and the opposite case, that is a user that is not able to access a resource even though the policy grants him explicit permissions. For each analyzed user, the service also provides the full Labelled Transition System (LTS) representing all the sequences of actions that the user can perform.