Journal entries

An Atom feed Atom feed of these posts is also available.

Progress on Secur(abl)e Syndication

Besides working on the new website, over the last couple of days I’ve been consolidating the theory and implementation of secure/securable syndicated actors.

I decided to implement a syndicated-actor chat service similar to the one @dustyweb implemented for Spritely Goblins (see blog post and code), to help draw out the requirements and implementation constraints.

The code is here:

It went well. Using Preserves Schemas to define a protocol, and then using capability attenuation to enforce conformant use of the shared dataspace led to a system that prevented users1 from forging messages from other users, and prevented nick collisions from happening.

Here’s the schema defining the protocol:

    version 1 .
    embeddedType Actor.Ref .

    UserId = int .

    Join = <joinedUser @uid UserId @handle ref>.
    NickClaim = <claimNick @uid UserId @name string @k ref>.
    UserInfo = <user @uid UserId @name string>.
    Says = <says @who UserId @what string>.
    NickConflict = <nickConflict>.

The system has two moving pieces (besides the dataspace server itself): a single “moderator”, and zero or more “clients”.

A client asserts interest in a Join record. In response to their interest, the moderator allocates a user ID for the new connection and a new session handle, and asserts a Join record back to the client giving them access to their session.

The session handle is just a reference to the dataspace, attenuated to allow access only using the uid assigned to the connection:

    attenuate(ds, rfilter(
        pRec($Observe, pLit($user), pEmbedded()),
        pRec($Observe, pLit($says), pEmbedded()),
        pRec($claimNick, pLit(uid), pString(), pEmbedded()),
        pRec($says, pLit(uid), pString()))),

Using this reference and trying to assert anything or send any message not matching one of those patterns results in the assertion or message being silently dropped.

  1. There’s one key difference between the sketch I built and the system @dustyweb implemented: Goblins has sealers for making unforgeable signed secret envelopes containing values. My implementation doesn’t yet have sealers. Sealers make it possible to prove that the chatroom hasn’t forged any messages, as well as that users can’t forge each other’s messages. My sketch can only prove that attached users haven’t forged messages: you have to trust the chatroom more than in @dustyweb’s system. 

New website

Over the past couple of weeks I’ve been working on a new website for the Syndicate project.

A big part of this has been to widen its focus from just Syndicate per se, in order to avoid the confusion caused by treating “Syndicate” as an umbrella term for a novel Actor model, for Dataspaces, for Conversational Concurrency, for the Domain-Specific Language (DSL) features supporting syndicated-actor programming, and so on.

The new site splits out a few concepts to be treated independently:

  • The Syndicated Actor model is the name for the theory that I started to develop in my dissertation and that I’m still working on.

  • A dataspace is a special kind of syndicated actor whose job is to relay and replicate syndicated state from peer to peer, decoupling information flow from actor identity.

  • The Syndicate DSL is a bundle of language features that make programming with syndicated actors and dataspaces more ergonomic. These features are layered atop base languages like Java, Racket, TypeScript/JavaScript and so on.

  • Conversational concurrency is a term I introduced in my dissertation that captures the style of design of syndicated-actor programs.

The site’s not finished yet, but I think it’s rapidly approaching publishable shape.