Foothill Project: Rigorous Protocol Design

Peter Sewell

Communication protocols will form a key part of any ubiquitous computing system. Traditional Internet communication is dominated by the UDP and TCP transport protocols, together with various routing protocols, above IP. These rely on properties of the existing network — relatively stable connectivity, loss dominated by router congestion, and so on — that will not hold for the variety of network technologies in ubiquitous systems. New protocols will be needed.

If these are to be predictable and robust they must be well-understood, for which new design techniques are also needed. Traditional internet protocol design is largely based on natural language specifications and interoperability testing between implementations. This often leads to unnecessary complexity and subtle flaws and implementation differences.

We therefore have an opportunity and test-bed for an integrated systems and semantics approach to protocol design. The goal of this foothill project is to establish a suite of protocols for particular GUC scenarios, developing and using rigorous design techniques for the purpose. It may build on the Netsem project, which has demonstrated a viable approach to the formal specification of existing real-world protocols, expressing their behaviour with operational semantics in the automated proof assistant HOL and developing symbolic model-checking techniques to validate the specification against captured traces.

The main challenges are:

• The large-scale systems question of broadly what protocols are required, their APIs and design principles.
• Establishing idioms for expressing detailed design that:
  • are an effective means of communication in the design and implementation teams, among those with theoretical and practical backgrounds;
  • support direct and automated conformance testing of production implementations against the protocol designs; and
  • can be refined (i.e. resolving any looseness in the specifications) to give prototype implementations that can be used for experimentation and simulation.
• Establishing higher-level (more abstract) models that are suitable for approximate (probabilistic or stochastic) reasoning and simulation, ideally with mathematically rigorous relationships to the detailed designs.
• Verifying (with automated proof and/or model-checking) properties of both detailed and high-level models.
• Deploying the protocols and gaining experience in their use.