Jay Ligatti - US grants

CT-ISG: Collaborative Research: Trustworthy Enforcement
of Domain-independent Run-time Policies
Abstract
Run-time monitors are a common and pervasive mechanism for ensuring that software and
systems adhere to security policies. Anti-virus and anti-spyware programs, personal firewalls,
intrusion-detection tools, Java's stack inspection, and even mechanisms that trap operatingsystem
exceptions in order to show a ?blue screen of death? can all be thought of as run-time
monitors. Although they differ greatly in their complexity and scope of policies that they can
enforce, these mechanisms all observe the behavior of a running system and detect and react
to potentially dangerous events. Despite the pervasiveness and real-world importance of runtime
monitors, their use has far outpaced theoretical work that makes it possible to rigorously
reason about monitors and the policies that they enforce, particularly in distributed settings.
This project develops models, tools, and mechanisms for reasoning about and implementing
distributed, concurrently executing run-time monitors. The research adopts a holistic,
four-prong approach that spans the breadth of the space between theoretical models and
practical systems for enforcing run-time policies. Specifically, this project (1) creates a
framework for reasoning about enforcement that permits the possibilities of concurrent, distributed
computations; (2) develops a type-safe policy-specification language that ensures
that specified policies compile into well-behaved monitoring mechanisms; (3) designs trustworthy
algorithms for automatically translating a desired overall policy into node-specific
policies that can be distributed and enforced throughout a network; and (4) designs, implements,
and tests a prototype system for specifying and enforcing run-time policies with
support for concurrently executing computations. Taken together, these research tasks enable
formal modeling and automatic enforcement of run-time security policies in concurrent
and distributed settings.

This project addresses the problem that, to be trustworthy yet practical, mechanisms for enforcing software security must (1) undergo rigorous analysis that provides formal security guarantees and (2) be developed quickly. The project addresses this problem by creating (1) formal, foundational theories of software security and (2) convenient tools for quickly generating provably sound enforcement mechanisms. The foundational theories consist of formal definitions and rules for precisely specifying and reasoning about general security principles: threats, policies, mechanisms, and the means by which mechanisms enforce policies to prevent attacks. These theories aim to enable researchers and developers to analyze real mechanisms precisely and to prove which attacks those mechanisms can and cannot prevent in practice. The enforcement tools consist of technologies for converting expressive specifications of policies to be enforced into concrete mechanisms guaranteed to enforce those policies. These tools aim to enable researchers and developers to quickly and conveniently define, concretize, and deploy new security mechanisms. The enforcement tools and foundational theories are connected in that the theories provide models in which to establish the trustworthiness of tool-generated mechanisms. Taken together, these research tasks for creating and connecting theories and tools enable rapid development and deployment of trustworthy enforcement mechanisms for secure software systems.

ANET: Mobius: A Multi-Tier Socially-Aware Network Infrastructure

Abstract

This research explores the benefits of embedding social knowledge in network protocols and services to support mobile social computing. Specifically, it investigates 1) which mobile social computing problems can be solved with socially aware networks; 2) what social information is amenable to being captured and utilized by these networks (assuming privacy preserving capabilities); 3) what mechanisms and system architectures are necessary to enable dynamic network adaptation to geo-social context changes; 4) how to leverage these mechanisms to design socially-aware protocols and services; 5) how to define and enforce individual and global privacy policies, in general and for accessing social context; and 6) which programming abstractions provide both flexibility and simplicity for rapid mobile social computing application development.

This research will lead to a self-organizing, self-adaptive, community-oriented, two-tier network infrastructure for mobile social computing. The mobile human-centric tier runs mobile applications and collects geo-social context information. The peer-to-peer system tier runs services in support of mobile applications and adapts to the geo-social context to enable energy-efficient, scalable, secure, and reliable applications. For large-scale evaluation, this project uses the NSF-sponsored SmartCampus testbed with hundreds smart phones distributed to students.

This research will expand the understanding of mobile social computing, an area of great practical relevance to the society at large. To spur the dissemination of results, the source code is made publicly available. Noteworthy educationally is that both institutions, University of South Florida and New Jersey Institute of Technology, are among the national leaders in the percentages of graduates from under-represented groups, and the researchers have specific plans to attract students from these groups to research opportunities in the project. Finally, the foundational results of the project are integrated in an inter-disciplinary studio course that creatively explores design ideas in mobile social computing.

The world of computing has entered the multi-core age. In addition to multi-core CPUs, co-processors containing thousands of computing cores in a single chip have become popular platforms for general-purpose computing. With the aggregated computing capabilities increasing at a steep rate, computing communities are still in an early stage in developing software systems, frameworks and applications to take full advantage of these new platforms. The co-existence of several different multi-core systems, including the Graphics Processing Units (GPUs), Intel?s Many Integrated Core (MIC) cards, and Accelerated Processing Units (APUs), further complicates the issue. This, on the other hand, provides opportunities for interesting research that spans different layers of the software stack. This infrastructure will support multiple, coordinated research projects that will develop frameworks and software systems enabling a new class of applications requiring high-performance computing capabilities.

