Access Control Policies Across Abstraction Layers

System administrators specify the access control policy they want and implement the relevant configuration for enforcing it. Specifying policies and implementing configurations require users to switch from one level of abstraction to another, often changing language and tools. The gap between these two abstraction layers seems to be a widespread problem, and may cause poor security and low efficiency. Our thesis aims at proposing solutions, based on formal semantics and logic, for security engineers to interact with access control systems at different abstraction layers for configuring, updating and verifying system behaviour. We consider different contexts: networks, operating systems and collaborative environments. For each of them we formally model the low level of the executable configurations and propose a high level language inspired by the needs of policy designers. For network security, we propose FWS, a tool that allows the administrator to manage a firewall configuration written in a legacy language (iptables, pf, ipfw) abstracting away from low level details like shadowing, tags and the limitations of packet matching. The idea is to provide the administrator with a declarative description of the behaviour, and with the means for reasoning about the system security. The possibly modified declarative description can be then compiled back to the preferred language. This also offers the possibility for transcompilation, but contrary to the expectation, legacy languages are not equally expressive. We study the expressive power of Unix firewall languages and propose the tool F2F to check if a given configuration is expressible in another firewall language. For system security, we target SELinux configurations. We propose IFL, a domain specific language for defining fine grained information flow requirements (including confidentiality, integrity and non-transitive properties). IFL expresses both functional requirements, i.e., which permissions must be granted to users for performing their authorized tasks, and security requirements, i.e., information flows to forbid because possibly dangerous. We extend CIL, a SELinux policy language for writing structured configurations, with IFL requirements. In this way, the administrator abstracts from the details of the system, expressing desired high level properties of the configuration. A verification procedure is given and implemented in the tool IFCILverif that statically checks that all the requirements are met in a configuration. Moreover, we empirically validate our formal semantics of CIL, and discover some unspecified corner cases and disagreements between the documentation and the compiler. Finally, we consider collaborative environments, in which the users interact by sharing or exchanging assets for mutual advantage. We designed MuAC, an high level language with which each user can express what they want in return for allowing access to their assets. We address both the case of infinite or reusable assets, where the asset is still available to the owner after he allows access to it, and the case of finite resources that are consumed when exchanged. The low level is a non-standard logical theory that also gives semantics to MuAC policies, and the evaluation of access requests rely on logical deductions. Finally, we propose a compilation from abstract policies to logical theories, and an algorithm for deciding access requests by changing ownership of the resources or updating an access control matrix, driving the system to behave correctly.