Stanford Security Lunch
Winter 2010

Get announcements:

January 6 Organizational meeting

Organizational meeting: Sign up to give a talk!

January 13 Lightweight Static Capabilities

Speaker: Oleg Kiselyov (FNMOC)

Abstract: We demonstrate a lightweight notion of static capabilities that brings together increasingly expressive type systems and increasingly accessible program verification. Like many programmers, before verifying that our code is correct, we want to assure safety conditions: array indices remain within bounds; modular arithmetic operates on numbers with the same modulus; a file or database handle is used only while open; and so on. The safety conditions protect objects such as arrays, modular numbers, and files. Our overarching view is that a capability authorizes access to a protected object and simultaneously certifies that a safety condition holds. Rather than proposing a new language or system, we describe a modular programming style that harnesses modern type systems in existing languages to check capabilities at compile time and assure safety with minimal impact to run-time performance.

Our programming style has three ingredients:

  1. a compact kernel of trust that is specific to the problem domain;
  2. unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application;
  3. static (type) proxies for dynamic values.

We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell and OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for

  1. an expressive core language,
  2. higher-rank polymorphism, and
  3. phantom types.

Joint work with: Chung-chieh Shan (Rutgers)

January 20 Uri Nadav

Note: Our other speaker didn't show up, so Uri gave an ex tempore talk.

January 27 Cloud Computing Security

Speaker: Alex Stamos (iSEC)

Abstract: Cloud Computing has become an unstoppable trend in computing for both small innovative startups and large traditional enterprises, mostly due to the promise of reduced capital expenditures and the ability to increase capacity on demand. The security complications of a multitenant cloud computing environment have not been lost on potential customers; a recent survey shows that security is the #1 reason why companies don't use cloud computing. Are these concerns well founded or just artifacts of trying to fit cloud computing into the traditional ideas of IT security?

This talk will recap the current state of cloud computing security research, and use real life examples to demonstrate how customers of these technologies are failing to adapt their software and systems to the new reality. We will discuss the security benefits given up in a cloud computing environment, and some of the ways security assurance can be restored. We will also outline some of the gaping holes in security research in this field, and discuss the opportunities to solve some of these issues through academic work or new ventures.

February 3 Effectiveness of Black-Box Web Vuln Scanners

Abstract: Black-box web application vulnerability scanners are automated tools that probe web applications for security vulnerabilities. In order to assess the current state of the art, we obtained access to eight leading tools and carried out a study of:

  1. the class of vulnerabilities tested by these scanners
  2. their effectiveness against target vulnerabilities, and
  3. the relevance of the target vulnerabilities to vulnerabilities found in the wild.

To conduct our study we used a custom web application vulnerable to known and projected vulnerabilities, and previous versions of widely used web applications containing known vulnerabilities. Our results show the promise and effectiveness of automated tools, as a group, and also some limitations. In particular, "stored" forms of Cross Site Scripting (XSS) and SQL Injection (SQLI) vulnerabilities are not currently found by many tools.

Speaker: Jason Bau

February 10Virtualization, Clound Computing and Security

Speaker: Tal Garfinkel

Virtualization has been one of the most potent forces reshaping the landscape of systems software in the last 10 years and has become ubiquitous in the realm of enterprise compute infrastructure and in the emerging field of cloud computing. This presents a variety of new opportunities when designing host based security architectures. We present several paradigms for enhancing host security leveraging the new capabilities afforded by virtualization. First, we present a virtualization based approach to trusted computing. This allows multiple virtual hosts with different assurance levels to run concurrently on the same platform using a novel "open box" and "closed box" model that allows the virtualized platform to present the best properties of traditional open and closed platforms on a single physical platform. Next, we present virtual machine introspection, an approach to enhancing the attack resistance of intrusion detection and prevention systems by moving them "out of the box" i.e. out of the virtual host they are monitoring and into a seperate protection domain where they can inspect the host they are monitoring from a more protected vantage point. Finally, we present overshadow data protection, and approach for providing a last line of defense for application data even if the guest OS running an application has been compromised. We accomplish this by presenting two views of virtual memory, an encrypted view to the operating system and a plain text view to the application the owning that memory. This approach more generally illustrates the mechanisms necessary to introduce new orthogonal protection mechanisms into a Guest Operating system from the virtualization layer while maintaining backwards compatibility with existing operating systems and applications.

February 17 Pseudorandom Functions from Lattices

Speaker: Hart

February 24 Invisitype: Object-Oriented Security Policies

Speaker: Jiwon Seo

Abstract: Many modern software platforms today, including browsers, middleware server architectures, cell phone operating systems, web application engines, support third-party software extensions. This paper proposes InvisiType, an object-oriented approach that enables platform developers to efficiently enforce fine-grained safety checks on third-party extensions without requiring their cooperation. This allows us to harness the true power of third-party software by giving it access to sensitive data while ensuring that it does not leak data.

In this approach, a platform developer encapsulates all safety checks in a policy class and selectively subjects objects at risk to these policies. The runtime enforces these policies simply by changing the types of these objects dynamically. It uses the virtual method dispatch mechanism to substitute the original methods and operations with code laced with safety checks efficiently. The runtime hides the type changes from application code so the original code can run unmodified.

We have incorporated the notion of InvisiType into the Python language. We have applied the technique to 4 real-world Python web applications totaling 156,000 lines of code. InvisiType policies greatly enhance the security of the web applications, including MoinMoin, a popular, 94,000-line Wiki Engine. MoinMoin has a large number of third-party extensions, which makes security enforcement important. With less than 150 lines of Python code, we found 16 security bugs in MoinMoin. This represents a significant reduction in developers' effort from a previous proposal, Flume, which required 1,000 lines of C++ code and modifications to 1,000 lines of Python code.

Our InvisiType policies successfully found 19 cross-site scripting vulnerabilities and 6 access control errors in total. The overhead of applying the policies is less than 4 percent, indicating that the technique is practical.

March 3Lossy Trapdoor Functions

Speaker: David Freeman

"Lossy trapdoor functions," introduced by Peikert and Waters, are a cryptographic primitive that can be used in a black-box manner to construct cryptographic objects such as collision-resistant hash functions, oblivious transfer, and CCA-secure public-key encryption. I will discuss some new constructions of lossy trapdoor functions based on various number-theoretic assumptions, including the quadratic residuosity assumption and the decision Diffie-Hellman assumption.

Note: To appear at PKC 2010

Joint work with: O. Goldreich, E. Kiltz, A. Rosen and G. Segev

March 10 Andrea Bittau

March 17 No talk (Exams)