HP Internet Philanthropic Initiative - Next Generation Internet
Safetynet: Implementing Network-Safe Programming Languages for Active Networks

Ian Wakeman - Alan Jeffrey

Contents

Participants

 

The Safetynet project
Ian Wakeman Principal Investigator ianw@cogs.susx.ac.uk +44-1273-678364
Alan Jeffrey Principal Investigator alanje@cogs.susx.ac.uk +44-1273-678526
Rory Graves PhD student roryg@cogs.susx.ac.uk
Tim Owen PhD student timothyo@cogs.susx.ac.uk
Ben du Boulay Dean of School bend@cogs.susx.ac.uk +44-1273-678324
Table 1: Participants

 

Summary

 

Active networks extend the functionality of existing networks by opening up the computation capabilities of the switches to the network users. This allows faster roll-out of new services and new applications which have lower latency and are more scalable. However, in opening up the shared resources of the switches to running programs, existing services might suffer a performance degradation, and more dangerously, a loss of service due to buggy or malicious programs.

In our research we aim to circumvent these problems by defining appropriate policies to protect the integrity of the network, such as defining limits on TTL fields in packets, then designing these policies into the type system of an Active Network programming language. Any program which type-checks is guaranteed not to contravene our safety policies. In addition, by using a strongly typed language, we can remove many of the run-time checks required by other language models, and so improve performance.

Recent work in the foundations of programming languages has provided mathematical models of language features such as distribution, code migration, resource bounds and security. We will use these techniques to provide a formal model of Active Network programming, and to show the correctness of the type system and the safety policies.

In parallel with the theoretical work upon the semantics, we shall be developing a compiler and run-time environment for the language. These will be used to build demonstration Active Network programs, which will be tested both within an extended simulation environment built upon the VINT ns simulator, and in limited scale experiments upon real networks. It is in this strand of work that we expect any donation from the HP Pan-European Internet Initiative to have impact.

Major Milestones for the first year

 

 

Milestone Date due Description
Safety Policies June 1998 An analysis of the safety and security policies that the safetynet language should implement.
Core language specification August 1998 The syntax and draft semantics of the core language
Compiler Feb 1999 The prototype compiler and runtime system for the core language
Autoconfiguration Demonstration March 1999 A paper describing the algorithms and results from implementing auto-configuration of transcoders within safetynet
Table 2: Major Milestones

We intend to submit papers to Sigcomm 99, to Transactions on Networking, to POPL 99 and to Journal of Functional Programming within the coming year.

Background

 

Active networks

Active networks allow switches within the network to execute code on behalf of some granularity of packet. However, these switches are resources shared by all who use the network, and as guardians of the common good, it is the responsibility of switch managers to be certain that the benefit of the additional services outweighs the possible damage that ANs may visit upon a switch. From private conversations, most switch managers do not view ANs with enthusiasm. They need to be sure that:

As an illustration, if an active switch were to allow arbitrary C programs to be executed, then there would be scope for many attacks, for example: Existing strongly typed language such as Java would help against the first attack, by banning pointer arithmetic, but requires a number of run-time checks to achieve this.

If we can ensure the network integrity, then active networks hold out the promise of developing many novel scalable low latency applications. Many distributed applications can improve latency by shifting processing closer to the bottleneck, for instance in transcoding a delivered multicast audio stream to fit over congested links [20]. We present other applications as demonstrations in our proposal..

Semantics of programming languages

The problems faced by ANs are not new: they are shared by many other distributed languages with mobile processes. This is a topic which has been investigated in the semantics of programming languages community, which has developed an array of mathematical techniques for proving languages to be safe. We believe that these techniques are directly relevant to ANs, and in particular that:

Relevant work includes: There is one other project combining work from the semantics community and active networks: Gunter et al's [13] PLAN. Their aims are different: they are using semantic techniques to model individual nodes, rather than modelling the whole network, and their type system is based on SMLs, rather than being the focus of attention. An Active Bridge [2]has been built, using CML to build the modules. We will be building and extending this work in our research.

