NOV
29
2017
TALK A Universally Composable Treatment of Network Time.
Speaker | AANCHAL MALHOTRA  Boston University Location | Stata, D463 (Star) Time | Wed 4pm
Abstract
The security of almost any real-world distributed system today depends on the participants having some "reasonably accurate'' sense of current real time. Indeed, to name one example, the very authenticity of practically any communication on the Internet today hinges on the ability of the parties to accurately detect revocation of certificates, or expiration of passwords or shared keys. However, as recent attacks show, the standard protocols for determining time are subvertible, resulting in wide-spread security loss. Worse yet, we do not have security notions for network time protocols that (a) can be rigorously asserted and (b) rigorously guarantee security of applications that require a sense of real time.

In this talk I will:
  • Describe new notions of security for time sync protocols within Universally Composable (UC) security framework
  • Show that these notions suffice for protocols that need real time and Prove security of protocols that realize these notions


Joint work with Ran Canetti, Kyle Hogan and Mayank Varia.
Bio
Aanchal Malhotra is a Ph.D student at Boston University and is part of the BU Security Group. Her research uses cryptography, and the insights gained from network measurement and simulations to improve the security and reliability of core Internet protocols like BGP, DNS, and NTP. She received her M.S. from Boston University in 2014, and has worked as a researcher at Cisco, Akamai, and NLNet Labs, Netherlands. She is an active member of working groups at the Internet Engineering Task Force (IETF).
OCT
25
2017
TALK Algorand: Scaling Byzantine Agreements for Cryptocurrencies
Speaker | YOSSI GILAD  MIT CSAIL and Boston University Location | Stata, G449 Time | Wed 4pm
Abstract
Algorand is a new cryptocurrency that confirms transactions with latency on the order of a minute while scaling to many users. Algorand ensures that users never have divergent views of confirmed transactions, even if some of the users are malicious and the network is temporarily partitioned. In contrast, existing cryptocurrencies allow for temporary forks and therefore require a long time, on the order of an hour, to confirm transactions with high confidence.

Algorand uses a new Byzantine Agreement (BA) protocol to reach consensus among users on the next set of transactions. To scale the consensus to many users, Algorand uses a novel mechanism based on Verifiable Random Functions that allows users to privately check whether they are selected to participate in the BA to agree on the next set of transactions, and to include a proof of their selection in their network messages. In Algorand’s BA protocol, users do not keep any private state except for their private keys, which allows Algorand to replace participants immediately after they send a message. This mitigates targeted attacks on chosen participants after their identity is revealed.

We implement Algorand and evaluate its performance on 1,000 EC2 virtual machines, simulating up to 500,000 users. Experimental results show that Algorand confirms transactions in under a minute, achieves 125× Bitcoin’s throughput, and incurs almost no penalty for scaling to more users.
Bio
Yossi Gilad is a postdoctoral researcher at MIT and Boston University. His research interests include designing, building, and analyzing secure and scalable networked systems. Prior to this position he was a postdoctoral researcher at the Hebrew University of Jerusalem, and a research staff member at IBM Research. He is a recipient of the IETF/IRTF Applied Networking Research Prize (2017), the IBM Research Inventor Recognition Award (2015), and the Check Point Institute Information Security Prize (2013-2014).
OCT
18
2017
TALK Behavioral Intrusion Detection at Scale: Case Studies in Machine Learning
Speaker | JOSEPH ZADEH  JASK Location | Stata, D407 Time | Wed 4pm
Abstract
Intrusion detection at scale is one of the most challenging problems a modern enterprise will face while maintaining a global IT infrastructure. Building defensive systems that help automate some of the pain points, in this space, has been a goal since the early days of enterprise security. From an artificial intelligence standpoint, the problem of designing a model to predict adversarial behavior is part of a class of problems that is impossible to automate completely. At the core of the problem lies an underlying no-go principle: threat actors change tactics to evolve with the technological threat surface. This means that to build pattern recognition systems, for cyber defense, we have to design a solution that is capable of learning behaviors of the attackers and to programmatically evolve that learning over time.

In our presentation we outline a solution to this problem called the “The Lambda Defense”. The Lambda Defense is a tool for modeling any problem in which one is trying to automate the detection of attacks, over a complex threat surface (particular in the context of big data). We will highlight how we have applied this pattern to two important security use cases: Exploit Detection and Webshell Mitigation. The first use case is important for current trends because we have seen the delivery of both ransomware and banking Trojans, targeting fortune 500 customers using exploit kits. This malicious behavior can be captured as a prediction problem very easily, with the framework of the Lambda Defense. The second use case we highlight is the detection of webshells. This is important for the finding more stealthily and advanced actors that engage in long term attack campaigns. We will describe the way we have approached the mitigation of these two types of attacks, along with sharing some related open source data sets, and code that are meant to be standalone examples: https://github.com/jzadeh
Bio
Joseph Zadeh is the Director of Data Science at JASK. Zadeh has an M.S. in Mathematics, Computational Finance and a PhD in Mathematics from Purdue University. Zadeh comes to JASK as one of the foremost experts on AI and security operations. Prior to JASK, he served as Senior Data Scientist at Splunk through the aquisition of Caspida, where he developed behavior-based analytics for intrusion detection. He applied his research background to artificial intelligence and cybersecurity, delivering presentations, such as Multi-Contextual Threat Detection via Machine Learning at Bsides Las Vegas, Defcon, Blackhat and RSA. Previously, Zadeh was part of the data science consulting team on Cyber Security analytics at Greenplum/Pivotal, as well as part of Kaiser Permanente’s first Cyber Security R&D team.
OCT
11
2017
TALK Software Security Today: Understanding Code-Reuse Attacks and Reducing Attack Surface
Speaker | GEORGE PORTOKALIDIS  Stevens Institute of Technology Location | Stata, D407 Time | Wed 4pm
Abstract
Our society is increasingly reliant on software, so software security is of critical importance today more than ever. Through the years, defenses, such as address space layout randomization (ASLR), data-execution prevention (DEP), and stack and heap protections have significantly raised the bar for attackers, making software exploitation hard. However, attacks have also evolved to a new level of sophistication. Modern attacks combine multiple vulnerabilities to launch code-reuse attacks that “re-purpose” existing code to execute arbitrary computations. Working exploits are extremely valuable, for example, companies like Zerodium offer $1.5M for zero-day exploits against iOS. Modern attacks have reignited the interest in various instantiations of control-flow integrity (CFI), diversification, and isolation-based defenses. In this talk, I will present our work on evaluating the effectiveness of such defenses, based on analyzing them and producing proof-of-concept (PoC) attacks that expose their weaknesses. I will first focus on CFI to show that it is vulnerable, specially in its more practical iterations. I will then move to approaches that employ information hiding to emulate isolation techniques, and finish by looking at randomization techniques. I will conclude my talk by presenting new directions in hardening software and reducing attack surface.
Bio
Georgios Portokalidis is an Assistant Professor in the Department of Computer Science at Stevens Institute of Technology. He obtained his doctorate degree in Computer Science from Vrije Universiteit in Amsterdam. His research interests are mainly around the area of systems and security. Some of the subjects he is actively working on include the detection and prevention of state-of-the-art attacks against software systems, efficient information-flow tracking systems, user authentication, and IoT security.
SEP
27
2017
TALK A Brief History of Symbiote Defense
Speaker | SALVATORE J STOLFO  Columbia University Location | Stata, G882 Time | Wed 4pm
Abstract
Market watchers estimate the IoT Security marketplace is now valued at over $6 Billion and expected to reach $22 Billion by 2020. Just 5 years ago, embedded device security was barely on the map. Our early work in the IDS Lab at Columbia demonstrated the seriousness of the embedded device insecurity problem, and the relatively easy exploitation of devices such as printers, IP phones and routers. Recent advances in offensive technologies targeting a wide range of IoT devices have shown that the exploitation of these lucrative but poorly designed devices is not terribly difficult, including medical products, SCADA devices, automobiles and refrigerators. The goal of our early work was to defend embedded devices with an entirely new defensive capability we call the Software Symbiote, a host-based defensive technology that automatically injects intrusion detection functionality within the firmware of any device. In this talk we will provide a brief history of our work on the Symbiote technology, and the transition from academic research to practical and wide-spread use in common commodity products.
Bio
Salvatore Stolfo is a Professor of Computer Science at Columbia University. He is regarded as creating the area of machine learning applied to computer security in the mid-1990’s and has created several anomaly detection algorithms and systems addressing some of the hardest problems in securing computer systems. Of particular note is his recent interest in the practical application of deception security in scale. Stolfo is also co-inventor of the Symbiote technology that automatically injects intrusion detection functionality into arbitrary embedded devices. Stolfo has had numerous best papers and awards, most recently the RAID Most Influential Paper and Usenix Security Distinguished Paper awards. He has published well over 230 papers and has been granted over 60 patents and has been an advisor and consultant to government agencies, including DARPA, the National Academies and others, for well over 2 decades. Two security companies were recently spun out of his IDS lab, Allure Security Technology and Red Balloon Security.
MAY
10
2017
TALK Opaque: An Oblivious and Encrypted Distributed Analytics Platform
Speaker | RALUCA ADA POPA  Berkeley Location | Stata, G882 Time | Wed 4pm
Abstract
Many systems run rich data analytics on sensitive data in the cloud, but are prone to data breaches. A recent hardware enclave architecture promises data confidentiality and isolated execution of arbitrary computations, yet still suffers from leakage due to memory and network accesses patterns. In this talk, I will describe Opaque, a distributed data analytics platform supporting a wide range of queries while protecting the data. Even a compromised operating system sees only encrypted data. Opaque also protects against leakage from memory and network accesses outside of the enclave (a property called obliviousness). To accomplish this goal, Opaque introduces new distributed oblivious relational operators, as well as new query planning techniques to optimize these new operators. Opaque is implemented on Spark SQL with few changes to the underlying system. Opaque provides data encryption, authentication, and computation verification with a performance ranging from 52% faster to 3.3x slower than vanilla Spark SQL; obliviousness comes with a 1.6–46x overhead. At the same time, Opaque provides an improvement of three orders of magnitude over state-of-the-art oblivious protocols. Joint work with W. Zheng, A. Dave, J. G. Beekman, J. E. Gonzalez, and I. Stoica.
Bio
Raluca Ada Popa is an assistant professor of computer science at UC Berkeley working in computer security, systems, and applied cryptography. She is a co-director of the RISELab at UC Berkeley, as well as a co-founder and CTO of a cybersecurity startup called PreVeil. Raluca has received her PhD in computer science as well as her Masters and two BS degrees, in computer science and in mathematics, from MIT. She is the recipient of an Intel Early Career Faculty Honor award and a George M. Sprowls Award for best MIT CS doctoral thesis.
MAY
03
2017
TALK Iron: Functional Encryption using Intel SGX
Speaker | DHINAKARAN VINAYAGAMURTHY  University of Waterloo Location | Stata, G882 Time | Wed 4pm
Abstract
Ben A Fisch , Dhinakaran Vinayagamurthy , Dan Boneh , and Sergey Gorbunov

Functional encryption (FE) is an extremely powerful cryptographic mechanism that lets an authorized entity compute on encrypted data, and learn the results in the clear. However, all current cryptographic instantiations for general FE are too impractical to be implemented. We build Iron, a practical and usable FE system using Intel’s recent Software Guard Extensions (SGX). We show that Iron can be applied to complex functionalities, and even for simple functions, outperforms the best known cryptographic schemes. We argue security by modeling FE in the context of hardware elements, and prove that Iron satisfies the security model.
Bio
Dhinakaran Vinayagamurthy is a PhD student in computer science at University of Waterloo, advised by Sergey Gorbunov and David Jao. His current interests are in designing systems with provable security guarantees to perform computations over encrypted data. Dhinakaran is a recipient of David R. Cheriton Graduate Scholarship, and holds an MSc from University of Toronto and a BE from College of Engineering, Guindy.
APR
26
2017
TALK Cryptographically Protected Database Search
Speaker | BENJAMIN FULLER  University of Connecticut Location | Stata, G882 Time | Wed 4pm
Abstract
Protected database search systems cryptographically isolate the roles of reading from, writing to, and administering the database. This separation limits unnecessary administrator access and protects data in the case of system breaches. Since protected search was introduced in 2000, the area has grown rapidly; systems are offered by academia, start-ups, and established companies.

