EPSRC Reference: |
EP/C015517/1 |
Title: |
Back to Bits |
Principal Investigator: |
King, Professor A |
Other Investigators: |
|
Researcher Co-Investigators: |
|
Project Partners: |
|
Department: |
Sch of Computing |
Organisation: |
University of Kent |
Scheme: |
Standard Research (Pre-FEC) |
Starts: |
01 October 2005 |
Ends: |
30 September 2007 |
Value (£): |
105,157
|
EPSRC Research Topic Classifications: |
Fundamentals of Computing |
|
|
EPSRC Industrial Sector Classifications: |
|
Related Grants: |
|
Panel History: |
|
Summary on Grant Application Form |
Programming a computer is a difficult task due to ways different user inputs (given through the keyboard, mouse or files) can affect the execution of a program. Many programs misbehave on certain user inputs; we say that such a program contains a bug. Some bugs in a program have the effect that an incorrect piece of computer memory is accessed. An incorrect piece of memory in this context is one that does not belong to the part of the program that is currently executing.These types of bugs are known as security vulnerabilities because they can enable a malicious attacker to delete data on another person's computer without having direct access to that computer. Such an attacker exploits the fact that the program will access an incorrect piece of memory by overwriting part of the program with a small program called a worm . When this worm is executed it notonly 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 copy itself to 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.One topic that is currently attracting much interest in the research community is that of automatically showing that a program cannot contain security vulnerabilities. The idea in this research is to simulate the program. In contrast to running the program on a computer where each program variable contains a specific value at any given time, the simulation keeps track of a set of possible values for each program variable. Furthermore, whenever the program expects user input, the simulation assumes that the user inputs any possible data. If the simulation completes without the program overwriting a piece of memory that it may not overwrite, then the program contains no security vulnerability. However, if the simulation cannot guarantee this, the developer of the program faces the challenge of finding the point in the program that needs fixing. Finding the source of the problem is difficult because the developer has to understand the operations on sets of values as they are executed in the simulation. The research suggested in this proposal aims at creating new techniques to generate so-called test-data, that is, user inputs that will exhibit the bug in the program. Given this single input, it is much easier for the developer to step through the program and to locate the point at which the program goes wrong. Any data in the computer is stored as a sequence of bits where a bit is the smallest unit of information in that it can only be zero or one. For a program simulation to be useful, it must terminate and this can only be achieved by applying approximation during the simulation. Approximation leads to the problem that some correct programs cannot be shown to be bug free by simulation. By modeling data at the bit-level it is possible to find more bugs. In addition, to our knowledge, only bit-level modeling can infer inputs that exhibit a bug and thereby generate test-data that aids the developer to understand the bug.
|
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.kent.ac.uk |