UC Irvine – project transprose: transporting programs securely
New Approaches to Mobile Code:
Reconciling Execution Efficiency
with Provable Security
Michael Franz
University of California at Irvine
Technical Objective (1)

design the third line of defense in a mobile-code system
false
authentication
intrusion
malicious
mobile program
prevent
execution unless
provably secure
new third line of defense
second line of defense: authentication
first line of defense: access control (physical, logical)
Technical Objective (2)

make this “third line of defense” a pervasive property
of every computer system, not just a luxury good
afforded by only a few expensive ultra-secure highend installations
 rather
than simply demonstrating the viability of
mobile-code security, also make it practical across a
wide spectrum of applications
 in
this context, practical means scalable to large
applications, with excellent final code quality, at
resonable just-in-time compilation speed and cost
Existing Practice: Mobile Code
Java Virtual Machine code is the de-facto standard
format for distributing mobile programs
 the mobile code must be re-checked upon arrival
because it may have been corrupted in transit
 most Java code is translated into the appropriate native
code of the target machine “just-in-time”
 performance resulting from “just-in-time” compilation
is not competitive with off-line compilers
 JVM approach will not scale to large programs
requiring top-level performance

Existing Practice: Security
with Proof Carrying Code, the code producer attaches
a “proof” to the mobile program
 the code consumer generates a verification condition
that, if true, guarantees that the code is safe to execute
 the “proof” is used to discharge the verification
condition in linear time (linear in size of the proof, not
size of the program!)
 the “proof” can be extremely voluminous and
addresses many issues that wouldn’t need to be
“proved”, e.g., if source code were shipped instead

Existing Practice: Performance
raising the performance of JVM-code has been
addressed by “annotating” the byte-code stream with
compiler back-end related information
 “annotated” class-files run much faster if an
annotation-aware byte-code compiler is available on
the target platform
 security is lost: the “annotations” are not optional to
the annotation-aware compiler; if an adversary
falsifies them, the compiler will create a program that
may be unsafe!

Technical Approach

study the interaction of security-related information,
optimization-enhancing information, and compression,
rather than considering them separately
– use syntax-directed compression as a means of obtaining
guaranteed referential integrity
– use compiler-related annotations to obtain top-level
performance on the eventual target machine
– use a Proof-Carrying Code approach to guard the compilerrelated annotations from falsification in transit
Guaranteed Referential Integrity
programs are represented using some grammar
 can design a bit-level encoding for a grammar in such
a manner that all redundancy is removed
 as a consequence, strings that do not conform to the
grammar can provably not be represented in the
encoding
 focusing on:

– probabilistic approaches
– dictionary-based approaches
Interval Coding (Probabilistic)
encode the program based on the grammar of the
intermediate representation augmented by a
continuously adapted probabilistic model
 map the program to a sub-interval within [0, 1)
 during encoding/decoding, this interval is successively
refined
 every real number that falls inside the refined subinterval is considered to represent the program

Example of Interval Coding
int i, j, k; float x;
{ i = i + j; ...
assignment
70%
if
20%
statement
while
...
0
1
assign
if
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
local
90%
global
7%
assignment target
selector
...
0
1
local variable
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
i
30%
j
30%
local
k
...
0
1
i
j
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
i
30%
j
30%
local
k
...
0
1
j:=
[.19, .38)
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
final interval enclosed in [.19, .38) < 0.5
the first bit of the real-number representation
of this interval must be zero
=> output a zero and re-normalize
0
1
j:=
[.19, .38)
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
.0
0
1
j:=
[.38, .76)
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
local
25%
expression
50%
assignment source
global
...
0
1
[.38, .48)
Example of Interval Coding
int i, j, k; float x;
{ j = i; ...
.001
output two more digits and scale by 4
0
1
[.38, .48)
Result of Interval Coding
extremely compact representation in which every
possible bit-stream represents a program conforming
to the original grammar
 elements that are illegal at any given point have zero
probability and hence cannot be represented
 can apply this idea not just to source-language
grammar, but also to grammars “closer” to what the
code generator needs
 currently experimenting with SSA-related intermediate
representations

Performance-Enhancing Information
compiler-related information intended for improving
code quality re-introduces redundancy that can be
exploited by an adversary
 for example, a program in SSA form can be encoded
with guaranteed referential integrity using a grammar
close to the semantics of the source language
 but in order to allow optimizations such as coalescing
live ranges, the grammar needs to be relaxed
 the “holes” in the relaxed grammar need to be guarded
by other means based on PCC concepts

Approach Taken
use encoding-inherent security wherever possible
 use proof-based security where necessary to support
optimizations

– transporting results of alias analysis
– removing range or type checks

working on integrating these proofs into the stream
being encoded
– revealing the proof “line-by-line” rather than shipping it
separately from the program
– the dynamic code generator generates the verification
condition and discharges it at the same time
Project Workflow
source languages
semantic
modelling
grammar
based
encodings
proof
carrying
code
performance
annotation
modeling
Accomplishments to Date

grammar-based encodings
– developing two prototypes for exploring statistical and
dictionary-based compression/decompression

semantic modeling and annotation modeling
– developing a universal abstract syntax tree for representing
the source languages and an annotated version of it for
modeling optimizations

proof-carrying code
– working on proof representations and how to integrate
proofs with the encoding itself
Quantitative Metrics

security
– validate by simulating a series of attacks in which an
adversary supplies a hand-crafted mobile program that has
not originated in our source-language compiler

efficiency
– measure by comparing generated code quality with that of
existing on-the-fly compilers

code density
– measure by comparing with competing proof-carrying code
and mobile-code distribution formats
Expected Major Achievements
define a mobile-code solution that simultaneously
provides security, fast generation of highly efficient
native code, and exceptional information density
 develop a prototype that can form the basis of a
subsequent standardization effort

Task Schedule as per Proposal
Y1 Milestones:
•front-end prototype
•encoding format
design recommendation
1999
investigate:
•multiple source languages
•graph-based encoding
schemes
•proof-carrying code
Y2 Milestones:
•system prototype
•encoding format
comprehensive definition
2000
2001
investigate:
•requirements of
optimizing code generators
•integration of security vs.
compiler-related data
End of Project:
•system deliverable
•comprehensive
documentation
2002
investigate:
•mutual interaction of
security, efficiency,
and compression density
•security of system by
simulating attacks
Transition of Technology
the final mobile code format will be specified in
enough detail that unrelated third parties will be able
to craft alternate front-ends and back-ends compatible
with our system
 a design rationale will be published that explains key
choices among design alternatives
 our prototype implementation will be made available
in source form
 the graduate students involved in this work are likely
to transfer into the industrial sector

Thank You
Descargar

Beyond Java