A Toosht o Whigmaleeries

We have recently completed the final version of our paper for this year's Haskell Symposium in Edinburgh.  We develop some reasoning principles for transaction-based programs in STM Haskell.  This has been a fun project for me, bringing together a range of my interests: operational semantics for concurrency, Haskell (the subject of my PhD), the ambient calculus (many papers some time ago), oh and types (subject of many papers now and no doubt in the future).

We're interested in all and any comments you may have.  Enjoy!

A Compositional Theory for STM Haskell.

J. Borgstroem, A.D. Gordon, and K. Bhargavan

We address the problem of reasoning about Haskell programs that use Software Transactional Memory (STM). As a motivating example, we consider Haskell code for a concurrent non-deterministic tree rewriting algorithm implementing the operational semantics of the ambient calculus. The core of our theory is a uniform model, in the spirit of process calculi, of the run-time state of multi-threaded STM Haskell programs. The model was designed to simplify both local and compositional reasoning about STM programs. A single reduction relation captures both pure functional computations and also effectful computations in the STM and I/O monads. We state and prove liveness, soundness, completeness, safety, and termination properties relating source processes and their Haskell implementation. Our proof exploits various ideas from concurrency theory, such as the bisimulation technique, but in the setting of a widely used programming language rather than an abstract process calculus. Additionally, we develop an equational theory for reasoning about STM Haskell programs, and establish for the first time equations conjectured by the designers of STM Haskell. We conclude that using a pure functional language extended with STM facilitates reasoning about concurrent implementation code.

Slides from a very interesting sounding workshop on formal and computational models of cryptography are up on the web.

A very enjoyable meeting, to celebrate the work of Sir Tony Hoare, is just over this afternoon.

Many of the speakers had favourite quotes by Tony.  My favourite of the favourites was in a note received by Phil Wadler during the design of Haskell, and quoted this morning by Simon Peyton Jones: "I fear that Haskell is doomed to succeed"!

I also discovered that by coincidence today is the eleventh anniversary of Tony taking Bill's shilling, the day he sent in his first invoice to Microsoft.  See the email I include at the end of my presentation Roles, Stacks, Histories: A Triple for Hoare.  (The accompanying paper is here.)

I'm happy to be giving a talk at an event later this month to celebrate Tony Hoare's 75th birthday.

We have just posted (here) a full draft of a paper to accompany the talk.  Check it out!  Comments would be most welcome, as we are continuing to develop the paper.  And come to think of it, perhaps it's time to start work on the talk.

Roles, Stacks, Histories: A Triple for Hoare.

J. Borgstroem, A. D. Gordon, and R. Pucella. Draft, 2009.

Behavioural type and effect systems regulate properties such as adherence to object and communication protocols, dynamic security policies, avoidance of race conditions, and many others. Typically, each system is based on some specific syntax of constraints, and is checked with an ad hoc solver. Instead, we advocate types refined with first-order logic formulas as a basis for behavioural type systems, and general purpose automated theorem provers as an effective means of checking programs. In particular, we describe a triple of security-related type systems: for stack inspection, for history-based access control, and for role-based access control. The three are all instances of a refined state monad. Our semantics allows a precise comparison of the similarities and differences of these mechanisms. Moreover, the benefit of behavioural type-checking is to rule out the possibility of unexpected security exceptions, a common problem with code-based access control.

Adam Chlipala is working on a textbook on the Coq proof assistant.  Good to know.

The Security Protocols Workshop is taking place next week in Cambridge, Wednesday to Friday.  The draft programme is now available on the web.  I have a paper with Aybek Mukhamedov and Mark Ryan on "Towards a Verified Reference Implementation of a Trusted Platform Module".  The line up of speakers is great, and I just have to travel across town.  It should be a Good One!

I'm giving a series of lectures on refinement types at various places this year, so I've started a new webpage to collect relevant resources and the schedule.  More to come, but here it is.

See here for the official advert for postdoc positions at our lab.  These are well-funded two-year positions.  Contact me if you are interested in a postdoc in the areas of programming languages or security.

I’m sitting on the programme committee for this year’s ML workshop.  It takes place up in Edinburgh on Sunday August 30, the day before ICFP.  It is the place for innovative work in the ML family of languages – send us your best work!

We seek papers on topics related to ML, including, but not limited to:

• applications: case studies, experience reports, pearls, etc.
• extensions: higher forms of polymorphism, generic programming, objects, concurrency, distribution and mobility, semi-structured data handling, etc.
• type systems: inference, effects, overloading, modules, contracts, specifications and assertions, dynamic typing, error reporting, etc.
• implementation: compilers, interpreters, type checkers, partial evaluators, runtime systems, garbage collectors, etc.
• environments: libraries, tools, editors, debuggers, cross-language interoperability, functional data structures, etc.
• semantics: operational, denotational, program equivalence, parametricity, mechanization, etc.

