Wed 4:30pm, May 22, 2013 Stata, G882 |
Talk: A Decade of OS Access-Control Extensibility Speaker: Dr. Robert N. M. Watson, University of Cambridge Abstract: To discuss operating-system security is to marvel at the diversity of deployed access-control models: Unix and Windows NT multiuser security, Type Enforcement in SELinux, anti-malware products, app sandboxing in Apple OS X, Apple iOS, and Google Android, and application-facing systems such as Capsicum in FreeBSD. This diversity is the result of a stunning transition from the narrow 1990s Unix and NT status quo to security localization—the adaptation of operating-system security models to site-local or product-specific requirements. This transition was motivated by three changes: the advent of ubiquitous Internet connectivity; a migration from dedicated embedded operating systems to general-purpose ones in search of more sophisticated software stacks; and widespread movement from multiuser computing toward single-user devices with complex application models. The transition was facilitated by extensible access-control frameworks, which allow operating-system kernels to be more easily adapted to new security requirements. One such extensible kernel reference-monitor framework is the TrustedBSD MAC (Mandatory Access Control) Framework, developed beginning in 2000 and shipped in the open source FreeBSD operating system in 2003. This talk first discusses the context and challenges for access-control extensibility and high-level framework design, then turns to practical experience deploying security policies in several framework-based products, including FreeBSD, nCircle appliances, Juniper's Junos, and Apple's OS X and iOS. While extensibility was key to each of these projects, they motivated considerable changes to the framework itself, so the talk also explores how the framework did (and did not) meet each product's requirements, and finally reflects on the continuing evolution of operating-system security. Bio: Dr Robert N. M. Watson is a Senior Research Associate in the Security Research Group at the University of Cambridge Computer Laboratory. He lead a cross-layer research team spanning computer architecture, compilers, program analysis, operating systems, networking, and security; his recent contributions include work in hybrid capability systems and extensible access control. Prior to his PhD at the Computer Laboratory, Dr Watson was a Senior Research Scientist at McAfee Research, where he developed the kernel access control framework now used in many open-source and commercial products including FreeBSD, iOS, Mac OS X, and Junos. He is a member of the board of directors of the FreeBSD Foundation, and has been an active contributor to the open-source FreeBSD operating system in the areas of security, networking, and release engineering since the late 1990s. |
Wed 4pm, May 1, 2013 Stata, G882 |
Talk: Bitcoin's Security, Inside and Out Speaker: Gavin Andresen, Bitcoin Foundation, Chief Scientist Abstract: Bitcoin is the world's first decentralized digital currency, and the first widely used crypto-currency. It is also an open source software project and an open, peer-to-peer payment network. Bitcoin's security model is different from traditional payment networks, where typically transactions are communicated between trusted entities over secure communication channels. The security model for users of Bitcoin is also different from other electronic payment solutions, with the responsibility for keeping funds secure shifted from a third-party like a bank to the users themselves. In this talk I will follow a bitcoin transaction as it makes its way from one person to another, describing exactly what happens and what the security implications are at each step of the way. I will also briefly describe ongoing work to make Bitcoin transactions more secure and convenient. Bio: Gavin Andresen is Chief Scientist of the Bitcoin Foundation. He took over from Satoshi Nakamoto as lead developer for the Bitcoin project two years ago. Gavin started his career at Silicon Graphics writing 3D graphics software. He lives in Amherst, MA with his wife and two children. |
Wed 4pm, April 3, 2013 Stata, G575 |
Talk: Verification with Small and Short Worlds Speaker: Prof. Sanjit A. Seshia, UC Berkeley This is joint work with Rohit Sinha, Cynthia Sturton, Petros Maniatis, and David Wagner. Abstract: We consider the verification of safety properties in systems with large arrays and data structures. Such systems are common at the low levels of software stacks; examples are hypervisors and CPU emulators. The very large data structures in such systems (e.g., address-translation tables and other caches) make automated verification based on straightforward state-space exploration infeasible. We present S2W, a new abstraction-based model-checking methodology to facilitate automated verification of such systems. As a first step, inductive invariant checking is performed. If that fails, we compute an abstraction of the original system by precisely modeling only a subset of state variables while allowing the rest of the state to evolve arbitrarily at each step. This subset of the state constitutes a "small world" hypothesis, and is extracted from the property. Finally, we verify the safety property on the abstract model using bounded model checking. We ensure the verification is sound by first computing a bound on the reachability diameter of the abstract model. For this computation, we developed a set of heuristics that we term the "short world" approach. We present several case studies, including verification of the address translation logic in the Bochs x86 emulator, and verification of security properties of several hypervisor models. Bio: Sanjit A. Seshia is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley, currently on sabbatical at MIT. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and synthetic biology. His Ph.D. thesis work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a widely-used textbook on embedded systems. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE) from the White House, an Alfred P. Sloan Research Fellowship, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University. |
Wed 4pm, March 20, 2013 Stata, G575 |
Talk: Language Interoperability without Sacrificing Safety Speaker: Dr. David Chisnall, University of Cambridge, UK Abstract: The advantages of high-level type-safe languages are hard to deny. They are useful to eliminate entire categories of potential bugs, many of which can lead to security vulnerabilities. Unfortunately, very few programs are written entirely in such a language and even the ones that are, typically run in environments that are not. The Oracle JVM, for example, has been described as the most complex and convoluted piece of C++ code in existence, yet the safety properties of the Java language depend upon its correctness. More commonly, they will use some native libraries, typically written in C or C++. The bridging overhead of such approaches often leads to some parts of a program that are not performance critical being written in low-level languages. In extreme (yet sadly common) cases, an entire application ends up being written in C or C++ simply because it wants to use a library written in one of these languages. This talk will discuss ways of minimising the bridging overhead between languages and the ongoing work on the CHERI architecture, developed by Cambridge and SRI. CHERI is a 64-bit MIPS compatible processor with a capability coprocessor, enforcing fine-grained permissions on memory accesses. This can be used for relatively coarse-grained sandboxing, for example isolating a library in a very lightweight processes, and for enforcing object-granularity isolation. Bio: David Chisnall completed his PhD in 2007 and promptly left academia for a few years. During this time, he wrote four books, the first on the internals of the Xen Hypervisor, two more about Objective-C and the most recent on the new Go programming language from Google. He consulted for a variety of organisations on compiler and language runtime design issues ranging from high-level dynamic languages to GPGPU optimisation. His open source work includes having written the Objective-C runtime used by GNUstep and deployed in millions of Android devices running ports of iOS applications and the C++ runtime library shipped with FreeBSD 9.1. He also maintains the associated compiler support in the clang compiler. His interests in language interoperability began during his PhD and his explorations of this have involved the creation of the LanguageKit framework, which allows implementing high-level languages that share an underlying object model with Objective-C, as well as a Smalltalk front end. He returned to academia just under a year ago, attached to the CRASH/CTSRD project at the University of Cambridge, where he now works on preserving safety properties of high-level languages in the presence of code written in low-level languages by sinking the safety guarantees into the hardware. |
Tue 4pm, March 19, 2013 Stata, G575 |
Talk: Measuring Side Channel Vulnerability using SVF Speaker: Prof. Simha Sethumadhavan, Columbia University Abstract: There have been many attacks that exploit side-effects of program execution to expose secret information, and many proposed countermeasures to protect against these attacks. However there is currently no systematic, holistic methodology for understanding information leakage. As a result, it is not well known how design decisions affect information leakage or the vulnerability of systems to side-channel attacks. In this talk, I will describe a metric for measuring information leakage called the Side-channel Vulnerability Factor (SVF). SVF is based on our observation that all side-channel attacks ranging from physical to microarchitectural to software rely on recognizing leaked execution patterns. SVF quantifies patterns in attackers’ observations and measures their correlation to the victim’s actual execution patterns and in doing so captures systems’ vulnerability to side-channel attacks. In a detailed case study of on-chip memory systems, I will show how SVF measurements help expose unexpected vulnerabilities in whole-system designs and shows how designers can make performance-security trade-offs. SVF provides a quantitative approach to secure computer architecture. Time permitting I will also mention the SPARCHS hardware security project at Columbia. URL: ISCA'12 paper |
Wed 4pm, March 13, 2013 Stata, G575 |
Talk: Time-Optimal Interactive Proofs for Circuit Evaluation Speaker: Justin Thaler, Harvard University Abstract: A potential problem in outsourcing work to commercial cloud computing services is trust. If we store a large data set with a service provider, and ask them to perform a computation on that data set -- for example, to compute the shortest path between two vertices in a large graph -- how can we know the computation was performed correctly? Obviously we don't want to compute the result ourselves, and we might not even be able to store all the data locally. Surprisingly powerful protocols for verifying outsourced computations were discovered within the computer science theory community several decades ago, in the form of interactive proofs and their brethren. However, until recently these protocols were considered theoretical curiosities, far too inefficient for actual deployment. In this talk, I will describe research efforts that have sought to overturn this point of view. These efforts have revisited some of the most powerful protocols in the theory literature and drastically improved their efficiency. We complement the theory with implementations demonstrating that practical general-purpose interactive proofs may be right around the corner. Bio: Justin Thaler is currently finishing his PhD at Harvard University. His research focuses on algorithms for massive data sets, verifiable computation, and computational learning theory. |
Monday 4pm, February 11, 2013 Stata, G575 |
Talk: Building a Secure Foundation for Mobile Apps Speaker: Haohui Mai, University of Illinois at Urbana-Champaign Abstract: Security for applications running on mobile devices is important. In this talk we present ExpressOS, a new OS for enabling high-assurance apps to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our use of formal methods for proving key security invariants about our implementation. In our use of formal methods, we focus solely on proving that our OS implements our security invariants correctly, rather than striving for full functional correctness, requiring significantly less verification effort while still proving the security relevant aspects of our system. We built ExpressOS and tested its performance. Our evaluation shows that the performance of ExpressOS is comparable to an Android-based system. In one test, we ran the same web browser on Rach and on an Android-based system and found that ExpressOS adds 30% overhead on average to the page load latency time for nine popular web sites. Bio: Haohui Mai is a fifth-year Ph.D. student in University of Illinois, at Urbana-Champaign, advised by Sam King. He is interested in improving the security and reliability of real-world computer system. |
Monday 4pm, December 10, 2012 Stata, G575 |
Talk: Binary Static Analysis Speaker: Chris Eng, Veracode - industry talk Abstract: Binary Static Analysis is the process of modeling the semantics of a computer program from its executable form and then inspecting that model for properties and patterns of interest. Today static analysis if being used for detecting quality and security flaws in software. This talk will give an overview of the binary modeling process, the inspection process, and some examples of security defects that can be detected with this technique. Bio: Chris Eng is Vice President of Research at Veracode, where he helps define and implement the static and dynamic analysis capabilities of Veracode’s service offerings. He is a frequent speaker at industry conferences such as BlackHat, RSA, OWASP, and CanSecWest, and has presented on a diverse set of application security topics including cryptographic attacks, testing methodologies, mobile application security, and security metrics. Chris’ professional experience includes stints at Symantec, @stake, and the US Department of Defense, where he specialized in software security assessments, penetration testing, and vulnerability research. URL: Full length bio at http://www.veracode.com/about/chris-eng.html. |
Monday 4pm, December 3, 2012 Stata, G575 |
Talk: Mining Your Ps and Qs: Detection of Widespread Weak Keys in Network Devices Speaker: Dr. Nadia Heninger, Microsoft Research, New England Joint work with Zakir Durumeric, Eric Wustrow, and J. Alex Halderman. Abstract: RSA and DSA can fail catastrophically when used with malfunctioning random number generators, but the extent to which these problems arise in practice has never been comprehensively studied at Internet scale. We perform the largest ever network survey of TLS and SSH servers and present evidence that vulnerable keys are surprisingly widespread. We find that 0.75% of TLS certificates share keys due to insufficient entropy during key generation, and we suspect that another 1.70% come from the same faulty implementations and may be susceptible to compromise. Even more alarmingly, we are able to obtain RSA private keys for 0.50% of TLS hosts and 0.03% of SSH hosts, because their public keys shared nontrivial common factors due to entropy problems, and DSA private keys for 1.03% of SSH hosts, because of insufficient signature randomness. We cluster and investigate the vulnerable hosts, finding that the vast majority appear to be headless or embedded devices. In experiments with three software components commonly used by these devices, we are able to reproduce the vulnerabilities and identify specific software behaviors that induce them, including a boot-time entropy hole in the Linux random number generator. Finally, we suggest defenses and draw lessons for developers, users, and the security community. Bio: Nadia Heninger is a postdoctoral visiting researcher at Microsoft Research New England. Last year she was an NSF mathematical sciences postdoctoral fellow at UC San Diego. She finished her PhD in 2011 at Princeton. |
Monday 4pm, November 26, 2012 Stata, G575 |
Talk: Automating End User Security Tasks Speaker: Eunsuk Kang, MIT This is joint work with Prof. Daniel Jackson in CSAIL. Abstract: Many systems continue to fail due to vulnerabilities that are well-understood by the security community. This is perhaps not surprising, since most users who configure and use these systems have little or no background in security, with a vague sense of what information should be protected, and how to go about doing so. I will describe an approach to building tools that can help users avoid common security mistakes. The key part of our approach is a set of declarative models that encode domain-specific knowledge about different types of vulnerabilities and their effects on the system. An underlying analysis engine leverages the information in these models to check the system against a user-specified policy, generating concrete feedback if a violation is detected. I will describe some applications of our approach (including web servers, routers, social networks), and a case study where we analyzed configuration of web sites in CSAIL for security vulnerabilities. |
Monday 4pm, November 19, 2012 Stata Center, D463 (Star) |
Talk: Making proof-based verified computation almost practical Speaker: Prof. Mike Walfish, UT Austin Abstract: How can a machine specify a computation to another one and then, without executing the computation, check that the other machine carried it out correctly? And how can this be done without assumptions about the performer (replication, trusted hardware, etc.) or restrictions on the computation? This is the problem of _verified computation_, and it is motivated by the cloud and other third-party computing models. It has long been known that (1) this problem can be solved in theory using probabilistically checkable proofs (PCPs) coupled with cryptographic tools, and (2) the performance of these solutions is wildly impractical (trillions of CPU-years or more to verify simple computations). I will describe a project at UT Austin that challenges the second piece of this folklore. We have developed an interactive protocol that begins with an efficient argument [IKO CCC '07] and incorporates new theoretical work to improve performance by 20+ orders of magnitude. In addition, we have broadened the computational model from Boolean circuits to a general-purpose model. We have fully implemented the system, accelerated it with GPUs, and developed a compiler that transforms computations expressed in a high-level language to executables that implement the protocol entities. The resulting system, while not quite ready for the big leagues, is close enough to practicality to suggest that in the near future, PCPs could be a real tool for building actual systems. Talk will be based on these papers and ongoing work: http://www.cs.utexas.edu/~mwalfish/papers/ginger-usec12.pdf http://www.cs.utexas.edu/~mwalfish/papers/pepper-ndss12.pdf Bio: Michael Walfish is an assistant professor in the Computer Science Department at The University of Texas at Austin. His research interests are in systems, security, and networking. His honors include an Air Force Young Investigator Award, an NSF CAREER Award, a Sloan Research Fellowship, a Teaching Excellence Award from the UT College of Natural Sciences, the Intel Early Career Faculty Honor Program, and the UT Society for Teaching Excellence. He received his B.A. from Harvard and his Ph.D. from MIT, both in Computer Science. |
Monday 4pm, November 5, 2012 Stata, G575 |
Talk: Breaks in the Cloud Speaker: Dr. Ari Juels, Chief Scientist, RSA, the Security Division of EMC This talk is based on papers published at ACM CCS '12 and SoCC '12, and is joint work with Yinqian Zhang and Mike Reiter (UNC), Ben Farley, Venkatanathan Varadarajan, Tom Ristenpart, and Mike Swift (Univ. of Wisconsin), and Kevin Bowers (RSA). Abstract: One appeal of cloud computing is the simple abstraction layer it presents to tenants--in the case of IaaS, of homogeneously resourced, isolated virtual machines. In reality, breakdowns in such abstractions create opportunities for tenant abuse. I'll describe two potential vulnerabilities of public clouds in this talk: (1) A cross-VM side-channel attack that permits attacker exfiltration of cryptographic keys from a victim VM and (2) A "placement gaming" scheme that enables a tenant to harvest higher-value resources than those otherwise assigned by the cloud provider, potentially at the expense of co-tenants. Bio: Dr. Ari Juels is Chief Scientist of RSA, The Security Division of EMC, and Director of RSA Laboratories. He works to bring sparks of invention and insight from RSA's scientists and affiliates to the company at large and advises on the science behind RSA’s technology strategy and vision. He joined RSA in 1996. Ari's dozens of research publications span a range of topics, including biometric security, RFID security and privacy, electronic voting, browser security, combinatorial optimization, and denial-of-service protection. Ari has served as the program chair or co-chair for a number of conferences and workshops, and is a frequent invited speaker at industry events. In 2004, MIT's Technology Review Magazine named Dr. Juels one of the world's top 100 technology innovators under the age of 35. Computerworld honored him in its "40 Under 40" list in 2007. |
Monday 4pm, October 22, 2012 Stata, G575 |
Talk: TARDIS: Time and Remanence Decay in SRAM to Implement Secure Protocols on Embedded Devices without Clocks Speaker: Amir Rahmati, UMass Amherst Joint work with Mastooreh Salajegheh, Dan Holcomb, Jacob Sorber, Wayne P. Burleson, and Kevin Fu. Abstract: Lack of a locally trustworthy clock makes security protocols challenging to implement on batteryless embedded devices such as contact smartcards, contactless smartcards, and RFID tags. A device that knows how much time has elapsed between queries from an untrusted reader could better protect against attacks that depend on the existence of a rate-unlimited encryption oracle. The TARDIS (Time and Remanence Decay in SRAM) helps locally maintain a sense of time elapsed without power and without special-purpose hardware. The TARDIS software computes the expiration state of a timer by analyzing the decay of existing on-chip SRAM. The TARDIS enables coarse-grained, hourglass-like timers such that cryptographic software can more deliberately decide how to throttle its response rate. Our experiments demonstrate that the TARDIS can measure time ranging from seconds to several hours depending on hardware parameters. Key challenges to implementing a practical TARDIS include compensating for temperature and handling variation across hardware. Our contributions are (1) the algorithmic building blocks for computing elapsed time from SRAM decay; (2) characterizing TARDIS behavior under different tempera- tures, capacitors, SRAM sizes, and chips; and (3) three proof-of-concept implementations that use the TARDIS to enable privacy-preserving RFID tags, to deter double swiping of contactless credit cards, and to increase the difficulty of brute-force attacks against e-passports. |
Monday 4pm, October 1, 2012 Stata, G575 |
Talk: Techniques for performing secure computation on encrypted data Speaker: Chris Fletcher, MIT Joint work with Marten van Dijk and Srini Devadas. Abstract: Privacy of data is a huge problem in cloud computing, and more generally in outsourcing computation. From financial information to medical records, sensitive data is stored and computed upon in the cloud. Computation requires the data to be exposed to the cloud servers, which may be attacked by malicious applications, hypervisors, operating systems or insiders. In the ideal scenario, no one other than the user sees the private data in decrypted form, as is achieved through the use of fully homomorphic encryption (FHE) techniques. The first part of the talk will focus on (a) techniques to run general purpose programs under FHE and (b) how some programs are naturally better suited for FHE than others. I will talk about the how ambiguity in program control flow and data structures leads to large overheads for certain programs, in addition to the crypto overheads already imposed by FHE (which impose about a billion times slowdown). Motivated by large FHE overheads, the rest of the talk describes two schemes that approximate FHE with a minimal trusted computing base (TCB) made out of secure hardware. The first scheme's TCB is a simple hardware unit (an ALU, plus commodity encrypt/decrypt logic) that performs arithmetic operations faster than FHE but still suffers from the program/data ambiguity problem. To address the ambiguity problem, the second scheme's TCB is a secure processor that uses oblivious RAM techniques (to obfuscate external requests) and specialized circuits (to obfuscate internal behavior). Surprisingly, this secure processor incurs only a ~5X performance overhead. In both schemes, no software (the user application, server operating system, etc) or anything outside the hardware unit (external RAM or communication channels) is trusted. |
Monday 4pm, September 24, 2012 Stata, G575 |
Talk: Improving integer security for systems Speaker: Xi Wang, MIT Abstract: Integer errors have emerged as a threat to systems security, because they allow exploits such as buffer overflow and privilege escalation. We present KINT, a static analysis tool that detects integer errors in C programs. KINT generates predicates from source code and user annotations, and feeds them into a constraint solver for deciding whether an integer error is possible. KINT identified more than 100 integer errors in the Linux kernel, the lighttpd web server, and OpenSSH, which were confirmed and fixed by the developers. Based on the experience with KINT, we further propose a new integer family with NaN semantics to help developers avoid integer errors in C programs. |
Monday 4pm, September 17, 2012 Stata, G575 |
Talk: RockSalt: Better, Faster, Stronger Software Fault Isolation for the x86 Speaker: Prof. Greg Morrisett, Harvard University Joint work with Gang Tan (Lehigh), Jean-Baptiste Tristan (Oracle Labs), Joe Tassarotti, and Edward Gan (Harvard). Abstract: Software-based fault isolation (SFI), as used in Google's Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures variable length instructions such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google's original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level verification tasks. |
Monday 4pm, May 7, 2012 Stata, G575 |
Talk: Jeeves, a Language for Enforcing Privacy Speaker: Jean Yang, MIT Abstract: It is becoming increasingly important for applications to protect sensitive data. With current techniques, the programmer bears the burden of ensuring that the application’s behavior adheres to policies about where sensitive values may flow. Unfortunately, privacy policies are difficult to manage because their global nature requires coordinated reasoning and enforcement. To address this problem, we describe a programming model that makes the system responsible for ensuring adherence to privacy policies. The programming model has two components: 1) core programs describing functionality independent of privacy concerns and 2) declarative, decentralized policies controlling how sensitive values are disclosed. Each sensitive value encapsulates multiple views; policies describe which views are allowed based on the output context. The system is responsible for automatically ensuring that outputs are consistent with the policies. We have implemented this programming model in a new functional constraint language named Jeeves. In Jeeves, sensitive values are introduced as symbolic variables and policies correspond to constraints that are resolved at output channels. We have implemented Jeeves as a Scala library using an SMT solver as a model finder. In this talk I describe the Jeeves programming language and our experience using Jeeves to implement a conference management system. Bio: Jean Yang is a Ph.D. student at MIT working with Armando Solar-Lezama. She graduated from Harvard University in 2008 in Computer Science. She received the Best Paper Award at PLDI in 2010 for her paper "Safe to the Last Instruction: Automated Verification of a Type-Safe Operation System" with Chris Hawblitzel of Microsoft Research. She is a recipient of the NSF Graduate Research Fellowship and of the Facebook Fellowship. |
Monday 4pm, April 23, 2012 Stata, G575 |
Talk: Concealing Access Patterns to Cloud Storage for Privacy Speaker: Emil Stefanov, Berkeley Abstract: Encryption is not always enough to ensure privacy. If adversaries can observe your access patterns to encrypted storage, they can still learn sensitive information about what your applications are doing. These types of attackers are especially troubling as cloud storage becomes increasingly popular. Oblivious RAM (O-RAM) protocols solve this problem by continuously shuffling storage as it is being accessed; thereby completely hiding what data is being accessed and even when it was previously accessed. Until now, Oblivious RAM algorithms have mostly been a theoretical interest. We take an important step forward in making Oblivious RAM practical. We designed an O-RAM protocol that is 63 times less bandwidth consuming than the best existing scheme for the exact same amount of allocated local storage. To achieve this improvement, we propose several novel techniques for constructing Oblivious RAMs: specifically, we describe a secure algorithm to obliviously evict blocks from an array of client-side caches into randomly assigned server-side partitions on the storage server. We also describe a secure method for concurrently shuffling and reading data to drastically reduce the worst-case cost per operation. |
Monday *3*pm, April 9, 2012 Stata, G575 |
Talk: Keys and Clouds: Searching for the Equilibrium Speaker: Robert Griffin, RSA, Security Division of EMC Abstract: As enterprises look to move their production workloads into the public and hybrid clouds, encryption is increasingly important tool for ensuring the confidentiality and integrity of their data. But what happens with the keys? Does the enterprise continue to maintain sole control of them? Do they entrust the keys to the cloud service provider? What are the technical alternatives and what are the risks that the different alternatives entail? This discussion explores these alternatives and then looks at what game theory can say about the pros and cons of these alternatives. In particular, we'll look at whether there are Nash equilibriums that yield unexpected insights into strategies for the relationship of keys and clouds. Bio: Bob Griffin is Chief Security Architect at RSA, the Security Division of EMC, where he is responsible for technical architecture, standards and strategy, particularly for RSA’s data security products. He represents EMC to several standards organization, including as co-chair of the OASIS Key Management Interoperability Protocol (KMIP) technical committee. Bob has extensive experience in security strategy, corporate governance, business process transformation and software development. He has had the primary architectural responsibility for a number of production systems environments and for major software engineering projects at RSA, Entrust and Digital Equipment Corporation. He is a frequently requested speaker for professional and industry conferences and has instructed courses within both professional and university settings. |
Monday *4*pm, April 2, 2012 Stata, G575 |
Talk: New approaches to securing cloud data Speaker: Dr. Alina Oprea, RSA Labs Abstract: Despite many economical benefits of cloud computing for both tenants and cloud providers, public clouds are still not widely adopted, especially within the enterprise setting. The main reason is that existing cloud infrastructures are prone to security risks, due to many different types of failures (e.g., hardware failures, software bugs, power outages, server mis-configuration) that easily unfold at such large scale. I will talk about some of the research RSA Laboratories has done on extending the trust perimeter from the enterprise data center into public clouds. We have developed cryptographic techniques for providing data integrity, protection of sensitive workloads and enhancing data availability in the cloud. I will also describe in more detail a file system called Iris that offers strong integrity protection for data migrated to the cloud. Bio: Alina Oprea is a Principal Research Scientist at RSA Laboratories, the security division of EMC. Her research interests span multiple areas in computer and communications security including applied cryptography, storage security, security in distributed systems, and malware detection. More recently, her research has focused on providing strong assurances to cloud computing users about handling of their data and computation. She is the recipient of the 2011 TR35 award for her research in cloud security. |
Monday *4*pm, February 27, 2012 Stata, G575 |
Talk: Privacy and Integrity in the Untrusted Cloud Speaker: Ariel J. Feldman, Princeton Abstract: For a myriad of user-facing applications from word processing and calendaring to social networking, cloud deployment is becoming increasingly popular. Cloud services are attractive because they offer availability, reliability, global accessibility, and convenience that desktop applications cannot match. Unfortunately, these benefits come at the cost of having to trust the service provider with the confidentiality and integrity of one’s data. Private data stored with cloud providers could be leaked to malicious outsiders and insiders or turned over to government agencies, potentially without warrants. Furthermore, a malicious or compromised cloud provider could corrupt users’ data or even equivocate, showing different users divergent views of the system’s state. In this talk, I will present two systems that make it possible to benefit from a centralized cloud provider without having to trust it with the privacy and integrity of users’ data. In both systems, the provider’s servers see only encrypted data and cannot deviate from correct execution without detection. The first system, SPORC, allows concurrent, low-latency editing of shared state, permits disconnected operation, and supports dynamic access control even in the presence of concurrency. The second, Frientegrity, provides strong defenses against server equivocation as well as dynamic access control that scale to the demands of a large social networking service. Both of these systems explore what is possible when the confidentiality and integrity of users’ data depends on the security of their own cryptographic keys, and not on a service provider’s good intentions. Bio: Ariel J. Feldman is a Ph.D. candidate in computer science at Princeton University whose research focuses on systems security and applied cryptography. His recent work has been aimed at developing practical cloud-based systems that protect the confidentiality and integrity of users’ data by design rather than through promises and legal contracts. Previously, he has worked on improving the security of electronic voting systems and disk encryption. |
Monday 3pm, February 13, 2012 Stata, G575 |
Talk: Recent advances in homomorphic encryption Speaker: Dr. Shai Halevi, IBM T. J. Watson Research Center Abstract: In this talk I plan to give a survey of the state-of-the-art in constructions of fully-homomorphic encryption (FHE), with emphasis on efficiency considerations. The talk is meant as mostly a high-level overview, and should be accessible without much prior knowledge. I will begin with a general-purpose introduction to the promise of FHE, and the challenges involved in making the current constructions practical. Then I will mention the recent advances of Brakerski- Vaikuntanathan and Brakerski-Gentry-Vaikuntanathan [BV11b,BGV12], and talk about the direction of exploiting parallelism, which is due to Smart and Vercauteren [SV11]. In the last part of the talk I will cover at a more technical level some of the techniques from the Gentry-Halevi-Smart work that achieves FHE with only poly-logarithmic overhead [GHS12]. [SV11] N.P. Smart and F. Vercauteren: Fully homomorphic SIMD operations. Manuscript, 2011. [BV11b] Z. Brakerski and V. Vaikuntanathan: Efficient fully homomorphic encryption from (standard) LWE. In FOCS 2011. [BGV12] Z. Brakerski, C. Gentry, and V. Vaikuntanathan: Fully homomorphic encryption without bootstrapping. In ITCS 2012. [GHS12] C. Gentry, S. Halevi, and N.P. Smart: Fully homomorphic encryption with polylog overhead. In Eurocrypt 2012 Bio: Shai's webpage is here. |
Monday 3pm, January 30, 2012 Stata, G575 |
Talk: The Case for Prefetching and Prevalidating TLS Server Certificates Speaker: Emily Stark, MIT Joint work with Lin-Shung Huang, Dinesh Israni, Collin Jackson, and Dan Boneh. Abstract: A key bottleneck in a full TLS handshake is the need to fetch and validate the server certificate before a secure connection can be established. We propose a mechanism by which a browser can prefetch and prevalidate server certificates so that by the time the user clicks on an HTTPS link, the server's certificate is immediately ready to be used to set up a TLS session. Combining this with a recent proposal called Snap Start reduces the TLS handshake to zero round trips so that an HTTP request can be sent over HTTPS immediately upon request. Prefetching and prevalidating certificates improves web security by making it less costly for websites to enable TLS and by removing time pressure from the certificate validation process. We study the effects of four different prefetching strategies on server performance, and we present results from a study of a popular certificate validation mechanism called OCSP. The OCSP data collected, which is of independent interest, enabled us to evaluate the effectiveness of prefetching and prevalidating in reducing TLS handshake latency. In some cases we show a factor of four speed-up over the existing full TLS handshake. |
Monday 3pm, January 23, 2012 Stata, G575 |
Talk: Verifying Keyword and Database Search in the Cloud Speaker: Nikos Triandopoulos - RSA Labs & Boston University Joint work with Charalampos Papamanthou and Roberto Tamassia. Abstract: Verifying the correctness of outsourced computations on remotely stored data will be an essential operation for fully trustworthy cloud services in the future. Such verification will need to be practical, though: It can’t rely on substantial tenant-side computation or extra cloud storage. For instance, when a user searches remotely archived e-mail, it would be desirable for her to be able to check---in a cryptographically strong sense, e.g., via digital signatures and/or SHA-1 checksums---that the returned result is correct. A correct result in this case contains all e-mail messages that correspond to the user’s query, without omissions. Such verification isn’t available in cloud systems today because existing known techniques are impractical: They could generate proofs as large as the entire e-mail repository! We present a new technique for the verification of outsourced computations that involve set operations. For a large class of searches over a collection of sets, our technique allows for substantially more efficient verification protocols: Search results can be publicly verified using optimally compact cryptographic proofs, proportional in size to the returned results. We also discuss important applications of our work, including: (1) Keyword searches over the inverted index of a collection of documents and (2) Equi-join queries over relational database tables. For instance, basic conjunctive or disjunctive keyword searches over e-mail as well as basic SQL queries over outsourced databases can be verified by tenants in an optimal manner. |
Monday 3pm, December 19, 2011 Stata, G575 |
Talk: Focused Threat Response and Forensic Information Sharing: Current Challenges and Limits in Cloud Computing Scenarios Speaker: Dr. Dennis Moreau, EMC Corporation Abstract: Consumer and enterprise concerns over cloud information security, especially in the face of increasing focused threat (APT) activity, continue to rank as driving inhibitors to cloud technology adoption. In response, regulatory authorities are asserting increasing requirements for increased transparency and increased attestation that can adversely impact asset utilization and provider operational costs (PCI Supplemental Virtualization Guidance 2011, revised European Data Protection Directive 2011, the FedRamp initiative ...). Yet none of the specific requirements of these regulatory efforts is likely to improve cloud security against focused threats. Effective response to focused threats in cloud computing scenarios is a particularly thorny problem for a number of reasons. Focused threats may:
Bio: Dennis is a Senior Technology Strategist in the Office of the CTO at RSA, specializing in Security, Attestation and Trust in Virtual and Cloud-based Computing. He works actively with the National Institute of Standards and Technology (NIST), the U.S. Department of Defense (DoD) and the Mitre Corporation on the development of security information standards and guidance. Dennis has over 35 years of experience in designing and implementing system management and security infrastructures. Prior to joining RSA, Dennis was a founder and the Chief Technology Officer for Configuresoft, a compliance technology now in the VMWare portfolio. He was also the CTO for Baylor College of Medicine (BCM). He holds a doctorate in Computer Science and has held faculty positions in Computational Medicine and Computer Science. He speaks regularly at IT management and security conferences worldwide. |
Monday 4pm, December 12, 2011 Stata, G575 |
Talk: Regaining Control Over Cloud and Mobile Data Speaker: Prof. Roxana Geambasu, Columbia University Abstract: Emerging technologies, such as cloud and mobile computing, offer previously unimaginable global access to data; however, they also threaten our ability to control the use of our data, its lifetime, accessibility, privacy, management properties, etc. My research focuses on restoring to users control they've ceded to the cloud and mobile devices. In this talk I will describe two examples of this work. First, I'll present Keypad, an auditing file system for theft- and loss-prone mobile devices that permits users to track and control accesses on their mobile data, even after a device has been stolen. Second, I'll describe Vanish, a global-scale distributed-trust system that allows users to cause all copies of desired Web data objects, online or offline, to simultaneously self destruct at a specified time. A common thread of these efforts is the integration of systems and crypto techniques to solve new problems in data management brought on by technological change. Bio: Roxana Geambasu is an Assistant Professor in the Computer Science Department at Columbia University. Her interests span broad areas of systems research, including cloud and mobile computing, operating systems, file systems, and databases, with a focus on security and privacy. She obtained her Ph.D. from the University of Washington in August 2011 and her B.S. in Computer Science from the Polytechnic University of Bucharest in 2005. She was the recipient of the first Google Fellowship in Cloud Computing in 2009. URL: Roxana's homepage is here. |
Monday 3pm, November 28, 2011 Stata, G575 |
Talk: Web Security via Types and Theorem-Proving in the Ur/Web Programming Language Speaker: Prof. Adam Chlipala, MIT Abstract: Web security vulnerabilities are predictable enough to make it possible to create lists like OWASP's Top 10, which describes 10 broad categories of vulnerability that cover most real-world problems. If we have such a clear idea of what Web developers are doing wrong, why aren't existing tools doing much to help? In this talk, I will describe a clean-slate solution based on a new programming language. Mainstream languages tend to suffer from the "everything is a string" design philosophy, where key pieces of Web applications (e.g., HTML and SQL code) are manipulated as strings, such that the programming language implementation can't help the programmer understand the consequences of his code. The Ur/Web language starts from an expressive type system and encodes the key pieces of Web applications as richly typed libraries, such that the compiler is able to do sound program analysis to rule out 6 of OWASP's Top 10 vulnerabilities. Some of the guarantees require programmers to write specifications, but these can assume the relatively accessible form of SQL queries that "select allowable behaviors." I'll touch on three key design elements in the Ur/Web language that promote security. First, as key pieces of applications are first-class, these pieces may be encapsulated inside modules, with strong guarantees about the inability of most application code to interfere with the operation of security kernels. Second, an expressive type system allows correct-by-construction, injection-attack-proof generation of code in key languages like HTML and SQL, and this static typing need not come at the cost of abandoning today's Web programmers' favorite productivity-boosting features, like generative metaprogramming (i.e., parameterized code generators). Finally, more application-specific access control and information flow policies may be checked soundly in terms of simple declarative policies written in SQL, a language most Web developers are already comfortable with. URL: Homepage http://adam.chlipala.net/. |
Monday 4pm, November 21, 2011 Stata, 32-D463 (Star) |
Talk: Inference of Expressive Information Security Policies Speaker: Prof. Stephen Chong, Harvard University This is joint work with Jeff Vaughan at UCLA. Abstract: Many computer systems store and manipulate sensitive data. Programming language techniques can ensure that the computer systems handle this information correctly. However, current techniques for language-based information security can be difficult to use, requiring the programmer to invest considerable effort before receiving any information security guarantees. We explore the inference of expressive human-readable information security policies as a step towards providing practical tools and techniques for strong language-based information security. We focus on inference, as opposed to specification, to reduce the burden on the programmer. We define a novel security policy language that can express _what_ information a program may release, under what conditions (or, _when_) such release may occur, and which procedures are involved with the release (or, _where_ in the code the release occur). We've implemented a dataflow analysis for precisely inferring these policies for Java programs. Bio: Stephen Chong is an Assistant Professor of Computer Science in the Harvard School of Engineering and Applied Sciences. Steve's research focuses on programming languages, information security, and the intersection of these two areas. He received a PhD from Cornell University, and a bachelor's degree from Victoria University of Wellington, New Zealand. URL: http://people.seas.harvard.edu/~chong/ |
Monday 3pm, November 14, 2011 Stata, G575 |
Talk: Verifying and Enforcing Network Paths with ICING Speaker: Dr. Jad Naous, MIT Joint work with Michael Walfish, Antonio Nicolosi, David Mazières, Michael Miller, and Arun Seehra. Abstract: There has been much recent work about how senders and receivers express policies about the paths that their packets take. For instance, a company might want fine-grained control over which providers carry which traffic between its branch offices, or a receiver may want traffic sent to it to travel through an intrusion detection service. While the ability to express policies has been well-studied, the ability to enforce policies has not. The core challenge is: if we assume an adversarial, decentralized, and high-speed environment, then when a packet arrives at a node, how can the node be sure that the packet followed an approved path? Our solution, ICING, incorporates an optimized cryptographic construction that is compact, and requires negligible configuration state and no PKI. We demonstrate ICING's plausibility with a NetFPGA hardware implementation. At 93% more costly than an IP router on the same platform, its cost is significant but affordable. As far as we know, this is the first system that can verify that packets have followed their network paths at a reasonable cost. URL: http://yuba.stanford.edu/~jnaous/papers/icing-conext-2011.pdf |
Monday 3pm, October 31, 2011 Stata, G575 |
Talk: How to Tell if Your Cloud Files are Vulnerable to Drive Crashes Speaker: Kevin Bowers, RSA Labs Joint work with Marten van Dijk, Ari Juels, Alina Oprea and Ronald L. Rivest. Abstract: Much work has been done in verifying properties of remotely stored data. Adding to that list, we show that it is possible to verify that data is stored redundantly across hard drives and thus resilient to hard drive failures. This testing can be done remotely and is efficient both in communication and computation time. I will discuss our Remote Assessment of Fault Tolerance (RAFT) protocol, its uses and limitations. Bio: Kevin Bowers is a Senior Research Scientist at RSA Laboratories, the Security Division of EMC. His research interests include user authentication, cryptographic protocols and usable security. Kevin holds a B.S. in Electrical, Computer and Systems Engineering and Computer Science, and a B.S. in Mathematics, both from Rensselaer Polytechnic Institute as well as an M.S. in Computer Science from Carnegie Mellon University. Kevin joined RSA Labs in 2007 and currently provides technical leadership for the Advanced Development team as well as proof-of-concept support and practical implementation expertise for RSA Labs. Kevin's publication history covers many diverse topics including numerous cryptographic protocols for remote verification of integrity and resilience, time stamping, as well as advanced authentication techniques, and steganography. URL: http://www.rsa.com/rsalabs/node.asp?id=3402 |
Monday, 3pm, October 17, 2011 |
Talk: CryptDB: Protecting Confidentiality with Encrypted Query Processing Speaker: Raluca Ada Popa, MIT Joint work with Catherine M. S. Redfield, Nickolai Zeldovich, and Hari Balakrishnan. Abstract: Online applications are vulnerable to theft of sensitive information because adversaries can exploit software bugs to gain access to private data, and because curious or malicious administrators may capture and leak data. CryptDB is a system that provides practical and provable confidentiality in the face of these attacks for applications backed by SQL databases. It works by executing SQL queries over encrypted data using a collection of efficient SQL-aware encryption schemes. CryptDB can also chain encryption keys to user passwords, so that a data item can be decrypted only by using the password of one of the users with access to that data. As a result, a database administrator never gets access to decrypted data, and even if all servers are compromised, an adversary cannot decrypt the data of any user who is not logged in. An analysis of a trace of 126 million SQL queries from a production MySQL server shows that CryptDB can support operations over encrypted data for 99.5% of the 128,840 columns seen in the trace. Our evaluation shows that CryptDB has low overhead, reducing throughput by 14.5% for phpBB, a web forum application, and by 26% for queries from TPC-C, compared to unmodified MySQL. Chaining encryption keys to user passwords requires 11-13 unique schema annotations to secure more than 20 sensitive fields and 2-7 lines of source code changes for three multi-user web applications. Bio: Raluca is a second year graduate student at MIT. Here is her website. |
Monday, 3pm, October 3, 2011 |
Talk: RePriv: Re-Imagining Content Personalization and In-Browser Privacy Speaker: Dr. Ben Livshits, Microsoft Research, Redmond Abstract: RePriv is a browser-based technology that allows for Web personalization, while controlling the release of private information within the browser. We demonstrate how to perform mining of core user interests within a browser. We propose a protocol on top of HTTP that can be used to seamlessly integrate RePriv with existing Web infrastructure and also show how pluggable miners can be used to extract more detailed information and how to check these third-party miners for privacy leaks. We show that RePriv's default in-browser mining can be done with no noticeable overhead to normal browsing, and that the results it produces converge quickly. We then go on to show similar results for each of our case studies: that RePriv enables high-quality personalization, and that the performance impact each case has on the browser is minimal. We conclude that personalized content and individual privacy on the Web are not mutually exclusive. Bio: Ben Livshits is a researcher at Microsoft Research in Redmond, WA and an affiliate professor at the University of Washington. Originally from St. Petersburg, Russia, he received a bachelor's degree in Computer Science and Math from Cornell University in 1999, and his M.S. and Ph.D. in Computer Science from Stanford University in 2002 and 2006, respectively. Dr. Livshits' research interests include application of sophisticated static and dynamic analysis techniques to finding errors in programs. Ben has published papers at PLDI, Oakland Security, Usenix Security, CCS, SOSP, ICSE, FSE, and many other venues. He is known for his work in software reliability and especially tools to improve software security, with a primary focus on approaches to finding buffer overruns in C programs and a variety of security vulnerabilities (cross-site scripting, SQL injections, etc.) in Web-based applications. He is the author of several dozen academic papers and patents. Lately he has been focusing on how Web 2.0 application and browser reliability, performance, and security can be improved through a combination of static and runtime techniques. Ben generally does not speak of himself in the third person. URL: http://research.microsoft.com/en-us/um/people/livshits/default.aspx |
Thursday, 4pm, August 4, 2011 |
Talk: Cloud Computing and Software Security Speaker: Dr. Úlfar Erlingsson, security researcher at Google Abstract: Software-as-a-service can provide great benefits, such as ubiquitous, reliable access to data, but cloud computing also raises new challenges and opportunities for computer security. Large-scale Web services must address both traditional security concerns, such as user authentication and key management, as well as newer issues like those raised by the need to maintain users' privacy. At the same time, cloud computing has innate security advantages, such as its use of easily updated and malleable software, which enables instrumentation ranging from individual specialization to large-scale execution summarization. This talk will briefly outline some of these issues and potential research topics in cloud security, with examples from Google's past and current technology efforts used to give context. Bio: Úlfar Erlingsson leads efforts in security research at Google. Previously, he has been a researcher at Microsoft Research, an Associate Professor at Reykjavik University, Iceland, and led security technology at two startups: GreenBorder and deCODE Genetics. He holds a PhD in CS from Cornell. |
Thursday, 4pm, April 14, 2011 |
Talk: HomeAlone: Co-Residency Detection in the Cloud via Side-Channel Analysis Speaker: Dr. Alina Oprea, RSA Labs Joint work with Y. Zhang, A. Juels, and M. K. Reiter Abstract: Security is a major barrier to enterprise adoption of cloud computing. Physical co-residency with other tenants poses a particular risk, due to pervasive virtualization in the cloud. Recent research has shown how side channels in shared hardware may enable attackers to exfiltrate sensitive data across virtual machines (VMs). In view of such risks, cloud providers may promise physically isolated resources to select tenants, but a challenge remains: Tenants still need to be able to verify physical isolation of their VMs. I will talk about HomeAlone, a system that lets a tenant verify its VMs' exclusive use of a physical machine. The key idea in HomeAlone is to invert the usual application of side channels. Rather than exploiting a side channel as a vector of attack, HomeAlone uses a side-channel (in the L2 memory cache) as a novel, defensive detection tool. By analyzing cache usage during periods in which "friendly" VMs coordinate to avoid portions of the cache, a tenant using HomeAlone can detect the activity of a co-resident "foe" VM. Key technical contributions of HomeAlone include classification techniques to analyze cache usage and guest operating system kernel modifications that minimize the performance impact of friendly VMs sidestepping monitored cache portions. HomeAlone requires no modification of existing hypervisors and no special action or cooperation by the cloud provider. |
Thursday, 4pm, April 7, 2011 |
Talk: Sequential Aggregate Signatures with Lazy Verification for S-BGP Speaker: Prof. Leonid Reyzin, Boston University Joint work with Sharon Goldberg and Kyle Brogle Abstract: Sequential aggregate signature schemes allow n signers, in order, to sign a message each, at a lower total cost than the cost of n individual signatures. We present a sequential aggregate signature scheme based on trapdoor permutations (such as RSA) that, unlike prior such proposals, does not require a signer to verify the received aggregate before adding a signature on a new message to it. In fact, a signer need not even know the public keys of the other signers. Our scheme is especially designed for Secure BGP (S-BGP), a protocol designed for securing the global Internet routing system. With S-BGP, routers digitally sign the routing announcements they forward to other routers. Because routing announcements are sent in a chain along a route, aggregating multiple signatures to reduce the total signature length is a natural way to reduce communication costs. Practical implementations of S-BGP must offer routers the option of performing "lazy verification": that is, to add their own signature to an unverified aggregate and forward it immediately, postponing verification until load permits or the necessary public keys are obtained. However, many prior schemes do not allow for lazy verification; indeed, adding a signature to an unverified aggregate breaks the security guarantees, and can lead to devastating attacks. Our scheme explicitly allows for lazy verification. We report a technical analysis of the scheme (which is provably secure in the random oracle model), a detailed implementation-level specification, and implementation results based on RSA and OpenSSL. Our scheme has much shorter signatures than nonaggregate RSA (with the same sign and verify times) and two orders of magnitude faster verification than nonaggregate ECDSA, although ECDSA has shorter signatures when the number of signers is small. |
Thursday 4pm, Feb 24, 2011 |
Talk: Let the Market Drive Deployment: A Strategy for Transitioning to BGP Security Speaker: Prof. Sharon Goldberg, Boston University Joint work with Phillipa Gill and Michael Schapira. Abstract:
With
a cryptographic root-of-trust for Internet routing (RPKI) on the
horizon, we can finally start planning the deployment of one of the
secure interdomain routing protocols proposed over a decade ago (Secure
BGP, secure origin BGP). However, if experience with IPv6 is any
indicator, this will be no easy task. Security concerns alone seem
unlikely to provide sufficient local incentive to drive the deployment
process forward. Worse yet, the security benefits provided by the S*BGP
protocols do not even kick in until a large number of ASes have
deployed them.
Instead, we appeal to ISPs' interest in increasing revenue-generating traffic. We propose a strategy that governments and industry groups can use to harness ISPs' local business objectives and drive global S*BGP deployment. We evaluate our deployment strategy using theoretical analysis and large-scale simulations on empirical data. Our results give evidence that the market dynamics created by our proposal can transition the majority of the Internet to S*BGP. Relevant URL: http://www.cs.bu.edu/~goldbe/papers/sbgpTrans.html |
Wednesday 4pm, Nov 3, 2010 |
Talk: Privacy Integrated Queries: A Programming Language for Differentially-Private Computation Speaker: Dr. Frank McSherry, Microsoft Research Abstract: Large volumes of sensitive
data are currently collected by
an array of
agencies, companies, and other organizations. While these data clearly
hold great potential for analysis, they can also reflect sensitive
information about their participants. Scientists have struggled with
the tension between extracting valuable statistical information from
these datasets without accidentally disclosing specifics of individual
records.
A recent privacy criterion, differential privacy, formally constrains
the disclosure of specifics of individual records, without precluding
the release of statistical information. Differential privacy requires
that the outcome of a computation be almost as likely with and without
any one record; to each participant, the analysis behaves as if it did
not have access to the participant's data.
While differential privacy is very strong, its use to date has been
restricted to privacy experts; a small collection of highly-trained
individuals who, no matter how motivated, are not able to satisfy the
enormous volume of the world's data analysis needs. To this end, we
have assembled a programming language in which any program provides
differential privacy, without requiring an expert privacy analysis. The
language is almost identical to LINQ, a SQL-like extension to C#, and
is readily useable by analysts with only a modest background in
programming. We will discuss the design, implementation, and
application of this language across a variety of data analysis
contexts.
Bio: Frank McSherry is a researcher at Microsoft Research's Silicon Valley lab. His research focus is on large scale data analysis, with a recent focus on issues of privacy and confidentiality. In particular, he helped to develop the recent definition of Differential Privacy, and designed and implemented the Privacy Integrated Queries data analysis platform providing these guarantees. Relevant URL: http://research.microsoft.com/en-us/people/mcsherry/ |
Thursday 4pm, Oct 28, 2010 |
Talk: Fabric: Using language-based security to build secure distributed systems Speaker: Prof. Andrew Myers, Cornell University Abstract:
Computation and persistent storage are rapidly moving into the
distributed domain. Yet we are offered very weak security and privacy
assurance, especially as complex information systems share information
across trust boundaries. Fabric aims to improve this situation by
implementing a higher-level abstraction for building complex
distributed information systems securely and composably.
Fabric is a decentralized system that allows heterogeneous network nodes to securely share both information and computation resources despite mutual distrust. Its Java-like object model is extended with data resources labeled with confidentiality and integrity policies, enforced by a combination of compile-time and run-time mechanisms. Optimistic, nested transactions ensure consistency across all objects and nodes. A peer-to-peer dissemination layer helps to increase availability and to balance load. Results from applications built using Fabric suggest that Fabric has a clean, concise programming model, offers good performance, and enforces security. This talk will describe the current Fabric prototype and point to a few directions for further investigation. Bio: Andrew Myers is a Professor in the Computer Science Department at Cornell University in Ithaca, NY. He received his Ph.D. from MIT in 1999. He is a visiting professor at MIT during the 2010-2011 academic year and hopes to talk to lots of people while he is back here. His research interests include computer security and programming languages. He has been working most recently on language-based information flow security, language-based extensibility, secure web application frameworks, secure Internet voting, and distributed and persistent object systems. His awards include two best paper awards from SOSP and a most influential paper award from POPL. |
Friday 3pm, Oct 15, 2010 |
Talk: Quantification of Integrity Speaker: Dr. Michael Clarkson, Cornell University Abstract:
Methods for quantification of corruption (that is,
damage to information integrity) have received little attention
to date, whereas quantification of information leakage (damage to
confidentiality) has been a topic of research for over twenty years.
This talk introduces two kinds of integrity measures:
contamination and suppression. Contamination measures how much "bad"
information is present in outputs; it generalizes taint
analysis and is the dual of leakage. Suppression measures how
much "good" information is lost from outputs; it generalizes
program correctness but does not have a confidentiality dual.
Hence the classic duality between confidentiality and integrity
is incomplete. As a case study, database privacy conditions from
the literature, including differential privacy, are examined using
this theory of quantitative integrity and confidentiality.
|