2000 Project Summary
|Project Website:||http://www.ics.uci.edu/~franz/ITS.html -- Additional project information provided by the performing organization|
|Quad Chart:||Link to Quad Chart provided by the performing organization|
|Objective:||Using mobile code is fraught with risks. If an
adversary succeeds in deceiving us into executing a malicious program supplied
by him or her, this may have catastrophic consequences and may lead to
loss of confidentiality, loss of information integrity, loss of the information
itself, or a combination of these outcomes. Hence, we must at all costs
avoid executing programs that can potentially cause such harm.
The first line of defense against such incidents is to shield all computer systems, all communications among them, as well as all of the information itself against intruders, using physical and logical access controls.
A second line of defense is to use cryptographic authentication mechanisms to detect mobile code that hasn't originated with a known and trusted code provider or that has been tampered with in transit.
This project investigates a third line of defense that is independent of and complimentary to the first two mentioned above: Assume that an intruder has successfully managed to penetrate our system (breaking defense #1) and is able to present us with a mobile program that falsely authenticates itself as being uncompromised and originating from a trusted party (breaking defense #2), how do we nevertheless prevent it from causing any damage?
The objective of the project is to make such a "third line of defense" of intrinsic mobile-code security a pervasive property of every computer system, not just a luxury good afforded by only a few expensive ultra-secure high-end installations. In order to become pervasive, mobile-code security must not only be viable, it must also become practical. This is where we expect to make contributions.
|Approach:||We are working on a representation for target-machine
independent mobile programs that can provably encode only legal programs.
Hence, there is no way an adversary can substitute a malicious program
that can corrupt its host computer system: Every well-formed mobile program
that is expressible in our encoding is guaranteed to map back to a source
program that is deemed legal in the original source context, and mobile
programs that are not well-formed can be rejected trivially. Further, our
encoding not only guarantees referential integrity and type-safety within
a single distribution module, but it also enforces these properties across
A problem of previous approaches to mobile-code security has been that the additional provisions for security lead to a loss of efficiency, often to the extent of making an otherwise virtuous security scheme unusable for all but "toy" programs. This research strives to deviate from the common approach of studying security in isolation, and instead attempts to integrate it with other aspects of mobile-code quality. Among the additional qualities to consider are the mobile code format's encoding density (an important factor for transfer over wireless networks) and the ease with which high-quality native code can be generated by a just-in-time compiler at the eventual target site.
Recent FY-99/FY-00 Accomplishments
|New Project (Started June 1999)|
|FY-00 Plans:||Goal 1: Explore the use of a core calculus as
a verifiable "bottleneck interface" for modeling secure mobile programs.
An actual core calculus is being developed in a prototype implementation.
This prototype implementation consists of an actual front-end/back-end
pair for a small but not trivial source language and a simple target architecture
(a RISC simulator). As a proof of concept, the eventual prototype will
be able to compile a source program, map it to the core calculus, map back
from the core calculus, and then also actually execute it.
Goal 2: Study the concepts of dictionary-based encodings in much greater depth than has been done before. In particular, we are exploring ways of explicitly limiting the encoding dictionary to constructs that are legal in the source language, either by aggressive pruning or by generating the legal variants on-the-fly. For example, it is unknown at this point how big the combinatorial explosion will be if all legal constructs are explicitly enumerated at each point in the encoding process. We are in the process of constructing a prototype encoder/decoder pair to explore these issues using the Java source language.
Goal 3: Construct a unified abstract syntax tree (UAST) model for multiple source languages. Based on this model, we will build a common front-end system and later explore the question of which compiler-derived annotations are useful for the back-end, and how these should be represented in the model. It is hoped that many of these annotations can be done "across" the source languages, and that the number of instances in which one needs to take the "flavor" of source program into account is minimal. The annotation mechanism will be implemented as a tree-to-tree mapping: a tree in the UAST language will be the input and an attributed tree in some compiler-specific representation will be the output.
Goal 4: Study proof-carrying code in the context of adaptive compression and dynamic code generation. This also involves experimentation with how predicates and proofs should be represented. We envisage a format in which the proof is interspersed with the code being compiled, and in which the proof verifier (as well as the equivalent of a verification condition generator) are integrated into the dynamic compiler. In such a format, the proof is revealed successively while the encoding is being parsed. We hope to be able to lift many of the existing restrictions of the original PCC idea, for example, with respect to dynamic compilation, dynamic dispatch, and exception handling.
Goal 5: Study bit-level compression schemes related to the research effort. In particular, the expected output of the dictionary encoding scheme is going to be a stream of (number n out of distribution d). We would like to obtain an optimal encoding for such a stream of symbols, in which each symbol has a different (known) distribution. For example, one solution might be to use the same encoding for each distribution of d possibilities, but different encodings for different such distributions.
|Technology Transition:||A new mobile code format will be specified in
enough detail that unrelated third parties will be able to craft alternate
front-ends that produce mobile code compatible with our deployment environment,
and also construct alternate run-time environments that are compatible
with our front-end system. The design rationale document accompanying our
format specification will enable third parties to understand the specific
choices between key design alternatives that we made, allowing potential
follow-up projects to proceed without having to repeat these steps. It
is anticipated that the results of our basic research will subsequently
lead to development projects in industry.
At the end of the project, we will also make available working prototypes of an integrated compiler front-end system for producing mobile code from multiple source languages and of a secure environment for deploying mobile code in this format on a modern RISC processor both in executable versions as well as in source form, along with appropriate documentation for their operation. The executable versions will allow third parties to put the system into use immediately while the source-language versions are likely to form the basis of alternative implementations of the system in research, military, and commercial contexts. The availability of source code will greatly enhance the acceptance of the working prototype to third parties and is likely to speed up the transitioning of the technology into industry.
|Principal Investigator:||Michael Franz
University of California, Irvine
Irvine, CA 92697-3425
Phone: (949) 824-4825
Fax: (949) 824-4056