By the way, for some reason the organisers chose to schedule ICFP in the final week of the Edinburgh International Festival, so if you are planning to attend ICFP or the ML workshop, I’d book your hotel room now!

George Danezis and I organised a research meeting at MSRC Thursday and Friday last week.

This was the first meeting of a network of researchers – CryptoForma - initiated by Eerke Boiten; the goal is to bring together leading UK-based researchers in cryptography and in formal methods for security.  These areas have been disjoint, but bringing them together is increasingly possible and desirable – eg we are getting to the point where we can apply scalable static analysis to establish strong security properties of implementation code in computational models familiar to cryptographers.

We had a series of stimulating presentations, a fine dinner at King’s College, and built up considerable enthusiasm for the project.  A follow-up meeting is planned at the Information Security Group at Royal Holloway in the summer.

http://research.microsoft.com/en-us/people/gdane/cryptoformaschedule.aspx

Main speakers and titles (there were also some short talks):

• Dan Grundy (Kent) "Calculational proofs for one-way functions"
• Misha Aizatulin (OU) "Balanced Contract Signing"
• James Heather (Surrey) "Re-encryption in a symmetric setting"
• Eerke Boiten (Kent) "The bottom-up formal methods perspective”
• MSR Talk: Ross Smith (MS) "Dude, where’s my boss? Using Serious Games to improve software development productivity"
• Mark Ryan (Birmingham) "TPM Protocols and their Verification"
• Jan Juerjens (MSRC/OU) "Modularity and refinement in the verification of crypto-protocols"
• Aybek Mukhamedov (Birmingham) "Formal analysis of the Trusted Platform Module"
• Alfredo Pironti (Torino) "Towards provably correct black-box monitoring of security protocols"
• Cédric Fournet (MSRC) "A Cryptographic Compiler for Information-Flow Security"
• Karthik Bhargavan (MSRC) "Computational Verification of TLS Implementations"
• Liqun Chen (HP) "Parsing ambiguities in authentication and key establishment protocols"
• Tom Chothia (Birmingham) "Measuring Information Leakage Using Network Information Theory"
• Bogdan Warinschi (Bristol) "A compositional soundness result"

• Kenny Paterson (RHUL) "Limitations of provable security with respect to crypto specifications and implementations"

Standing: Johannes Borgstroem (MSRC), Kenny Paterson (RHUL), James Heather (Surrey), Nigel Smart (Bristol), Mark Ryan (Birmingham), Eerke Boiten (Kent), Dan Grundy (Kent), Essam Ghadafi (Bristol), Claudia Diaz (Leuven), Gaven Watson (RHUL), Liqun Chen (HPL), Bogdan Warinschi (Bristol), Stephen Williams (Bristol), Mike Roe (MRSC), Alfredo Pironti (Torino), Aybek Mukhamedov (Birmingham), Francois Dupressoir (OU)

Kneeling: Karthik Bhargavan (MSRC), Jan Juerjens (OU/MSRC), Andy Gordon (MSRC), George Danezis (MSRC), Jean Martina (Cambridge), Tom Chothia (Birmingham)

Not pictured: Misha Aizatulin (OU), Mo Becker (MSRC), Aaron Coble (Cambridge), Cédric Fournet (MSRC)

Some good stuff over at Notices of the American Mathematical Society on various proof tools for mechanized mathematical reasoning.

• Thomas Hales Formal Proof
• Georges Gonthier Formal Proof--The Four-Color Theorem
• John Harrison Formal Proof--Theory and Practice
• Freek Wiedijk Formal Proof--Getting Started

Here are some write-ups of a couple of recent, informative workshops I attended.

• Mike Gordon has created a blog for ongoing discussion re the Linking Tools for Verification Workshop
• Paul Anderson has created a webpage as a record of the LISA Virtual Infrastructure Workshop

I'm back from being rapporteur at the habilitation defence of Bruno Blanchet yesterday.  His slides are an excellent introduction to his world-leading tools ProVerif and CryptoVerif.  His work is excellent and I feel honoured to be rapporteur.  Well done, Bruno!

Automatic verification of security protocols: formal model and computational model

This report summarizes my work on security protocol verification, which has mainly consisted in the design and implementation of two automatic protocol verifiers, ProVerif and CryptoVerif.

The verifier ProVerif is based on the formal model of cryptography. Dolev-Yao model). In this model, cryptographic primitives are considered as black boxes. ProVerif is based on an abstract representation of the protocol by Horn clauses. It can handle many different cryptographic primitives, specified both as rewrite rules or as equations. It can handle an unbounded number of sessions of the protocol and an unbounded message space. It can prove secrecy properties, correspondences (authentication) and some process equivalences.