Why Active Networking at Sussex.

 

Safetynet

has been evolving over the last year, and we are making considerable progress in defining the semantics of the core language, as can be seen in our work in progress.. The current people on the project are the principal investigators Dr Alan Jeffrey and Dr Ian Wakeman, and two PhD students, Rory Graves who is developing applications of AN to group communications for his PhD thesis and Tim Owen who will be developing the prototype compiler and run-time system. We have submitted a proposal to the EPSRC to support further development of this work by funding two research fellows and two further PhD students. This proposal was supported by Rob Cole from HP Research Labs in Bristol and Microsoft Research Laboratories in Cambridge UK.

Dr Alan Jeffrey

has been a lecturer at Sussex since 1994. He researches the mathematical foundations of concurrent programming languages. In particular, he is interested in the interaction between concurrent and functional languages. He has presented an operational and denotational semantics for CMML, a concurrent functional language based on Reppy's Concurrent ML and Moggi's Monadic Meta-Language. Together with William Ferreira and Matthew Hennessy, he developed an operational semantics for Concurrent ML, and the accompanying theory of weak bisimulation. He has developed a theory of the concurrent graph reduction implementation technique for non-strict functional programming languages, and has shown that this has the same fully abstract model as the sequential tree reduction model. Dr Jeffrey received his D.Phil from Oxford University in 1992, for his work on the semantics of highly distributed timed systems.

Dr Ian Wakeman

has been a lecturer at Sussex since 1995 and was previously at UCL as a research fellow. His research has centred around networked multimedia, from developing multicast congestion control mechanisms for internet video through to conference control architectures. He currently runs projects on application level adaptation for low bandwidth networks and on developing distributed algorithms within Active Networks. He has published over twenty papers in the area.

The Computer Science and Artificial Intelligence subject group

at the University of Sussex is an interdisciplinary group looking at many aspects of CS and AI, including formal models of programming languages, designing network architecture, implementing compilers, adaptive systems, vision, neural computing and human-centered computing. The group is part of the School of Cognitive and Computing Sciencese, which also includes Psychology, Philosophy and Linguistics. There is a thriving postgraduate student body including a new M.Res in CSAI specializing in Distributed Programming Languages. CSAI is an active research group, with a 5 rating at the last RAE.

Dissemination and Exploitation

 

We will produce a Web page to disseminate our work and to act as a focal point within the UK. We already run a UK mailing list for active networking. The prototype implementations will be made available as public domain software for the Active Network community, and will be integrated within the ABone.

The work will be published in academic conferences and journals, both to a semantics audience and to a networks audience.

We will be providing collections of papers and running seminars on our work to our industrial sponsors and any other interested parties.

Activity Description

 

Aims and objectives

The aims of this project are:

The measureable objectives are: For each objective, its success will be measured by publication in the semantics and networking literature, and by acceptance as a programming platform within the AN community.

Methodology

The methodology we will use comes from an interdisciplinary approach, using techniques from both the semantics community and from the networks community.

From the semantics community, we will use well-established techniques for modelling strongly typed languages:

We will build prototype compilers based on the formal specification of the language and the type system. Initially, the resulting programs will communicate using type-annotated abstract syntax trees to represent migrating code, which will be interpreted at the active nodes. We will later investigate how this process can be made more efficient, for example by the use of typed bytecode to represent programs. The compilers will build on existing Java network architecture, enhanced by classes defining AN functionality such as remote process spawning and security.

To test the viability of our approach for end systems, we shall design and implement several prototype AN applications, such as a multicast congestion transcoder [20], a distributed reliable ordering multicast protocol and a distributed conference key management protocol. These will then be tested in simulation, using a network simulator such as VINT ns, and a simulated virtual machine we have already developed at Sussex [10]. In this way, we expect to be able to make comparisons not only about the network performance of the techniques, but about the relative processing requirements and the likely performance impact upon switches. We will then build our virtual machine into an ABone router, so that the our AN applications can be tested in the wild on the ABone.

