Stanford Security Lunch
Fall 2009

Get announcements:

September 23 Organizational meeting

Organizational meeting: Sign up to give a talk!

September 30 Keith

October 7 Zero-knowledge sets and related constructions

Speaker: Mike

Abstract: We begin with an abstraction of a secure DNS system. A dealer has a finite map M from strings to strings. He wishes to set up an agent (a secure DNS server) which can sign statements of the form "M(x) = y" or "M(z) is undefined".

We would like two security properties:

We explore three solutions to this problem:

Joint work with: Dan Boneh

October 11 Party at John's house

October 14 Gemalto round-table discussion

Abstract: Representatives from Gemalto will be visiting for a round-table discussion of security research. Topics include:

October 21 Understanding CAPTCHA security

Speaker: Elie Bursztein

Abstract: CAPTCHAs are used to tell real users apart from bots. They currently our first, last and only line of defense against automatic action on the web. Over the last few years, building CAPTCHA schemes and breaking them has become part of the security field; however we still have a limited understanding of the CAPTCHA security model. Our overall goal is to be able to design a security metric that will allow us to understand what assets a given CAPTCHA scheme can protect. The key questions that we need to answer to reach this goal are:

In this talk I will present our plan to answer these questions and what we have so far. In particular I will present on the defensive side what I think can be used as a security metrics based on our experience in breaking CAPTCHAs. On the offensive side, I will present how we used machine learning techniques to break eBay's audio CAPTCHAs (WOOT 09), and if I am done by then, how we used them to break a famous visual CAPTCHA.

October 28 DNSSEC

Speaker: Jason

Abstract: Domain Name System Security Extensions (DNSSEC) with Hashed Authenticated Denial of Existence (NSEC3) is a protocol slated for adoption by important parts of the DNS hierarchy, including the root zone, as a solution to DNS security vulnerabilities such as “cache-poisoning” attacks. We study the security goals and operations of DNSSEC/NSEC3 to analyze its security guarantees and shortcomings. In addition to limitations stated in the DNSSEC RFCs, such as the insecure "last-hop" channel, by checking DNSSEC/NSEC3 security properties using a finite-state enumeration tool, we uncover several more weaknesses in the DNSSEC protocol, including incorrect temporal dependencies in the DNSSEC signature attestation chain and NSEC3 options that allow a forged name to be inserted into a DNSSEC domain. We then demonstrate the exploitability of the NSEC3 vulnerability by using it to carry out a browser cookie-stealing attack on a laboratory DNSSEC domain.

On the plus side, we were able to demonstrate that a signed address (A) resource record with a full signature chain to a trust anchor cannot be spoofed by modeled network attackers short of signature compromise. To conclude, we state the implementation and configuration requirements which minimize the exploitability of the DNSSEC system.

November 4 Hristo

Abstract: Hristo will talk about his on-going work on adding address space layout randomization (ASLR) to the Google Android platform. The talk will cover the motivation, constraints, and current approach to solving the problem, as well as a perspective on Android platform work gained from mostly reading the code.

Joint work with: Dan Boneh and the Android team

November 11 Protocol Composition Logic

Speaker: Stephan

Abstract: I present a thoroughly revamped version of Protocol Composition Logic (PCL). PCL is formalized in the framework of universal order-sorted algebra, that is, universal algebra with subtyping. With respect to the previous version of PCL, many bugs, underspecification issues, and redundancies were fixed. In addition, PCL now has an unambiguous semantics that would in principle allow someone to implement it and feed it to a theorem prover. My GenMsg (generable messages) and DolevYao (Dolev-Yao closure) definitions are inspired by Paulson's analz and synth operators. Finally, my presentation is meant to be an easy-to-understand introduction to the formalism of the new PCL.

November 18 Object Capabilities and Mashups

Speaker: Ankur

Abstract: When a web site combines active content (applications) from untrusted sources, it is important to protect each untrusted application from the others. The object-capability model provides an appealing approach: if separate applications are provided disjoint capabilities, a sound object-capability framework will prevent untrusted applications from interfering with each other. However, in developing language-based foundations for isolation proofs based on object-capabilities, we identify a more general notion of authority safety that also implies resource isolation. After proving that capability safety implies authority safety, we consider three example languages and show the applicability of our framework. Perhaps surprisingly, although we prove that one JavaScript subset based on Google Caja is capability safe, a more expressive subset of JavaScript is actually authority safe and therefore suitable for isolating untrusted applications.

November 25 No talk (Thanksgiving)

December 2 Andrea

December 9 No talk (Exams)