Data-Centric Synchronization (DCS) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCS is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters. To overcome these limitations, in this paper we present AtomiS, a new DCS approach that requires only qualifying types of parameters and return values in interface definitions, and of fields in class definitions. The latter may also be abstracted away in type parameters, rendering class implementations virtually annotation-free. From this high level specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives that are responsible for ensuring the absence of data-races, atomicity-violations and deadlocks. We provide a Java implementation and showcase the applicability of AtomiS in real-life code. For the benchmarks analysed, AtomiS requires fewer annotations than the original number of regions requiring locks, as well as fewer annotations than Atomic Sets (a reference DCS proposal).

Noninterference is the classic information flow property that establishes the absence of illegal information flows. Legality of flows is originally defined with respect to a single security setting that is based on a security lattice that orders security levels according to their confidentiality and/or integrity. This paper proposes a natural generalization of noninterference to a distributed security setting where each computation domain establishes its own local security lattice. Referred to as distributed noninterference (DNI), the new security property implies that information flows respect the allowed flow policy of the domains where they are computed. The semantic coherence between DNI and other information flow related properties for distributed settings is established. We present a type and effect system that enforces DNI for an expressive distributed higher-order lambda-calculus with imperative features and code migration.

With the emergence of the new possibilities offered by global computing, new security issues follow from the fact that these possibilities can be equally exploited by parties with malicious intentions. Many attacks arise at the application level, and can be tackled by means of programming language techniques. For instance, confidentiality can be violated during the execution of programs that reveal secret information. This kind of program behaviour can be avoided by information flow analyses that detect the encoding of illegal flows. This paper studies information flows that occur in distributed programs with code mobility from a language-based security perspective. New forms of security leaks that are introduced by code mobility, which we callmigration leaks, are presented and compared with well-known forms of illegal flow. We propose an information flow property that is adequate for networks consisting of a generalisation of the non-disclosure policy. We design a type and effect system for enforcing it on an expressive distributed calculus, and explain a soundness proof methodology in detail.

In existing RBAC literature, administrative privileges are inherited just like ordinary user privileges. We argue that from a security viewpoint this is too restrictive, and we believe that a more flexible approach can be very useful in practice. We define an ordering on the set of administrative privileges, enabling us to extend the standard privilege inheritance relation in a natural way. This means that if a user has a particular administrative privilege, then she is also implicitly authorized for weaker administrative privileges. We prove the non-trivial result that it is possible to decide whether one administrative privilege is weaker than another and show how this result can be used to decide administrative requests in an RBAC security monitor.