The verifier CryptoVerif is based on the computational model of cryptography. In this model, messages are bitstrings and cryptographic primitives are functions on bitstrings. CryptoVerif generates proofs by sequences of games, as used by cryptographers. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. CryptoVerif provides a generic mechanism for specifying the security assumptions on cryptographic primitives. It can also evaluate the probability of breaking the protocol as a function of the probability of breaking each cryptographic primitive and of the number of sessions.

There is already some excellent work by my esteemed co-author Nikhil Swamy and colleague Mike Hicks on SELinks, a security-enhanced version of the Wadler et al's Links programming language.  Links is a multi-tier language; within a single source program you can express logic that runs on the client, web server, and database tiers.  SELinks focuses on securing Links' interactions with the database tier.

Meanwhile, I have been working with PhD student Yiannis Baltopoulos on securing Links' interactions with the client, ie, the browser.  In particular, we have been looking at what happens when the browser is under the control of an untrustworthy user.  Links stores session state as continuations in the current web pages.  We found some situations in which a user can use a browser to inspect and change these continuations so as to discover secret data, to change data (eg a price for an item), or to change control flow (eg to reach an unexpected page).  The fix is for the server to authenticate, with a hash, and to encrypt any continuations that may flow to the client.  Yiannis has a diff for the Links' sources to implement this fix.  Moreover, we formalize this fix within the type theory RCF (see MSR-TR-2008-118), and indeed implement our formal model of a subset of Links by compilation to F7, our enhanced typechecker for the F# programming language.

We finished a paper today that we present at TLDI in January.  But this is just the start, there is loads more to do in this area. First things first though - we plan to publish a full technical report to accompany the TLDI paper by the end of the year.

Secure Compilation of a Multi-Tier Web Language. With I. Baltopoulos. In ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2009), Savannah, Georgia, 24 January, 2009. ACM Press. To appear.

Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vulnerable to untrustworthy clients. We study this general problem in the context of the Links multi-tier programming language. Like other systems, Links stores unencrypted application data, including web continuations, on the client tier; hence, Links is open to attacks that expose secrets, and modify control flow and application data. We characterise these attacks as failures of the general principle that ecurity properties of multi-tier applications should follow from review of the source code (as opposed to the detailed study of the files compiled for each tier, for example). We eliminate these threats by augmenting the Links compiler to encrypt and authenticate any data stored on the client. We model this compilation strategy as a translation from a core fragment of the language to a concurrent lambda-calculus equipped with a formal representation of cryptography. To formalize source-level reasoning about Links programs, we define a type-and-effect system for our core language; our implementation can machine-check various integrity properties of the source code. By appeal to a recent system of refinement types for secure implementations, we show that our compilation strategy guarantees all the properties provable by our type-and-effect system.

Well, in a packed week last week I attended the Large Installation Systems Administration conference in San Diego, and also the kick-off of the Cluster of Excellence "Multimodal Computing and Interaction", Saarbruecken.

Some links from the journey:

• Anna Fischer of HP Labs Bristol spoke at the LISA workshop on virtualization infrastructure on secure network virtualization.  She points me to a tech report comparing various approaches at HP to network virtualization.
• Hannah Bast gave me a great demo of her CompleteSearch system for the DBLP database.  Very neat.
• Martin Kersten told me about his cool column-oriented database, MonetDB; it can perform an order of magnitude faster than conventional record-oriented RDBMs.

I'm serving on the Programme Committee for CSF next year.  The submission deadline is February 6, 2009; this would be the place to send your best work on theoretical foundations of computer security.  Go for it!

Check out a special report on Corporate IT from the Economist.  Its focus is the current shift towards cloud computing.  A good overview of the technical, operational, and economic factors behind the shift towards an internet of ubiquitous devices and gigantic data centres.

I'm back (for a week actually) from another wonderful visit to Warsaw, this time, as I've mentioned, it was for a summer school GLOBAN 2008 organised by Andrzej Tarlecki and his gang at MIM.

It was an excellent school, with keen students and plenty of interactions during and after lectures.  Some of these students at least will be esteemed colleagues for many years.

Some records:

• My slides are up on the summer school website.
• There are plenty of cool photos over here, including me in action writing lambda-terms with a tablet PC.
• No links, but the lecturers were treated to a wonderful meal at home by Andrzej and his wife Teresa: a feast, including Polish dumplings and turkey, and eventually home made liqueurs, which we didn't do such a great job of identifying.  I know Teresa loves whisky, having lived in Scotland, and next time I promise at least to bring some Dalwhinnie!
• I'm proud to say I was presented at the end of my course with gifts: The Cyberiad Stories by Stanislaw Lem, and (to me) the inscrutable (but likely highly drinkable) nalewki i inne.  But I've no idea what "inne" means.  Can anyone help?

