8:30 AM |
Check-in & Continental Breakfast |
|
9:00 AM |
Welcome & Security Lab Overview
Professor Dan Boneh |
|
9:15 AM |
Professor John Mitchell
Simulation-Based Security Conditions and Commitment
Bio:
John Mitchell studies computer security, including access control mechanisms, cryptographic protocols and mobile code security. Other research areas include programming languages, formal methods for software correctness and other application of logic to computer science. He received his PhD from MIT in 1984.
|
PDF |
9:45 AM |
Professor Dan Boneh
Collision Resistant Hashing---Will Composition Help?
Bio:
Dr. Boneh heads the applied crypto group at the Computer Science department at Stanford University. Dr. Boneh's research focuses on applications of cryptography to computer security. His work includes topics such as e-mail security, security for handheld devices, digital copyright protection, and cryptanalysis. He is a recipient of the Packard Award, the Alfred P. Sloan Award, and the Terman Award.
|
PDF |
10:15 AM |
Break |
|
10:30 AM |
Professor Dawson Engler
Automatically Generating Inputs of Death Using Symbolic Execution
Bio:
Dawson Engler’s main research interest is metacompilation (MC). MC allows programmers to add simple system-specific compiler extensions that automatically check or optimize their code. As an example, we wrote a number of extensions to find violations of operating system rules such as “system calls must check user pointers for validity before using them,” “disabled interrupts must be re-enabled,” and “to avoid deadlock, do not call a blocking function with interrupts disabled.” These extensions have found a couple thousand errors in Linux, OpenBSD, and the Xok exokernel and led to numerous kernel patches. Most extensions were less than a hundred lines of code and written by implementors who had a limited understanding of the systems checked. Dr. Engler’s research focuses both on building interesting software systems and on discovering and exploring the underlying principles of all systems. He received his Ph.D. from MIT in 1998.
|
PDF |
11:00 AM |
Martin Casado
Designing a SANE Protection Architecture for Enterprise Networks
Abstract:
Connectivity in enterprise networks is provided by technologies not designed to offer protection. As a response to growing security demands, network designers have attempted to retrofit access controls onto an otherwise permissive architecture using various interdiction mechanisms such as ACLs, packet filters, and other middleboxes. This has lead to enterprise networks that are inflexible, fragile, and difficult to manage.
To address these limitations, we offer Ethane, a backwards compatible network architecture where connectivity is restricted by default and only granted to senders on request. All routing and access control decisions are made by a logically-centralized server that grants access to services by explicitly setting up routes, according to declarative access control policies (e.g., "Alice can access http server foo"). Access controls are enforced at each switch, which are simple and only minimally trusted. Ethane offers strong attack resistance and containment in the face of compromise, yet is practical for everyday use.
Bio:
Martin Casado is a third-year PhD student in Computer Science and is a member of the high performance networking group. Prior to joining the Ph.D. program he worked at Lawrence Livermore National Laboratory as a computer scientist in the information operations and assurance group. His interests include secure network architecture design, network measurement and, coincidently, writing personal bios just like this one.
|
PDF |
11:30 AM |
Elizabeth Stinson
Host-based, Run-time Win32 Bot Detection
Abstract:
Malicious bots pose a serious threat from the perspective of network service providers, e-commerce sites, and home users. Bots are generally managed in an ongoing fashion via a command-and-control (C&C) network. We present a mechanism to detect execution of most parameterized bot commands for a variety of Win32 bots (including variants of Agobot, DSNXbot, g-sysbot, SDbot, and Spybot), each of which may implement any such command in a manner entirely independent from the others.
Our approach entails Win32 and native API function inter- position where certain functions are instrumented to provide one of: (1) taint instantiation, (2) taint propagation, and (3) checking for tainted input. We consider data received over the network to be tainted. When a tainted buffer is copied to another buffer, that destination buffer is transitively marked tainted. Finally, we define a small set of gate functions: those that perform critical tasks (process or file management, network interaction, etc.).
Since bot execution on a victim computer is tantamount to remote management of that computer, our approach entails detection of the following heuristic: are any of the arguments to gate functions tainted? We claim this heuristic holds generally for the execution of parameterized bot commands and is not exhibited by most benign programs.
Bio:
Liz Stinson is pursuing a Masters with Distinction in Research at Stanford and has been doing research under Professor Mitchell for the past year. She has a BA from Georgetown University and has completed extensive under- graduate work in Computer Science at Columbia University.
|
PDF |
12:00 PM |
Lunch |
|
1:30 PM |
Michael Martin
Guided Model Checking of Java Web Applications
Abstract:
It is generally held that static and dynamic program analyses have complementary advantages and disadvantages: static techniques are universal but lack precision, while dynamic techniques provide perfect precision while suffering from coverage problems. This paper presents a technique for applying model-checking techniques to ameliorate coverage problems for complex dynamic analyses on web applications.
The dynamic analysis we extend is the PQL matcher, a dynamic analysis that enforces design rules dealing with sequences of events associated with a set of related objects. We incorporate it into the Java PathFinder modelchecker, and then automatically generate harnesses to check web applications.
These harnesses are based on both the target application and the precise pattern being matched. Inputs are generated to systematically exercise the behavior of Java web applications. The application is also statically analyzed, both to prioritize which HTTP requests are most likely to give matches, and also to deduce sequences of requests that are likely to be relevant.
We have implemented these techniques, and applied it to web applications both that we were familiar with and that were new to us. With familiar applications, we successfully duplicated our earlier results, and enriched them by deducing specific inputs to trigger all matches. With unfamiliar applications, we discovered several bugs new to us.
Bio:
Michael Martin is a Ph.D. student working under Professor Monica Lam. His primary research interests are applications of and optimizations to program trace-based pattern matching. His goal is to, by searching for sequences of relevant events in the run of a program, verify the presence of beneficial properties, or the absence of vulnerabilities or other bugs. He is the primary designer and maintainer of the PQL pattern language, and has contributed to many other open-source projects.
|
PDF |
2:00 PM |
Collin Jackson
Client-side Defenses for Context-Aware Phishing and Transaction Generator Spyware
Abstract:
I will describe several client-side web authentication projects that are implemented as open source Firefox extensions. SafeCache and SafeHistory defend against context-aware phishing attacks by restricting the information your browser leaks about other sites you've been to. PwdHash produces site-specific passwords with a spoof-resistant user interface. SpyBlock takes PwdHash to the next level by protecting web passwords from malicious spyware and keyloggers. In addition, SpyBlock defends against other web threats such as session hijacking malware that generates malicious requests on behalf of the user.
Bio:
Collin Jackson is a second year Ph.D. student in the computer security group at Stanford University. His current research focuses on the design of usable systems for authentication of web servers and browser clients. He received a B.S. from Yale University in 2004, and in 2005 he helped develop an anti-phishing component for the Firefox web browser that is now available on Google Labs.
|
PDF |
2:30 PM |
Break |
|
2:45 PM |
Jinyuan Li
Secure Untrusted Data Repository (SUNDR)
Abstract:
SUNDR is a network file system designed to store data securely on untrusted servers. SUNDR lets clients detect any attempts at unauthorized file modification by malicious server operators or users.
SUNDR's protocol achieves a property called fork consistency, which guarantees that clients can detect any integrity or consistency failures as long as they see each other's file modifications. An implementation is described that performs comparably with NFS (sometimes better and sometimes worse), while offering significantly stronger security.
Bio:
Jinyuan Li is a ph.D. student at Computer Science Department, New York University. Currently he is a visiting researcher at Stanford University. His research interest is in security in operating systems and distributed systems.
|
PDF |
3:15 PM |
Craig Gentry
New Methods for Password Authenticated Key Exchange
Abstract:
Password authenticated key exchange (PAKE) allows users to generate a strong cryptographic key from a short shared password in such a way that an attacker cannot extract the password using an offline dictionary attack. Previous PAKE protocols all can be viewed as following a small number of fundamental approaches, and all are based on either the Diffie-Hellman or RSA assumptions. They are also covered by broadly-worded patents, and therefore are not widely used
In this talk, I'll discuss a PAKE protocol that is designed in a fundamentally different way. Apart from being of theoretical interest, this protocol (arguably) circumvents previous patents and is quite practical (based on experiments without our rudimentary implementation).
Bio:
Craig Gentry is a first year Ph.D. student working under Dan Boneh. His research tends towards the mathematical side of applied cryptography, both constructive (designing efficient and highly-functional cryptosystems) and destructive (cryptanalysis). From 2000 to 2005, he worked as a senior research engineer at DoCoMo USA Labs on the security and cryptography project. He received a J.D. from Harvard Law School in 1998 and a B.S. in mathematics from Duke University in 1995.
|
PDF |