However, there is no best protected search system or set of techniques. Design of such systems is a balancing act between security, functionality, performance, and usability. This challenge is made more difficult by ongoing database specialization, as some users will want the functionality of SQL, NoSQL, or NewSQL databases. This database evolution will continue, and the protected search community should be able to quickly provide functionality consistent with newly invented databases.

At the same time, the community must accurately and clearly characterize the tradeoffs between different approaches. In this talk, we survey the range of tradeoffs between security and privacy. In particular, we
1) identify of the important primitive operations across database paradigms,
2) evaluate of the current state of protected search systems in implementing these base operations, and
3) analyze of attacks against protected search for different base queries.
Bio
Benjamin Fuller is an Assistant Professor of Computer Science and Engineering at the University of Connecticut. His research focuses on driving cryptography to use in practice. His primary interests are authentication and searchable encryption. He has worked on a variety of problems from testing broadcast encryption while flying to scanning his iris for cryptographic key derivation. Prior to joining UConn, Ben was a research scientist at MIT Lincoln Laboratory from 2007-2016 working on searchable encryption. He received his PhD and MA from Boston University in 2015 and 2011 respectively.
MAR
22
2017
TALK Prio: Private, Robust, and Scalable Computation of Aggregate Statistics
Speaker | HENRY CORRIGAN-GIBBS  Stanford University Department of Computer Science Location | Stata, G882 Time | Wed 4pm
Abstract
This talk will present Prio, a privacy-preserving system for the collection of aggregate statistics. Each Prio client holds a private data value (e.g., its current location), and a small set of servers compute statistical functions over the values of all clients (e.g., the most popular location). As long as at least one server is honest, the Prio servers learn nearly nothing about the clients' private data, except what they can infer from the aggregate statistics that the system computes. To protect functionality in the face of faulty or malicious clients, Prio uses secret-shared non-interactive proofs (SNIPs), a new cryptographic technique that yields a hundred-fold performance improvement over conventional zero-knowledge approaches. Prio extends classic private aggregation techniques to enable the collection of large class of useful statistics. For example, Prio can perform a least-squares regression on high-dimensional client-provided data without ever seeing the data in the clear.

This is joint work with Dan Boneh. Our paper on Prio is to appear at NSDI 2017.
Bio
Henry Corrigan-Gibbs is a fourth-year PhD student in computer science at Stanford, advised by Dan Boneh. His work uses cryptographic techniques to bring rigorous privacy properties to large-scale computer systems. For these research efforts, Henry and his co-authors have received the 2015 IEEE Security and Privacy Distinguished Paper Award and the 2016 Caspar Bowden Award for Outstanding Research in Privacy Enhancing Technologies. He is the recipient of an NSF Graduate Research Fellowship and an NDSEG Fellowship.
MAR
15
2017
TALK Dandelion: Redesigning the Bitcoin Network for Anonymity
Speaker | SHAILESHH BOJJA VENKATAKRISHNAN  University of Illinois Urbana-Champaign Location | Stata, G882 Time | Wed 4pm
Abstract
Bitcoin and other cryptocurrencies have surged in popularity over the last decade. Although Bitcoin does not claim to provide anonymity for its users, it enjoys a public perception of being a ‘privacy-preserving’ financial system. In reality, cryptocurrencies publish users’ entire transaction histories in plaintext, albeit under a pseudonym; this is required for transaction validation. Therefore, if a user’s pseudonym can be linked to their human identity, the privacy fallout can be significant. Recently, researchers have demonstrated deanonymization attacks that exploit weaknesses in the Bitcoin network’s peer-to-peer (P2P) networking protocols. In particular, the P2P network currently forwards content in a structured way that allows observers to deanonymize users. In this work, we redesign the P2P network from first principles with the goal of providing strong, provable anonymity guarantees. We propose a simple networking policy called Dandelion, which achieves nearly-optimal anonymity guarantees at minimal cost to the network’s utility. We also provide a practical implementation of Dandelion for deployment.
Bio
Shaileshh Bojja Venkatakrishnan is a Ph.D. student in ECE under the supervision of Prof. Pramod Viswanath at the University of Illinois Urbana-Champaign. He received the B.Tech. degree from the Indian Institute of Technology Madras in 2012 and the M.S. degree from UIUC in 2014. His research interests lie primarily in the broad area of distributed algorithms for networks. Specific topics he has worked on include scheduling algorithms for data center networks, peer-to-peer networks and anonymity in cryptocurrency networks. He is also interested in information theory and wireless communication. During the summer of 2016 he interned at Google, where he worked on congestion control for Google’s data centers. He is also a recipient of the Joan and Lalit Bahl fellowship at UIUC.
FEB
22
2017
TALK Sophos - Forward Secure Searchable Encryption
Speaker | RAPHAEL BOST  Direction Générale pour l'Armement Location | Stata, G882 Time | Wed 4pm
Abstract
Searchable Symmetric Encryption (SSE) aims at making possible searching over an encrypted database stored on an untrusted server while keeping privacy of both the queries and the data, by allowing some small controlled leakage to the server. Recent work shows that dynamic schemes – in which the data is efficiently updatable – leaking some information on updated keywords are subject to devastating adaptative attacks breaking the privacy of the queries. The only way to thwart this attack is to design forward private schemes whose update procedure does not leak if a newly inserted element matches previous search queries. This work proposes Sophos as a forward private SSE scheme with performance similar to existing but less secure schemes, and that is conceptually simpler (and also more efficient) than previous forward private constructions. In particular, it only relies on trapdoor permutations and does not use an ORAM-like construction. I will also explain why Sophos is an optimal point of the security/performance tradeoff for SSE. Finally, I will try to give insights into important and interesting problems about SSE.
Bio
Raphael Bost is an engineer in the 'Cryptographic Algorithms' lab at the Direction Générale pour l'Armement (the French defense procurement agency), and a PhD student at Université de Rennes 1 (France).His research interests cover applied and 'real world' cryptography, in particular secure outsourced storage and searchable encryption, and more generally computer security. Raphael graduated from Ecole Polytechnique (France) and received his M.Sc. from Brown University. He also visited the MIT in 2013.
FEB
15
2017
TALK Detecting Malware Callouts in Realtime Network Traffic
Speaker | DOMENIC PUZIO  CapitalOne Location | Stata, G882 Time | Wed 4pm
Abstract
Domain generation algorithm (DGA) malware makes callouts to unique web addresses to avoid detection by static rules engines. To counter this type of malware, we created an ensemble model that analyzes domains and evaluates if they were generated by a machine and thus potentially malicious. The model works entirely on the URL being accessed, thereby eliminating the need for DNS data, which can be difficult to access in large organizations. The ensemble consists of a transliteration pipeline to handle non-English language domains, a highly advanced NLP-based linguistic entropy algorithm, and a collocation and linear word embeddings algorithm to identify dictionary DGAs. We are also researching sequence-based machine learning analysis to detect dictionary DGAs. Our system analyzes enterprise-scale network traffic in real time, renders predictions, and raises alerts for cyber security analysts to evaluate. This talk will discuss the machine learning algorithms that were used to build the model, the features that we found to be informative, and the tools used in model testing and creation. We will then present the tools leveraged in building our model-as-a-service architecture for low-latency stream processing of high velocity and high volume traffic.
Bio
Domenic Puzio is a Data Engineer with Capital One. He graduated from the University of Virginia with degrees in Mathematics and Computer Science. On his current project - code-named Purple Rain - he is a core developer of a custom platform for ingesting, processing, and analyzing Capital One's cyber-security data sources. Built entirely from open-source tools (NiFi, Kafka, Storm, Elasticsearch, Kibana), this framework processes hundreds of millions of events per hour. Currently, his focus is on the creation and productionization of machine learning models that provide enrichment to the data being streamed through the system. He is a contributor to two Apache projects, and his research interests include natural language processing and deep learning.
NOV
02
2016
TALK Security for C++
Speaker | KOSTYA SEREBRYANY  Google Location | Stata, G882 Time | Wed 11am
Abstract
The talk will give an overview of various dynamic testing tools, fuzzers, and security hardening techniques developed at Google, both for user space and the Linux Kernel: The sanitizers (AddressSanitizer, ThreadSanitizer, ...) allow you to find memory corruption bugs, races, and more, both in user space and in the Kernel. libFuzzer (user space) and Syzkaller (kernel) are guided evolutionary fuzzers; they will find inputs that touch the darkest corners of your code. ControlFlowIntegrity and SafeStack are security mitigation techniques that will protect your binaries in production even if security bugs still exist and are known to adversaries.

