| EPSRC Reference: |
EP/C523997/1 |
| Title: |
A verified packet-forwarder on leading-edge hardware |
| Principal Investigator: |
Bornat, Professor R |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Science and Technology |
| Organisation: |
Middlesex University |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
27 May 2005 |
Ends: |
26 November 2008 |
Value (£): |
190,916
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Recent logical developments have opened up the possibility of specifying and verifying the resource-safety of low-level programs which use pointers. Space leaks, race conditions, thread encapsulation, safe malloc/free, proper use of NULL - all these currently fruitful sources of bugs appear to be within the range of verification. Intel's IXP is a network processor chip designed for speed. We intend to show that it is possible to use it safely whilst exploiting its speed to the full, by constructing and demonstrating a specified and verified packet processor. We shall restrict ourselves at first to the business of packet forwarding, with forays into as much of IP address interpretation as we can manage and which seem appropriate to a convincing demonstration. We intend to steer clear of the dark arts of protocols, though we expect to be able to deal with the simple case of forwarding table updates.A verified program is bug-free insofar as its specification rules out bugs. We shall concentrate on problems of resource safety. We do not expect, at this stage, to be able to help with other problems such as liveness, security or protocol specification. A verified program need not check proven facts. A resource-safe program might, therefore, be faster than one written without logical support which has to check the validity of its own or its partners' activity at runtime.We have set ourselves a significant challenge at both the practical and the theoretical level. Separation logic, our instrument of choice, appears to provide the concepts we need, but it will need to be extended in order to cope with the practical challenges of pipelined threads and a distributed memory architecture. We shall cooperate with theoreticians throughout the project to make sure that our logical innovations are valid.Our proofs will be manual at first, as we explore the range of specification s that we must construct. Early on in the project we shall begin to mechanise our proofs, to make them more reliable and to ensure that we don't overlook any of the devils that will hide in the detail.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.mdx.ac.uk |