Abstract: Existing web services and mashups exemplify the need for flexible construction of distributed applications. How to do so securely remains a topic of current research. We present TAPIDO, a programming model to address Trust and Authorization concerns via Provenance and Integrity in systems of Distributed Objects. Creation of TAPIDO objects requires (static) authorization checks and their communication provides fine-grain control of their embedded authorization effects. TAPIDO programs constrain such delegation of rights by using provenance information. A type-and-effect system with effect polymorphism provides static support for the programmer to reason about security policies. We illustrate the programming model and static analysis with example programs and policies.

Abstract: In computing systems, trust is an expectation on the dynamic behavior of an agent; static analysis is a collection of techniques for establishing static bounds on the dynamic behavior of an agent. We study the relationship between code identity, static analysis and trust in open distributed systems. Our primary result is a robust safety theorem expressed in terms of a distributed higher-order pi-calculus with code identity and a primitive for remote attestation; types in the language make use of a rich specification language for access control policies.

Abstract: We address the programmatic realization of the access control model of security in a distributed system. Our aim is to bridge the gap between abstract/declarative policies and their concrete/operational implementations. The programming formalism of Daisy is an applied pi-calculus with an explicit notion of principal. The specification logic of Daisy is an extended Datalog built on top of authorization logics. We provide two kinds of static analysis methods to tie implementation to specification in Daisy -- type checking to show that a program is a sound implementation (i.e., that all granted accesses are in conformance with the policy), and model-checking to determine the degree of completeness (i.e., if the accesses permitted by the policy are actually granted in the implementation).

Abstract: We present a preliminary report on typing systems for polyadic muABC, a minimal language designed to capture the fundamental constructs of aspect oriented programming--pointcuts and advice--and nothing else. Tuples of uninterpreted names are used to trigger advice. The resulting language is remarkably unstructured: the least common denominator of the pi-calculus and Linda. As such, developing meaningful type systems is a substantial challenge.

Our work is guided by the translation of richly typed languages into muABC, specifically function- and class-based languages augmented with advice. The ``impedance mismatch'' between source and target is severe, and this leads us to a novel treatment of types in muABC.

Abstract: We define and study bisimulation for proving contextual equivalence in an aspect extension of the untyped lambda-calculus. To our knowledge, this is the first study of coinductive reasoning principles aimed at proving equality of aspect programs. The language we study is very small, yet powerful enough to encode mutable references and a range of temporal pointcuts (including cflow and regular event patterns).

Examples suggest that our bisimulation principle is useful. For an encoding of higher-order programs with state, our methods suffice to establish well-known and well-studied subtle examples involving higher-order functions with state.

Abstract: Firewalls are usually distributed in the network and typically configured in isolation. However, they are expected to work cooperatively to provide various desired security properties for the network. To make matters worse, such properties might be extremely difficult to verify because they can involve multiple devices. Without a global view of the network configuration, such a system is ripe for misconfiguration, causing conflicts and major security vulnerabilities. To enforce security and ensure seamless configuration management, we propose a high-level Firewall configuration Policy Language for traffic access control (called FLIP). With the support of FLIP, firewall security policies are defined as high-level service-oriented goals, which then are translated automatically into access control rules distributed at the appropriate enforcement security devices in the network. FLIP supports policy inheritance and customization features that enable defining a global firewall policy for large-scale enterprise network quickly and accurately. FLIP also guarantees generating non-conflicting intra- or inter-firewall rules. We prove the soundness and completeness of the policy translation algorithm and then we show in our evaluation study the improvement of the efficiency and accuracy of firewall policy management for large-scale networks using FLIP.

Abstract: We study mechanisms that permit program components to express role constraints on clients, focusing on programmatic security mechanisms, which permit access controls to be expressed, in situ, as part of the code realizing basic functionality. In this setting, two questions immediately arise:

• The user of a component faces the issue of safety: is a particular role sufficient to use the component?
• The component designer faces the dual issue of protection: is a particular role demanded in all execution paths of the component?

Abstract: Remote attestation allows programs running on trusted hardware to prove their identity (and that of their environment) to programs on other hosts. Remote attestation can be used to address security concerns if programs agree on the meaning of data in attestations. This paper studies the enforcement of code-identity based access control policies in a hostile distributed environment, using a combination of remote attestation, dynamic types, and typechecking. This ensures that programs agree on the meaning of data and cannot violate the access control policy, even in the presence of opponent processes. The formal setting is a pi-calculus with secure channels, process identity, and remote attestation. Our approach allows executables to be typechecked and deployed independently, without the need for secure initial key and policy distribution beyond trusted hardware.

