| EPSRC Reference: |
EP/E034519/1 |
| Title: |
VIP: Verification with Integer Polyhedra |
| Principal Investigator: |
Howe, Dr JM |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing |
| Organisation: |
City, University of London |
| Scheme: |
Standard Research |
| Starts: |
04 June 2007 |
Ends: |
03 December 2010 |
Value (£): |
136,174
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Security is a continuing source of concern with the use of computers and software. Subtle programming errors that can be exploited by malicious hackers are continually being spotted even in the most widely used computer programs.One common error is code that allows buffers to overrun, that is, the program permits data to be written to a part of a memory which should really be forbidden. If a hacker can exploit such a memory access, then they might be able to launch a security attack. Such an attack is made by overwriting part of the program with a small program. One example of such a program is a worm that when executed not only erases precious work stored on the computer but often attacks other computers running the same buggy program. Since most computers today are connected via the Internet, it only takes a split second for a worm to attack other computers in the vicinity which in turn will attack many more. Worms like the MS Blaster Worm have incurred losses of hundreds of million of dollars to society by rendering computers unusable. Moreover, even those buffer overruns that cannot be exploited for malicious intent, still need to be tracked down because they are often symptomatic of errors or oversights introduced or made by the programmer.Therefore, detecting these errors is of great importance. Theoretically, it is known how to do this, by tracking the flow of information in a program and giving the programmer warning messages when a potential error is detected. However, the automation of this process via a program analyser based on polyhedra is problematic. The analyser needs to run quickly enough so that the programmer can use it whilst continuing to be productive. Speed can be gained at the expense of accuracy, that is, issuing more false warning messages, but then the programmer can be swamped with messages that have to be followed up, but do not indicate a real source of the problem. Time is then lost in another way.The aim of this project is to produce analysers for buffer overrun vulnerabilities that are both faster and more accurate than those developed to date. In particular, it aims to provide the underpinning theory that will allow new analysers to be developed. The project is based on the observation that many, but not all, of the variables tracked by such an analyser are integral. Previous polyhedral analysers have worked with real or rational numbers at all stages, missing chances to simultaneously increase the accuracy of analysis and to reduce the amount of computation involved in the analysis overall.The exploitation of this observation is not all straightforward.Although there are mathematical results on the integer points contained within polyhedra that have not so far been applied in verification and bug detection, and the development of appropriate algorithms and their realisation in software presents numerous challenges. This mix of previously unexploited theory and concrete application leads to a project that is theoretically interesting, practically useful and timely in that it addresses a pressing problem in computer security.
|
|
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.city.ac.uk |