CT-ISG: Collaborative Research: Non-bypassable Kernel Services for Execution Security

NSF Support

This research has been supported by the National Science Foundation, grant CNS-0716764.

Project Description

Society is dependent on many engineered systems whose increasing complexity and inter-connectedness have, in turn, increased their vulnerability to adversarial attacks. In many of these systems, protecting the execution of their computations is as crucial as ensuring the security of their data.

This research investigates how to maintain survivable operation of such systems, even in the face of invasive attacks where computations are intentionally subverted to interfere with other computations' execution constraints. The goal of this research is to develop new techniques for isolating the effects of interactions among computations through specific resources in these systems, including: flexible specification and rigorous enforcement of computations' execution constraints; explicit control of all OS kernel components under a single scheduler; detailed on-line monitoring of computations and their supporting OS kernel components; automated learning to discover previously unknown interactions among computations; and formal modeling and verification of computations, execution constraints, and system components and resources.

The expected benefits of this project include: a novel approach to non-bypassable isolation of computations from the effects of adversarial attack in which isolation can be enforced flexibly according to the system-specific execution constraints that must be satisfied; a high quality open-source software implementation of kernel-level scheduling and monitoring services that provide and measure such non-bypassable isolation; new formal models, analyses, and methodologies for verifiably correct configuration and management of those services; and empirical studies of the services' ability to protect computations from interference under a wide range of adversarial attacks.

Project Participants


Christopher Gill, Associate Professor of Computer Science and Engineering, is PI for this research at Washington University in St. Louis.

William D. Smart, Associate Professor of Computer Science and Engineering, is co-PI for this research at Washington University in St. Louis.

Douglas Niehaus, Associate Professor, Electrical Engineering and Computer Science Department, is PI for collaborative research at the University of Kansas.

Doctoral and post-Doctoral Researchers

Robert Glaubius and Terry Tidwell have contributed to this research as doctoral students; following completion of his dissertation in December 2009, Robert Glaubius extended his contributions as a post-doctoral researcher supported by NSF grant CCF-0448562 (CAREER).

Undergraduate Researchers

Undergraduate students at Washington University in St. Louis who have contributed to this research are Carter Bass, Eli Lasker, Justin Meden, David Pilla, and Braden Sidoti. Cameron Cross (DePauw University) and Micah Wylde (Wesleyan University) also contributed to this research during their summer research visits to Washington University in 2009 and 2010 respectively.

Doctoral Dissertation





Our previous research on developing time and event based models of system software (supported by NSF CAREER grant CCF-0448562) has shown that detailed models of essential middleware mechanisms can be developed, composed, and for constrained examples verified tractably, using state of the art timed automata model checkers. Building on that original work, our subsequent research on integrating the semantics of system software, scheduling, and applications through run-time monitoring and enforcement (supported by NSF EHS grant CCF-0615341) has shown that repeated (quasi-cyclic) structure of threads execution is induced by bounded fair scheduling policies, and that bounds on the divergence of threads' execution can be determined from that quasi-cyclic structure and used to reduce state space complexity.

The goal of this research has been to develop new techniques for non-bypassable specification and enforcement of execution guarantees for system tasks, leveraging and extending those prior results. In this research, our discoveries to date include seven major contributions towards this goal. First, we have established a novel approach to scheduling policy design and verification, that is specifically designed for resource allocations to tasks with variable execution times. Second, we have developed a novel technique for using repeated (periodic) structure to wrap the state space into a tightly bounded form. Third, have shown how a state space suitable for verification with existing timed automaton model checkers can be generated by first enumerating verification states that consist of sets of utilization states, and then defining suitable difference bound matrices (DBMs). Fourth, we have developed a new technique called Expanding State Policy Iteration (ESPI) that allows computation of an optimal policy for a wrapped state model. Fifth, we have shown that for highly structured examples like proportional sharing of a resource, the structure of the generated scheduling policies themselves can be approximated with high accuracy, leading to a scalable technique for generation of high quality scheduling policies for larger numbers of concurrent activities. Sixth, we have shown that even when distributions of tasks execution times are unknown in advance, if the distributions are stable then reinforcement learning can be used to obtain suitable policies on-line. Seventh, we have extended our approach to include periodic tasks whose individual utility can be expressed as functions of their completion times.