UCL have offered to host an ABone router off the Cairnet, to provide direct attachment to the ABone.

Timeliness

Active Networks are a current area of research and bring areas of programming language design into networking.

Much of the research on ANs has been carried out in the US, for example the Switchware project at the University of Pennsylvania [11], MIT [27], Columbia [28], GSU [5] and BBN [14]. However, only the Switchware project are using the techniques of Higher Order programming [13] to ensure safe programming, and even then the language support is not as complete as our approach. As yet there has been little work in the UK, barring the thought exercises we have undertaken [18], and work towards an open switching architecture at Cambridge[24].

The UK has a large body of expertise in language design, and in the use of mathematical models to help in the design and validation of languages. In the particular area of concurrent systems, there is active work at Cambridge, Edinburgh, Oxford, Sussex and Warwick.

The field of semantics has recently moved into areas of direct relevance to ANs, for example the tex2html_wrap_inline578-calculus [21] models capability-based communication; Ambients [9], Distributed tex2html_wrap_inline578 [25] and Dtex2html_wrap_inline578 all model distributed languages with process migration; CHOCS [26], tex2html_wrap_inline614CML [6] all model higher-order languages; Stex2html_wrap_inline578 [8] models security and encryption.

This is a unique opportunity to take the theoretical work developed in the UK and to apply it to a real problem in active network programming.

Work programme: overview

Network safety policy definition

In the first phase of the project, we shall determine the safety policies we wish to embed within the Safetynet language. We will make use of the expertise of network professionals in determining safety policies, and language theorists to translate these policies into the restrictions on program execution that will form the basis of the Safetynet type system, extending the work in [15].

Language design

We intend to design a programming language for processes in an active network. The core language will be based on existing work at Sussex on higher-order concurrent languages [6, 16, 17] and languages with explicit notions of location [12]. The user language will consist of the core language together with enough syntax sugar to make the core language easily accessible to programmers.

The core language will be strongly typed, using a formally-defined type system, and will be given an operational semantics based on that of Milner's pi-calculus. There will then be two properties to prove:

As a corollary of these two properties, all well-typed programs are guaranteed to conform to the safety and security policies during their execution.

The language design will evolve during the project, but we expect there to be three phases:

  1. The design of a strongly typed language extending the pi-calculus with explicit locations, higher-order functions and process migration supporting the safetynet policies.
  2. The development of extensions to the type system to minimize the amount of run-time checking required whilst still maintaining safety in the presence of non-type-safe attackers. We shall also minimize the amount of shared type information required, since such shared information has a communications overhead.
  3. Using the type system to model real-world safety and security issues such as encryption and code signing, based on the security work on the Stex2html_wrap_inline578-calculus.

Each phase will include a formal definition of the language and its types, together with the type system and proofs of type safety and subject reduction.

If our resources are increased, we shall be developing a suitable typed bytecode for use in the implementation virtual machine, together with a proof of correctness for the translation from the core language to the VM.

Language implementation

The implementation of the prototype compiler and run-time system will initially be built upon existing Java infrastructure such as the Java VM, garbage collection, communication and serialisation. This will allow easy integration with existing AN infrastructure such as the ANTS toolkit from MIT.

For each phase of the language, we will implement a compiler from the Safetynet language down to Java. Most of this activity will concentrate on the innovative use of a formally defined type system.

In the first two phases, the prototype system will pass an abstract syntax tree representation of programs, which will be compiled at each node. If available resources allow, in the final phase we shall look at ways to remove this inefficiency by producing the designed typed bytecode to pass between processes to run on a Safetynet specific Virtual Machine and runtime environment.

The runtime system for the language will be defined during the first phase, and implemented as a number of Java classes, building upon the ANTS toolkit from MIT. During each phase of the project, this runtime system will be extended to support the new functionality.

Prototype Applications

In each phase of the project we will be writing AN applications to demonstrate the applicability of our approach, such as a multicast congestion transcoder, a ordered reliable multicast applications and a distributed conference key management system. These will first be demonstrated in simulation using our adapted VINT ns simulator, and then in the wild on the ABone.

