This page is a list of project ideas suitable for undergraduate projects, Senior theses, and graduate theses. I believe PhD students should be largely responsible for defining their own research area and project. This list is by no means exhaustive - if you have an idea for a research project that isn't listed here please contact me.
Computing is rapidly moving away from traditional computers. Of the 8 billion computing units will be deployed worldwide this year, only 150 million are stand-alone computers [Tennenhouse2000]. Many programs in the future will run on collections of mobile processors interacting with the physical world and communicating over dynamic, ad hoc networks. We can view such a collection of devices as a swarm. As with natural swarms, such as a school of fish or an ant colony, the behavior of the swarm emerges from the simple behaviors of its individual members. The swarm is resilient to a small fraction of misbehaving members and to changes in the environment.
A fundamental challenge for computer scientists over the next decade is to develop methods for creating, understanding and validating properties of programs executing on swarms of communicating computational units. The key difference between swarm programming and traditional programming is that the behavior of a swarm program emerges from the total behavior of its individual computing units. Unlike traditional distributed programming, swarm programs must deal with uncertain environments and mobile nodes. The scientific challenges of swarm computing are to understand how to create programs for individual units based on the desired behavior, and conversely, how to predict high-level behavior based on the programs running on the individual computing units.
Recently, the building blocks for swarm computing have come into place. Advances in microelectomechanical systems and wireless networking have led to tiny, inexpensive devices with significant computing and communicating capabilities. Protocols for naming and communicating among disparate devices are emerging. Although there are many issues to resolve, many of the technological challenges have already been solved and there is an active and growing research community working on the devices and networking protocols that will provide the infrastructure for swarm computing.
We are a long way, however, from solving the deeper problem of how to program swarms of computing devices. Our work focuses on creating and reasoning about swarm programs. We are developing an environment for simulating swarm programs, and exploring the primitives and combination mechanisms suitable to swarm computing. We are developing techniques for describing both the desired behavior of a swarm program and the constraints on acceptable behavior in extreme environments. Since proving properties in general is infeasible, we will use lightweight mechanical analyses to approximate checking. This sacrifices soundness and completeness, but enables certain classes of properties to be checked efficiently and with limited programmer effort.
Simulating Swarm Programs
Extend a message-passing simulator (developed by Robert Shutt) to include a notion of proximity. In a swarm environment, messages are not passed to specific nodes, but transmitted to nearby nodes. The likelihood of a node receiving a message depends on its distance from the sender, the amount of power used in the transmission, and properties of the physical environment.Modeling Devices and Environments
A meaningful simulation of a swarm program depends on modeling both the devices on which it executes and the physical environment they inhabit. Develop mechanisms for modeling devices and environments, and a library of reasonable models.Visualizing Swarm Executions
In order to gain a good intuition of the behavior of a swarm program, it would be useful to be able to represent it graphically. Develop a tool for taking output from a swarm program execution in the simulator and producing a graphical animation depeciting the execution.
Detecting buffer overflows
A surprisingly high fraction of security vulnerabilities result from buffer overflows (see CERT). LCLint-style checking offers the possibility to statically detect buffer overflows in code with suitable annotations. This project would involve designing annotations and writing associated checking to detect buffer overflows, and using it (to hopefully detect some bugs) in security sensitive programs.Support for user-defined annotations
Design a language programmers can use to define their own annotations and corresponding checking. The language should be powerful enough to support most (if not all) of the pre-defined LCLint annotations.Building a general framework for static checking
LCLint is tied closely to C, and considerable effort would be needed to produce a similar tool for checking programs in some other source language. Most of the work done by LCLint, however, is relatively language-independent. Can static checking be done on an intermediate language in a way supports multiple source languages, but still enables precise checking and good error messages?
Low-level code safety for Naccio/Win32
The prototype implementation of Naccio/Win32 is vulnerable to attacks where malicious code attempts to access arbitrary locations, modify checking state, or use kernel traps to circumvent safety checking. Some ideas for providing the necessary guarantees are described in [Twyman99], but there are many open questions and no implementation has been built.Win32 Platform Interface
Write a platform interface that describes the Win32 API in terms of abstract resource manipulations. This is essential for using Naccio to enforce safety policies, but would be useful for other applications as well. Figure out how to automate some of the process of producing a platform interface based on an analysis of source or object code.Validate a platform interface
Use formal methods to show that a platform interface and platform implementation are consistent with respect to some execution model. This would lead to useful techniques for proving certain correctness properties that are relevant to security.Naccio/Win32 Deployment as Virus Protection
Use Naccio/Win32 to develop a tool that protects users from email viruses (such as Melissa and ILoveYou). Invent a policy precise enough to allow useful macros, but safe enough to prevent harm from malicious attacks.Deploy Naccio/JavaVM in a browser
Deploy Naccio/JavaVM in a realistic environment. There are several subprojects ranging from interface design to system security:Build a new Naccio implementation
- Designing an appropriate user-interface for selecting and creating safety policies.
- Design mechanisms that support securely re-using transformed library code.
- Figure out what to do after a violation has been detected.
- Develop a way to handle multiple applets running in the same VM with either different or identical safety policies.
Build an implementation of Naccio that explores research issues not addressed by the Naccio/JavaVM and Naccio/Win32 prototypes. Some platforms that would be interesting include Linux, Solaris, and Word macros.