|
- Author
- Richard Drews Dean
- Abstract
-
We believe that formal methods of all kinds are critical to mobile
code security, as one route to gaining the assurance level necessary
for running potentially hostile code on a routine basis. We begin by
examining Java, and understanding the weaknesses in its architecture,
on both design and implementation levels. Identifying dynamic linking
as a key problem, we produce a formal model of linking, and prove
desirable properties about our model. This investigation leads to a
deep understanding of the underlying problem. Finally, we turn our
attention to cryptographic hash functions, and their analysis with
binary decision diagrams (BDDs). We show that three commonly used hash
functions (MD4, MD5, and SHA-1) do not offer ideal strength against
second preimages. The ability of a cryptographic hash function to
resist the finding of second preimages is critical for its use in
digital signature schemes: a second preimage enables the forgery of
digital signatures, which would undermine confidence in digitally
signed mobile code. Our results show that modern theorem provers and
BDD-based reasoning tools are effective for reasoning about some of
the key problems facing mobile code security today.
- Published
- PhD Dissertation, Princeton University, January 1999.
- Text
- GZip'ed Postscript (575k)
PDF (Adobe Acrobat) (479k)
|
|
