Acknowledgement

Introduction

This project is aimed at developing a new approach for securing mobile (or downloaded) code, which has become an integral part of the Internet. Examples of untrusted partially trusted software include: document handlers and viewers (e.g., Real Audio, ghostview), games, peer-to-peer applications (e.g., file sharing, instant messaging), freeware, shareware and trialware, and mobile code (applets, JavaScript, ActiveX). Contemporary operating systems provide little support for coping with such applications.

The goal of the Model-Carrying Code (MCC) project is to develop a practical and usable tools that enable mobile-code consumers to:

• precisely specify their security policies,
• formally verify whether a piece of mobile code satisfies these policies, and
• execute mobile code with the guarantee that it will not violate these policies.

A key benefit of the MCC approach is that once static verification succeeds, the consumer can safely assume that the mobile code will complete its task without encountering further security errors. Should the verification not succeed, the consumer has the option of refining his/her security policies in ways that allow the mobile code to provide its functionality without unduly increasing the security risk posed by it. The task of policy refinement can itself be partially automated in order to assist unsophisticated users.

Overview of Approach

Formal verification of software has been a subject of intense research over many decades, and has proven to be a difficult problem. For mobile code, the situation is further complicated by the fact that code producers tend to provide only binary (rather than source) versions of their code. The fundamental insight in the MCC project that has enabled us to overcome these difficulties is that of decomposing verification into two stages:

• model extraction: the process by which code producers generate abstract models of the security-relevant behavior of their code.
• consistency resolution: the process by which code consumers verify that their security policies are satisfied by the mobile code.

Since models are significantly simpler than programs, automated verification of security policies against models (using model-checking techniques) becomes feasible under the MCC approach. Furthermore, the decomposition provided by MCC shields a code producer from having to know about specific security concerns of different consumers, and the code consumer from having to understand implementation decisions made by a code producer. As a result, consumers need not reveal their security policies to a producer, nor do producers have to reveal their source code to a consumer.

The techniques developed in the MCC project is being incorporated into software tools that are placed at the entry points for mobile code, namely, software installers, through which explicitly downloaded and installed software enters the system, and email/web browser, through which implicitly downloaded code enters the system. These tools will be available as downloadable software for on Linux/Intel systems. The project results are expected to be commercialized through our industrial partners.

The figure above shows the key idea in MCC: introducing program behavioral models that help bridge the semantic gap between (very low-level) binary code and high-level security concerns of consumers. MCC includes a model generator, which automatically generates models at the producer-side. A consumer receives both the model and the program from the producer. The policy selection component checks whether the model satisfies the consumer's policy. If the model is not consistent with the policy, the consistency resolver reports a compact and user-friendly conflict feedback to the consumer. The consumer can either discard the code at this point, or refine his/her policy to permit execution of the code without posing undue security risks. If the model is consistent with the (refined) policy, then the code and the model are forwarded to the enforcement component. The enforcement/recovery component checks whether the model captures all the program's behaviors. Our current implementation of enforcement is based on system call interception. If the enforcement component detects a deviation from the model, the the execution of the untrusted code is terminated.

This research is conducted at the Secure Systems Lab and the Applied Logic Lab at Stony Brook University. For more technical details of MCC, please refer to our SOSP03 paper.

Last updated: August 1, 2005.
Suggestions, comments or questions: contact R. Sekar (sekar@cs.sunysb.edu)