>home/research/

Systems

Quality of Service Management for Enterprise-Application Computing Utilities 
PI: Tzi-cker Chiueh

A growing concern among corporate information technology (IT) managers is the elevating gap between the increasing system maintenance and administration cost of the IT infrastructure and the decreasing hardware/software acquisition cost. This gap is escalating because system administration and management is still heavily labor-intensive and does not scale very well with system size and complexity, despite extensive research efforts to automate the process. One promising approach to drastically reduce this cost is to adopt a computing utility model, in which a centrally managed computing infrastructure is shared among multiple enterprise applications in a way that preserves their high-level business objectives. The primary technical challenge in the computing utility model is how to provision and schedule system resources to support the desired quality of service (QoS) of individual business applications that share the same physical infrastructure without human intervention.

This project proposes to develop a multi-dimensional resource virtualization system called Iguacu, which multiplexes multiple system resources among a set of enterprise applications on a large-scale PC cluster such that the delay and/or throughput requirement of each such application is satisfied. Iguacu features three key innovations. First, unlike most previous QoS efforts that focus on a single system resource, Iguacu coordinates the allocation and scheduling of multiple system resources, including CPU, disk, and network link, to meet application-specific QoS requirements while significantly improving individual resource utilization efficiency. Second, Iguacu supports a unified and reusable implementation framework that could quickly convert, with zero or minor modification, a given database-intensive enterprise application into a form that provides guarantees based on service-specific performance metrics. The development of such a framework greatly mitigates the efforts required to deploy QoS-aware enterprise applications in a complicated IT environment. Third, Iguacu features a novel procedure that automatically translates high-level QoS specifications into physical system resource requirements for distributed enterprise applications running on a cluster environment. (NSF)

Multi-Dimensional Storage Virtualization
PI: Tzi-cker Chiueh

A growing concern among corporate information technology (IT) managers is the elevating gap between the increasing system maintenance and administration cost of the IT infrastructure and the decreasing hardware/software acquisition cost. This gap is escalating because system administration and management is still relatively labor-intensive and thus non-scalable, despite extensive research/commercial efforts to automate the process. In view of this trend, commercial enterprises resort to IT out-sourcing in order to share expensive and precious system management expertise. Despite its compelling cost saving advantage, IT out-sourcing so far has not been the mainstream, chiefly because the lack of technology to enforce and certify the so-called Service Level Agreement (SLA) between the out-sourcing and out-sourced parties. This proposal will develop a multi-dimensional storage virtualization system called Stonehenge, which is able to guarantee a wide variety of storage-related Quality of Service (QoS) metrics and thus provides the enabling technology to enforce SLAs associated with storage service in particular and Internet services in general. The set of techniques developed in the Stonehenge system carry the storage virtualization field one large step further because they allow virtualization of storage resource almost in all possible performance attributes that can be associated with physical disks. As a result, Stonehenge allows creation of virtual disks that are as tangible as physical disks, and yet much more flexible and easier to manage and maintain. As an integral component of this project, we will also develop a unified and reusable implementation framework that could quickly convert, with zero or minor modification, a given cluster-based Internet service into QoS-aware, such that they are capable of supporting contractual SLAs that are described in terms of service-specific performance metrics.  (NSF)

From Rules to Analysis Algorithms with Time and Space Guarantees
PI: Y. Annie Liu

Many computation problems, including program analysis and model checking problems, for security applications in particular, are most clearly and easily specified using relational rules. Yet, developing and implementing efficient algorithms for these problems is a nontrivial, recurring task. This project develops a unified method for transforming rule-based specifications into efficient algorithms and characterize the specifications and the transformations to provide both time and space guarantees for the derived algorithms. The project focuses in particular on rule-based specifications for program analysis and model checking problems and develop fully automatic methods for the transformations and the time and space analysis in this domain.  (NSF)

Model Checking for Detecting Computer System Vulnerabilities
PIs: C.R. Ramakrishnan, I.V. Ramakrishnan, R. Sekar, Scott A. Smolka, and Scott Stoller 

Securing our nation's computing and networking infrastructure against damage due to malicious attacks or spontaneous faults is a problem of paramount importance. This project aims to contribute to this mission by developing novel techniques and tools based on model checking and program analysis for vulnerability analysis: the problem of identifying and monitoring weaknesses in computer systems that can be exploited to compromise system security. A major expected outcome of the project is a set of tools for determining the consistency and safety of computer system configurations, such as those specified by firewall rules and domain type rules.  (NSF)

Model Checking for Detecting Computer System Vulnerabilities
PIs: C.R. Ramakrishnan, I.V. Ramakrishnan, S. Smolka, R. Sekar, and Scott Stoller