Abstract: Aspect-oriented programming (AOP) has been touted as a promising paradigm for managing complex software-security concerns. Roughly, AOP allows the security-sensitive events in a system to be specified separately from core functionality. The events of interest are specified in a pointcut. When a pointcut triggers, control is redirected to advice, which intercepts the event, potentially redirecting it to an error handler.

Many interesting security properties are history-dependent; however, currently deployed pointcut languages cannot express history-sensitivity (mechanisms like cflow in AspectJ capture only the current call stack.) We present a language of pointcuts with past-time temporal operators and discuss their implementation using a variant of security automata. The main result is a proof that the implementation is correct.

Abstract: We study the incorporation of generic types in aspect languages. Since advice acts like method update, such a study has to accommodate the subtleties of the interaction of classes, polymorphism and aspects. Indeed, simple examples demonstrate that current aspect compiling techniques do not avoid runtime type errors.

We explore type systems with polymorphism for two models of parametric polymorphism: the type erasure semantics of Generic Java, and the type carrying semantics of designs such as generic C#. Our main contribution is the design and exploration of a source-level type system for a parametric OO language with aspects. We prove progress and preservation properties.

Abstract: Aspect-oriented programming is emerging as a powerful tool for system design and development. In this paper, we study aspects as primitive computational entities on par with objects, functions and horn-clauses. To this end, we introduce muABC, a name-based calculus, that incorporates aspects as primitive. In contrast to earlier work on aspects in the context of object-oriented and functional programming, the only computational entities in muABC are aspects. We establish a compositional translations into muABC from a functional language with aspects and higher-order functions. Further, we delineate the features required to support an aspect-oriented style by presenting a translation of muABC into an extended pi-calculus.

Abstract: Aspect-oriented programming (AOP) is a polarizing paradigm--attractive to some and repulsive to others. On the up side, AOP allows for new forms of encapsulation: each concern (eg, functionality, security) can be coded separately rather than interleaved in the same code base. On the down side, AOP destroys old forms of encapsulation: straight-line code no longer runs in a straight line. Static weaving has proven eminently practical, but many potential applications depend upon dynamic properties which do not lend themselves to this implementation technique. To realize its full potential, AOP must become both more controlled and more expressive. In each case, the issues are complex and difficult to arbitrate without formal models.

Abstract: Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. In earlier work, we described an untyped calculus of aspect programs with a direct description of the dynamic semantics. This calculus provides a specification for the correctness of weaving.

In this paper, we turn our attention to the interaction of aspects and types, whose subtleties are amply illustrated by the difficulties encountered by current compilers of aspect languages. We develop a typed calculus of aspect programs that includes inner classes, concurrency and dynamic arrival of new advice. To our knowledge, this is the first source-level typing system for a class-based aspect-oriented language.

Abstract: Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. The dynamic semantics of aspects is typically specified by appealing to an underlying object-oriented language via a compiler transformation known as weaving. This treatment is unsatisfactory for several reasons. Firstly, this semantics violates basic modularity principles of object-oriented programming. Secondly, the converse translation from object-oriented programs into an aspect language has a simple canonical flavor. Taken together, these observations suggest that aspects are worthy of study as primitive computational abstractions in their own right. In this paper, we describe an aspect calculus and its operational semantics. The calculus is rich enough to encompass many of the features of extant aspect-oriented frameworks that do not involve reflection. The independent description of the dynamic semantics of aspects enables us to specify the correctness of a weaving algorithm. We formalize weaving as a translation from the aspect calculus to a class-based object calculus, and prove its soundness.

Abstract: We propose an extension of the asynchronous pi-calculus in which a variety of security properties may be captured using types. The types are an extension of the Input/Output types for the pi-calculus in which I/O capabilities are assigned specific security levels. We define a typing system that ensures that processes running at security level sigma cannot access resources that have a security level higher than sigma. The notion of access control guaranteed by this system is formalized in terms of a Type Safety theorem. We then show that, for a certain class of processes, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behavior can not be influenced by changes to high-level behavior. This is formalized as a Non-Interference Theorem with respect to may testing.

Abstract: Flattening is a program transformation that eliminates nested parallel constructs, introducing flat parallel (vector) operations in their place. We define a sufficient syntactic condition for the correctness of flattening, providing a static approximation of Blelloch's ``containment''. This is acheived using a typing system that tracks the control flow of programs. Using a weak improvement preorder, we then show that the flattening transformations are intensionally correct for all well-typed programs.

Abstract: In open distributed systems of mobile agents, where code from remote sites may run locally, protection of sensitive data and system resources is of paramount importance. We present a capability-based typing system that provides such protection, using a mix of static and runtime typing. We formalize security violations as runtime errors and prove that, using our semantics, runtime errors cannot occur at ``good'' sites, i.e., sites under control of a particular administrative domain.