UCL have offered to provide an ABone router directly attached to Cairnet to provide connectivity. This will require the installation of ABone software on the FreeBSD machine hosted at UCL.

Workpackage 1: Network Architecture

Activity 1: Policy Definition

In this activity, we will be defining the safety policies required to protect the network and the switch resources. Network and language experts will determine what policies are feasible and practical, extending the work in [15]. The deliverable will be a set of safety policies.

Activity 2: Programming Model Definition

As well as the safety policies, we shall develop a programming paradigm for Active Networks, based on higher-order concurrent and distributed langauges such as tex2html_wrap_inline584, Ambients and Concurrent ML. This will be used to produce an initial specification of the runtime system.

Workpackage 2: Language Design

Activity 1: Initial Language Design

Develop a typed higher-order distributed language. Deliverables are a specification of the syntax, type system and semantics of the language.

Activity 2: Distributed Type Checking

Develop extensions to the type system to support distributed type checking. Deliverables are a further draft of the specification of the syntax, type system and semantics of the language.

Activity 3: Security within the Type System

Include security features such as encryption and code signing. Deliverables are a further draft of the specification of the syntax, type system and semantics of the language.

Workpackage 3: Compiler Implementation

Activity 1: Initial Language Implementation

A prototype compiler will be built, in two stages. A parser and abstract syntax tree generator will be developed, and a separate code generator to turn the AST into Java.

Activity 2: Distributed Type Checking

The compiler will be extended with the appropriate run-time type checking features.

Activity 3: Security within the Type System

The compiler will be extended with the appropriate security features, based on Java's security libraries.

Workpackage 4: Runtime System

Activity 1: Initial Runtime System

>From the requirements document, the necessary Java infrastructure will be built, including features such as dynamic process spawning and the generation of unique server Ids.

Activity 2: Distributed Type Checking

The type checking algorithm will be implemented in Java.

Activity 3: Security within the Type System

The infrastructure will be extended with key generation and other security manipulation features.

Workpackage 5: Demonstration Applications

Activity 1: Multicast Congestion Transcoders in Java

For multicast realtime streams, if a link is congested, then an alternative to throwing the packets away is to transcode the flow into some lower bandwidth stream, such as audio from PCM to LPC. The intent is to demonstrate how the selection of strategic points in the multicast tree and the installation of transcoders can be achieved automatically through the use of active nets rather than a complicated auto-configuration protocol.

Activity 2: Multicast Congestion Transcoders in Safetynet

The implementation in Java from Activity 5.1 will be rewritten in the prototype safetynet language.

Activity 3: Reliable Ordering for Multicast

The necessity for satisfying the ordering constraints upon the delivery of reliable multicast such as total ordering requires the use of coordinating servers and holdback queues. This activity will demonstrate the use of Safetynet to produce low latency and scalable ordering of reliable multicast delivery.

Activity 4: Key Distribution Mechanisms for Secure Conferencing

The generation and distribution of multicast keys for large dynamically changing multicast groups, such as in a pay-per-play large scale game requires intensive processing per user. In this scenario, we will demonstrate how the use of Safetynet security features and the dynamic placement of processing produces a solution that is scalable in the number of receivers.

Project Management

Currently the Safetynet team consists of Alan Jeffrey, Ian Wakeman, Rory Grave and Tim Owen arriving in June. We expect the team to be extended by two additional research fellows and two additional students if the proposal to the EPSRC is accepted.

All members of the team will be participating in Work Package 1. We expect to be able to ask colleagues such as Jon Crowcroft at UCL for additional input.

Alan Jeffrey (AJ) will be undertaking the work in WP1. Ian Wakeman (IW) and Tim Owen (TO) will be undertaking the work in WP3 and WP4, whilst Rory Graves (RG) will be undertaking the work in WP5.

Management will be coordinated by weekly project meeting.

Document Coordination

