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.
Society is dependent on many engineered systems whose increasing complexity and inter-connectedness have, in turn, increased their vulnerability to disruption. In many of these systems, protecting the execution of the tasks they perform is as crucial as ensuring the security of their data, and since they often compete for common resources such protection depends significantly on how resources are allocated among those tasks. The goal of this research has been to develop new techniques to ensure timely execution of system tasks, through principled sharing of resources among them, even when: (1) how long each task will use the resource is known only statistically (and possibly must be learned as the system runs); (2) once granted, a task's use of the resource is not preempted until the task releases the resource; and (3) different systems may have different measures of how useful it is for each task to access a resource at different times. This research has produced several technical contributions towards that goal: we have established a novel approach for automated generation and verification of policies for how the use of a resource can be scheduled rigorously among such tasks; we have identified explicit structure both in the policy design approach and in specific policies generated by it, which can be exploited to produce policies more efficiently and for a wider range of systems; we have shown how reasonable policies can be generated even when information upon which they depend must be learned on-line; and we have generalized our approach to handle cases where the utility of each task having the resource may vary over time.