We developing a formal modeling framework for the modeling, simulation, and analysis of ad hoc wireless networks and their protocols, such as the Ad Hoc On-Demand Distance Vector (AODV) protocol. We model such protocols in the omega-calculus, a new modeling formalism for mobile ad hoc network protocols, which is a part of our ongoing research work. AODV is an on-demand routing protocol for mobile ad hoc wireless networks, and we model the behavior of a node running AODV in terms of its reaction to the events it may encounter. These are: receiving a data packet, route request, route reply, or route error. In the omega-calculus, nodes are modeled as agents and both broadcast and unicast inter-agent communication primitives are provided. An agent in the calculus is a process tagged with an interface. A process triggers the actions of an agent, and the interfaces of all the agents running in parallel represent the topology of the network formed by these agents. As such agent mobility is inherent in the calculus and need not be modeled explicitly. Rather, changes in the network topology due to agent mobility are captured in the calculus by corresponding changes to agent interfaces.  (NSF ITR) 

Generating Efficient Trust Management Software from Policies 
PIs: Scott D. Stoller, Yanhong Liu 

In today's widely distributed large-scale computer systems, there is a growing need to establish and enforce enterprise-wide security policies. This has stimulated development and deployment of more scalable and expressive security policy frameworks, notably role-based access control (RBAC) and trust management. Clear, precise, high-level specifications of these frameworks and policies help assure their correct design, implementation, and use.  This project addresses the challenge of generating efficient, high-assurance implementations of security policy frameworks and policies from simple, declarative, high-level specifications. We are developing implementation methods for high-level languages that analyze and transform such specifications to automatically produce efficient implementations. This is a significant advance over the state of the art, which is time-consuming and error-prone manual coding of implementations.  (Office of Naval Research)

Checking Critical Software for Concurrent, Distributed, Open, Secure Systems  
PI: Scott D. Stoller 

This project is developing analysis methods and tools that will increase the quality of concurrent and distributed software by helping programmers to debug, systematically test, and verify such software. The primary focus is on:
1) New techniques that significantly reduce the time and memory needed for state-space exploration of concurrent systems, by increasing the granularity of transitions, while preserving properties of interest.
2) Automated support for generation of programs that simulate the environment of an open system. This is particularly useful for generating hostile environments for testing of secure distributed systems. (3) Algorithms and tools for efficient run-time detection of synchronization errors in multi-threaded programs; targeted errors include data races, deadlocks, and atomicity (serializability) violations.   (Office of Naval Research)

A Layered Approach to Securing Network File Systems
PI: Erez Zadok 

This project explores a layered approach to file system security. By transparently stacking (or layering) file systems in strategic locations along a data path, we can explore security guarantees at different levels, including end-to-end guarantees. Stacking file systems at the client allows us to capture user-information early and encrypt data on the wire. Stacking at the server allows us to capture file system events close to the storage source, something that system-call--based security systems cannot do at the server since in-kernel file server code is invoked from the networking subsystem. Moreover, we can stack a file system in one place, then export it to another, creating a transparent secure file server proxy in between clients and servers. We are developing fan-out file system support for security. Such file systems can transparently provide many features useful to security: load-balancing to cope with DoS attacks, private branching for sandboxing, replication for disaster recovery, and more. We chose stackable file systems for our work because it offers a novel, new, and uniform API for developing secure file systems on clients, servers, and proxies. The stackable API is the ideal location for such work: neither too low (i.e., network packets) nor too high (system calls).  (NSF)

 An In-Kernel Runtime Execution Environment for User-Level Programs
PI: Erez Zadok 

It is vital to ensure that kernel and OS code is bug free because, today, malicious hackers are specifically looking for bugs and other OS vulnerabilities to exploit in order to gain unauthorized access to computer systems. In this project we explore techniques to add bounds-checking and other memory pointer checking for kernel code. Using a modified gcc, we build kernel modules with additional checking in them. When run, this kernel modules also check for array bounds, illegal pointer arithmetic, and other invalid pointer uses that normally will not cause the kernel to panic (but may still corrupt kernel memory). (NSF)

 

Runtime-Monitoring and Model Checking for High-Confidence Systems Software
PI: Erez Zadok
Co-PIs: Grosu, Liu, Smolka, and Stoller

The project investigates advanced model-checking techniques, coupled with operating-system code instrumentation, to achieve always-on monitoring of system software. The end goal is to allow complex software to be self-monitoring and to raise and lower its internal self-monitoring level, increasing software reliability over time. System software provides the critical infrastructure on which all other applications run, yet is quite difficult both to develop and to maintain. For example, it is often written in the C programming language, which is easily adapted to most platforms and with its descendants probably the most popular programming language in the world, yet prone to programming errors that may not be easily identifiable. Many elements intended to improve performance also make systems more complicated. The project will also examine an important component of the Linux operating system, the open-source system which is receiving increasing attention as a potential competitor to Windows. (NSF) 

Admission Control 
PI: Eugene Feinberg 

This project studies admission control in telecommunication systems as an application of a new approach to the analysis and optimization of stochastic discrete-event systems. Admission control with Quality of Service constraints is a focus. Examples of such constraints include constraints on blocking probabilities for certain customer classes. This project describes the structures of optimal control policies and develops algorithms for their computations and implementations.  (NSF)