A type discipline for authorization policies

A type discipline for authorization policies. Cedric Fournet; Andrew D. Gordon; Sergio Maffeis

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi-calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

I guess it's dependent types day around here...


Gianluigi Ferrari, Eugenio Moggi and Rosario Pugliese

MetaKlaim - a Type Safe Multi-stage Language for Global Computing

This paper describes the design and the semantics of MetaKlaim, an higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and “traditional” computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types ´a la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide are network applications are maintained whenever computations interoperate with potentially untrusted components.

Recovering resources in the pi-calculus

Recovering resources in the pi-calculus

Although limits of resources such as memory or disk usage
are one of the key problems of many communicating applications, most
process algebras fail to take this aspect of mobile and concurrent systems
into account. In order to study this problem, we introduce the Controlled
pi-calculus, an extension of the pi-calculus with a notion of recovery of
unused resources with an explicit (parametrized) garbage-collection and
dead-process elimination. We discuss the definition of garbage-collection
and dead-process elimination for concurrent, communicating applications,
and provide a type-based technique for statically proving resource
bounds. Selected examples are presented and show the potential of the
Controlled pi-calculus.

Foundational Calculi for Programming Languages (intro)

Since pi calculus is a hot topic lately, Pierce's Foundational Calculi for Programming Languages might be of interest as an introduction. It very briefly introduces and justifies foundational calculi in general, spends about 10 pages on lambda calculus, then builds on that with another 7 pages on pi calculus.

Linear Forwarders

Linear forwarders are actually the basic mechanism of an earlier implementation of the pi calculus called the fusion machine. We modify the fusion machine, replacing fusions by forwarders. The result is more robust in the presence of failures, and more fundamental.

And also:

The point of this paper is to solve the problem of input capability with a language that is “just right” – it neither disallows more features than necessary (as does the join calculus), nor adds more implementation work than is necessary (as does the fusion machine).

Yes, these are the same capabilities as in capability-based security. I am looking forward to read the complete paper, as it seems to confirm my unclear ideas of how capabilities and various pi calculi are related.

SOAP considered canonical

This article by Steve Maine argues that SOAP may be used as a canonical form for all varieties of messaging between participants in a distributed system, because they are all isomorphic to each other anyway:

For example, RPC and Messaging have already been shown to be isomorphic models of the same thing. There are similar dualities between "messages sent to a stateful service" and "methods called on a stateful object". All of these ideas are just attempts to build a conceptual model around the interactions between distributed systems. Unfortunately, each of these thought-models carries with it a certain amount of implicit semantic baggage, and that fact has really hampered the development of scalable, widely interoperable distributed systems to date.

I'm not sure if it's a rat I smell, or just my own inherent dislike of SOAP.

Dear Sir, I tried your distributed messaging protocol three years ago, and since then I have used no other...

The Kell Calculus

The Kell Calculus: A Family of Higher-Order Distributed Process Calculi
This paper presents the Kell calculus, a family of distributed process calculi, parameterized by languages for input patterns, that is intended as a basis for studying component-based distributed programming. The Kell calculus is built around a pi-calculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higher-order communication, programmable membranes, and dynamic binding. The paper discusses these principles, and defines the syntax and operational semantics common to all calculi in the Kell calculus family. The paper provides a co-inductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higher-order bisimulation called strong context bisimulation. The paper also contains several examples that illustrate the expressive power of Kell calculi.

NB: a family of calculi, parameterized by languages

See also: The Kell Calculus

In this page you will find information about the current state of the Kell calculus, links to published papers and drafts, information about where the Kell calculus is going[...]

Implicit parallel functional programming

This discussion over on the Haskell Mailing List might interest those readers following the debates on concurrency issues in the discussion group...

O'Haskell - a functional object-oriented concurrent PL

We mentioned O'Haskell previously on LtU, but a recent discussion of OOP vs. FP vs. everything made be to believe that it's worth to remember this (unfortunately unsupported) programming language.

It's instructive to read the rationale for this PL, as it helps to see how OOP and FP solve similar tasks in orthogonal (or just different) ways.

Note that the author of O'Haskell abandoned it in favor of Timber.

Process algebra needs proof methodology

It's widely appreciated that knowing that a distributed system or protocol behaves correctly is generally hard, and that process algebras provide useful formalisms for reasoning about these. Less appreciated is how hard it is to turn informal correctness proofs into formal proofs using process algebras.

Process algebra needs proof methodology (Fokkink, Groote & Reniers), an introductory article published a year ago in the Bulletin of the EATCS, provides a nice introduction to the problem of making process algebras more tractable for correctness reasoning, using Tanenbaum's sliding window protocol as a running example of a surprisingly hard-to-formalise proof.

Perhaps as interesting for LtU readers is that the article comes from the negelected "third" approach to process algebra (after CCS and CSP), namely the Algebra of Communicating Processes of Bergstra and Klop.

XML feed