Research Projects
Algorithms for Satisfiability Modulo Theory Problems
Faculty: Isil and Tom DilligProject homepage: Isil's Homepage
A satisfiability modulo theory (SMT) problem is a generalization of the boolean satisfiability problem where propositional variables are replaced by predicates from a variety of richer underlying theories, such as linear arithmetic over reals and integers, bitvector logic, and theory of equality. New algorithms for solving SMT problems have enabled great progress in many subfields of computer science, including software and hardware verification, test case generation, static and dynamic program analysis, and programming languages.
In the context of this project, we explore new algorithms for various SMT-related problems, particularly those with applications to program verification. More specifically, the problems we are interested in include the following:
- simplification techniques for obtaining smaller SMT formulas;
- new SMT solving algorithms that can be parallelized, for instance, on the GPU;
- algorithms for computing minimum satisfying assignments of SMT formulas; and
- algorithms for abductive inference in SMTs.
Armstrong: Making Cell Phones More Secure
Faculty: Qun LiProject homepage: Wireless Networking Group
Smartphones are one of the hottest growth sectors in the economy right now. We rely more and more on phones for almost everything, including e-mail, document editing, online banking, gaming, and other numerous applications. While the phones are becoming very powerful, the risk of viruses, malware, and identity theft are increasing greatly. While a lot of work has been done on PC security, the investigation of cell phone security is in its infancy. In this project, we aim to develop operating system support to make cell phones more secure and efficient.
Autocorrelated Flows in Systems: Analytic Models
Faculty: Evgenia SmirniProject homepage: Evgenia Smirni's Homepage
Experiments have shown that burstiness in arrival intensities or service demands in a single server system may result in user response times that are slower by several orders
of magnitude. This is the first project that resulted in analytic queueing models that explicitly
capture and formalize burstiness using autocorrelation in flows. This project provided two significant contributions: the KPCToolBox package of matlab scripts that can automatically fit a trace into a Markovian Arrival Process (MAP), and the broader MAP queuing networks (MAPQNs) that are a new class of closed queueing network models for the analysis of computer and communication systems where service times are affected by autocorrelation. This research is supported by the National Science Foundation.
AutoECG: ECG Automatic Analysis System
Faculty: Qun LiProject homepage: Wireless Networking Group
The automatic analysis of ECG signals is very important for diagnosing cardiac diseases. We are building an automatic ECG analysis system including an ECG sensor, a set of PDAs, and a database. The ECG sensor implements a wavelet-transform based algorithm and detects the abnormal signals associated with cardiac diseases. The patient's PDA, which is connected to the sensor, serves as a relay station that connects to the database and a doctor's PDA. The ECG sensor will trigger an alert if it detects abnormal signals. The doctor will then be made aware of the alert, validate it, and provide immediate assistance to the patient.
CarProof: Secure and Privacy-Preserved Data Collection in ITS Systems
Faculty: Qun LiProject homepage: Wireless Networking Group
Intelligent transportation systems (ITS) are gaining more and more attention as traffic problems in urban and suburban areas grow. ITSs are commonly used to transfer data about vehicles, drivers, and road conditions from vehicles to ITS operators for real-time traffic control, road maintenance, and the development of new traffic management strategies. However, privacy concerns from drivers have become a major obstacle that hinders the deployment of such applications. In this project, we study how to provide a secure and privacy-preserved environment for such data collection applications.
Classification of Accounts on Twitter
Faculty: Haining WangProject homepage: Haining Wang's Homepage
Twitter is a new web application playing the dual roles of online social networking and micro-blogging. Its popularity and open structure have attracted a large number of automated programs, known as bots, that appear to be a double-edged sword. Legitimate bots generate many benign tweets delivering news and updating feeds, while malicious bots spread spam or malicious content. More interestingly, between human and bot, there has emerged a class of accounts we call cyborgs (either bot-assisted humans or human-assisted bots). To assist human users in identifying with whom they are interacting, this project focuses on the classification of human, bot and cyborg accounts on Twitter. The project conducts a set of large-scale measurements on Twitter accounts and observes the differences among humans, bots, and cyborgs in terms of tweeting behavior, tweet content, and account properties. The proposed classification system uses a combination of features extracted from an unknown user to determine the likelihood of being a human, bot, or cyborg.
Confident Sensing in Heterogeneous Sensor Networks
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Many mission-critical applications such as military surveillance, human health monitoring, and obstacle detection in autonomous vehicles impose stringent requirements for event detection accuracy and demand long system lifetimes. Through quantitative study, we show that traditional approaches to event detection have difficulty meeting such requirements. Specifically, they cannot explore the detection capability of a deployed system and choose the right sensors, homogeneous or heterogeneous, to meet user specified detection accuracy. They also cannot dynamically adapt the detection capability to runtime observations to save energy. Therefore, we are motivated to propose a modality-agnostic event detection framework that clusters the right sensors to meet user specified detection accuracy during runtime while significantly reducing energy consumption.
DeSybil: Defending against Sybil Attacks Using Social Networks
Faculty: Qun LiProject homepage: Wireless Networking Group
Distributed systems are vulnerable to sybil attacks, in which the adversary creates many bogus identities, called sybil identities, and compromises the running of the system or pollutes the system with false information. Sybil identities can "suppress" honest identities in a variety of tasks, including online content ranking, DHT routing, file sharing, reputation systems, and Byzantine failure defenses. Sybil attacks can be mitigated by assuming the existence of a trusted central authority. This authority can limit the introduction of false identities by requiring users to provide some credentials, like social security numbers, or by requiring payment. However, such requirements may deter users from accepting these systems in that they impose additional burdens on users. A central authority can also easily be the target of denial-of-service attacks and thus reduce the reliability of the entire system. In this project we are investigating the use of social networks to mitigate sybil attacks.
Effective Resource Allocation under Temporal Dependence
Faculty: Evgenia SmirniProject homepage: Evgenia Smirni's Homepage
Temporal dependence within the workload of any computing or networking system has been widely recognized as a significant factor affecting performance. More specifically, autocorrelation in flows is catastrophic for performance. In a simple single server system, autocorrelation in the arrival intensities or service demands may result in user response times that are slower by several orders of magnitude. In homogeneous clusters, where size-based load balancing policies have been proved optimal for performance, autocorrelation in the arrival intensities of jobs obliterates any performance benefit of traditional load balancing policies. In multi-tiered systems, if a service process of any of the tiers is autocorrelated, then user response times are very high, in spite of the facts that the bottleneck resource in the system is far from saturation and that the measured throughput and utilization in all other tiers are also modest, falsely indicating that the system can sustain higher capacities. In storage systems, autocorrelation in the arrival or service processes at the disk level may result in significant user-perceived performance degradation. This project aims at providing a practical way to characterize and quantify the performance impacts of autocorrelated flows in systems. The main focus is on the development of new technologies for resource allocation that consider autocorrelation as an important characteristic of any stochastic process. On-line monitoring of autocorrelation provides the necessary information for scheduling parameterization, making an important step toward the development of autonomic systems. This research is supported by the National Science Foundation.
Efficient power management for mobile electronic devices
Faculty: Qun LiProject homepage: Wireless Networking Group
Mobile electronic devices, such as smartphones, laptops, and tablets, are becoming ubiquitous in people's daily lives. Battery life is an important consideration when it comes to providing good user experiences on these battery-powered devices. Aiming at increasing battery life, this project investigates the efficient management of battery power on mobile electronic devices. Our plan is composed of the following two steps. First, we examine the most power-hungry components on a mobile device (such as WiFi and GPS) and study how to make each of these components more power efficient. Second, we model, measure, and manage the power consumption on mobile devices in a holistic manner to further optimize the system power consumption.
EfficientRFID: Efficient RFID Protocol Design
Faculty: Qun Li and Weizhen MaoProject homepage: Wireless Networking Group
The "Internet of things" captures the vision that every object in the world can be tagged and connected through wireless or wired networks. Although RFID is one of most important enabling technologies in the Internet of things, a wide range of problems arise in RFID applications (e.g., inventory control, asset tracking, animal tracking, contactless payment). We have accomplished a number of results in RFID tag population estimation, RFID reading performance improvement, and secure RFID query and search protocol. In this project, we aim to further investigate a number of topics, including making RFID reading protocol more efficient and preserving privacy in RFID systems.
ETCH: Efficient Distributed Spectrum Allocation in DSA Networks
Faculty: Qun LiProject homepage: Wireless Networking Group
Dynamic spectrum access (DSA) is a promising technique that solves the spectrum scarcity problem and increases network capacity. In DSA networks, unlicensed users (i.e. secondary users) are granted the right to access the licensed spectrum when licensed users (i.e., primary users) are not using them. In other words, DSA allows much larger spectrums for secondary users, but secondary users must stop using these spectrums when they sense that the spectrum's primary users appear. In this project, we study how to efficiently allocate radio spectrums to secondary users in a distributed manner that reduces communication setup time and increase communication throughput.
An Explanation-Centric Approach to Software Verification
Faculty: Isil and Tom DilligProject homepage: Isil's Homepage
Automated software verification systems perform sophisticated reasoning to prove the correctness of various program properties, such as memory safety, validity of assertions, and lack of run-time exceptions. If the verification tool concludes that the program does not violate a certain property, we can rest assured that the program indeed obeys the desired property. On the other hand, if the verification tool claims that the program may violate a given property, there are two possibilities: 1) either the program is indeed buggy, or 2) the report generated by the tool is a false alarm. Since program verification is, in general, undecidable, false alarms are inevitable no matter how sophisticated the reasoning performed by the analysis tool. Thus, users of program analysis and verification tools must spend a considerable amount of time and effort to decide whether an error report generated by the tool is a false alarm or a genuine bug.
In this project, we explore an explanation-centric approach to automated program verification that is capable of systematically assisting end-users in deciding whether a given report corresponds to a real bug or false alarm. To reach this goal, we will design program analyses that are "introspective": Instead of merely giving yes/no answers, this new approach allows verification tools to interact with users and ask them small, relevant questions until the property can be proven or the report is confirmed as a real bug.
Exploration and Exploitation of Cache Sharing on CMP
Faculty: Xipeng ShenProject homepage: Compilers and Adaptive Programming Systems
Supported by the NSF, Dr. Shen and his team at the College of
William & Mary have achieved some discoveries that could lead to the significantly enhanced utilization of modern computers through intelligent job scheduling. In current computers, each processor typically
includes multiple computing units, and the number of units has been
increasing continuously. Different assignments of jobs to computing
units may influence computing performance significantly. An open
problem is how to efficiently determine optimal assignments.
By applying graph theory, Dr. Shen and his team have solved
the open problem in systems with dual computing units on each
processor. On more complex systems, they have proved that the optimal
assignment problem is equivalent to one of the hardest problems in
computation. Subsequently, they have developed a set of heuristics-based
techniques to accurately approximate optimal solutions, reducing cost by orders of magnitude compared to brute-force approaches.
They are currently transforming these findings into practical techniques
and integrating them into real computing systems.
Fall Detection
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Falls are dangerous for the aged population as they can adversely affect health. Prevalent methods of fall detection use accelerometers to isolate falls from activities of daily living. This makes it difficult to distinguish real falls from certain fall-like activities, such as sitting down quickly and jumping, resulting in many false positives. Body orientation is also used as a means of detecting falls, but it is not very useful when the ending position is not horizontal, e.g., falls that happen on stairs. In this project we use both accelerometers and gyroscopes to divide human activities into two categories: static postures and dynamic transitions. By using two tri-axial accelerometers at separate body locations, the system can recognize four kinds of static postures: standing, bending, sitting, and lying. Motions between these static postures are considered as dynamic transitions. Linear acceleration and angular velocity are measured to determine whether motion transitions are intentional. If the transition before a lying posture is not intentional, a fall event is detected. Our algorithm, coupled with accelerometers and gyroscopes, reduces both false positives and false negatives, thereby improving fall detection accuracy. In addition, our solution features low computational cost and real-time response.
IMDGuard: Protect Implantable Medical Devices
Faculty: Qun LiProject homepage: Wireless Networking Group
Recent studies have revealed security vulnerabilities in implantable medical devices (IMDs), including pacemakers and implantable cardiac defibrillators. Researchers have demonstrated that an adversary can collect private medical information and reprogram the IMDs without a patient's knowledge. Security design for IMDs is challenging due to the requirement that IMDs remain operable in an emergency when appropriate security credentials (such as the patient's authorization) may be unavailable. We designed and evaluated IMDGuard, a secure scheme for heart-related IMDs, to fulfill this requirement. IMDGuard incorporates two novel techniques to provide the appropriate protection for IMDs. One is ECG-based secure key establishment without prior shared secrets, and the other is an access control mechanism resilient to adversary spoofing attacks.
Input-centric Program Behavior Analysis and Adaptation
Faculty: Xipeng ShenProject homepage: Compilers and Adaptive Programming Systems
Despite decades of remarkable progress in program optimizations, nowadays, the one billionth run of a typical program is no more efficient than its first-time run. This project revisits the idea of lifelong continuous program optimizations, a paradigm proposed years ago but never realized in practice. It examines the three major challenges that face the development of the paradigm: program input characterization, online data collection, and incremental learning upon sparse data sets. Based on recent progress in program input characterizations and runtime profiling, this project aims to address each of the three difficulties systematically and make it possible to automatically recognize the relations between the inputs to a program and the appropriate ways to optimize the program. The whole process should happen transparently across production runs; there is no need for offline profiling or programmer intervention. With this new paradigm, a program would be able to evolve (in terms of performance) continuously through its life.
Interleaving Workloads with Performance Guarantees on Storage Clusters
Faculty: Alma Riska and Evgenia SmirniProject homepage: Evgenia Smirni's Homepage
This research focuses on the design and implementation of a lightweight yet versatile middleware framework that provides effective and scalable solutions to the problem of interleaving storage workloads with a wide spectrum of demands. The framework uses the simple and non-intrusive collection of workload statistics such as workload histograms and measures of temporal dependence to accurately forecast system workload characteristics and their impact on system metrics. The framework maps complex processes in storage clusters to robust allocation decisions accurately and swiftly. Central to the framework is its ability to estimate the effect of resource allocation policies on system metrics, which enables it to navigate through multiple possible allocations of system resources and select the one that best meets system targets. This research has the potential to revolutionize autonomic resource management in storage systems and provide methodologies to meet conflicting targets such as discovering trade-offs and dependencies between performance and other metrics including cost, energy consumption, reliability, and availability.
This research is supported by the National Science Foundation.
Measurement-based Content Creation for Computer Graphics
Faculty: Pieter PeersProject homepage: Pieter Peers' Homepage
Whether it is the amazing imagery of the alien world in Avatar, the
lifelike digital actors in The Curious Case of Benjamin Button, or the
underwater adventures in Finding Nemo, all have benefited from the
progress made in visualization and animation research in Computer
Graphics. However, all these amazing visuals would not be possible
without the hard work of the talented artists that create the models and
scenes that populate these digital worlds. In many cases objects and
scenes from the physical world around us are used as a source of
inspiration, or perhaps even directly digitally duplicated. Manually
duplicating physical objects is an arduous task, even for skilled artists.
The world around us has an abundance in detail, e.g., wrinkles on a human
face, dirt, dust and scratches on furniture in a room, etc. While
seemingly insignificant, these details are highly important for creating
photoreal digital imagery. The continuing developments in digital cameras,
and their widespread availability, have made it feasible to capture
snapshots from the world around us which include all these important
details. This makes digital cameras an exciting tool for creating digital
content. This project endeavors to develop novel measurement techniques
for creating the digital counterparts of physical objects – techniques that are
not only faster and more accurate, but more importantly, techniques that
novice users can easily use to, for example, capture the way an object
looks (i.e., appearance) or measure its shape (i.e., geometry). This development of measurement techniques involves porting existing techniques from controlled laboratory settings
into the "uncontrolled" real world. Furthermore, in many cases direct
duplication is not desired, but often something that is similar in
appearance is envisioned. Therefore, a secondary goal of this project is
to develop novel manipulation tools that allow users to change these
measured digital entities in a physically plausible manner without
limiting artistic freedom. Helping artists to deal with the abundance of
detail in these captured digital entities is one of the key focus
areas, something existing tools fail to provide. In short, this project
aims to make measurement-based content creation more accessible to expert
and novice users alike.
Mobile Online Social Networks
Faculty: Qun LiProject homepage: Wireless Networking Group
In the past few years, online social networks (OSNs) have gained great popularity and are among the most frequently visited sites on the Web. Through the services provided by OSNs, users establish and strengthen connections by sharing thoughts, activities, photos, and other personal information. Similarly, the popularity of mobile devices such as cell phones and tablets keeps growing, and these mobile devices are becoming smarter. Most cell phones sold today are capable of accessing the Internet over WiFi or cellular networks and determining their locations through GPS or cellular geolocation. As a result, it is not surprising to see the rapid fusion of OSNs with mobile computing, that is, a new paradigm called mobile online social networks (mOSNs). In this project, our goal is to solve the emerging privacy problems with mOSNs.
Modeling Techniques for Tools and Stochastic Models in Systems Biology
Faculty: Peter KemperProject homepage: Peter Kemper's Homepage
This research project is performed in close cooperation with the Smith lab (Applied Sciences). We jointly work on modeling techniques and tools to support the modeling of signaling complexes in systems biology. The stochastic gating of voltage- and ligand-gated ion channels in biological membranes that is observed by single channel recording techniques is often modeled using discrete-state continuous-time Markov chains (CTMCs). While these single channel models can be relatively simple (e.g., two physicochemically distinct states) or complex (hundreds of states), the challenge is to compose them into models of calcium release sites that consist of a large number of single channels such that the composed model shows a dynamic behavior that is consistent with experimental data for release sites. From a computer science point of view, we look for ways to represent and analyze multi-scale stochastic models that are able to reproduce and explain dynamic behavior observed in wet-lab experiments.
Multi-frequency MAC
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Multi-frequency media access control has been well-understood in general wireless ad hoc networks, but in wireless sensor networks (WSNs) it has not received much attention. In WSNs, each device is typically equipped with a single radio transceiver and applications adopt much smaller packet sizes compared to those in general wireless ad hoc networks. Hence, the multi-frequency medium access control (MAC) protocols proposed for general wireless ad hoc networks are not suitable for WSN applications, which we demonstrate through simulation experiments. In this project, we develop Multifrequency Media access control for wireless Sensor Networks (MMSN), which takes advantage of multi-frequency availability while taking into consideration the restrictions of wireless sensor networks. In MMSN, four frequency assignment options are provided to meet different application requirements. Scalable media access is designed with efficient broadcast support. Also, an optimal non-uniform backoff algorithm is derived and its lightweight approximation is implemented in MMSN, which significantly reduces congestion in the time-synchronized media access design.
Parallel Job Scheduling with Setup Times
Faculty: Weizhen MaoProject homepage: Weizhen Mao's Home Page
Malleable parallel jobs can distribute their workload among any number of available processors in a parallel computer in order to decrease their execution time. In contrast, nonmalleable parallel jobs must use a fixed number of processors. The ideal execution time of a malleable parallel job with length p is p/k if it utilizes k processors. However, inherently serial code and parallel processing overhead (from process management, shared memory access and contention, communication, and/or synchronization) often prevent actual execution times from achieving this ideal. It is natural to consider this extra time as a type of setup time, a term commonly used by the scheduling community. We have derived an execution time function that takes both speedup (i.e., p/k) and setup time into account for the parallel execution of malleable jobs. We have tested the validity of our mathematical model through numerous experiments on large parallel systems. We are working on the study of various algorithms that can efficiently schedule malleable parallel jobs online under the proposed model.
Paxos++: State Machine Replication Protocols in WANs
Faculty: Qun LiProject homepage: Wireless Networking Group
In distributed systems, state machine replication is the most general approach for providing a highly available service. With this approach, a reliable service is implemented by replicating it on several failure-independent replicas, which consistently change their states by applying deterministic commands from an agreed sequence. A consensus instance is used to decide on each command in the sequence. Chubby, the distributed lock service used by the Google File System, is a typical example of services that use state machine replications. With the rapid development of wide-area services such as web services, a fundamental research question is how to provide efficient general state machine replication in the wide area that only assumes the servers and clients are spread across a wide-area network. The goal of this project is to design and evaluate state machine replication protocols in WANs.
Performance Assurance within the Crowded Spectrum
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Recent years have witnessed the increasing deployment of cheap commercial off-the-shelf wireless devices for performance-sensitive applications such as patient monitoring with body sensor networks and home networking for multimedia applications and gaming. These applications often require assured performance on system throughput, delay, and reliability. However, by their nature, wireless devices must rely on shared physical media for communications, which often results in significant interference and poor performance if they are closely located. This becomes a growing issue as wireless devices populate the public unlicensed 2.4GHz ISM band, such as 802.11b/g routers, ZigBee sensors, Bluetooth headsets, and 2.4GHz cordless phones. There is a critical need to support performance-sensitive applications in the crowded 2.4GHz radio spectrum.
Practical Activity Recognition Using Smartphone-based Body Sensor Networks
Faculty: Gang ZhouProject homepage: Matt Keally's Homepage
The vast array of small wireless sensors is a boon to body sensor network applications, especially in the context awareness and activity recognition arena. However, most activity recognition deployments and applications are challenged to provide personal control and practical functionality for everyday use. We argue that activity recognition for mobile devices must meet several goals in order to provide a practical solution: user friendly hardware and software, accurate and efficient classification, and reduced reliance on ground truth. To meet the challenges of a practical solution, we present Practical Body Networking (PBN). Through the unification of TinyOS motes and Android smartphones, we combine the sensing power of on-body wireless sensors with the additional sensing power, computational resources, and user-friendly interface of an Android smartphone. We provide an accurate and efficient classification approach through the use of ensemble learning. We explore the properties of different sensors and sensor data to further improve classification efficiency and reduce reliance on user annotated ground truth. We evaluate our PBN system with multiple subjects over a two week period and demonstrate that the system is easy to use, accurate, and appropriate for mobile devices.
Quality of Service for Body Sensor Networks
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Wireless body sensor networks (BSNs) represent a promising solution for a growing national crisis –- affordable quality healthcare for all. Instead of expensive and invasive in-patient monitoring and high-contact care, wireless sensor nodes distributed at strategic locations on the body can continuously and non-invasively monitor individuals for a variety of physiological and biokinetic markers. The data that is wirelessly transmitted through the BSN and ultimately onto an existing wireless networking infrastructure can be used to follow trends for improved diagnosis and treatment or to detect events that require immediate intervention. With such technology, individuals can receive high-quality healthcare at a dramatically lower cost while maximizing their ability to live independently as they age. However, this promise will not be realized if BSNs cannot meet application and user requirements. Given that people’s lives are at stake in these target applications, it is essential that BSNs reliably provide high fidelity data and analysis. When applications require that an event be detected quickly for an immediate response, low latency is necessary. When a large number of BSN wearers live in proximity (as is the case in many continuous care retirement communities), network throughput becomes an important metric. Finally, the practical issue of wearability in terms of BSN node form factor and battery life is central to non-invasiveness and, therefore, compliance, requiring high energy efficiency to enable a small battery to last for a long time.
Radio Interference Detection and Mitigation
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
In wireless sensor networks, many protocols assume that if node A is able to interfere with node B's packet reception, then node B is within node A's communication range. It is also assumed that if node B is within node A's communication range, node A is able to interfere with node B's packet reception from any transmitter. While these assumptions may be convenient for protocol designs, they are not valid according to the real experiments we conducted. For a strong link that has a high packet delivery ratio, the interference range that we observed is smaller than the communication range, while for a weak link that has a low packet delivery ratio, the interference range is larger than the communication range. So using communication range information alone is not enough to design real collision-free media access control protocols. In this project, we develop a radio interference detection protocol to detect run-time radio interference relations among nodes. The interference detection results are used to design "real" collision-free time division multiple access (TDMA) protocols. We also explore the application of interference detection on contention-based medium access control (MAC) protocols.
RogueDetector: Client-side Rogue AP Detection
Faculty: Qun LiProject homepage: Wireless Networking Group
This project aims to prevent attacks from a category of rogue access points (APs) that pretend to be legitimate APs to lure users to connect to them. According to IEEE 802.11 standard, when multiple APs exist nearby, a WLAN user will always choose the AP with the strongest signal to associate. To attract users, therefore, a rogue AP needs to be close to users so that its signal could be stronger than legitimate APs. Once an innocent client is connected to a rogue AP, the adversary can manipulate and monitor the incoming and outgoing traffic of the client and launch various kinds of attacks. For instance, the adversary can easily launch phishing attacks by redirecting the user’s web page request to a rogue server to steal sensitive information (e.g., bank account numbers). We demonstrate a pure user-centric rogue AP detection algorithm that is compatible with existing network protocols.
Scientific and High Performance Computing
Faculty: Andreas StathopoulosProject homepage:Andreas Stathopoulos's Homepage
Traditionally, science and the scientific method rely on an interplay
between theory and experiment. With the advent of computers, computation
has emerged as the "third way" for scientific discovery.
The so-called computational sciences or scientific computing involves working closely with scientific applications while developing mathematical
models, algorithms, methods, and optimized software to run on
high performance architectures. It is now increasingly appreciated that high performance computing will become more important
in the future. The reason is simple: complexity. Real-world problems can
be modeled only through millions or billions of parameters or require a
search in a combinatorially exploding state space. In either case,
algorithms and high performance computing go hand-in-hand.
Numerical methods have been the main focus in this research, in
particular eigenvalue methods. Such methods are central in problems
as diverse as graph partitioning, data mining, stability analysis,
queuing theory, physics, chemistry, economics, and many others.
A state-of-the-art eigensolver, PRIMME, has been developed at W&M
and is used by many groups around the world. We are attempting to extend
this software with new methods and algorithms.
Another project is our on-going collaboration with the department of
Physics at W&M and the Jefferson Lab studying numerical methods for lattice
quantum chromodynamics. Examples of such methods include linear systems
of equations, Monte Carlo estimation of functions of matrices, and multilevel methods. We currently work on extensions of this work
in collaboration with IBM with applications stemming from data mining.
In addition, we are always interested in exploiting parallelism in our
methods, both at the multi-core level and at the supercomputing level.
With the architectural sea change of the last decade, this area has
been rising in importance.
SCUBE – Searching, Selecting, and Synthesizing Source Code
Faculty: Denys PoshyvanykProject homepage: Software Engineering Maintenance and Evolution Research Unit
Software developers rely on reusing source code snippets from existing libraries or
applications to develop software features on time and within budget. The reality is that most previously implemented features are embedded in billions of lines of scattered
source code. State-of-the-art code search engines provide no guarantee that retrieved
code snippets implement these features. Even if relevant code fragments are located,
developers face the rather complex task of selecting and moving these fragments into
their applications. This research program proposes an integrated model for addressing the fundamental problems of searching, selecting, and synthesizing (S3) source code. The
S3 model relies on integrating program analysis and information retrieval to produce
transformative models to automatically search, select, and synthesize relevant source
code fragments. The S3 model will directly support new methodologies for software
change and automated tools that assist programmers with various development, reuse, and maintenance activities. Thus far, we have built three source code search engines.
Exemplar is a search engine that combines information
retrieval and program analysis techniques to reliably link high-level concepts to the
source code of the software applications via standard API calls that these applications
use. CLAN is an engine for computing similarities among
software applications in large software repositories.
Finally, Portfolio is a source code search engine that retrieves and visualizes
relevant functions and their uses in 18,203 C/C++ software projects from over 260
million lines of code in FreeBSD Ports. This project is sponsored by the NSF.
SE2 — Software Evolution Based on Semantic and Evolutionary Information
Faculty: Denys PoshyvanykProject homepage: Software Engineering Maintenance and Evolution Research Unit
Software maintenance and evolution are a vital yet resource-consuming phase of the software lifecycle. Introducing software changes is particularly complex in long-lived, large-scale, and globally distributed systems. Years of research efforts have recognized three core tasks to support developers during software maintenance: feature location (identifying the starting point for a change in source code), impact analysis (determining which other software entities are also change-prone), and expert developer recommendations (assigning the appropriate developers to implement changes). This project will develop a novel one-stop solution for these tasks by integrating and mining latent information cluttered in the structured and unstructured software artifacts that are produced and constantly changed during the evolution of software systems, and that are largely untapped in current solutions. This project has three main goals: 1) to define a new integrated framework, SE2, for a comprehensive analysis of software evolution based on conceptual and evolutionary information; 2) to define new methodologies for software maintenance tasks based on SE2; and 3) to perform empirical studies to evaluate SE2 and supported methodologies. Central to our solution are state-of-the-art data mining, information retrieval, and program analysis methods. This project is sponsored by the NSF.
SiFi: Exploiting VoIP Silence for WiFi Energy Savings in Smart Phones
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Since one-third of a smart phone’s battery energy is consumed by its WiFi interface, it is critical to switch the WiFi radio from its active or Constantly Awake Mode (CAM), which draws high power (726mW with screen off), to its sleep or Power Save Mode (PSM), which consumes little power (36mW). Applications like VoIP do not perform well under PSM mode, however, due to their real-time nature, so the energy footprint is quite high. The challenge is to save energy while maintaining performance. In this project we present SiFi: Silence prediction based WiFi energy adaptation. SiFi examines audio streams from phone calls and tracks when silent periods start and stop. This data is stored in a prediction model. Using this historical data, we predict the length of future silent periods and put the WiFi radio to sleep during these periods. Implementing the design on an Android Smart phone, we have achieved a 40% energy saving while maintaining high voice fidelity.
Smart Grid
Faculty: Qun LiProject homepage: Wireless Networking Group
The smart grid is an electricity delivery system with bidirectional communication facilities and information technologies that enable more reliable and efficient grid operation. In this project, we address the security and efficiency issues for the smart grid. First, regarding security, it is possible for an adversary to attack this critical infrastructure. We have analyzed an attack scenario in which multiple meters are manipulated by attackers to confuse power system operators. We are designing an efficient strategy to detect and defend against such attacks. Second, regarding efficiency, users can reduce energy expenses by considering the dynamic pricing provided by the smart grid. To this end, we are designing scheduling algorithms for household appliances.
SmartAP: Designing a Better AP Association Protocol
Faculty: Qun LiProject homepage: Wireless Networking Group
In wireless local area networks (WLANs), the client's selection of an access point (AP) heavily influences its performance and that of others. Through theoretical analysis, we revealed that previously proposed association protocols are not effective in maximizing the minimal throughput among all clients. Accordingly, we proposed an online AP association strategy that not only achieves a minimal throughput (among all clients) that is provably close to the optimum, but also works effectively in practice with reasonable computational overhead. The association protocol applying this strategy was implemented on commercial hardware and is compatible with legacy APs without any modification. We demonstrate its feasibility and performance through both real experiments and intensive simulation.
Software Behavior-Oriented Parallelization
Faculty: Xipeng ShenProject homepage: Compilers and Adaptive Programming Systems
Software development is facing a dilemma as the processor industry
shifts its focus to multicore multiprocessors. Although more
processors are becoming available in a single computer, most existing
programs are sequential and cannot benefit from the hardware
advancement. Dr. Shen and his colleagues at the University of Rochester
have built an adaptive system for parallelizing complex sequential
programs in a cost-efficient manner. The system is unique in two
respects. It integrates machine learning techniques into the process of
program parallelization, which enables transparent learning of the
profitability of a program region. It also allows a user to convert a
sequential application to a parallel program incrementally without
the need for parallel programming or debugging.
Static Assurance for Android Applications
Faculty: Isil and Tom DilligProject homepage: Isil's Homepage
The goal of this project is to design program analysis techniques and
build practical tools for proving the absence of malware in Android
applications. For example, we would like to certify that applications
downloaded from a trusted marketplace do not adversely affect their users
by leaking private user information, sending out sensitive data, or
executing commands they receive from a remote server. Using the tools we
build, an auditor will be able to decide which applications are
trustworthy and which are potentially malicious, and only certified
applications will be included in the trusted marketplace.
Stochastic Workload Models for Storage Systems and Networks
Faculty: Peter KemperProject homepage: Peter Kemper's Homepage
Workload modeling is a classic area in modeling and simulation. The goal is to find a concise representation of a time series of requests that a system is tasked with such that relevant statistical characteristics of that workload are captured. A simple replay of measurement traces is not the best one can do; in this project, we explore the potential of Markovian Arrival Processes to represent workloads of storage systems. Relevant characteristics of these workloads include burstiness — sudden peaks of demand that far exceed average demand — which makes modeling challenging. This project is funded by NetApp.
TraceLab — Traceability Instrument to Facilitate and Empower Traceability Research and Technology Transfer
Faculty: Denys PoshyvanykProject homepage: Software Engineering Maintenance and Evolution Research Unit
This work will support a critical research agenda of the software engineering community and will facilitate the transfer of traceability solutions technology to business and industry. The traceability instrument, TraceLab, will contain a library of reusable trace algorithms and utilities; a benchmarked repository of trace-related datasets, tasks, metrics, and experimental results; a plug-and-play environment for conducting trace-related experiments; and predefined experimental templates representing common types of empirical traceability experiments. The traceability instrument will also facilitate the application of traceability solutions across a broad range of software engineering activities including requirements analysis, architectural design, maintenance, reverse engineering, and independent verification and validation. This is a collaborative effort led by Jane-Cleland Huang (PI), DePaul University; Jonathan Maletic (co-PI), Kent State University; and Denys Poshyvanyk (co-PI), William and Mary. This project is sponsored by the NSF.
Transmission Power Control
Faculty: Gang ZhouProject homepage: Gang Zhou's Homepage
Extensive empirical studies presented in this project confirm that the quality of radio communication between low-power sensor devices varies significantly with time and environment. This phenomenon indicates that previous topology control solutions, which use static transmission power, transmission range, and link quality, might not be effective in the physical world. To address this issue, online transmission power control that adapts to external changes is necessary. In this project, we develop a lightweight algorithm for adaptive transmission power control (ATPC) in wireless sensor networks. In ATPC, each node builds a model for each of its neighbors describing the correlation between transmission power and link quality. With this model, we employ a feedback-based transmission power control algorithm to dynamically maintain individual link quality over time. ATPC is robust even with environmental changes over time.
Traviando: Trace Analysis of Simulation Traces
Faculty: Peter KemperProject homepage: Peter Kemper's Homepage
Discrete event simulation is a common technique in the performance and dependability assessment of systems. Simulation comes with few restrictions so the real crux in simulation modeling is not to obtain numbers as results but to achieve valid results. Given that most simulation frameworks can export simulation runs in form of a trace, this project investigates possible ways to shed light on what really happens in a single simulation run. The goal is to simplify for a modeler the detailed dynamic behavior of a simulation model. Traviando is the name of a corresponding software package, which is currently used as a back-end for trace analysis in multiple simulation frameworks.
VANET: Vehicular Network Communication Protocol Design
Faculty: Qun LiProject homepage: Wireless Networking Group
Vehicular ad hoc networks (VANETs) have attracted significant attention in recent years with the goal of providing information regarding traffic (congestion, collisions ahead), highway conditions (potholes, cracks on the road, ice on the road, a blind spot ahead), and traveler support (local updated maps, parking areas, gas station locations). There are basically three types of communication in a vehicular network: inter-vehicle communication, vehicle-to-roadside communication, and hybrid vehicular communication. We have built a testbed for the three types of communication. In this project, our goal is to design secure and efficient communication protocols for this type of network.