User loginNavigation 
Parallel/DistributedA 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 highlevel authorization policies. To this end, the code for these systems relies on lowerlevel 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 spicalculus. 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... By Ehud Lamm at 20050510 19:51  Logic/Declarative  Parallel/Distributed  Type Theory  login or register to post comments  other blogs  3722 reads
MetaKlaim
Gianluigi Ferrari, Eugenio Moggi and Rosario Pugliese
MetaKlaim  a Type Safe Multistage 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 multistage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of metaprogramming 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 runtime 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. By Bryn Keller at 20050407 21:35  Functional  MetaProgramming  Parallel/Distributed  1 comment  other blogs  3862 reads
Recovering resources in the picalculusRecovering resources in the picalculus
By Andris Birkmanis at 20050403 07:48  Parallel/Distributed  Theory  6 comments  other blogs  8579 reads
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. By Anton van Straaten at 20050316 08:16  Lambda Calculus  Parallel/Distributed  login or register to post comments  other blogs  6275 reads
Linear ForwardersLinear 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 capabilitybased 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. By Andris Birkmanis at 20050308 13:58  Parallel/Distributed  Theory  2 comments  other blogs  5717 reads
SOAP considered canonicalThis 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:
I'm not sure if it's a rat I smell, or just my own inherent dislike of SOAP.
By Dominic Fox at 20050214 09:50  Parallel/Distributed  XML  5 comments  other blogs  7295 reads
The Kell Calculus
The Kell Calculus: A Family of HigherOrder 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 componentbased distributed programming. The Kell calculus is built around a picalculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higherorder 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 coinductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higherorder 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[...] By Andris Birkmanis at 20050214 08:55  Parallel/Distributed  Theory  1 comment  other blogs  15212 reads
Implicit parallel functional programmingThis discussion over on the Haskell Mailing List might interest those readers following the debates on concurrency issues in the discussion group... By Ehud Lamm at 20050124 13:19  Functional  Parallel/Distributed  8 comments  other blogs  9043 reads
O'Haskell  a functional objectoriented 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. By Andris Birkmanis at 20050122 12:46  ObjectFunctional  Parallel/Distributed  1 comment  other blogs  9259 reads
Process algebra needs proof methodologyIt'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 hardtoformalise 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. By Charles A Stewart at 20050116 15:46  Parallel/Distributed  2 comments  other blogs  6086 reads

Browse archivesActive forum topics 
Recent comments
4 days 15 hours ago
5 days 10 hours ago
5 days 14 hours ago
5 days 14 hours ago
5 days 16 hours ago
5 days 16 hours ago
5 days 17 hours ago
5 days 17 hours ago
5 days 21 hours ago
5 days 21 hours ago