Communication between the team of the syntax and semantics of the language is a core part of the project. This will be achieved through the formal use of live specifications to be handed over as deliverables from the language design work package to the compiler developer. These documents will be kept under version control and made available on the Web.

Risks

The defined programme of work is ambitious for the current team strength. However since the programme of work is incremental, we are prepared to drop some of the later activities.

The critical path in each phase of the project begins with the language design package passing a language specification to the compiler implementation.

  figure160
Figure 1: Gant Chart

 
Activity Start End AJ IW TO RG Deliverables Due
1.1 0 3 1 2 0 1 Policy specification 3
1.2 0 3 0 1 0 2 Runtime specification 3
2.1 1 9 5 0 0 0 Specification of language syntax 5
Update Runtime system requirements 6
Documentation of the semantics of Safetynet 9
2.2 10 16 5 0 0 0 Updated Specification of language syntax 13
Update Runtime system requirements 13
Distributed Type Checking Theory 16
2.3 16 24 4 0 0 0 Updated Specification of language syntax 19
Update Runtime system requirements 19
Semantics of security extensions 24
3.1 4 12 0 0 4 0 Prototype Compiler for A2.1 11
3.2 13 17 0 0 3 0 Prototype compiler extensions for A2.2 17
3.3 19 24 0 0 3 0 Prototype compiler extended to A2.3 24
4.1 3 11 0 4 5 0 Runtime system for A3.1 11
4.2 11 17 0 2 2 0 Runtime extensions for A3.2 17
4.3 17 24 0 3 4 0 Runtime extensions for A3.3 24
5.1 0 8 0 0 0 6 Software simulation 8
5.2 8 12 0 0 0 4 Safetynet software 12
5.3 12 18 0 0 0 6 Ordering software 18
5.4 18 24 0 0 0 6 Key distribution software 24
Table 3: Activity Summary (Month 0 is April 1998)

Internet Futures

 

We anticipate benefits both to the providers and users of telecommunication services. The increased speed with which new services can be deployed enables providers to quickly adapt to a rapidly changing market, and to keep pace with the development of hardware. The resulting increased sophistication in network management will aid in protecting the network. For the users, we expect active networks to enable the development of highly scalable wide area applications, such as multi-user games and virtual reality environments.

In the academic networking community, we will provide a formal basis for the network architecture that multimedia applications can run on. It is also of interest to the semantics community, since it extends existing work on typed distributed languages in ways which are both theoretically interesting and practically relevant.

Requested Support

  HP could most obviously help us in providing a development environment to build the prototype compiler, a memory-rich environment in which we can run simulations, a separate quarantined network in which we can run our small scale experiments, and portable machines so that we can demonstrate the software and work to any interested parties. We therefore request the following equipment:

 

Description Number
Vectra VL with 256 MB 4
Omnibook 7100 Laptops 2
Laserjet Network Printer 1
100 Base/T Switch 1
Table 4: Requested equipment

References

1
S. Abramsky. Computational interpretations of linear logic. Theoret. Comput. Sci., 111:3-57, 1993.

2
Scott Alexander, Scott Nettles, Marianne Shaw, and Jonathan Smith. Active bridging. In Proceedings of SIGCOMM 97, Cannes, France, August 1997. ACM.

3
N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proc. Computer Science Logic '94, number 933 in LNCS. Springer-Verlag, 1995.

4
N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In Proc. Int. Conf. Typed Lambda Calculi and Applications, number 664 in LNCS. Springer-Verlag, 1993.

