Transcript 31-May-02

SAFKASI: A Security Mechanism for
Language-based Systems
Dan S. Wallach
Rice University
Andrew W. Appel and Edward W. Felten
Princeton University
Excerpt By: Raghuram Vijapurapu
Contents
●
What is this all about?
●
What is SAFKASI?
●
What is Stack Inspection?
●
How Stack Inspection Works?
●
Limitations of Stack Inspection
●
Improvements from SAFKASI
●
Access Control Logic (ABLP)
●
Improved Implementation
●
Security Passing Style and its Implementations.
What is this all about?
Security in Java is considered one of the toughest
when compared to many other languages. This is
with respect to the execution of an unsafe
operation by a client, that is in File System
interaction and in execution of “dangerous
routines”. This security in Java is provided by a
feature in JVM called Stack Inspection. In actual
implementation of Stack Inspection there exists
an “unclear relationship to the actual
achievement of security, over constrained the
implementation of a Java system”.
What is SAFKASI?
Its Pronounced as : saff-KAH-zee
[D. Wallach; a new approach to mobile code security]
Security Architecture Formerly Known As Stack Inspection
SAFKASI is an improved implementation of Stack
Inspection using the “calculus of SecurityPassing Style”. It is a model by which Stack
Inspection can be improved.
What is Stack Inspection?
Stack inspection is an algorithm for preventing
untrusted code from using sensitive system
resources. Before a dangerous operation
proceeds, a call is made to the
security
manager, which implements a reference
monitor. The security manager will consider, in
sequence, the principals* that own each stack
frame. If a stack frame's principal is found to be
unprivileged for the operation in question,
permission is denied and the operation fails.
*Principal is either the Web site from which the code was loaded or
a signer who applied a digital signature to the code.
How is it Implemented in Java?
Two Basic Operations of Stack Inspection are:
BeginPrivilege( ): Enables Privileges
CheckPrivilege(T): Check whether privileges for a
given target T are enabled. Check-Privilege is
implemented by searching stack frames from the
current one.
A Demo on how Stack Inspection Works:
Stack Inspection Demo
DeleteFile(xyz) <=
AliceFrame
CheckPrivilege
Stack Inspection Demo
DeleteFile( )
QuickSort( )
AliceFrame
<=
CheckPrivilege
Stack Inspection Demo
DeleteFile( ) <=
SubRoutine( )
BeginPrivilege
LoadURL( )
AliceFrame
CheckPrivilege
Limitations of Stack Inspection
●
●
●
It is not clear whether the mechanism achieves
real security, or how to reason about the security
that it might achieve.
The operational definition of stack-inspection
over constraints its implementation.
The high cost of the CheckPrivilege operation
discourages its usage.
Improvements from SAFKASI
●
●
●
Describing Stack Inspection using ABLP* Logic
Applying new semantics for Stack Inspection
called “Security Passing Style” and providing the
flexibility to express all the security operations in
plain Java. Not only does this avoid interference
with program analysis and optimizations, but
standard dataflow-based compiler optimizations
now help optimize security operations for free.
Each of the operations in our new implementation
can be performed in O(1) time.
* Abadi, Burrows, Lampson and Plotkin [Abadi et al. 1993]
Access Control Logic
The Authors decided to adopt an access control
logic described in Taos Operating Systems, where
the Operating System maintains all the records of
access control whether it is Network or Resource.
The logic needs relatively simple propositional or
modal logic with no negation of statements (and
with certain restrictions on the form of
statements), allows the theorem prover to run fast
enough to not dramatically impact system
performance. This kind of access logic provided
by ABLP Logic was used to model Stack
Inspection.
ABLP Logic
ABLP is based on some simple Concepts:
●
Principle
●
Target
●
Statement
●
Conjunction of Principles
●
Quotation
●
Authority
Mapping Java to ABLP
Principles: Code is Signed using a PKI.
Targets: The resource we wish to protect. For every
target we create a dummy principle whose name
is identical to the target. This Dummy target do
not make any statements themselves, but various
principles speak for them.
Setting Policy: Standard access matrix is
implemented with with hash-tables to keep track
of which principals have permission to access
which targets.
Mapping Java to ABLP
Stacks: When a Java program is executing, we
treat each stack frame as a principal.
Starting a Program: When a program starts, we need to
set the security context of the initial stack frame
Enabling Privileges: If a stack frame F calls
BeginPrivilege(T) for some target T, it is really saying it
authorizes access to the target.
Calling a Procedure: When a stack frame F makes a
procedure call, this creates a new stack frame G.
Mapping Java to ABLP
Checking Privileges: Before making a system call
or otherwise invoking a dangerous operation, the
Java virtual machine calls CheckPrivilege() to
make sure that the requested operation is
authorized.
THEOREM 1: Termination. The check decision procedure always
terminates.
●
THEOREM 2: Soundness. If the check decision procedure returns
true when invoked in stack frame F, then there exists a proof in
ABLP logic that EF Ok(T).
●
THEOREM 3: (Equivalence to Stack Inspection). The check
decision procedure is equivalent to the Java stack inspection
●
algorithm.
Mapping Java to ABLP
Extensions to the Model: There are a number of
cases in which Java implementations differ from
the model we have described. These are minor
differences with no effect on the strength of the
model.
Groups.
Threads.
Enabling a Privilege.
Disabling a Privilege.
Frame Credentials. Java implementations do not treat stack frames
or their code as separate principals.
Improved Implementation
The model can improve the performance in two
ways.
By showing the evolution of security contexts
can be represented by a deterministic pushdown
automaton; this opens up a variety of efficient
implementation techniques.
Security-passing style, an efficient and
convenient integration of the pushdown
automaton with the state of the program.
Security Passing Style
In security passing style the security state is tracked
using JVM. (In other implementations an additional
security subsystem looks into the implementation.)
In Security passing style an implicit argument is added
to every procedure. The argument is a pointer to the
finite space of the automation. This eliminates the need
to have a separate push down stack for security
contexts or maintain stack annotations on the existing
run-time stack.
The main advantage of security-passing style is that once a
program has been rewritten into SPS, it no longer needs any special
security functionality from the JVM.
●
Security-passing style allows us to express the stack inspection
model within the existing semantics of the Java language
●
Implementing Security Passing Style
Rewriting Java Bytecodes
Stack inspection was originally implemented by
adding support for it in the runtime system. These
extensions required changing the stack frame
representation, which in turn affected the garbage
collector and JIT compiler.
With SPS conversion, we can express the stackinspection security architecture in vanilla Java
bytecodes (or source). Every method has an extra
parameter for passing the security context, but this
parameter and its representation are just Java.
Issues in Implementation of SPS
Native Methods:
Java programs can call native methods
(functions not written in Java) that might then call back to Java
methods. We cannot apply SPS conversion within the native
methods. Instead, when calling from Java to native, we store the
security context s into a per-thread global variable; when calling
from native back to Java we fetch as the security context for the
Java code.
Reflection:
Ideally, the security-passing transformation should
not be visible in any way to an application. The Java reflection API
allows a program to learn how many parameters each of its methods
takes; since SPS conversion introduces extra arguments. Thus
needs reconstruction of reflection api and is still not supported by
SAFKASI.
Issues in Implementation of SPS
Bootstrapping: This code is written in Java therefore proved
to be a problem for running with SPS therefore Bootstrapping code
is written in 3 stages:
Classes involved in the very beginning of bootstrapping the
runtime were identified by hand and added to a list of classes that
are not modified by the SPS converter.
SPS-converted classes begin execution but the SPS runtime itself
is not yet initialized. A dummy security context, later sub-classed
to implement the real security context, is created.
Finally, when real security contexts are available, the
application s main routine can be invoked with a proper security
context and execution continues normally.
Issues in Implementation of SPS
●
Consistency and Inheritance:
●
Portability:
●
Production vs. prototype implementations:
To run the SPS
converted code in various environments requires assessing which
classes need to be handled specially. To solve this problem of
inconsistency a rule has been made that if a class is SPS
converted then all classes that implement that interface also need
to be SPS converted.
Running SPS-converted code in a different Java
environment would require assessing which classes need to be
handled specially. But on the whole porting this code on any
machine is possible with minimum changes.
Our
prototype implementation makes a number of simplifying
assumptions that would not be acceptable in a production system.
Question?
●
Is there any way a Program can implement
security to disable access to a client / resource
without using the facilities of Java?