Abstract: We present a partially-typed semantics for Dpi, a distributed pi-calculus. The semantics is designed for mobile agents in open distributed systems in which some sites may harbor malicious intentions. Nonetheless, the semantics guarantees traditional type-safety properties at ``good'' locations by using a mixture of static and dynamic type-checking. We show how the semantics can be extended to allow trust between sites, improving performance and expressiveness without compromising type-safety.

Abstract: We study type-safety properties of open distributed systems of mobile agents, where not all sites are known to be well-typed. We adopt the underlying model of an anonymous network, allowing that code may be corrupted on transmission and that the source of incoming code is unknowable. Nonetheless, we are able to guarantee a weak form of type-safety at ``good'' sites using a mix of static and dynamic typing.

Abstract: We describe a typing system for a distributed pi-calculus which guarantees that distributed agents cannot access the resources of a system without first being granted the capability to do so. The language studied allows agents to move between distributed locations and to augment their set of capabilities via communication with other agents. The type system is based on the novel notion of a location type, which describes the set of resources available to an agent at a location. Resources are themselves equipped with capabilities, and thus an agent may be given permission to send data along a channel at a particular location without being granted permission to read data along the same channel. We also describe a tagged version of the language, where the capabilities of agents are made explicit in the syntax. Using this tagged language we define access violations as runtime errors and prove that well-typed programs are incapable of such errors.

Abstract: We describe a foundational language for specifying dynamically evolving networks of distributed processes, Dpi. The language is a distributed extension of the pi-calculus which incorporates the notions of remote execution, migration, and site failure. Novel features of Dpi include:

• Communication channels are explicitly located: the use of a channel requires knowledge of both the channel and its location.
• Names are endowed with permissions: the holder of a name may only use that name in the manner allowed by these permissions.

Abstract: Site failure is an essential aspect of distributed systems; nonetheless its effect on programming language semantics remains poorly understood. To model such systems, we define a process calculus in which processes are run at distributed locations. The language provides operators to kill locations, to test the status (dead or alive) of locations, and to spawn processes at remote locations. Using a variation of bisimulation, we provide alternative characterizations of strong and weak barbed congruence for this language, based on an operational semantics that uses configurations to record the status of locations. We then derive a second, symbolic characterization in which configurations are replaced by logical formulae. In the strong case the formulae come from a standard propositional logic, while in the weak case a temporal logic with past time modalities is required. The symbolic characterization establishes that, in principle, barbed congruence for such languages can be checked efficiently using existing techniques.

Abstract: The work/step framework provides a high-level cost model for nested data-parallel programming languages, allowing programmers to understand the efficiency of their codes without concern for the eventual mapping of tasks to processors. Vectorization, or flattening, is the key technique for compiling nested-parallel languages. This paper presents a formal study of vectorization, considering three low-level targets: the EREW, bounded-contention CREW, and CREW variants of the VRAM. For each, we describe a variant of the cost model and prove the correctness of vectorization for that model. The models impose different constraints on the set of programs and implementations that can be considered; we discuss these in detail.

Abstract: This paper presents a framework for the abstract interpretation of processes that pass values. We define a process description language that is parameterized with respect to the set of values that processes may exchange and show that an abstraction over values induces an abstract semantics for processes. Our main results state that if the abstract value interpretation safely/optimally approximates the ground interpretation, then the resulting abstracted processes safely/optimally approximate those derived from the ground semantics (in a precisely defined sense). As the processes derived from an abstract semantics in general have far fewer states than those derived from a concrete semantics, our technique enables the automatic analysis of systems that lie beyond the scope of existing techniques.

Abstract: The Proteus language is a wide-spectrum parallel programming notation that supports the expression of both high-level architecture-independent specifications and lower-level architecture-specific implementations. A methodology based on successive refinement and interactive experimentation supports the development of parallel algorithms from specification to various efficient architecture-dependent implementations. The Proteus system combines the language and tools supporting this methodology. This paper presents a brief overview of the Proteus system and describes its use in the exploration and development of several non-trivial algorithms, including the fast multipole algorithm for N-body computations.

Abstract: We summarize work on the Proteus project for prototyping and refining parallel applications. We describe the programming notation, the development methodology, the refinement system, and performance metrics. Several case studies are presented.

Abstract: We study the use of abstraction to reason operationally about concurrent programs. Our thesis is that abstraction can profitably be combined with operational semantics to produce new proof techniques. We study two very different applications:

• the implementation of nested data-parallelism, and
• the verification of value-passing processes.