5
Samrat Bhattacharjee, Ken Calvert, and Ellen W. Zegura. An architecture for active networking. In High Performance Networking (HPN'97), White Plains, NY,, April 1997.

6
W. Ferreira, M. Hennessy, and A.S.A. Jeffrey. A theory of weak bisimulation for core CML. In Proc. ACM SIGPLAN Int. Conf. Functional Programming, pages 201-212. ACM Press, 1996. To appear in J. Functional Programming.

7
J.-Y. Girard. Linear logic. Theoret. Comput. Sci., 50:1-102, 1987.

8
A. Gordon and M. Abadi. A calculus for cryptographic protocols: The spi calculus. Research Report 149, Digital Equipment Corporation Systems Research Center, 1998. To appear in Information and Computation.

9
A. Gordon and L. Cardelli. Mobile ambients. In Proc. FoSSaCS '98, LNCS. Springer-Verlag, 1998.

10
Rory Graves and Ian Wakeman. Experiences of implementing a jvm for simulation. Technical report, School of Cognitive and Computing Sciences, Uni of Sussex, 1998.

11
Carl A. Gunter, Scott M. Nettles, and Jonathan M. Smith. The switchware active network architecture. To be published in IEEE Network special issue on Active Nets.

12
M. Hennessy and J. Riely. Resource access control in systems of mobile agents. Computer Science Technical Report 98:02, Univ. Sussex, 1998.

13
Michael Hicks, Pankaj Kakkar, Jonathan T. Moore, Carl A. Gunter, and Scott Nettles. Plan: A programming language for active networks. submitted to PLDI'98.

14
Alden W. Jackson and Craig Partridge. Smart packets. Presented at 2nd Active Nets Workshop, March 1997.

15
Alan Jeffrey and Ian Wakeman. A survey of semantic techniques for active networks. submitted to IEEE Network.

16
A.S.A. Jeffrey. A fully abstract semantics for a concurrent functional language with monadic types. In Proc. LICS 95, pages 255-264. IEEE Computer Society Press, 1995.

17
A.S.A. Jeffrey. Semantics for core concurrent ML using computation types. In Andrew Gordon and Andrew Pitts, editors, Proc. Higher Order Operational Techniques in Semantics. Cambridge University Press, 1997.

18
A.S.A. Jeffrey and I. Wakeman. A survey of semantic techniques for active networks. Submitted to IEEE Network, 1997.

19
N. Kobayashi, B.C. Pierce, and D.N. Turner. Linearity and the pi-calculus. In Proc. POPL '96, 1996.

20
Isidor Kouvelas, Vicky Hardman, and Jon Crowcroft. Network adaptive continuous-media applications through self organised transcoding. Submitted for publication to NOSSDAV 98, 1998.

21
R. Milner, J. Parrow, and D. Walker. A calculus of mobile proceses. Inform. and Comput., 100(1):1-77, 1992.

22
B.C. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Proc. LICS '93, pages 376-385. IEEE Computer Society Press, 1993.

23
B.C. Pierce and D.N. Turner. Pict: A programming language based on the pi-calculus. Technical Report CSCI 476, Computer Science Department, Indiana University, 1997. To appear in Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, eds, MIT Press.

24
Sean Rooney. Connection closures adding application-defined behaviour to network connections. Computer Communications Review,, April 1997.

25
Peter Sewell. Global/local subtyping for a distributed tex2html_wrap_inline578-calculus. Technical Report 435, Computer Laboratory, University of Cambridge, 1997.

26
B. Thomsen. A theory of higher order communicating systems. Inform. and Comput., 116(1):38-57, 1995.

27
David J. Wetherall, John Guttag, and David L. Tennenhouse. Ants: a toolkit for building and dynamically deploying network protocols. In Proceedings of first IEEE Conference on Open Architectures for Signalling, San Francisco, Ca, April 1998.

28
Y. Yemini and S. da Silva. Towards programmable networks. In IFIP/IEEE International Workshop on Distributed Systems: Operations and Management,, L'Aquila, Italy, October 1996.

About this document ...

HP Internet Philanthropic Initiative - Next Generation Internet
Safetynet: Implementing Network-Safe Programming Languages for Active Networks

This document was generated using the LaTeX2HTML translator Version 96.1-h (September 30, 1996) Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -t HP Case for Support: Safetynet - Implementing Network-Safe Programming Languages for Active Networks -split 0 -no_navigation -dir . cfs-hp.

The translation was initiated by Ian Wakeman on Fri Apr 17 16:21:00 BST 1998

Ian Wakeman
Fri Apr 17 16:21:00 BST 1998