All these tools are opensource.
clang.llvm.org/docs/AddressSanitizer.html
clang.llvm.org/docs/ThreadSanitizer.html
clang.llvm.org/docs/MemorySanitizer.html
clang.llvm.org/docs/ControlFlowIntegrity.html
clang.llvm.org/docs/SafeStack.html
llvm.org/docs/LibFuzzer.html
https://github.com/google/syzkaller
Bio
Konstantin (Kostya) Serebryany is a Software Engineer at Google. His team develops and deploys dynamic testing tools, such as AddressSanitizer, MemorySanitizer, ThreadSanitizer, and libFuzzer. Prior to joining Google in 2007, Konstantin spent 4 years at Elbrus/MCST working for Sun compiler lab and then 3 years at Intel Compiler Lab. Konstantin holds a PhD from mesi.ru and a M.S. from msu.ru.
OCT
12
2016
TALK How Bitcoin enables a Machine-Payable Web
Speaker | BALAJI SRINIVASAN  21.co and a16z Location | Stata, G882 Time | Wed 4pm
Abstract
First, we had the World Wide Web, a web of links between documents. Then we had the Social Web, a social network of relationships between people. We believe the third web will be the Machine-Payable Web, where each node in the network is a machine and each edge is a micropayment between machines. Towards this end, we've developed open source software called 21 that makes it easy to perform Bitcoin micropayments over HTTP. The software allows you to get digital currency onto any machine headlessly, set up web services that accept and transmit bitcoin over HTTP, and discover other machines with similar services to autonomously trade with. The overall effect is to turn digital currency into a scarce system resource on par with CPU, RAM, and hard drive space. That is, just as one can create a database index that spends disk space to save time, we show that one can instead spends digital currency to outsource a computation to save time. To illustrate the applications, we conclude with several working examples: bitcoin-aware intelligent agents, APIs that implement autonomous surge pricing, and the development of a market data structure as an alternative in many situations to the well known queue. We ask that audience members bring their laptops to code along with the speaker!
Bio
Balaji S. Srinivasan is the CEO & cofounder of 21.co and a Board Partner at Andreessen Horowitz. Prior to taking the role of CEO at 21, Dr. Srinivasan was a General Partner at Andreessen Horowitz. He was named to the MIT TR35, was the cofounder and CTO of Founders Fund-backed Counsyl, and taught a MOOC with 200k+ students at startup.stanford.edu. He holds a BS, MS, and PhD in Electrical Engineering and an MS in Chemical Engineering from Stanford University.
SEP
28
2016
TALK TumbleBit: An Untrusted Bitcoin-Compatible Anonymous Payment Hub
Speaker | ETHAN HEILMAN  BU Location | Stata, G882 Time | Wed 4pm
Abstract
This paper presents TumbleBit, a new unidirectional unlinkable payment hub that is fully compatible with today's Bitcoin protocol. TumbleBit allows parties to make fast, anonymous, off-blockchain payments through an untrusted intermediary called the Tumbler. TumbleBit's anonymity properties are similar to classic Chaumian eCash: no one, not even the Tumbler, can link a payment from its payer to its payee. Every payment made via TumbleBit is backed by bitcoins, and comes with a guarantee that Tumbler can neither violate anonymity, nor steal bitcoins, nor "print money" by issuing payments to itself. We prove the security of TumbleBit using the real/ideal world paradigm and the random oracle model. Security follows from the standard RSA assumption and ECDSA unforgeability. We implement TumbleBit, mix payments from 800 users and show that TumbleBit's off-blockchain payments can complete in seconds.
Bio
Ethan is a PhD student in the Boston University Security Group (BUSEC) of the Computer Science Dept. His research interests are: cryptocurrencies, network security, and cryptanalysis. His most recent projects have been related to internet routing and Bitcoin.
SEP
14
2016
TALK Blockstack: A Global Naming and Storage System Secured by Blockchains
Speaker | MUNEEB ALI  Princeton and Blockstack Location | Stata, G882 Time | Wed 4pm
Abstract
Blockchains like Bitcoin and Namecoin and their respective P2P networks have seen significant adoption in the past few years and show promise as naming systems with no trusted parties. Users can register human meaningful names and securely associate data with them, and only the owner of the particular private keys that registered them can write or update the name-value pair. In theory, many decentralized systems can be built using these blockchain networks, such as new, decentralized versions of DNS and PKI. As the technology is relatively new and evolving rapidly, however, little production data or experience is available to guide design tradeoffs. In this paper, we describe our experiences operating a large deployment of a decentralized PKI service built on top of the Namecoin blockchain. We present various challenges pertaining to network reliability, throughput, and security that we needed to overcome while registering and updating over 33,000 entries and 200,000 transactions on the Namecoin blockchain. Further, we discuss how our experience informed the design of a new blockchain-based naming and storage system called Blockstack. We detail why we switched from the Namecoin network to the Bitcoin network for the new system, and present operational lessons from this migration. Blockstack is released as open source software and currently powers a production PKI system for 55,000 users.
Bio
Muneeb Ali is co-founder and CTO of Blockstack Labs, a Y Combinator and Union Square Ventures backed startup focusing on blockchain technologies. Muneeb is also a final-year PhD candidate at Princeton University, where he has worked in the Systems and Networks group and at PlanetLab. He helped start a new course at Princeton on “How to be a CTO” and gives guest lectures on cloud computing at Princeton. Muneeb has been awarded a J. William Fulbright Fellowship and has served as the Program Co-Chair of ACM NSDR.
APR
20
2016
TALK CrossFire: An Analysis of Firefox Extension-Reuse Vulnerabilities
Speaker | ENGIN KIRDA  Northeastern University Location | Stata, G882 Time | Wed 4pm
Abstract
Extension architectures of popular web browsers have been carefully studied by the research community; however, the security impact of interactions between different extensions installed on a given system has received comparatively little attention. In this talk, I consider the impact of the lack of isolation between traditional Firefox browser extensions, and identify a novel extension-reuse vulnerability that allows adversaries to launch stealthy attacks against users. This attack leverages capability leaks from legitimate extensions to avoid the inclusion of security-sensitive API calls within the malicious extension itself, rendering extensions that use this technique difficult to detect through the manual vetting process that underpins the security of the Firefox extension ecosystem. I then present CROSSFIRE, a lightweight static analyzer to detect instances of extension-reuse vulnerabilities. CROSSFIRE uses a multi-stage static analysis to efficiently identify potential capability leaks in vulnerable, benign extensions. If a suspected vulnerability is identified, CROSSFIRE then produces a proof-of-concept exploit instance – or, alternatively, an exploit template that can be adapted to rapidly craft a working attack that validates the vulnerability. The results of our validation indicate that popular extensions, downloaded by millions of users, contain numerous exploitable extension-reuse vulnerabilities. A case study also provides anecdotal evidence that malicious extensions exploiting extension-reuse vulnerabilities are indeed effective at cloaking themselves from extension vetters.
Bio
Engin Kirda is a professor of computer science and engineering at Northeastern University. He is also the director of the Northeastern Information Assurance Institute. He has been working on practical security problems for more than a decade. He chaired NDSS in 2015, and is chairing USENIX Security in 2017. Lately, he has started liking cats, and one day, he would like to have one.
APR
13
2016
TALK CDN on Demand: An Affordable DDoS Defense over Untrusted IaaS Clouds
Speaker | YOSSI GILAD  MIT/BU Location | Stata, G882 Time | Wed 4pm
Abstract
We present CDN-on-Demand, a software-based defense that administrators of small to medium websites install to resist powerful DDoS attacks with a fraction of the cost of comparable commercial CDN services. Upon excessive load, CDN-on-Demand serves clients from a scalable set of proxies that it automatically deploys on multiple IaaS clouds. CDN-on-Demand can use less expensive and less trusted clouds to minimize costs. This is facilitated by the clientless secure-objects, which is a new mechanism we present. This mechanism avoids trusting the hosts with private keys or user-data, yet does not require installing new client programs. CDN-on-Demand also introduces the origin-connectivity mechanism, which ensures that essential communication with the content-origin is possible even in case of severe DoS attacks. Once installed CDN-on-Demand is completely automated and transparent, i.e., it does not introduce changes to web-server configuration or website content. We implement CDN-on-Demand and evaluate each component separately as well as the complete system.
Bio
Yossi Gilad is a postdoctoral researcher at Boston University and MIT within the Modular Approach to Cloud Security (MACS) project. His research interests include network and system security, anonymity services, and privacy. Prior to this position he was a research staff member at IBM Research, a postdoctoral researcher at the Hebrew University of Jerusalem, and a software architect at Marvell's Switching Division. He is a recipient of the IBM Research Inventor Recognition Award (2015) and the Check Point Institute Information Security Prize (2013-2014).
MAR
09
2016
TALK Privacy in a Data-Driven World
Speaker | ROXANA GEAMBASU  Columbia University Location | Stata, G882 Time | Wed 4pm
Abstract
The concept of personal privacy as a precious and fragile commodity worthy of protection has come under siege in today's data-driven world. Users are eager to share their data online, and mobile applications and web services aggressively collect and monetize that information. This talk describes our vision for a new, privacy-preserving world; in it, users are more aware of the privacy implications of their online actions, and systems and applications are designed from the ground up with privacy in mind. In support of this vision, we describe our research agenda to develop new transparency tools that increase users' visibility into how personal data is being used by applications, and programming tools that facilitate the construction of privacy-mindful applications. We provide two examples of such tools and abstractions. First, we describe Sunlight, a new web transparency tool that helps privacy watchdogs track how web services use individuals' personal data to target ads, personalize content, or adjust prices. Second, we describe FairTest, a new testing toolkit that helps programmers test for unfair or discriminatory effects within their data-driven applications. Overall, our tools and abstractions aim to increase privacy by promoting a more responsible, fair, and accountable approach to user data management.
Bio
Roxana Geambasu is an Assistant Professor of Computer Science at Columbia University. She joined Columbia in Fall 2011 after finishing her Ph.D. at the University of Washington. For her work in cloud and mobile data privacy, she received an Early Career Award in Cybersecurity from the University of Washington Center for Academic Excellence, a Microsoft Research Faculty Fellowship, a 2014 "Brilliant 10" Popular Science nomination, an NSF CAREER award, an Honorable Mention for the 2013 inaugural Dennis M. Ritchie Doctoral Dissertation Award, a William Chan Dissertation Award, two best paper awards at top systems conferences, and the first Google Ph.D. Fellowship in Cloud Computing.
MAR
02
2016
TALK Attacking the Network Time Protocol
Speaker | AANCHAL MALHOTRA  Boston Universitiy Location | Stata, G882 Time | Wed 4pm
Abstract
We explore the risk that network attackers can exploit unauthenticated Network Time Protocol (NTP) traffic to alter the time on client systems. We first discuss how an on- path attacker, that hijacks traffic to an NTP server, can quickly shift time on the server’s clients. Then, we present a extremely low-rate (single packet) denial-of-service attack that an off-path attacker, located anywhere on the network, can use to disable NTP clock synchronization on a client. Next, we show how an off-path attacker can exploit IPv4 packet fragmentation to shift time on a client. We discuss the implications on these attacks on other core Internet protocols, quantify their attack surface using Internet measurements, and suggest a few simple countermeasures that can improve the security of NTP.
Bio
Aanchal Malhotra is a PhD student at Boston University and is part of the BU Security Group (BUSec). Her research uses cryptography, and the insights gained from network measurement and simulations, to improve the security and reliability of core Internet protocols like BGP, DNS, and NTP.
FEB
10
2016
TALK Thunderstrike: EFI firmware bootkits for Apple MacBooks
Speaker | TRAMMELL HUDSON  Two Sigma Location | Stata, G882 Time | Wed 4pm
Abstract
This talk describes Thunderstrike, an attack that installs persistent firmware modifications into the boot ROM of Apple's popular MacBooks. The bootkit can be installed by an evil-maid via the externally accessible Thunderbolt ports. Alternatively, a remote SW attack can amplify root privileges yielding the same result. Once installed, 1) it can prevent software attempts to remove it, 2) it can survive reinstallation of the operating system as well as hard drive replacement, and 3) it can spread virally across air-gaps by infecting additional Thunderbolt devices. Thunderstrike exploits several "features" of modern laptops. The Thunderbolt connection exposes the PCI bus to external devices, and external Thunderbolt devices contain flash memory which store option roms containing code that is executed early in the boot process. Unfortunately, current Macbooks lack full hardware or software cryptographic checks of firmware validity. Once malicious code has been flashed to the ROM, the attack controls the system from the very first instruction and can hide from attempts to detect it. Since Thunderbolt devices' Option ROMs can be rewritten by software, the bootkit can write copies of itself to new Thunderbolt devices. And since the devices remain functional, a stealthy bootkit may spread across air-gap security perimeters through shared Thunderbolt devices. Thunderstrike is the first firmware worm for Macintosh systems built upon several previously disclosed vulnerabilities that were ported from Windows systems to Apple's firmware. Our research shows that vulnerabilities targeting the these firmwares may transcend operating systems as they share millions of lines of code in their common root ancestor, Intel's reference implementation. We explain the vulnerabilities enabling the attack, how they were uncovered, mitigation strategies, and fixes by Apple.
Bio
Trammell Hudson is a programmer, photographer, frequent hacker and occasional watchmaker. He enjoys reverse engineering things, restoring antique computers and making things blink. Sometimes he uses his Amateur Extra rating (NY3U) and hack on Radio and RF projects. He also has other hobbies involving coffee, aviation, sailing and other vehicles. And on the weekends he enjoys teaching classes at NYC Resistor.
DEC
09
2015
TALK How to Use Bitcoin to Play Decentralized Poker
Speaker | RANJIT KUMARESAN  MIT Location | Stata, D507 Time | Wed 4pm
Abstract
Back and Bentov (arXiv 2014) and Andrychowicz et al. (Security and Privacy 2014) introduced techniques to perform secure multiparty computations on Bitcoin. Among other things, these works constructed lottery protocols that ensure that any party that aborts after learning the outcome pays a monetary penalty to all other parties. Following this, Andrychowicz et al. (Bitcoin Workshop 2014) and concurrently Bentov and Kumaresan (Crypto 2014) extended the solution to arbitrary secure function evaluation while guaranteeing fairness in the following sense: any party that aborts after learning the output pays a monetary penalty to all parties that did not learn the output. Andrychowicz et al. (Bitcoin Workshop 2014) also suggested extending to scenarios where parties receive a payoff according to the output of a secure function evaluation, and outlined a 2-party protocol for the same that in addition satisfies the notion of fairness described above. In this work, we formalize, generalize, and construct multiparty protocols for the primitive suggested by Andrychowicz et al. We call this primitive secure cash distribution with penalties. Our formulation of secure cash distribution with penalties poses it as a multistage reactive functionality (i.e., more general than secure function evaluation) that provides a way to securely implement smart contracts in a decentralized setting, and consequently suffices to capture a wide variety of stateful computations involving data and/or money, such as decentralized auctions, markets, and games such as poker, etc. Our protocol realizing secure cash distribution with penalties works in a hybrid model where parties have access to a claim-or-refund transaction functionality $\mathcal{F}_{\mathrm{CR}}^\star$ which can be efficiently realized in (a variant of) Bitcoin, and is otherwise independent of the Bitcoin ecosystem. We emphasize that our protocol is dropout-tolerant in the sense that any party that drops out during the protocol is forced to pay a monetary penalty to all other parties. Our formalization and construction generalize both secure computation with penalties of Bentov and Kumaresan (Crypto 2014), and secure lottery with penalties of Andrychowicz et al. (Security and Privacy 2014). Joint work with Tal Moran (IDC Herzliya) and Iddo Bentov (Technion). This will appear in CCS 2015.
Bio
Ranjit Kumaresan is a postdoc at MIT CSAIL. Previously he did a postdoc at the Technion after a Ph.D. from the University of Maryland. His research interests are in cryptography,distributed algorithms, and theory of computation.
NOV
18
2015
TALK Software-Defined Metadata Processing
Speaker | ANDRE DEHON  University of Pennsylvania Location | Stata, G882 Time | Wed 4pm
Abstract
At a time when computers are increasingly involved in all aspects of our lives, our computer systems are too easily broken or subverted. The current state of affairs is unsurprising given the the design and security compromises that went into the base design of today's mainstream systems. The past 30 years has also brought vast changes in the availability and costs of computer hardware as well as significant advances in formal methods. How do we exploit these advances to make computer systems worthy of the trust we are now placing in them? We specifically look at spending now cheap hardware to reduce or eliminate traditional security-performance tradeoffs and to provide stronger hardware safety and security interlocks that prevent gross security and safety violations even when there are bugs in the code. We introduce an extension to Instruction Set Architectures to support generic metadata processing in parallel with normal instruction execution. We illustrate how this mechanism can be used to support safety and security by enforcing policies on instruction and data usage (e.g. type safety, memory safety, control flow-integrity, taint tracking). Our architectural mechanism is programmable (software-defined) and extensible, following the 0-1-infinity rule and supporting unbounded metadata including the enforcement of an unbounded number of policies, each with their own metadata components. This hardware support makes it possible to embrace well-known security principles of least and separate privileges and complete mediation of operations. In this talk, we review work from the SAFE project at Penn, Harvard, and BAE and touch on on-going work at Draper to integrate these hardware protections into a RISC-V base and protect applications in C and Linux.
Bio
Andre DeHon received S.B., S.M., and Ph.D. degrees in Electrical Engineering and Computer Science from the Massachusetts Institute of Technology in 1990, 1993, and 1996 respectively. From 1996 to 1999, Andre co-ran the BRASS group in the Computer Science Department at the University of California at Berkeley. From 1999 to 2006, he was an Assistant Professor of Computer Science at the California Institute of Technology. In 2006 he joined the Electrical and Systems Engineering Department at the University of Pennsylvania, where he is now a Full Professor. He is broadly interested in how we physically implement computations from substrates, including VLSI and molecular electronics, up through architecture, CAD, and programming models. He places special emphasis on spatial programmable architectures (e.g. FPGAs) and interconnect design and optimization. During AY2015--2016 Andre is on sabbatical at Draper working with the newly created Inherently Secure Processing Hive.
NOV
11
2015
TALK Bitcoin's future: scalability and protocol modifications
Speaker | YONATAN SOMPOLINSKY  The Hebrew University of Jerusalem Location | Stata, G882 Time | Wed 4pm
Abstract
The future of Bitcoin depends (also) on its ability to scale and achieve the same transaction volume as other payment methods. At the same time, the security of Bitcoin depends on the synchronization of nodes in its network, which imposes a limit on the amount of transactions it can handle. I will present two protocol modifications that are aimed to improve the scalability of Bitcoin while still maintaining the security of the system, namely, the GHOST protocol, and Inclusive blockchain protocols.If time permits, I will also briefly discuss recent results on the incentives of nodes to follow the Bitcoin protocol (Selfish mining) which also become tougher if block-size is increased and Bitcoin is scaled up.
Bio
Yonatan Sompolinsky is a Computer Science PhD candidate at The Hebrew University of Jerusalem since 2015. He earned his M.Sc in Computer Science (2014), and his B.Sc in Mathematics (2012), from The Hebrew University.
NOV
04
2015
TALK Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice
Speaker | ZAKIR DURUMERIC  University of Michigan Location | Stata, G882 Time | Wed 4pm
Abstract
We investigate the security of Diffie-Hellman key exchange as used in popular Internet protocols and find it to be less secure than widely believed. First, we present Logjam, a novel flaw in TLS that lets a man-in-the-middle downgrade connections to “export-grade” Diffie-Hellman. To carry out this attack, we implement the number field sieve discrete log algorithm. After a week-long precomputation for a specified 512-bit group, we can compute arbitrary discrete logs in that group in about a minute. We find that 82% of vulnerable servers use a single 512-bit group, allowing us to compromise connections to 7% of Alexa Top Million HTTPS sites. In response, major browsers are being changed to reject short groups. We go on to consider Diffie-Hellman with 768- and 1024-bit groups. We estimate that even in the 1024-bit case, the computations are plausible given nation-state resources. A small number of fixed or standardized groups are used by millions of servers; performing precomputation for a single 1024-bit group would allow passive eavesdropping on 18% of popular HTTPS sites, and a second group would allow decryption of traffic to 66% of IPsec VPNs and 26% of SSH servers. A close reading of published NSA leaks shows that the agency’s attacks on VPNs are consistent with having achieved such a break. We conclude that moving to stronger key exchange methods should be a priority for the Internet community.
Bio
Zakir Durumeric is a Ph.D. Candidate in Computer Science and Engineering at the University of Michigan and the 2014 Google Ph.D. Fellow in Computer Security. His research focuses on network security, particularly how global network measurement can inform and improve the security of heterogeneous distributed systems. Zakir is widely known for creating ZMap, an Internet-wide network scanner capable of scanning the entire public IPv4 address space in minutes. His recent work includes studies on Internet-wide scanning, the operational deployment of HTTPS, widespread weaknesses in cryptographic keys and protocols, and network mismanagement. Zakir was named one of MIT Technology Review's 35 Innovators under 35 in 2015. He received his M.S. from the University of Michigan in 2013 and B.S. in computer science and mathematics from the University of Iowa in 2011.
OCT
28
2015
TALK On the trade-offs between performance and security in network protocols design
Speaker | CRISTINA NITA-ROTARU  Northeastern University Location | Stata, G882 Time | Wed 4pm
Abstract
The proliferation of mobile and web applications and their performance requirements have exposed the limitations of current secure transport protocols, particularly during connection establishment. As a result, protocols like QUIC and TLS v1.3 were proposed to address such limitations. In this work we analyze the trade-offs between provable security and performance guarantees in the presence of attackers by focusing on QUIC. We first introduce a security model for analyzing performance-driven protocols like QUIC and prove that QUIC satisfies our definition under reasonable assumptions on the protocol’s building blocks. However, we find that QUIC does not satisfy the traditional notion of forward secrecy that is provided by some modes of TLS, e.g., TLS-DHE. Our analyses also reveal that with simple bit-flipping and replay attacks on some public parameters exchanged during the handshake, an adversary could easily prevent QUIC from achieving minimal latency advantages either by having it fall back to TCP or by causing the client and server to have an inconsistent view of their handshake leading to a failure to complete the connection. We have implemented these attacks and demonstrated that they are practical. Our results suggest that QUIC’s security weaknesses are introduced by the very mechanisms used to reduce latency, which highlights the trade- off between minimizing latency and providing security guarantees. This is joint work with Robert Lychev, MIT Lincoln Labs, Samuel Jero, Purdue University and Alexandra Boldyreva, Georgia Tech More details available in https://eprint.iacr.org/2015/582.pdf
Bio
Cristina Nita-Rotaru is a Professor of Computer Science in the College of Computing and Information Sciences at Northeastern University and an Adjunct Professor in the Department of Computer Science at Purdue University. Her research lies at the intersection of information security, distributed systems, and computer networks. The overarching goal of her work is designing and building practical distributed systems and network protocols that are robust to failures and attacks while coping with the resource constraints existent in computing systems and networks. Cristina Nita-Rotaru is a recipient of the NSF Career Award in 2006. She is also a recipient of the Purdue Teaching for Tomorrow Award in 2007, Purdue Excellence in Research Award, Seeds for Success in 2012, Purdue College of Science Research Award in 2013. She has served on the Technical Program Committee of numerous conferences in security, networking, and distributed systems. She served as an Assistant Director for CERIAS (2011 - 2013). She was an Associate Editor for Elsevier Computer Communications (2008 - 2011), Elsevier Computer Networks (2012 - 2014), IEEE Transactions on Computers (2011 - 2014), and ACM Transactions on Information Systems Security (2009 - 2013). She is currently an Associate Editor for IEEE Transactions on Mobile Computing and IEEE Transactions on Dependable and Secure Systems.
OCT
21
2015
TALK Selene: Voter-Friendly, Receipt Free, Verifiable Voting
Speaker | PETER Y A RYAN  University of Luxembourg Location | Stata, G882 Time | Wed 4pm
Abstract
A simple way to achieve a degree of verifiability and ballot privacy is to provide each voter with a unique, private tracking number. Votes are posted on a bulletin board in the clear along with their tracking number. Thus voters can visit the WBB confirm that there is an entry with their tracking number showing the correct vote. The beauty of this approach is its simplicity and understandability. There are, however, two drawbacks: we must ensure that trackers are unique and a coercer can demand that the voter reveal her tracking number before the votes are posted. It is interesting to note though that the coercer's window of opportunity is limited: he must ask for the tracker before posting. If he asks after posting the voter has a simple strategy to fool him: just reads off a tracker number with the coercer's required vote from the WBB. In this talk, I describe a scheme that addresses both of these problems. The main idea is to close off the coercer's window of opportunity by ensuring that the voters only learn their tracker numbers after votes have been posted. Notification of the trackers must provide high assurance but be deniable. The resulting scheme provides rather strong verifiability and a receipt-freeness but also provides a more immediately understandable form of verifiability: voters can find their vote, in the clear, in the tally identified by their secret tracker. This is in contrast to the usual cryptographic E2E verification schemes in which voters can confirm that their encrypted ballot goes into the tally, but they need to understand how the various audits steps guarantee that their vote is correctly included in the tally. However, there is a sting in the tail: a coerced voter might light on the coercer's tracker, or the coercer may simply claim that the tracker is his. I describe some elaborations of the simple scheme to counter this problem.
Bio
Peter Ryan is Professor of Applied Security at the University of Luxembourg since Feb 2009. He has around 25 years of experience in cryptography, information assurance and formal verification. He pioneered the application of process calculi to modelling and analysis of secure systems, in particular to the characterization of information flows (non-interference) and the application of process algebra (CSP) and model-checking tools (FDR) to the analysis of security protocols. He has published extensively on cryptographic protocols, security policies, mathematical models of computer security and, most recently, end-to-end verifiable election systems. He is the creator of the (polling station) Prêt à Voter and, with V. Teague, the (internet) Pretty Good Democracy verifiable voting schemes. He was also co-designer of the vVote system, based on Prêt à Voter that was used successfully for Lower House elections in Victoria State, Australia in November 2014. With Feng Hao, he also developed the OpenVote boardroom voting scheme and the J-PAKE password based authenticated key establishment protocol. Recently he co-authored the “Remark!” scheme for secure, anonymous marking of exams and has been working on Quantum Authenticated Key Establishment Protocols.
SEP
30
2015
TALK Eclipse Attacks on Bitcoin's Peer-to-Peer Network
Speaker | ETHAN HEILMAN  Boston University Location | Stata, G882 Time | Wed 4pm
Abstract
We present eclipse attacks on bitcoin's peer-to-peer network. Our attack allows an adversary controlling a sufficient number of IP addresses to monopolize all connections to and from a victim bitcoin node. The attacker can then exploit the victim for attacks on bitcoin's mining and consensus system, including N-confirmation double spending, selfish mining, and adversarial forks in the blockchain. We take a detailed look at bitcoin’s peer-to-peer network, and quantify the resources involved in our attack via probabilistic analysis, Monte Carlo simulations, measurements and experiments with live bitcoin nodes. Finally, we present countermeasures, inspired by botnet architectures, that are designed to raise the bar for eclipse attacks while preserving the openness and decentralization of bitcoin’s current network architecture.
Bio
Ethan is a PhD student in the Boston University Security Group (BUSec) of the Computer Science Dept. His research interests are: network security, crypto currencies, hash function cryptanalysis and side channel attacks. His most recent projects have been related to internet routing and Bitcoin.
MAY
20
2015
TALK On the Risk of Misbehaving RPKI Authorities
Speaker | SHARON GOLDBERG  Boston University Location | Stata, D507 Time | Wed 4pm
Abstract
The RPKI is a new security infrastructure that relies on trusted authorities to prevent some of the most devastating attacks on interdomain routing. The threat model for the RPKI supposes that authorities are trusted and routing is under attack. This talk considers the risks that arise when this threat model is flipped: when RPKI authorities are faulty, misconfigured, compromised, or compelled (e.g. by governments) to misbehave. We show how design decisions that elegantly address the vulnerabilities in the original threat model have unexpected side effects in this flipped threat model. We also propose new mechanisms to improve the transparency and robustness of the RPKI. Joint work with Ethan Heilman, Danny Cooper, Kyle Brogle and Leonid Reyzin.
Bio
Sharon Goldberg is an assistant professor in the Computer Science Department at Boston University. Her research uses tools from theory (cryptography, game-theory, algorithms), and networking (measurement, modeling, and simulation) to solve practical problems in network security. She received her Ph.D. from Princeton University in 2009, her B.A.Sc. from the University of Toronto in 2003, has worked as a researcher at IBM, Cisco, and Microsoft, as an engineer at Bell Canada and Hydro One Networks, and has served on working groups of the Federal Communications Commission (FCC) and the Internet Engineering Task Force (IETF). In 2014 she received two IETF/IRTF Applied Networking Research Prizes, an NSF CAREER Award, and a Sloan Research Fellowship.
MAY
06
2015
TALK Decentralizing Authorities into Scalable Strongest-Link Cothorities
Speaker | BRYAN FORD  EPFL Location | Stata, D507 Time | Wed 4pm
Abstract
Online infrastructure often depends on security-critical authorities such as logging, time, and certificate services. Authorities, however, are vulnerable to the compromise of one or a few centralized hosts yielding "weakest-link" security. We propose collective authorities or cothorities, an architecture enabling thousands of participants to witness, validate, and co-sign an authority's public actions, with moderate delays and costs. Hosts comprising a cothority form an efficient communication tree, in which each host validates log entries proposed by the root, and contributes to collective log-entry signatures. These collective signatures are small and efficient to verify, while embodying "strongest-link" trust aggregated over the collective. We present and evaluate a prototype cothority implementation supporting logging, timestamping, and public randomness (lottery) functions. We find that cothorities can scale to support over 4000 widely-distributed participants while keeping collective signing latencies to within a few seconds.
Bio
Bryan Ford currently leads the Decentralized/Distributed Systems (DeDiS) research group at Yale University, but will be moving to EPFL in Lausanne, Switzerland in July 2015. Ford's work focuses broadly on building secure systems, touching on many particular topics including secure and certified OS kernels, parallel and distributed computing, privacy-preserving technologies, and Internet architecture. He has received the Jay Lepreau Best Paper Award at OSDI, and multiple grants from NSF, DARPA, and ONR, including the NSF CAREER award. His pedagogical achievements include PIOS, the first OS course framework leading students through development of a working, native multiprocessor OS kernel. Prof. Ford earned his B.S. at the University of Utah and his Ph.D. at MIT, while researching topics including mobile device naming and routing, virtualization, microkernel architectures, and touching on programming languages and formal methods.
APR
29
2015
TALK How to Use Bitcoin to Incentivize Correct Computations
Speaker | RANJIT KUMARESAN  MIT Location | Stata, D507 Time | Wed 4pm
Abstract
We study a model of incentivizing correct computations in a variety of cryptographic tasks. For each of these tasks we propose a formal model and design protocols satisfying our model's constraints in a hybrid model where parties have access to special ideal functionalities that enable monetary transactions. We summarize our results: -- *Verifiable computation.* We consider a setting where a delegator outsources computation to a worker who expects to get paid in return for delivering correct outputs. We design protocols that compile both public and private verification schemes to support the incentivization described above. -- *Secure computation with restricted leakage.* Building on the recent work of Huang et al. (Security and Privacy 2012), we show an efficient secure computation protocol that monetarily penalizes an adversary that attempts to learn one bit of information but gets detected in the process. -- *Fair secure computation.* Inspired by recent work, we consider a model of secure computation where a party that aborts after learning the output is monetarily penalized. We then propose an ideal transaction functionality \fml\ and show a constant-round realization on the Bitcoin network. Then, in the \fml-hybrid world we design a constant round protocol for secure computation in this model. -- *Non-interactive bounties.* We provide formal definitions and candidate realizations of non-interactive bounty mechanisms on the Bitcoin network which (1) allow a bounty maker to place a bounty for the solution of a hard problem by sending a single message, and (2) allow a bounty collector (unknown at the time of bounty creation) with the solution to claim the bounty, while (3) ensuring that the bounty maker can learn the solution whenever its bounty is collected, and (4) preventing malicious eavesdropping parties from both claiming the bounty as well as learning the solution. All our protocol realizations (except those realizing fair secure computation) rely on a special ideal functionality that is not currently supported in Bitcoin due to limitations imposed on Bitcoin scripts. Motivated by this, we propose {\em validation complexity} of a protocol, a formal complexity measure that captures the amount of computational effort required to validate Bitcoin transactions required to implement it in Bitcoin. Our protocols are also designed to take advantage of optimistic scenarios where participating parties behave honestly. Joint work with Iddo Bentov (Technion).
Bio
Ranjit Kumaresan is a postdoc at MIT CSAIL. Previously he did a postdoc at the Technion after graduating from the University of Maryland. His research interests are in cryptography,distributed algorithms, and theory of computation.
FEB
25
2015
TALK Shielding applications from an untrusted cloud with Haven
Speaker | ANDREW BAUMANN  Microsoft Research Location | Stata, D507 Time | Wed 3pm
Abstract
Today's cloud computing infrastructure requires substantial trust. Cloud users rely on both the provider's staff and its globally-distributed software/hardware platform not to expose any of their private data. We introduce the notion of shielded execution, which protects the confidentiality and integrity of a program and its data from the platform on which it runs (i.e., the cloud operator's OS, VM and firmware). Our prototype, Haven, is the first system to achieve shielded execution of unmodified legacy applications, including SQL Server and Apache, on a commodity OS (Windows) and commodity hardware. Haven leverages the hardware protection of Intel SGX to defend against privileged code and physical attacks such as memory probes, but also addresses the dual challenges of executing unmodified legacy binaries and protecting them from a malicious host. This work motivated recent changes in the SGX specification.
Bio
Andrew Baumann is a researcher in the OS group at Microsoft Research, Redmond. His research interests include operating systems, distributed systems, multi-/many-core architectures, and a smattering of security. Past institutions include The University of New South Wales (BE/PhD), IBM T.J. Watson (extended internship), and ETH Zurich (postdoc). Past and current projects include the L4 microkernel, Mungi single-address-space OS, K42 multiprocessor OS, Barrelfish multikernel OS, and Drawbridge LibOS.
FEB
18
2015
TALK Controlled Functional Encryption
Speaker | MUHAMMAD NAVEED  UIUC Location | Stata, D507 Time | Wed 4pm
Abstract
Motivated by privacy and usability requirements in various scenarios where existing cryptographic tools (like secure multi-party computation and functional encryption) are not adequate, we introduce a new cryptographic tool called Controlled Functional Encryption (C-FE). As in functional encryption, C-FE allows a user (client) to learn only certain functions of encrypted data, using keys obtained from an authority. However, we allow (and require) the client to send a fresh key request to the authority every time it wants to evaluate a function on a ciphertext. We obtain efficient solutions by carefully combining CCA2 secure public-key encryption (or rerandomizable RCCA secure public-key encryption, depending on the nature of security desired) with Yao's garbled circuit. Our main contributions in this work include developing and formally defining the notion of C-FE; designing theoretical and practical constructions of C-FE schemes achieving these definitions for specific and general classes of functions; and evaluating the performance of our constructions on various application scenarios. Link to the paper: https://web.engr.illinois.edu/~naveed2/pub/CCS2014CFE.pdf
Bio
Muhammad Naveed is a fourth year PhD student in computer science at the University of Illinois at Urbana-Champaign. He works on novel models that can bring modern cryptographic technology to real applications. He is also interested in systems security and genomics privacy. For more details visit his homepage at www.naveed.pro.
FEB
11
2015
TALK Secure Computation by Superfolding Garbled Circuits
Speaker | FARINAZ KOUSHANFAR  Rice University Location | Stata, D507 Time | Wed 4pm
Abstract
Secure function evaluation allows two or more mutually distrustful parties to jointly compute a function on their private input and find the output without revealing input or intermediate values. Designing practical secure two-party computation based on Yao's garbled circuit (GC) has been subject of intensive research in the recent past with surprising progress on efficiency. In this talk, I present a novel methodology for automatic generation of highly compact and scalable Boolean circuits that further pushes down the limits. We achieve this by leveraging a new folded function description and logic synthesis methods and tools along with our created custom libraries and constraints. We show significant improvements in terms of the memory footprint and network bandwidth compared with the prior art. Furthermore, our approach enables us to implement functions that have not been reported before, small enough that they befit mobile/embedded devices. I discuss how our new findings enable practically addressing several known classical challenges as well as exciting applications such as privacy-preserving data mining.
Bio
Farinaz Koushanfar is currently an Associate Professor with the Department of Electrical and Computer Engineering, Rice University, where she directs the Adaptive Computing and Embedded Systems (ACES) Lab. She also serves as the: principal director of the Texas Instruments DSP Leadership University program; and, as the associate partner of the Intel Collaborative Research Institute for Secure Computing. She received her PhD degree in Electrical Engineering and Computer Science from University of California Berkeley. Her research interests include embedded/cyber-physical systems (CPS) security, hardware trust, adaptive and customizable embedded systems design, and secure function evaluation. Professor Koushanfar received a number of awards and honors for her research, mentorship, and teaching including the PECASE from president Obama, ACM SIGDA Outstanding New Faculty Award, NAS Kavli fellowship, Cisco IoT Security Grand Challenge Award, Young faculty/CAREER awards from NSF, DARPA, ONR, ARO, MIT Technology Review TR-35, and a Best Paper Award at ACM SIGMOBILE (Mobicom).
NOV
13
2014
TALK Fast, Synchronous Mashup Isolation in Web Applications
Speaker | JAMES MICKENS  Microsoft Research Location | Stata, G882 Time | Wed 4pm
Abstract
Pivot is a new JavaScript isolation framework for web applications. Pivot uses iframes as low-level isolation containers; however, Pivot uses code rewriting to implement synchronous cross-domain interfaces atop the asynchronous postMessage() primitive. Pivot layers a distributed scheduler across the frames, essentially treating each frame as a thread which can invoke RPCs that are serviced by external threads. By rewriting JavaScript call sites, Pivot can detect RPC invocations; Pivot exchanges RPC requests and responses via postMessage(), and it pauses and restarts frames using a novel rewriting technique that translates each frame's JavaScript code into a restartable generator function. By leveraging both iframes and rewriting, Pivot does not need to rewrite all code, providing an order-of-magnitude performance improvement over rewriting-only solutions. Compared to iframe-only approaches, Pivot provides synchronous RPC semantics, which developers typically prefer over asynchronous RPCs. Pivot also allows developers to use the full, unrestricted JavaScript language, including powerful statements like eval().
Bio
James Mickens is a researcher in the Distributed Systems group at Microsoft's Redmond lab. This semester, he is working at MIT as an MLK Visiting Professor. His current research focuses on storage systems for datacenter-scale computation. He also studies the client-side of web applications, designing new ways to improve their performance, reliability, and security. Mickens received a bachelor’s degree in computer science from Georgia Tech, and a PhD in computer science from the University of Michigan. During his stay at Michigan, he was notorious for scheduling his thesis defense in the early hours of the morning so that nobody would attend it. This technique, popularly called "The Mickens Gambit," is now banned in 36 states.
OCT
01
2014
TALK Code-Pointer Integrity
Speaker | VOLODYMYR KUZNETSOV AND GEORGE CANDEA  EPFL Location | Stata, G882 Time | Wed 4pm
Abstract
Systems code is often written in low-level languages like C/C++, which offer many benefits but also delegate memory management to programmers. This invites memory safety bugs that attackers can exploit to divert control flow and compromise the system. Deployed defense mechanisms (e.g., ASLR, DEP) are incomplete, and stronger defense mechanisms (e.g., CFI) often have high overhead and limited guarantees. We introduce code-pointer integrity (CPI), a new design point that guarantees the integrity of all code pointers in a program (e.g., function pointers, saved return addresses) and thereby prevents all control-flow hijack attacks, including return-oriented programming. We also introduce code-pointer separation (CPS), a relaxation of CPI with better performance properties. CPI and CPS offer substantially better security-to-overhead ratios than the state of the art, they are practical (we protect a complete FreeBSD system and over 100 packages like apache and postgresql), effective (prevent all attacks in the RIPE benchmark), and efficient: on SPEC CPU2006, CPS averages 1.2% overhead for C and 1.9% for C/C++, while CPI’s overhead is 2.9% for C and 8.4% for C/C++. A prototype implementation of CPI and CPS can be obtained from http://levee.epfl.ch. (Joint work with L. Szekeres, M. Payer, R. Sekar, and D. Song)
Bio
George Candea (http://dslab.epfl.ch/people/candea/) is an Associate Professor of Computer Science at EPFL. He got his BS ('97) and MEng ('98) from MIT and his PhD from Stanford ('05), all in Computer Science. He co-founded Aster Data Systems (now Teradata Aster) and served as its CTO and then Chief Scientist. Volodymyr Kuznetsov (http://people.epfl.ch/vova.kuznetsov) is a PhD student at EPFL in George's group, working on systems, security, and program analysis & verification. He received his BS ('07) and MS ('09) in Applied Physics and Mathematics from the Moscow Institute of Physics and Technology.
SEP
24
2014
TALK Nail: A Practical Tool for Parsing and Generating Data Formats
Speaker | JULIAN BANGERT  MIT Location | Stata, G882 Time | Wed 4pm
Abstract
Nail is a tool that greatly reduces the programmer effort for safely parsing and generating data formats defined by a grammar. Nail introduces several key ideas to achieve its goal. First, Nail uses a protocol grammar to define not just the data format, but also the internal object model of the data. Second, Nail eliminates the notion of semantic actions, used by existing parser generators, which reduces the expressive power but allows Nail to both parse data formats and generate them from the internal object model, by establishing a semantic bijection between the data format and the object model. Third, Nail introduces dependent fields and stream transforms to capture protocol features such as size and offset fields, checksums, and compressed data, which are impractical to express in existing protocol languages. Using Nail, we implement an authoritative DNS server in C in under 300 lines of code and grammar, and an unzip program in C in 220 lines of code and grammar, demonstrating that Nail makes it easy to parse complex real-world data formats. Performance experiments show that a Nail-based DNS server can outperform the widely used BIND DNS server on an authoritative workload, demonstrating that systems built with Nail can achieve good performance. Chupja (Korean for spy), which is a very effective covert timing channel that works over the Internet. It is implemented in the physical layer of the network stack and is many orders of magnitude faster than prior art while being very robust and virtually invisible to software endhosts. Key to our approach is software and real-time access and control over every bit in the physical layer of a 10 Gigabit network stack (a bit is 100 picoseconds wide at 10 gigabit per seconds), which allows us to modulate and interpret interpacket spacings at sub-microsecond scale. In the talk, I will discuss when and how a timing channel in the physical layer works, how hard it is to detect such a channel, and what is required to do so.
Bio
SEP
10
2014
TALK Chupja--PHY Covert Channels: Can you see the Idles?
Speaker | HAKIM WEATHERSPOON  Cornell Location | Stata, G882 Time | Wed 4pm
Abstract
Network covert timing channels embed secret messages in legitimate packets by modulating interpacket delays. Such channels are normally implemented in higher network layers (layer 3 or above), are often fairly slow, and can be easily detected or prevented. In this talk, I will present a new approach, Chupja (Korean for spy), which is a very effective covert timing channel that works over the Internet. It is implemented in the physical layer of the network stack and is many orders of magnitude faster than prior art while being very robust and virtually invisible to software endhosts. Key to our approach is software and real-time access and control over every bit in the physical layer of a 10 Gigabit network stack (a bit is 100 picoseconds wide at 10 gigabit per seconds), which allows us to modulate and interpret interpacket spacings at sub-microsecond scale. In the talk, I will discuss when and how a timing channel in the physical layer works, how hard it is to detect such a channel, and what is required to do so.
Bio
Hakim Weatherspoon is an assistant professor in the Department of Computer Science at Cornell University. His research interests cover various aspects of fault-tolerance, reliability, security, and performance of large Internet-scale systems such as cloud computing and distributed systems. Professor Weatherspoon received his Ph.D. from Berkeley in 1999. Before receiving his PhD, Prof. Weatherspoon received his B.S. from University of Washington. Prof. Weatherspoon is an Alfred P. Sloan Fellow and recipient of an NSF CAREER award, DARPA Computer Science Study Panel (CSSP), IBM Faculty Award, the NetApp Faculty Fellowship, Intel Early Career Faculty Honor, and the Future Internet Architecture award from the National Science Foundation (NSF).
MAY
15
2014
TALK Can You Hide in an Internet Panopticon?
Speaker | BRYAN FORD  Yale Location | Stata, G882 Time | Thurs 4pm
Abstract
Many people have legitimate needs to avoid their online activities being tracked and linked to their real-world identities - from citizens of authoritarian regimes, to everyday victims of domestic abuse or law enforcement officers investigating organized crime. Current state-of-the-art anonymous communication systems are based on onion routing, an approach effective against localized adversaries with a limited ability to monitor or tamper with network traffic. In an environment of increasingly powerful and all-seeing state-level adversaries, however, onion routing is showing cracks, and may not offer reliable security for much longer. All current anonymity systems are vulnerable in varying degrees to five major classes of attacks: global passive traffic analysis, active attacks, "denial-of-security" or DoSec attacks, intersection attacks, and software exploits. The Dissent project is prototyping a next-generation anonymity system representing a ground-up redesign of current approaches. Dissent is the first anonymity and pseudonymity architecture incorporating protection against the five major classes of known attacks. By switching from onion routing to alternate anonymity primitives offering provable resistance to traffic analysis, Dissent makes anonymity possible even against an adversary who can monitor most, or all, network communication. A collective control plane renders a group of participants in an online community indistinguishable even if an adversary interferes actively, such as by delaying messages or forcing users offline. Protocol-level accountability enables groups to identify and expel misbehaving nodes, preserving availability, and preventing adversaries from using denial-of-service attacks to weaken anonymity. The system computes anonymity metrics that give users realistic indicators of anonymity protection, even against adversaries capable of long-term intersection and statistical disclosure attacks, and gives users control over tradeoffs between anonymity loss and communication responsiveness. Finally, virtual machine isolation offers anonymity protection against browser software exploits of the kind recently employed to de-anonymize Tor users While Dissent is still a proof-of-concept prototype with important functionality and performance limitations, preliminary evidence suggests that it may in principle be possible - though by no means easy - to hide in an Internet panopticon.
Bio
Bryan Ford leads the Decentralized/Distributed Systems (DeDiS) research group at Yale University. His work focuses broadly on building secure systems, touching on many particular topics including secure and certified OS kernels, parallel and distributed computing, privacy-preserving technologies, and Internet architecture. He has received the Jay Lepreau Best Paper Award at OSDI, and multiple grants from NSF, DARPA, and ONR, including the NSF CAREER award. His pedagogical achievements include PIOS, the first OS course framework leading students through development of a working, native multiprocessor OS kernel. Prof. Ford earned his B.S. at the University of Utah and his Ph.D. at MIT, while researching topics including mobile device naming and routing, virtualization, microkernel architectures, and touching on programming languages and formal methods.
APR
23
2014
TALK Proving the Security of a Simple Private Information Retrieval Protocol using EasyCrypt
Speaker | ALLEY STOUGHTON  Lincoln Labs Location | Stata, G882 Time | Wed 4pm
Abstract
EasyCrypt is Gilles Barthe's group's framework for interactively finding security proofs of cryptographic protocols using the sequence of games approach. I'll give an introduction to EasyCrypt, describe a very simple private information retrieval protocol, and give a high level description of how this protocol can be proved secure using EasyCrypt.
Bio
APR
16
2014
TALK Integrating Safety and Security using Systems Theory
Speaker | WILLIAM YOUNG AND NANCY LEVESON  MIT Location | Stata, G882 Time | Wed 4pm
Abstract
By using a new model of causality based on systems theory, an integrated and more powerful approach to both safety and security is possible. While our novel safety techniques are now being used in most industries, we realized only recently that the same approach applies to security, both cyber and physical. We will discuss the model, its application to security, and recent evaluation of its application to cyber security on real defense systems.
Bio
William Young (wyoung@mit.edu) is a Ph.D. candidate in the Engineering Systems division at MIT. He is a Colonel in the U.S. Air Force. Nancy Leveson (leveson@mit.edu) is Professor of Aeronautics and Astronautics and also Professor of Engineering Systems at MIT. Previously she was a computer science professor at the Univ. of Washington. She is an elected member of the NAE.
APR
09
2014
TALK Bots, Bubbles, and Bottleneck: Safeguarding the User's Internet Experience
Speaker | NICK FEAMSTER  Georgia Tech Location | Stata, G882 Time | Wed 4pm
Abstract
A user's experience on the Internet rests in the hands of a large and increasingly diverse set of stakeholders. Internet service providers and content providers point fingers at one other about performance problems. Miscreants launch attacks against both other users and the Internet infrastructure itself. Content providers continually engage in practices to "personalize" what we see and when we see it. Many governments aim to control its citizens' access to information, while activists design circumvention tools. Safeguarding the user's Internet experience requires both gathering empirical network measurements to detect threats (typically in the absence of any "ground truth") and developing large-scale systems to mitigate them. In this talk, I will present three classes of safeguards against different threats to the user's Internet experience: (1) technologies to characterize and improve performance in the Internet's "last mile", including a worldwide deployment of home routers in around 200 home networks and ongoing studies with the Federal Communications Commission; (2) methods for lightweight and fast detection of message abuse, such as spam, that have since been widely adopted by industry; and (3) defenses against against information manipulation attacks, a new class of attacks against personalization algorithms. I will also discuss other such threats and how networking can draw from other disciplines to tackle them.
Bio
Nick Feamster is an associate professor in the College of Computing at Georgia Tech. He received his Ph.D. in Computer science from MIT in 2005, and his S.B. and M.Eng. degrees in Electrical Engineering and Computer Science from MIT in 2000 and 2001, respectively. His research focuses on many aspects of computer networking and networked systems, with a focus on network operations, network security, and censorship-resistant communication systems. In December 2008, he received the Presidential Early Career Award for Scientists and Engineers (PECASE) for his contributions to cybersecurity, notably spam filtering. His honors include the Technology Review 35 "Top Young Innovators Under 35" award, the ACM SIGCOMM Rising Star Award, a Sloan Research Fellowship, the NSF CAREER award, the IBM Faculty Fellowship, the IRTF Applied Networking Research Prize, and award papers at the SIGCOMM Internet Measurement Conference (measuring Web performance bottlenecks), SIGCOMM (network-level behavior of spammers), the NSDI conference (fault detection in router configuration), Usenix Security (circumventing web censorship using Infranet), and Usenix Security (web cookie analysis).
MAR
19
2014
TALK (In)Security in Home Embedded Devices
Speaker | JIM GETTYS  Bell Labs Location | Stata, G882 Time | Wed 4pm
Abstract
We now wander in Best Buy, Lowes and on Amazon and buy all sorts of devices from thermostats, hi-fi gear, tablets, phones, and occasionally laptops or desktops as well as home routers to build our home networks. Most of these we plug in and forget about. But should we?

"Familiarity Breeds Contempt: The Honeymoon Effect and the Role of Legacy Code in Zero-Day Vulnerabilities", by Clark, Fry, Blaze and Smith makes clear that ignoring these devices is foolhardy; unmaintained systems become more vulnerable, with time.

Structural issues in the market make the situation much worse, as pointed out in Bruce Schneier's Wired editorial in January: "The Internet of Things Is Wildly Insecure — And Often Unpatchable", which I instigated and fed Bruce the ammunition. "Binary blobs" used in these systems have the net effect of "freezing" software versions, often on many year old versions of system software. Even if update streams are available (which they seldom are), blobs may make it impossible to update to versions free of a vulnerability.

There are immediate actions you can personally take, e.g. by running open source router firmware in your network, but fixing this problem generically will take many years, as it involves fundamental changes and an attitude change in how we develop and maintain embedded systems, and hardest, changes in business models to enable long term support of popular hardware.
Bio
Jim Gettys is an American computer programmer at Alcatel-Lucent Bell Labs, USA. Until January 2009,[1] he was the Vice President of Software at the One Laptop per Child project, working on the software for the OLPC XO-1.[2] He is one of the original developers of the X Window System at MIT and worked on it again with X.Org, where he served on the board of directors. He previously served on the GNOME foundation board of directors. He worked at the World Wide Web Consortium (W3C)[3] and was the editor of the HTTP/1.1 specification in the Internet Engineering Task Force through draft standard. Gettys helped establish the handhelds.org community, from which the development of Linux on handheld devices can be traced.
FEB
19
2014
TALK Consent Management using User Managed Access (UMA) protocol
Speaker | THOMAS HARDJONO  MIT Location | Stata, G882 Time | Wed 4pm
Abstract
The mission of the MIT-KIT is to develop software components for equitable access to personal data. In the MIT OpenPDS model, each individual has one or more personal data store (PDS). Access to the data in the PDS requires the express consent of the owner of the PDS. In this presentation we discuss the OAuth2.0 authorization framework (RFC6749) as the basis for a consent-management protocol called UMA (User Managed Access). UMA also integrates and builds upon the OpenID-Connect protocol (OIDC) used for identity management and Single-Sign-On (SSO) over RESTful Web-APIs.
Bio
Thomas Hardjono is the technical lead and executive director of the MIT Kerberos & Internet Trust Consortium at MIT in Cambridge, MA. He is active in a number of technical communities and standards organizations, including the IETF, IEEE, TCG, Oasis and Kantara. In the IETF Thomas was chair of the Multicast Security (MSEC) working group and the Group Security Research Group. He is an author of RFC 3740 and RFC 3547. Thomas was also co-chair of the TCG Infrastructure Working Group. He is author and editor of a number of TCG specifications focusing on the security infrastructure supporting the TPM hardware. Currently he is co-chair of the Security Services TC (SSTC) in Oasis (home of the SAML2.0 standard), and active contributor to the UMA WG in the Kantara Initiative. Thomas is the MIT representative to the NSTIC Identity Ecosystem Steering Group (IDESG).
DEC
11
2013
TALK A Practical System for Verifying Recoverability of Big Data
Speaker | EMIL STEFANOV  Berkeley Location | Stata, G882 Time | Wed 4pm
Abstract
We designed and built a practical and efficient dynamic PoR (proof of retrievability) system that allows a client to quickly verify that an untrusted or compromised cloud is storing all of the client's data and that none of the data is corrupted beyond repair. Unlike previous work, our system requires very little client storage and uses about 300 times less client-server bandwidth, resulting in almost no bandwidth overhead. Our system is capable of verifying terabytes of data in less than 9 seconds, and can easily scale (logarithmically) to much larger storage systems.

We achieve this by introducing several powerful techniques, including a novel incrementally-constructible erasure code based on the Discrete Fourier Transform (DFT). Because the techniques we proposed are extremely scalable and efficient, corporations can use them to ensure the reliability of all (possibly petabytes) of the information they store in the cloud. Prior to our work, it was prohibitively impractical to verifiably impose this level of reliability at a large scale.
Bio
NOV
20
2013
TALK Shill: A Secure Shell Scripting Language
Speaker | PROF. STEPHEN CHONG  Harvard University Location | Stata, G882 Time | Wed 4pm
Abstract
Reasoning about the security of shell scripts is notoriously hard: it is difficult for programmers to deduce the effects of shell scripts on the underlying operating system. First, resource references, such as file paths, are typically resolved lazily and subject to race conditions. Second, shell scripts are typically run with the same privileges as the invoking user, making it hard to determine or enforce that a script has all (and only) permissions to execute successfully. Third, shell scripts invoke other programs, often arbitrary binaries.

In this talk, I present the preliminary design and implementation of Shill, a new secure shell scripting language that uses fine-grained capabilities to restrict access to resources. Capabilities bind resources at the time of their creation, and avoid vulnerabilities arising from lazy name resolution. Shill scripts come with a declarative interface that specifies and restricts which capabilities the script may use. A Shill script can invoke an arbitrary binary in a sandbox that limits the privileges of the binary based on a set of capabilities. Capabilities together with declarative interfaces and sandboxing enable the caller of a script to reason precisely about which resources a script (and the binaries it calls) may access, and thus, Shill helps reason safely and effectively about the use and composition of scripts. We have implemented Shill on top of FreeBSD, using Racket and the FreeBSD Trusted MAC framework.
Bio
Steve Chong is a Computer Science faculty member 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 is the recipient of an NSF CAREER award, and an AFOSR Young Investigator award. He received a PhD from Cornell University, and a bachelor's degree from Victoria University of Wellington, New Zealand.
NOV
14
2013
TALK Experiences and Challenges in Automated Malware Analysis: Quo Vadis Sandboxes?
Speaker | PROF. ENGIN KIRDA  Northeastern University Location | Stata, G575 Time | Thur 4pm
Abstract
Malicious software (or malware) is one of the most pressing and major security threats facing the Internet today. Anti-malware companies typically have to deal with tens of thousands of new malware samples every day. To cope with these large quantities, researchers and practitioners alike have developed a number of automated, dynamic malware analysis systems. These systems automatically execute a program in a controlled environment, and produce a report describing the program's behavior. Such dynamic malware analysis sandboxes are the latest rage, and a popular example of such a is Anubis, a freely-accessible, large-scale public malware analysis system that that we have developed, and have been maintaining for more than six years. In this talk, I will discuss the problems and challenges in dynamic malware analysis, and will report on our experiences in maintaining a large-scale malware analysis system. I will also talk about some of our research that aims to address the problem of evasive malware. Finally, I will elaborate on some of the remaining challenges and open research topics in the area.
Bio
Engin Kirda is the Sy and Laurie Sternberg Associate Professor of Information Assurance at the Northeastern University in Boston and the director of the Northeastern Information Assurance Institute. He is also a co-founder and Chief Architect at Lastline, Inc. Before moving to the US, he has held faculty positions at Institute Eurecom in the French Riviera and the Technical University of Vienna where he co-founded the International Secure Systems Lab (iSecLab) that is now distributed over five institutions in Europe and US. Engin's recent research has focused on malware analysis (e.g., Anubis, Exposure, Fire) and detection, web application security, and practical aspects of social networking security. His recent work on the deanonymization of social network users received wide media coverage. He co- authored more than 100 peer-reviewed scholarly publications and served on program committees of numerous well-known international conferences and workshops. In 2009, Engin was the Program Chair of the International Symposium on Recent Advances in Intrusion Detection (RAID), in 2010/11, Program Chair of the European Workshop on Systems Security (Eurosec), and in 2012 the Program Chair of the USENIX Workshop on Large Scale Exploits and Emergent Threats. He is currently the program co-chair of NDSS, and will be chairing it in 2015. In the past, Engin has consulted the European Commission on emerging threats, and gave a Congressional Briefing in Washington D.C. on advanced malware attacks and cyber-security in 2012.
OCT
23
2013
TALK PrivExec: Private Execution as an Operating System Service
Speaker | PROF. WILLIAM ROBERTSON  Northeastern University Location | Stata, G882 Time | Wed 4pm
Abstract
Privacy has become an issue of paramount importance for many users. As a result, encryption tools such as TrueCrypt, OS-based full-disk encryption such as FileVault, and privacy modes in all modern browsers have become popular. However, although such tools are useful, they are not perfect. For example, prior work has shown that browsers still leave many traces of user information on disk even if they are started in private browsing mode. In addition, disk encryption alone is not sufficient, as key disclosure through coercion remains possible. Clearly, it would be useful and highly desirable to have OS-level support that provides strong privacy guarantees for any application -- not only browsers.

In this talk, I will present the design and implementation of PrivExec, the first operating system service for private execution. PrivExec provides strong, general guarantees of private execution, allowing any application to execute in a mode where storage writes, either to the filesystem or to swap, will not be recoverable by others during or after execution. PrivExec does not require any explicit application support, recompilation, or any other preconditions. We have implemented a prototype of PrivExec by extending the Linux kernel that is efficient, practical, and that secures sensitive data against disclosure.
Bio
William Robertson is an assistant professor with a joint appointment in the College of Computer and Information Science and the College of Engineering at Northeastern University. His research interests revolve around various aspects of systems and network security, making use of techniques such as program analysis and machine learning. His work in these areas has had impact both in industry through collaborations with startup ventures such as Lastline Inc., as well as in the world of public policy, where his work on electronic voting security resulted in significant changes to voting procedures in the states of California and Ohio.

He co-chaired the 2013 USENIX Workshop on Offensive Technologies (WOOT), co- located with USENIX Security, and chaired the 2012 Conference on the Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA). He has participated on the program committees of a number of top-tier systems security venues, including IEEE Security and Privacy, USENIX Security, and RAID. He is also the author of numerous peer-reviewed journal and conference papers in the area of systems and network security.
OCT
09
2013
TALK Secure Data Deletion from Persistent Media
Speaker | JOEL REARDON  ETH Zurich Location | Stata, G882 Time | Wed 4pm
Abstract
Secure deletion is the task of deleting data irrecoverably from a physical medium. In this work, we present a general approach to the design and analysis of secure deletion for persistent storage that relies on encryption and key wrapping. We define a key disclosure graph that models the adversarial knowledge of the history of key generation and wrapping. We introduce a generic update function and prove that it achieves secure deletion of data against a coercive attacker; instances of the update function implement the update behaviour of all arborescent data structures including B-Trees, extendible hash tables, linked lists, and others. We implement a B-Tree instance of our solution. Our implementation is at the block-device layer, allowing any block-based file system to be used on top of it. Using different workloads, we find that the storage and communication overhead required for storing and retrieving B-Tree nodes is small and that this therefore constitutes a viable solution for many applications requiring secure deletion from persistent media.
Bio
OCT
02
2013
TALK Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior
Speaker | XI WANG  MIT Location | Stata, G575 Time | Wed 4pm
Abstract
This talk will give an overview of an emerging class of software bugs called optimization-unstable code: code that is unexpectedly discarded by compiler optimizations due to undefined behavior in the program. Unstable code is present in many systems, including the Linux kernel and the Postgres database. The consequences of unstable code range from incorrect functionality to missing security checks.

To reason about unstable code, this talk will present a novel model, which views unstable code in terms of optimizations that leverage undefined behavior. Using this model, we introduce a new static checker called STACK that precisely identifies unstable code. Applying STACK to widely used systems has uncovered 160 new bugs that have been confirmed and fixed by developers.
Bio
SEP
18
2013
TALK How to search over encrypted data
Speaker | DR. SENY KAMARA  Microsoft Research Redmond Location | Stata, G575 Time | Wed 4pm
Abstract
The problem of searching over encrypted data arises often and, most notably, in the design of secure database systems, file systems, cloud storage systems and in the design of cryptographic protocols. Many solutions to this problem have been proposed in the past, including searchable encryption, deterministic encryption, order preserving encryption, functional encryption, oblivious RAMs, secure two-party computation and fully-homomorphic encryption.

In this talk, I will survey the different solutions to the encrypted search problem and discuss their various strengths and limitations, paying particularly close attention to the tradeoffs made between security, efficiency and functionality. I will then present recent advances in the area of searchable encryption and give an overview of the state-of-the art constructions and implementations.
Bio
SEP
11
2013
TALK Random Number Generation, Revisited
Speaker | PROF. YEVGENIY DODIS  New York University Location | Stata, G882 Time | Wed 4pm
Abstract
A random number generator (RNG) is a process that produces "good" randomness using various imperfect sources of randomness (such as interrupt timing, processor heating, memory access times, mouse movements, etc.) as its inputs. In this upcoming CCS'13 paper, we revisit both practical and theoretical methods of known RNG designs, and we find that both of them have serious deficiencies: practical designs appear to have good security intuition, but rely too much on "security-by-obscurity", while theoretical approaches over-simplify the problem and ignore the issue we term "entropy accumulation".

As a result, we propose a new, "clean slate" model for RNG design and evaluation. Most importantly, our RNG definition includes a new security property of "entropy accumulation", stating that a good RNG should be able to eventually recover from compromise even if the entropy is injected into the system at a very slow pace, and expresses the expected real-life behavior of practical RNG designs. Unfortunately, we show that none of the existing designs (including Linux RNGs /dev/random and /dev/urandom) meets this property. On a positive, we propose a new RNG construction which provably satisfies our security definition, in particular meeting many classical (weaker) security notions, such as forward/backward security, resilience and robustness. In addition to being aesthetically more pleasing and provably secure, our design is also much faster than /dev/(u)random. A current draft of the paper is paper is available at http://eprint.iacr.org/2013/338.
Bio
evgeniy Dodis is a Professor of computer science at New York University. Dr. Dodis received his summa cum laude Bachelors degree in Mathematics and Computer Science from New York University in 1996, and his PhD degree in Computer Science from MIT in 2000. Dr. Dodis was a post-doc at IBM T.J.Watson Research center in 2000, and joined New York University as an Assistant Professor in 2001. He was promoted to Associate Professor in 2007 and Full Professor in 2012.

Dr. Dodis' research is primarily in cryptography and network security. In particular, he worked in a variety of areas including leakage-resilient cryptography, cryptography under weak randomness, cryptography with biometrics and other noisy data, hash function and block cipher design, protocol composition and information-theoretic cryptography. Dr. Dodis has more than 100 scientific publications at various conferences, journals and other venues, has been on program committees of many international conferences (including FOCS, STOC, CRYPTO and Eurocrypt), and gave numerous invited lectures and courses at various venues.

Dr. Dodis is the recipient of National Science Foundation CAREER Award, Faculty Awards from IBM, Google and VMware, and Best Paper Award at 2005 Public Key Cryptography Conference. As an undergraduate student, he was also a winner of the US-Canada Putnam Mathematical Competition in 1995.
AUG
28
2013
TALK Verifiable Anonymous Polling
Speaker | PROF. TAL MORAN  Interdisciplinary Center Herzliya Israel Location | Stata, G882 Time | Wed 4pm
Abstract
We consider the problem of polling responses from a large population of humans in a publicly-verifiable way, without violating the responders' anonymity. As a motivating example, think of online voting for "American Idol" or a similar TV show, where viewers might not trust the producers to accurately publish the results in an unbiased way.

The main difficulty we must overcome is the lack of strong identity verification ("On the Internet, nobody knows you're a dog"). In this setting, guaranteeing "one vote per person" appears to be infeasible. Instead, we will describe an approach for implementing publicly-verifiable "effort based" polling, where each vote must be accompanied by a "proof of human effort".

Our results are applicable to a variety of settings in which crowd-sourced information gathering is required. This includes political polling, recommendation systems, viewer voting in TV shows and prediction markets.
Bio
Tal Moran is a faculty member in the School of Computer Science at the Interdisciplinary Center Herzliya. Before that, he spent three years as a postdoc at Harvard's Center for Research on Computation and Society. He has a Ph.D. in Computer Science from the Weizmann Institute of Science. Tal's primary fields of interest are Cryptography and Security.
JUN
19
2013
TALK Hails: Protecting Data Privacy in Untrusted Web Applications
Speaker | AMIT LEVY AND DEIAN STEFAN  Stanford Location | Stata, G575 Time | Wed *3*pm
Abstract
Modern extensible web platforms like Facebook and Yammer depend on third-party software to offer a rich experience to their users. Unfortunately, users running a third-party "app" have little control over what it does with their private data. Today's platforms offer only ad-hoc constraints on app behavior, leaving users an unfortunate trade-off between convenience and privacy. A principled approach to code confinement could allow the integration of untrusted code while enforcing flexible, end-to-end policies on data access. This paper presents a new web framework, Hails, that adds mandatory access control and a declarative policy language to the familiar MVC architecture. We demonstrate the flexibility of Hails through GitStar.com, a code-hosting website that enforces robust privacy policies on user data even while allowing untrusted apps to deliver extended features to users.
Bio
MAY
22
2013
TALK A Decade of OS Access-Control Extensibility
Speaker | DR. ROBERT N. M. WATSON  University of Cambridge Location | Stata, G882 Time | Wed 4:30pm
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.
MAY
01
2013
TALK Bitcoin's Security, Inside and Out
Speaker | GAVIN ANDRESEN, BITCOIN FOUNDATION  Chief Scientist Location | Stata, G882 Time | Wed 4pm
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.
APR
03
2013
TALK Verification with Small and Short Worlds
Speaker | PROF. SANJIT A. SESHIA  UC Berkeley Location | Stata, G575 Time | Wed 4pm
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.
MAR
20
2013
TALK Language Interoperability without Sacrificing Safety
Speaker | DR. DAVID CHISNALL  University of Cambridge UK Location | Stata, G575 Time | Wed 4pm
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.
MAR
19
2013
TALK Measuring Side Channel Vulnerability using SVF
Speaker | PROF. SIMHA SETHUMADHAVAN  Columbia University Location | Stata, G575 Time | Tue 4pm
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.
Bio
MAR
13
2013
TALK Time-Optimal Interactive Proofs for Circuit Evaluation
Speaker | JUSTIN THALER  Harvard University Location | Stata, G575 Time | Wed 4pm
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.
FEB
11
2013
TALK Building a Secure Foundation for Mobile Apps
Speaker | HAOHUI MAI  University of Illinois at Urbana-Champaign Location | Stata, G575 Time | Monday 4pm
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.
DEC
10
2012
TALK Binary Static Analysis
Speaker | CHRIS ENG  Veracode - industry talk Location | Stata, G575 Time | Monday 4pm
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.
DEC
03
2012
TALK Mining Your Ps and Qs: Detection of Widespread Weak Keys in Network Devices
Speaker | DR. NADIA HENINGER  Microsoft Research New England Location | Stata, G575 Time | Monday 4pm
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.
NOV
26
2012
TALK Automating End User Security Tasks
Speaker | EUNSUK KANG  MIT Location | Stata, G575 Time | Monday 4pm
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.
Bio
NOV
19
2012
TALK Making proof-based verified computation almost practical
Speaker | PROF. MIKE WALFISH  UT Austin Location | Stata Center, D463 (Star) Time | Monday 4pm
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.
NOV
05
2012
TALK Breaks in the Cloud
Speaker | DR. ARI JUELS  RSA the Security Division of EMC Location | Stata, G575 Time | Monday 4pm
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.
OCT
22
2012
TALK TARDIS: Time and Remanence Decay in SRAM to Implement Secure Protocols on Embedded Devices without Clocks
Speaker | AMIR RAHMATI  UMass Amherst Location | Stata, G575 Time | Monday 4pm
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.
Bio
OCT
01
2012
TALK Techniques for performing secure computation on encrypted data
Speaker | CHRIS FLETCHER  MIT Location | Stata, G575 Time | Monday 4pm
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.
Bio
SEP
24
2012
TALK Improving integer security for systems
Speaker | XI WANG  MIT Location | Stata, G575 Time | Monday 4pm
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.
Bio
SEP
17
2012
TALK RockSalt: Better, Faster, Stronger Software Fault Isolation for the x86
Speaker | PROF. GREG MORRISETT  Harvard University Location | Stata, G575 Time | Monday 4pm
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.
Bio
MAY
07
2012
TALK Jeeves, a Language for Enforcing Privacy
Speaker | JEAN YANG  MIT Location | Stata, G575 Time | Monday 4pm
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.
APR
23
2012
TALK Concealing Access Patterns to Cloud Storage for Privacy
Speaker | EMIL STEFANOV  Berkeley Location | Stata, G575 Time | Monday 4pm
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.
Bio
APR
09
2012
TALK Keys and Clouds: Searching for the Equilibrium
Speaker | ROBERT GRIFFIN, RSA  Security Division of EMC Location | Stata, G575 Time | Monday *3*pm
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.
APR
02
2012
TALK New approaches to securing cloud data
Speaker | DR. ALINA OPREA  RSA Labs Location | Stata, G575 Time | Monday *4*pm
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.
FEB
27
2012
TALK Privacy and Integrity in the Untrusted Cloud
Speaker | ARIEL J. FELDMAN  Princeton Location | Stata, G575 Time | Monday *4*pm
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.
FEB
13
2012
TALK Recent advances in homomorphic encryption
Speaker | DR. SHAI HALEVI  IBM T. J. Watson Research Center Location | Stata, G575 Time | Monday 3pm
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.
JAN
30
2012
TALK The Case for Prefetching and Prevalidating TLS Server Certificates
Speaker | EMILY STARK  MIT Location | Stata, G575 Time | Monday 3pm
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.
Bio
JAN
23
2012
TALK Verifying Keyword and Database Search in the Cloud
Speaker | NIKOS TRIANDOPOULOS  RSA Labs & Boston University Location | Stata, G575 Time | Monday 3pm
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.
Bio
DEC
19
2011
TALK Focused Threat Response and Forensic Information Sharing: Current Challenges and Limits in Cloud Computing Scenarios
Speaker | DR. DENNIS MOREAU  EMC Corporation Location | Stata, G575 Time | 12/19/2011
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:
  1. employ chains of novel payloads, including 0-day exploits,
  2. be conveyed via highly de-correlated interactions,
  3. be quiescent for long periods of time, and
  4. employ human guided adaptation.
In cloud computing environments:
  1. Operational noise is created by the behavior of co-hosted workloads, limiting the ability to maintain "normal" (non-anomalous) behavioral measures/metrics.
  2. Forensic visibility is inhibited by isolation/abstraction mechanisms and by the need to avoid inter-tenant leakage of sensitive information.
  3. Multiple management entities may participate in managing the configuration and operation of hosted services.
Some of the most promising developments leverage forensic information sharing and collaboration for improved response. In this session we will address threat response issues, that are particular to cloud computing settings, and explore potential directional improvements.
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.

DEC
12
2011
TALK Regaining Control Over Cloud and Mobile Data
Speaker | PROF. ROXANA GEAMBASU  Columbia University Location | Stata, G575 Time | Monday 4pm
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.
NOV
28
2011
TALK Web Security via Types and Theorem-Proving in the Ur/Web Programming Language
Speaker | PROF. ADAM CHLIPALA  MIT Location | Stata, G575 Time | Monday 3pm
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.
Bio
NOV
21
2011
TALK Inference of Expressive Information Security Policies
Speaker | PROF. STEPHEN CHONG  Harvard University Location | Stata, 32-D463 (Star) Time | Monday 4pm
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.
NOV
14
2011
TALK Verifying and Enforcing Network Paths with ICING
Speaker | DR. JAD NAOUS  MIT Location | Stata, G575 Time | Monday 3pm
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.
Bio
OCT
31
2011
TALK How to Tell if Your Cloud Files are Vulnerable to Drive Crashes
Speaker | KEVIN BOWERS  RSA Labs Location | Stata, G575 Time | Monday 3pm
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.
OCT
17
2011
TALK CryptDB: Protecting Confidentiality with Encrypted Query Processing
Speaker | RALUCA ADA POPA  MIT Location | Stata, D504 Time | Monday, 3pm
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
OCT
03
2011
TALK RePriv: Re-Imagining Content Personalization and In-Browser Privacy
Speaker | DR. BEN LIVSHITS  Microsoft Research Redmond Location | Stata, D504 Time | Monday, 3pm
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.
AUG
04
2011
TALK Cloud Computing and Software Security
Speaker | DR. ÚLFAR ERLINGSSON  security researcher at Google Location | Stata, D504 Time | Thursday, 4pm
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.
APR
14
2011
TALK A Scalable Cloud File System with Efficient Integrity Checks
Speaker | DR. ALINA OPREA  RSA Labs Location | Stata, D504 Time | Thursday, 4pm
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.
Bio
APR
07
2011
TALK Sequential Aggregate Signatures with Lazy Verification for S-BGP
Speaker | PROF. LEONID REYZIN  Boston University Location | Stata, D504 Time | Wed 4pm
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.
Bio
FEB
24
2011
TALK Let the Market Drive Deployment: A Strategy for Transitioning to BGP Security
Speaker | PROF. SHARON GOLDBERG  Boston University Location | Stata, D504 Time | Thursday 4pm
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.
Bio
NOV
03
2010
TALK Privacy Integrated Queries: A Programming Language for Differentially-Private Computation
Speaker | DR. FRANK MCSHERRY  Microsoft Research Location | Stata, D504 Time | Wednesday 4pm
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.
OCT
28
2010
TALK Fabric: Using language-based security to build secure distributed systems
Speaker | PROF. ANDREW MYERS  Cornell University Location | Stata, D504 Time | Thursday 4pm
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.
OCT
15
2010
TALK Quantification of Integrity
Speaker | DR. MICHAEL CLARKSON  Cornell University Location | Time | Friday 3pm
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.
Bio
Designed by Lisa Feng