I'm on the programme committee for the Oakland conference next year.  The submission deadline is November 10.

Here is the text of the call, go for it!

Since 1980, the IEEE Symposium on Security and Privacy has been the premier forum for computer security research, presenting the latest developments and bringing together researchers and practitioners.

We solicit previously unpublished papers offering novel research contributions in any aspect of computer security or privacy. S & P is interested in all aspects of computer security and privacy. Papers may present advances in the theory, design, implementation, analysis, or empirical evaluation of secure systems. Papers without a clear application to security or privacy will be considered out of scope and may be rejected without full review.

Topics of interest include, but are not limited to:

• Access control
• Anonymity
• Application-level security
• Attacks and defenses
• Authentication
• Distributed systems security
• Embedded system security
• Forensics
• Hardware-based security
• Information flow
• Information security
• Intrusion detection
• Malicious code
• Language-based security
• Network security
• Physical security
• Privacy-preserving systems
• Recovery
• Secure protocols
• Security architectures
• Security and privacy policies
• System security
• Usability and security
• Web security

My course, Declarative Datacentres, at the GLOBAN Summer School on Global Computing, aims both to describe various software and management problems concerned with the datacentres that enable global computing, and to advocate some approaches, declarative and typeful in style, to these problems.

For some background reading on the problems, visit the website for the R2D2 workshop we held earlier this year.  You can read the slides and watch videos of most of the presentations; the contributions of Paul Anderson and John Wilkes are good places to start.  The proceedings is available as the following technical report.

• K. Bhargavan, A. D. Gordon, T. Harris, and P. Toft (editors).  The Rise and Rise of the Declarative Datacentre.  Technical Report MSR-TR-2008-61, Microsoft Research, May 2008.

For some background reading on the declarative and typeful techniques I will teach, see the following technical reports.  The core of my lectures will be the type theory RCF in the second of these two reports.

• K. Bhargavan, A. D. Gordon, and I. Narasamdya.  Service combinators for farming virtual machines. MSR Technical Report MSR-TR-2007-165, Microsoft Research, December 2007.
• J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis.  Refinement types for secure implementations. MSR Technical Report MSR-TR-2008-118, Microsoft Research, September 2008.

The values of a refinement type {x:T | C} are the values of the type T that satisfy the formula C.  For example, the type of odd numbers can be written as {x:int | Odd(x)}.  Refinement types are a way of unifying type systems with program logics; refinement types are a Hot Topic at present and I'm very much looking forward to lecturing about them.  Moreover, throughout the course I aim to bring up rather more problems than have known solutions, so attending the course may give some leads for future research.  In any case, I'm looking forward to seeing everyone in Warsaw.  See you soon!

The F# team, led by Don Syme, and split between MSR Cambridge and the Microsoft Developer Division, has just released their September CTP (Community Technical Preview) of the language.  There is also a new Developer Centre for F# on MSDN.  Great, great stuff.

A feeling of end times around here this weekend.  Saturday weather was excellent, people sitting out in the cafes on Mill Road, wistful that it's the penultimate day of August, of the whole summer.  And today a humid sunny daytime, but now torrential rain as night falls.

And at work, people are leaving.  Our intern Aslan Askarov left last weekend, back to Gothenburg, and then home to Azerbaijan.  Aslan is a specialist in information flow, and I've learnt a lot in conversations with him.  Bob Harper has been here for August, and Friday was his last day.  Several great conversations with Bob on type theory, and well other stuff - he has a radio show, Left Out, back in Pittsburg, and I've been catching up on it from the MP3s available online.  And Friday was Ric Pucella's last day.  Ric has been here for the whole summer; we've been working on representing stateful computations with types, having a lot of fun.  Bob's now back in Pittsburg, Ric in Montreal.

Tomorrow's September; at work, I make a new start, gearing up to the GLOBAN summer school in Warsaw.  I love teaching at summer schools, and I love visiting Warsaw; I'm looking forward to preparing my course and to meeting the students.

Well, I was driving past the Rose and Crown pub yesterday and it's all shut up, with metal sheets on the doors and windows.  Looks like the squat I mentioned is all over.  Funnily enough, the Rose and Crown is situated in Occupation Road, Cambridge...

Well, squatting seems to be catching on in Cambridge.  Earlier in the summer, a much protested but so far unopened Tesco store in Mill Road was turned into the Mill Road Social Centre.  Today, it turns out that the disused pub, the Rose and Crown, not far from Mill Road, has been squatted with the intention of turning it into a social centre.  Interesting days.