The main goal of this project is to build a computer cluster with heterogeneous, massive parallel computing capabilities to accelerate existing research and enable ground-breaking new research that shares the same need for intensive computation at the University of South Florida (USF). This project brings together eight USF investigators with research projects in several core disciplines of computer science and engineering: big data management, scientific computing, system security, hardware design, data mining, computer vision and pattern recognition. Specifically, the requested cluster supports research in:
(1) design and optimization of a novel data stream management system architecture in a heterogeneous many-core hardware environment;
(2) coarse-grained molecular simulation approach that allows accurate simulation of large-scale atomistic systems;
(3) new system to deploy security policies that excel in both policy composition and runtime performance;
(4) efficient modeling and design of energy-efficient and secure hardware systems;
(5) automated interpretation of activities using pattern theory;
(6) fast large scale clustering; and
(7) pattern identification from biomedical image data.
The intellectual merit of this project derives from the innovations of the individual projects and from the potential cross-disciplinary ideas it can germinate in the future. The infrastructure is expected to facilitate collaboration and cross-pollination of algorithms, models, representations, and data sets across individual project areas, building a collaborative network across the investigators. Furthermore, the cluster is expected to impact over a dozen application domains via on-going and planned research projects among the investigators and their collaborators throughout the USF system.

Direct benefits to education and research will also be extended to the larger community through the applied aspects of projects, teaching and training. Project results and media content of the cluster will be showcased in the popular USF Engineering EXPO event, which seeks to educate and motivate K-12 students on math, science, engineering, and technology subjects.

As wireless technologies become more pervasive, it becomes increasingly important for devices to authenticate the locations of other devices. For example, patients with implantable medical devices (IMDs) may reasonably expect that any device used to control their IMD would have to be within arm's reach, to help prevent unauthorized access to their device. In other words, IMDs should enforce policies based on the proximity, and in general the location, of wirelessly connected devices. Similar examples exist in many application areas: contactless payment terminals may require credit cards to be located in front of the terminals; wireless routers may require network users to be located in the same building; GPS devices may require signals to come from satellites (rather than from adversaries masquerading as satellites); and mobile phones may require signals to come from known, legitimate cell-tower locations. Hence, the security of many wireless devices could be improved by enforcing proximity-based policies on remote devices' locations.

This project aims to address the problem that, although proximity-policy enforcement would improve the security of many wireless devices, robust techniques and tools do not yet exist for enforcing such policies. The project addresses this problem by creating such techniques and tools. The proximity-authentication techniques will allow a device to passively authenticate the location of remote device, without having to send messages to, or share secrets with, the remote device. They identify the proximity of a remote target by utilizing the multipath effect, in which a wireless signal sent by a transmitter propagates to the receiver in the air along multiple paths due to reflection, diffraction, and scattering. The proximity authentication decision is made based on amplitude ratios of wireless signal copies traveling on these prorogation paths. The proximity-policy enforcement tools will include (1) an expressive language, and a graphical interface, for specifying remote-device location policies, (2) an engine for statically analyzing specified location policies, in order to notify security engineers as to how accurately their policies can be enforced and whether their policies are unsatisfiable, and (3) a compilation module to transform valid policies into concrete enforcement code that can be inlined or otherwise hooked into a device's existing connection-establishment code.

As software now pervades nearly every aspect of modern life, securing software is widely acknowledged as a critical problem. Although significant effort has gone into identifying flaws in software, as well as developing tools, libraries, and processes for detecting and mitigating these flaws during software development and maintenance, security problems remain pervasive. There has been comparatively little effort to empirically assess the effectiveness of existing tools and processes in realistic settings, and almost no effort to understand the root causes of professional developers making security errors. This lack of knowledge hinders the advancement of secure programming techniques that can effectively reduce the number of security bugs in deployed software. This research focuses on measuring and evaluating the effectiveness of particular approaches to securing software as carried out by typical developers. By combining anthropological observation of industrial development practice with experimental evaluation of tools and processes, this project will identify new or underappreciated approaches to improving software security in practice.

The research includes four interdependent approaches: anthropological observation via long-term embedding in partner industrial software development teams; conducting and analyzing results from secure-programming contests that serve as quasi-experiments; controlled lab experiments; and analysis of open-source software artifacts. The anthropological approach produces deep insights through zero-proximity observation and reflection by fieldworkers, and competitions illuminate how differences in approach (language, tools, etc.) to a substantive problem correlate (quantitatively and qualitatively) with success or failure. Both of these approaches will generate hypotheses, which can then be tested via controlled lab experiments, as well as additional field, contest, and artifact observations. This combination of approaches leverages the strength of each in order to maximize both ecological and internal validity, offering the best chance to understand the real causes of (in)secure software development and offer effective guidance.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.