Formal aspects of mobile code security

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.