Wednesday, July 7, 2004
5331 CS
11:30 AM - 12:30 PM
|
D.S. Wallach, A.W. Appel, E.W. Felten
Rice / Princeton / Princeton
SAFKASI: a security mechanism for language-based systems
TOSEM, Oct 2000
URL: http://doi.acm.org/10.1145/363516.363520
In order to run untrusted code in the same process
as trusted code, there must be a mechanism to allow
dangerous calls to determine if their caller is
authorized to exercise the privilege of using the
dangerous routine. Java systems have adopted a
technique called stack inspection to address this
concern. But its original definition, in terms of
searching stack frames, had an unclear relationship
to the actual achievement of security,
overconstrained the implementation of a Java system,
limited many desirable optimizations such as method
inlining and tail recursion, and generally
interfered with interprocedural optimization. We
present a new semantics for stack inspection based
on a belief logic and its implementation using the
calculus of security-passing style which addresses
the concerns of traditional stack inspection. With
security-passing style, we can efficiently represent
the security context for any method activation, and
we can build a new implementation strictly by
rewriting the Java bytecodes before they are loaded
by the system. No changes to the JVM or bytecode
semantics are necessary. With a combination of
static analysis and runtime optimizations, our
prototype implementation showes reasonable
performance (although traditional stack inspection
is still faster), and is easier to consider for
languages beyond Java. We call our system SAFKASI
(the Security Architecture Formerly Known as Stack
Inspection).
|
Wednesday, July 21, 2004
5331 CS
11:30 AM - 12:30 PM
|
B. Pinkas, T. Sander
HP Labs
Securing passwords against dictionary attacks
Published in CCS 2002
URL: http://doi.acm.org/10.1145/586110.586133
The use of passwords is a major point of
vulnerability in computer security, as passwords are
often easy to guess by automated programs running
dictionary attacks. Passwords remain the most widely
used authentication method despite their well-known
security weaknesses. User authentication is clearly
a practical problem. From the perspective of a
service provider this problem needs to be solved
within real-world constraints such as the available
hardware and software infrastructures. From a user's
perspective user-friendliness is a key
requirement.
In this paper we suggest a novel authentication
scheme that preserves the advantages of conventional
password authentication, while simultaneously
raising the costs of online dictionary attacks by
orders of magnitude. The proposed scheme is easy to
implement and overcomes some of the difficulties of
previously suggested methods of improving the
security of user authentication schemes.
Our key idea is to efficiently combine traditional
password authentication with a challenge that is
very easy to answer by human users, but is (almost)
infeasible for automated programs attempting to run
dictionary attacks. This is done without affecting
the usability of the system. The proposed scheme
also provides better protection against denial of
service attacks against user accounts.
|
Wednesday, July 28, 2004
5331 CS
11:30 AM - 12:30 PM
|
S. Delaune, F. Jacquemard
France Télécom R&D / INRIA
A theory of dictionary attacks and its complexity
Published in CSFW 2004
URL: http://ieeexplore.ieee.org/iel5/9168/29101/01310728.pdf?isNumber=29101&prod=CNF&arnumber=1310728&arSt=+2&ared=+15&arAuthor=+Delaune%2C+S.%3B++Jacquemard%2C+F.
We consider the problem of automating proofs of
cryptographic protocols when some data, like poorly
chosen passwords, can be guessed by dictionary
attacks. First, we define a theory of these attacks:
we introduce an inference system modeling the
guessing capabilities of an intruder. This system
extends the classical Dolev-Yao rules. Using proof
rewriting techniques, we show a locality lemma for
our inference system which yields the
PTIME-completeness of the deduction problem.
This result is lifted to the simultaneous solving of
intruder deduction constraints with
variables. Constraint solving is the basis of a NP
algorithm for the protocol insecurity problem in the
presence of dictionary attacks, assuming a bounded
number of sessions. This extends the classical
NP-completeness result for the Dolev-Yao model.
We illustrate the procedure with examples of
published protocols. The model and decision
algorithm have been validated on some examples in a
prototype implementation.
|