An Infinite Pebble Game and Applications

We generalize the well-known pebble game to infinite dag's, and we use this generalization to give new and shorter proofs of results in different areas of computer science (as diverse as "logic of programs" and "formal language theory"). Our applications here include a proof of a theorem due to Salomaa, asserting the existence of a context-free language with infinite index, and a proof of a theorem due to Tiuryn and Erimbetov, asserting that unbounded memory increases the power of logics of programs. The original proofs by Salomaa, Tiuryn, and Erimbetov, are fairly technical. The proofs by Tiuryn and Erimbetov also involve advanced techniques of model theory, namely, back-and-forth constructions based on a variant of Ehrenfeucht-Fraisse games. By contrast, our proofs are not only shorter, but also elementary. All we need is essentially finite induction and, in the case of the Tiuryn-Erimbetov result, the compactness and completeness of first-order logic.

Deanonymizing Users of the SafeWeb Anonymizing Service

The SafeWeb anonymizing system has been lauded by the press and loved by its users; self-described as "the most widely used online privacy service in the world," it served over 3,000,000 page views per day at its peak. SafeWeb was designed to defeat content blocking by firewalls and to defeat Web server attempts to identify users, all without degrading Web site behavior or requiring users to install specialized software. In this article we describe how these fundamentally incompatible requirements were realized in SafeWeb's architecture, resulting in spectacular failure modes under simple JavaScript attacks. These exploits allow adversaries to turn SafeWeb into a weapon against its users, inflicting more damage on them than would have been possible if they had never relied on SafeWeb technology. By bringing these problems to light, we hope to remind readers of the chasm that continues to separate popular and technical notions of security.