MAY
23
2024
TALK Modular Verification of Non-Leakage for Hardware Security Modules with K2
Speaker | ANISH ATHALYE  MIT Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
K2 is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by its functional specification. K2's proof covers the software and the hardware of an HSM, which enables it to catch all bugs above the cycle-level digital circuit abstraction, including timing side channels. K2's key contribution is a novel approach to proving non-leakage in a modular fashion, using transitive information-preserving refinement. This enables K2 to use different techniques for verifying different layers (software and hardware), reuse existing verified components, and largely automate several parts of the proof, while still providing a single top-to-bottom combined theorem. We use K2 to develop several HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. K2 provides a strong guarantee for these HSMs; for instance, it proves that the ECDSA-on-Ibex HSM implementation (2,300 lines of code and 13,500 lines of Verilog) leaks nothing more than what is allowed by a 50-line specification of its behavior.
Bio
MAY
16
2024
TALK Building principled and practical secure systems using Wasm
Speaker | DEIAN STEFAN  UCSD Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
In this talk I'm going to talk about our adventures (ab)using WebAssembly to build more secure systems. Wasm---at least in my view---is a secure compilation intermediate representation. It makes it possible for us to compile (potentially unsafe) code to a single IR, where we enforce different security properties, and compile this retrofitted code to native code, where it runs securely (e.g., isolated from every other piece of code). I'll start with our work sandboxing third-party C libraries in Firefox, our work speeding up and verifying Wasm compilers and runtimes, and our most recent work designing hardware extensions (and abusing existing ones) to both speed up Wasm and address different classes of attacks on Wasm especially as used by hyperscalers.
Bio
APR
25
2024
TALK Constrained Pseudorandom Functions from Weaker Assumptions
Speaker | SACHA SERVAN-SCHREIBER  MIT Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
In this talk, I will present a framework for constructing Constrained Pseudorandom Functions (CPRFs) with inner-product constraint predicates, using ideas from subtractive secret sharing and related-key-attack (RKA) security. I will show three instantiations of the framework: 1. an adaptively-secure construction in the random oracle model; 2. a selectively-secure construction under the DDH assumption; and 3. a selectively-secure construction under the assumption that one-way functions exist. All three instantiations are constraint-hiding and support inner-product predicates, leading to the first constructions of such expressive CPRFs under each corresponding assumption. Moreover, while the OWF-based construction is primarily of theoretical interest, the random oracle and DDH-based constructions are concretely efficient, which is shown via an implementation.
Bio
Sacha is a PhD student at MIT, advised by Srini Devadas.
APR
11
2024
TALK Recent Results on Threshold Signatures: Supporting Weights and Adaptive Security
Speaker | SOURAV DAS  UIUC Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
Threshold signatures protect the signing key by sharing it among a group of signers so that an adversary must corrupt a threshold number of signers to be able to forge signatures. In this talk, I will cover two of our recent results on threshold signatures. First, I will talk about how we design a weighted, non-interactive threshold signature scheme (https://eprint.iacr.org/2023/598). Existing threshold signatures with succinct signatures and constant verification times do not work if signers have different weights. We present a new approach to designing threshold signatures for pairing- and discrete logarithm-based cryptosystems. Our scheme supports arbitrary weight distributions among signers, arbitrary thresholds, and is concretely very efficient. Second, I will talk about the adaptive security of threshold signatures (https://eprint.iacr.org/2023/1553). A popular choice of threshold signature scheme is the BLS threshold signature introduced by Boldyreva (PKC'03). Some attractive properties of Boldyreva's threshold signature are that the signatures are unique and short, the signing process is non-interactive, and the verification process is identical to that of non-threshold BLS. These properties have resulted in its practical adoption in several decentralized systems. However, despite its popularity and wide adoption, up until recently, the Boldyreva scheme has been proven secure only against a static adversary. In this paper, we present the first adaptively secure threshold BLS signature scheme based on standard assumptions while retaining all of its existing properties.
Bio
APR
04
2024
TALK End-to-End Encrypted Group Chats with MLS: Design, Implementation and Verification
Speaker | THEOPHILE WALLEZ  Inria Paris Location | Stata, G882 (Hewlett) Time | Thurs 12pm
Abstract
Messaging Layer Security (MLS), currently undergoing standardization at the IETF, is an asynchronous group messaging protocol that aims to be efficient for large dynamic groups, while providing strong guarantees like forward secrecy (FS) and post-compromise security (PCS). While prior work on MLS has extensively studied its group key establishment component (called TreeKEM), many flaws in early designs of MLS have stemmed from its group integrity and authentication mechanisms that are not as well-understood. In this work, we identify and formalize TreeSync: a sub-protocol of MLS that specifies the shared group state, defines group management operations, and ensures consistency, integrity, and authentication for the group state across all members. We present a precise, executable, machine-checked formal specification of TreeSync, and show how it can be composed with other components to implement the full MLS protocol. Our specification is written in F* and serves as a reference implementation of MLS; it passes the RFC test vectors and is interoperable with other MLS implementations. Using the DY* symbolic protocol analysis framework, we formalize and prove the integrity and authentication guarantees of TreeSync, under minimal security assumptions on the rest of MLS. Our analysis identifies a new attack and we propose several changes that have been incorporated in the latest MLS draft. Ours is the first testable, machine-checked, formal specification for MLS, and should be of interest to both developers and researchers interested in this upcoming standard.
Bio
MAR
21
2024
TALK Extracting Secret Keys from a Device's Power LED Using COTS Video Cameras
Speaker | BEN NASSI  Cornell Tech Location | Stata, G882 (Hewlett) Time | Thurs 12pm
Abstract
Over the past 25 years, research has highlighted the fact that high-end hardware can be used by attackers to recover secret keys from devices. Numerous studies have demonstrated innovative secret key extraction techniques that rely on dedicated professional equipment to capture data-dependent physical leakage from target devices. These methods employ equipment like scopes to obtain power traces, software-defined radio and probes to capture electromagnetic radiation (EMR) traces, as well as ultrasonic microphones to capture acoustic traces. While these methods have deepened our understanding regarding the cryptanalytic risks associated with various types of leakage (EMR, acoustic, power) and high-end sensors to secret keys, much less is known about the cryptanalytic risks posed by optical leakage and accessible ubiquitous equipment such as video cameras.
In this talk, we will reveal the findings from the two research papers, optical cryptanalysis (CCS’23) and video-based cryptanalysis (SP’24), and discuss how attackers can extract cryptographic keys using video footage of a device’s power LEDs captured by standard video cameras. In the first part of the talk, we will review the history of the side-channel cryptanalytic attacks from the first timing attack that was published in 1996, through the cryptanalytic power-based attacks and cryptanalytic EMR attacks that were published since 1998 until the acoustic attack that was published at 2014 and conclude interesting insights regarding the lessons we learned from these works. Next, we will discuss information leakage from power LEDs (based on the findings presented at CCS 23), and understand why the intensity of the light emitted by a device’s power LED can be used as an alternative to power traces obtained from the device to recover secret keys (2048-bit RSA, 256-bit ECDSA and 378-bit SIKE keys) from commonly used cryptographic libraries (Libgcrypt, GnuPG, PQCryptoSIDH) using a photodiode. In the second part of the talk, we will discuss how standard video cameras (e.g., of an iPhone 13 PRO Max, and security camera) can be used as alternatives for the photodiodes (based on the findings presented at SP’24) to extract secret keys (256-bit ECDSA and 378-bit SIKE keys). We will discuss a video camera’s rolling shutter and understand how it can be used to increase the sampling rate of a video camera from the frame-per-second rate (60 measurements per second) to the rolling shutter rate (60,000 measurements per second). We will see videos of secret key recoveries that were taken by a smartphone and by an Internet-connected security camera to recover a 256-bit ECDSA key (using the Minerva side-channel attack) and a 378-SIKE key (using the HertzBleed side-channel attack). At the end of the talk, we will discuss countermeasures, and provide insights regarding the real potential of extracting cryptographic keys by video cameras in our days and in the near future, taking into account the expected improvements in the specifications of video cameras expected by Moore’s Law.
Bio
MAR
14
2024
TALK Confidential Computing and Trusted Execution Environment: Challenges, Opportunities, and the Future
Speaker | MENGYUAN LI  MIT Location | Stata, G882 (Hewlett) Time | Thurs 12pm
Abstract
Confidential Computing, or Trusted Execution Environment (TEE), represents a cutting-edge security feature in advanced server CPUs. This technology provides a shield for cloud tasks, ensuring they are safeguarded against various threats, including attacks from privileged software, physical attackers, and even untrustworthy hypervisors. As the demand for secure private data handling surges, the adoption of Confidential Computing has become widespread across industries. This is evidenced by the adoption of TEE support in the latest server-grade CPUs from major vendors like Intel, AMD, and ARM. Furthermore, leading cloud service providers, such as AWS, Google Cloud, Microsoft Azure, and IBM Cloud, now offer commercial Confidential Computing services. However, despite its increasing popularity, Confidential Computing still faces significant design and security challenges. These include finding the right balance between maintaining strong security and achieving efficient performance, as well as the need to reassess and possibly rebuild the kernel space or hypervisor, which may not be fully trustworthy.
In this talk, I will delve into the design intricacies and potential vulnerabilities associated with Confidential Computing. I will start by discussing the ciphertext side-channel attack, which arises from compromising security for performance. This type of attack can lead to the exposure of execution states or the decryption of sensitive information, even enabling attackers to extract private keys from secure implementations like RSA and ECDSA in the latest OpenSSL library. Following this, I will discuss the CROSSLINE attack, which shows the dangers of not properly redesigning untrusted hypervisors. This attack exploits the unprotected management of resources like address space identifiers (ASID), threatening the security of confidential VMs protected by AMD Secure Encrypted Virtualization (SEV). This highlights the urgency of reevaluating the role of hypervisors in Confidential Computing. To conclude, I will outline ongoing efforts and future directions in enhancing the security and effectiveness of Confidential Computing, emphasizing the importance of addressing these vulnerabilities and design challenges to advance the field.
Bio
MAR
07
2024
TALK Designing protocols that actually get deployed
Speaker | ERIC RESCORLA  Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
Designing good Internet protocols is hard. Designing protocols that actually get deployed is harder. We take a look at some protocols that have been widely deployed (e.g., TLS 1.3, QUIC, and the WebPKI), and some others which have been less so (e.g., IPsec, SCTP, and DNSSEC/DANE) and draw some lessons about the factors that lead to protocol success and failure.
Bio
Eric Rescorla has contributed extensively to many of the core security protocols used in the Internet, including TLS, DTLS, WebRTC, ACME, and QUIC. He was editor of the TLS 1.3 protocol, which secures the vast majority of Web traffic and co-founder of Let's Encrypt, a free and automated certificate authority that is now the largest on the Internet. He is the former Chief Technology Officer for Firefox and Internet Platform at Mozilla, where he was responsible for setting the overall technical strategy for the Firefox browser and Mozilla's participation in Internet standards and global policy.
FEB
29
2024
TALK Cryptographic theory into applied technology
Speaker | NICK SULLIVAN  CFRG Location | Stata, G882 (Hewlett) Time | Thurs 12pm
Abstract
Translating cryptographic theories into applied technologies is a complex process that requires both deep theoretical knowledge and practical insight. In this talk, Nick Sullivan, a cryptography industry veteran, will offer an insider’s view on some of the most significant cryptographic implementations of recent times. From his contributions to Apple's FairPlay system, which uses encryption for multimedia content protection, to leading the charge in securing web communications with TLS 1.3 and QUIC, to steering the post-quantum cryptography transition through industry standards, Sullivan's experiences cover a broad spectrum. This presentation will outline the real-world challenges and solutions encountered in applying cryptography, highlighting the research, development, and collaborative deployment cycle that Sullivan has experienced in his career. Through this lens, this talk hopes to offer insights into the critical role of applied cryptography in contemporary digital infrastructure, reflecting on both its technical intricacies and its broad impact on global security and privacy.
Bio
Nick Sullivan is the former Head of Research and Cryptography at Cloudflare, and is the co-chair of the Crypto Forum Research Group.
FEB
22
2024
TALK Reef: Fast Succinct Non-Interactive Zero-Knowledge Regex Proofs
Speaker | ELIZABETH MARGOLIN  Penn Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
This talk will present Reef, a system for generating publicly verifiable succinct non-interactive zero-knowledge proofs that a committed document matches or does not match a regular expression. I’ll describe applications such as proving the strength of passwords, the provenance of email despite redactions, the validity of oblivious DNS queries, and the existence of mutations in DNA. Reef supports the Perl Compatible Regular Expression syntax, including wildcards, alternation, ranges, capture groups, Kleene star, negations, and lookarounds. Reef introduces a new type of automata, Skipping Alternating Finite Automata (SAFA), that skips irrelevant parts of a document when producing proofs without undermining soundness, and instantiates SAFA with a lookup argument. Our experimental evaluation confirms that Reef can generate proofs for documents with 32M characters; the proofs are small and cheap to verify (under a second).
Bio
FEB
15
2024
TALK Approximate Lower Bound Arguments
Speaker | TOLIK ZINOVYEV  BU Location | Stata, D463 (Star) Time | Thurs 12pm
Abstract
Suppose a prover, in possession of a large body of valuable evidence, wants to quickly convince a verifier by presenting only a small portion of the evidence.
We define an Approximate Lower Bound Argument, or ALBA, which allows the prover to do just that: to succinctly prove knowledge of a large number of elements satisfying a predicate (or, more generally, elements of a sufficient total weight when a predicate is generalized to a weight function). The argument is approximate because there is a small gap between what the prover actually knows and what the verifier is convinced the prover knows. This gap enables very efficient schemes.
We present noninteractive constructions of ALBA in the random oracle and uniform reference string models and show that our proof sizes are nearly optimal. We also show how our constructions can be made particularly communication-efficient when the evidence is distributed among multiple provers, which is of practical importance when ALBA is applied to a decentralized setting.
We demonstrate two very different applications of ALBAs: for large-scale decentralized signatures and for proving universal composability of succinct proofs.
Based on https://eprint.iacr.org/2023/1655. Joint work with Pyrros Chaidos, Aggelos Kiayias and Leonid Reyzin.
Bio
Tolik is a PhD student at Boston University advised by Leo Reyzin. Before studying cryptography, he was a software engineer at Algorand where he got inspiration for research problems to work on.
DEC
13
2023
TALK Characterizing and Optimizing End-to-End Systems for Private Inference
Speaker | KARTHIK GARIMELLA  NYU Location | TBD Time | Wed 4pm
Abstract
In two-party machine learning prediction services, the client's goal is to query a remote server's trained machine learning model to perform neural network inference in some application domain. However, sensitive information can be obtained during this process by either the client or the server, leading to potential collection, unauthorized secondary use, and inappropriate access to personal information. These security concerns have given rise to Private Inference (PI), in which both the client's personal data and the server's trained model are kept confidential. State-of-the-art PI protocols consist of a pre-processing or offline phase and an online phase that combine several cryptographic primitives: Homomorphic Encryption (HE), Secret Sharing (SS), Garbled Circuits (GC), and Oblivious Transfer (OT). Despite the need and recent performance improvements, PI remains largely arcane today and is too slow for practical use. This paper addresses PI's shortcomings with a detailed characterization of a standard high-performance protocol to build foundational knowledge and intuition in the systems community. Our characterization pinpoints all sources of inefficiency -- compute, communication, and storage. In contrast to prior work, we consider inference request arrival rates rather than studying individual inferences in isolation and we find that the pre-processing phase cannot be ignored and is often incurred online as there is insufficient downtime to hide pre-compute latency. Finally, we leverage insights from our characterization and propose three optimizations to address the storage (Client-Garbler), computation (layer-parallel HE), and communication (wireless slot allocation) overheads.
Bio
Karthik is a graduate student at NYU.
NOV
16
2023
TALK Flamingo: Multi-Round Single-Server Secure Aggregation with Applications to Private Federated Learning
Speaker | SEBASTIAN ANGEL  University of Pennsylvania Location | Stata, D463 Time | Thurs 4pm
Abstract
In this talk I will discuss Flamingo, a system for secure aggregation of data across a large set of clients. In secure aggregation, a server sums up the private inputs of clients and obtains the result without learning anything about the individual inputs beyond what is implied by the final sum. Flamingo works particularly well in the multi-round setting found in federated learning in which many consecutive additions (averages) of model weights are performed to derive a good model. Furthermore, Flamingo can tolerate the failure of clients (e.g., clients that go offline) in the middle of the computation. Our implementation of Flamingo shows that it can securely train a neural network on the (Extended) MNIST and CIFAR-100 datasets significantly quicker than all prior secure aggregation systems, and the model converges without a loss in accuracy, compared to a non-private federated learning system.
Bio
Sebastian Angel is the Raj and Neera Singh Assistant Professor at the University of Pennsylvania.
OCT
04
2023
TALK Security of Computer Systems with Non-Computational Sensor Side Channels
Speaker | YAN LONG  University of Michigan Location | Stata, G575 Time | Wed 4pm
Abstract
Side channels are unintentional information channels caused by shared resources in complex systems, often leading to the security risk of information leakage. While the embedded security community has investigated how to eliminate these channels in the computation space, the increasingly complex sensor hardware employed by emerging cyber-physical systems (CPS) creates new side channels that compromise both the integrity and confidentiality of data generated by sensor hardware. Such sensor side channels are challenging to prevent due to the undefined interactions between physical signals, sensor semiconductors, and downstream software. Using the example of camera sensing, my talk explains how to characterize the causality, limits, and mitigations of sensor side channels through physics modeling and lab experiments. I will first explain how camera images can not only leak sensitive unintended optical information, but also leak unintended room audio modulated in pixels. Then I will demonstrate how the electromagnetic leakage from smart home camera circuits allow eavesdroppers to reconstruct real-time, high-quality camera images even through walls. Besides developing defenses to confine the problems, I will also explain how sensor side channels can be leveraged to defend sensing applications. Finally, I will discuss my research vision for software-defined sensors that leverage signal processing and modeling to guide the synthesis of unintended sensor transduction—effectively creating new sensor modalities with unchanged hardware. This research appears in IEEE Symposium on Security and Privacy 2023 and Network and Distributed System Security Symposium 2024.
Bio
Yan Long is a Ph.D. candidate in the EECS department at the University of Michigan, where he is advised by Professor Kevin Fu and Professor Mingyan Liu. His research is in the area of embedded systems security with a particular focus on protecting the security and privacy of sensing in various forms of cyber-physical and mobile systems using hardware-software co-design. His dissertation is on modeling and mitigating side channels in optical sensing systems and is a recipient of the Rackham Predoctoral Fellowship. His other research includes developing novel ubiquitous computing systems to facilitate security and healthcare.
SEP
27
2023
TALK K9db: Privacy-Compliant Storage For Web Applications By Construction
Speaker | KINAN DAK ALBAB  Brown Location | Stata, G882 Time | Wed 4pm
Abstract
Data privacy laws like the EU's GDPR grant users new rights, such as the right to request access to and deletion of their data. Manual compliance with these requests is error-prone and imposes costly burdens especially on smaller organizations, as non-compliance risks steep fines. K9db is a new, MySQL-compatible database that complies with privacy laws by construction. The key idea is to make the data ownership and sharing semantics explicit in the storage system. This requires K9db to capture and enforce applications' complex data ownership and sharing semantics, but in exchange simplifies privacy compliance. Using a small set of schema annotations, K9db infers storage organization, generates procedures for data retrieval and deletion, and reports compliance errors if an application risks violating the GDPR. Our K9db prototype successfully expresses the data sharing semantics of real web applications, and guides developers to getting privacy compliance right. K9db also matches or exceeds the performance of existing storage systems, at the cost of a modest increase in state size.
Bio
Kinan is a PhD candidate at Brown university advised by Malte Schwarzkopf. Kinan builds systems and tools to improve end user privacy using every tool possible from computer systems, cryptography, and programming languages. His work was cited in the United Nations Guide on Privacy-Enhancing Technologies, and the White House's National Strategy to Advance Privacy-Preserving Data Sharing and Analytics. When he is not behind a computer coding, he is probably at a Heavy Metal show, grilling in the backyard, or mixing new cocktails!
JUL
07
2023
TALK Accountable authentication with privacy protection: The Larch system for universal login
Speaker | EMMA DAUTERMAN  UC Berkeley Location | Stata, D463 (Star) Time | Friday 2pm
Abstract
Credential compromise is hard to detect and hard to mitigate. To address this problem, we present larch, an accountable authentication framework with strong security and privacy properties. Larch protects user privacy while ensuring that the larch log server correctly records every authentication. Specifically, an attacker who compromises a user’s device cannot authenticate without creating evidence in the log, and the log cannot learn which web service (relying party) the user is authenticating to. To enable fast adoption, larch is backwards-compatible with relying parties that support FIDO2, TOTP, and password-based login. Furthermore, larch does not degrade the security and privacy a user already expects: the log server cannot authenticate on behalf of a user, and larch does not allow relying parties to link a user across accounts. We implement larch for FIDO2, TOTP, and password-based login. Given a client with four cores and a log server with eight cores, an authentication with larch takes 150ms for FIDO2, 91ms for TOTP, and 74ms for passwords (excluding preprocessing, which takes 1.23s for TOTP). This talk is based on joint work with Danny Lin, Henry Corrigan-Gibbs, and David Mazières that will be appearing at OSDI 2023.
Bio
Emma is a fourth year PhD student at UC Berkeley, advised by Raluca Ada Popa.
JUN
28
2023
TALK ConSeal: A Secure Analytics Platform
Speaker | ROBERTA DE VITI  MPI-SWS Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
Many types of analytics on personal data can be made differentially private, thus alleviating concerns about the privacy of individuals. However, no analytics platform currently exists that can technically prevent data leakage and misuse with minimal trust assumptions; as a result, analytics that would be in the public interest are not done in privacy-conscious societies. To bridge this gap, we present secure selective analytics (SSA), where data sources can a priori restrict the use of their data to a pre-defined set of privacy-preserving analytics queries performed by a specific group of analysts, and for a limited period. Furthermore, we show that a scalable SSA platform can be built in a strong threat model based on minimal trust.
In this talk, I will present ConSeal, an SSA platform that relies on a minimal trust implementation of functional encryption (FE), using a combination of secret sharing, secure multi-party computation (MPC), and trusted execution environments (TEEs). ConSeal tolerates the compromise of a subset of TEE implementations as well as side channels. Despite the high cost of MPC, we show that ConSeal scales to very large databases using MapReduce-based query parallelization.
Bio
Roberta De Viti is a PhD student at the Max Planck Institute for Software Systems (MPI-SWS). She works in the Distributed Systems and Security and Privacy groups, co-advised by Peter Druschel and Deepak Garg. She is interested in designing and building privacy-preserving secure systems.
MAY
17
2023
TALK Don't be Dense: Efficient Keyword PIR for Sparse Databases
Speaker | JOON YOUNG SEO  Google Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
In this paper, we introduce SparsePIR, a single-server keyword private information retrieval (PIR) construction that enables querying over sparse databases. At its core, SparsePIR is based on a novel encoding algorithm that encodes sparse database entries as linear combinations while being compatible with important PIR optimizations including recursion. SparsePIR achieves response overhead that is half of state-of-the art keyword PIR schemes without requiring long term client storage of linear sized mappings. We also introduce two variants, SparsePIRg and SparsePIRc , that further reduces the size of the serving database at the cost of increased encoding time and small additional client storage, respectively. Our frameworks enable performing keyword PIR with, essentially, the same costs as standard PIR. Finally, we also show that SparsePIR may be used to build batch keyword PIR with halved response overhead without any client mappings.
Bio
Joon Young Seo is a senior software engineer at Google.
MAY
10
2023
TALK Oblivious Message Retrieval
Speaker | ZEYU LIU  Yale Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
Anonymous message delivery systems, such as private messaging services and privacy-preserving blockchains, need a mechanism for recipients to retrieve the messages addressed to them, without leaking metadata or letting their messages be linked. Recipients could download all posted messages and scan for those addressed to them, but communication and computation costs are excessive at scale.
We show how untrusted servers can detect messages on behalf of recipients, and summarize these into a compact encrypted digest that recipients can easily decrypt. These servers operate obliviously and do not learn anything about which messages are addressed to which recipients. Privacy, soundness, and completeness hold even if everyone but the recipient is adversarial and colluding.
Furthermore, the model and constructions generalize to the setting of group messaging or mailing lists: senders can generate messages that would be efficiently detected by multiple recipients of their choice.
Our starting point is an asymptotically-efficient approach, using Fully Homomorphic Encryption and homomorphically-encoded Sparse Random Linear Codes. We then address the concrete performance using bespoke tailoring of lattice-based cryptographic components, alongside various algebraic and algorithmic optimizations. This reduces the digest size to a few bits per message scanned. Concretely, the servers’ cost is ~$1 per million messages scanned, and the resulting digests can be decoded by recipients in ~20ms. Our schemes can thus practically attain the strongest form of receiver privacy for current applications such as privacy-preserving cryptocurrencies.
We also consider the case of group messaging, where each message may have multiple recipients (e.g., in a group chat or blockchain transaction). We devise new protocols where the servers' cost grows very slowly with the group size, while recipients' cost is low and independent of the group size.
Bio
Zeyu Liu is a first-year graduate student at Yale, advised by Ben Fisch.
MAY
03
2023
TALK Zero-Knowledge Middleboxes: Enforcing Network Policy without Sacrificing Privacy
Speaker | ZACHARY DESTEFANO  NYU Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
There is a fundamental conflict between network clients, who want to keep their traffic private, and administrators, who want to enforce a variety of policies on client traffic, using middleboxes. I'll describe a project that resolves this conflict: Zero-Knowledge Middleboxes (ZKMB). With ZKMB, clients send middleboxes zero-knowledge proofs about their encrypted traffic; these proofs reveal nothing about the underlying plaintext, except that it complies with the policy. We show how to make ZKMB work in real-time with unmodified encrypted-communication protocols (specifically TLS 1.3), making ZKMB invisible to servers. Our system gains performance by exploiting the bursty nature of web traffic and by modifying Spartan (CRYPTO '20) to amortize costs. We also show how to efficiently encode DNS filtering and complex DLP policies in zero knowledge in the ZKMB framework. Joint work with Arasu Arun, Joseph Bonneau, Paul Grubbs, Michael Walfish, Collin Zhang, and Ye Zhang.
Bio
Zachary DeStefano is a second year PhD student at NYU, advised by Michael Walfish. He has a background in computer science and mathematics, and his research is focused on the intersection of zero-knowledge proofs, systems, and formal methods.
APR
21
2023
TALK Towards private and accountable online advertising
Speaker | KE ZHONG  University of Pennsylvania Location | Stata, G449 (Patil/Kiva) Time | Friday 4pm
Abstract
Existing online advertising systems are used by billions of users every day. The current systems can be improved with several interesting properties including privacy, accountability, and anti-fraud efforts. I am going to talk about our recent works on improving the ads systems. And specifically, I will present Addax, a fast, verifiable, and private online ad exchange. When a user visits an ad-supported site, Addax runs an auction similar to those of leading exchanges; Addax requests bids, selects the winner, collects payment, and displays the ad to the user. A key distinction is that bids in Addax’s auctions are kept private and the outcome of the auction is publicly verifiable. Addax achieves these properties by adding public verifiability to the affine aggregatable encodings in Prio (NSDI’17) and by building an auction protocol out of them. Our implementation of Addax over WAN with hundreds of bidders can run roughly half the auctions per second as a non-private and non-verifiable exchange, while delivering ads to users in under 600 ms with little additional bandwidth requirements. This efficiency makes Addax the first architecture capable of bringing transparency to this otherwise opaque ecosystem.
Bio
Ke Zhong is a fourth year PhD student at UPenn, advised by Prof. Sebastian Angel.
APR
05
2023
TALK ELSA: Secure Aggregation for Federated Learning with Malicious Actors
Speaker | MAYANK RATHEE  UC Berkeley Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
Federated learning (FL) is an increasingly popular approach for machine learning (ML) when the training dataset is highly distributed. Clients perform local training on their datasets and the updates are then aggregated into the global model. Existing protocols for aggregation are either inefficient or don’t consider the case of malicious actors in the system. This is a major barrier to making FL an ideal solution for privacy-sensitive ML applications.
In this talk, I will present ELSA, a secure aggregation protocol for FL that breaks this barrier - it is efficient and addresses the existence of malicious actors (clients + servers) at the core of its design. Similar to prior work Prio and Prio+, ELSA provides a novel secure aggregation protocol built out of distributed trust across two servers that keeps individual client updates private as long as one server is honest, defends against malicious clients, and is efficient end-to-end. Compared to prior works, the distinguishing theme in ELSA is that instead of the servers generating cryptographic correlations interactively, the clients act as untrusted dealers of these correlations without compromising the protocol’s security. This leads to a much faster protocol while also achieving stronger security at that efficiency compared to prior work. We introduce new techniques that retain privacy even when a server is malicious at a small added cost of 7-25% in runtime with a negligible increase in communication over the case of a semi-honest server.
ELSA improves end-to-end runtime over prior work with similar security guarantees by big margins - single-aggregator RoFL by up to 305x (for the models we consider), and distributed-trust Prio by up to 8x (with up to 16x faster server-side protocol). Additionally, ELSA can be run in a bandwidth-saver mode for clients who are geographically bandwidth-constrained - an important property that is missing from prior works.
Based on joint work with Conghao Shen, Sameer Wagh, and Raluca Ada Popa.
Bio
Mayank is a third year PhD student at UC Berkeley, advised by Raluca Ada Popa.
MAR
15
2023
TALK What can cryptography do for decentralized mechanism design?
Speaker | KE WU  CMU Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
Recent works of Roughgarden (EC’21) and Chung and Shi (SODA’23) initiate the study of a new decentralized mechanism design problem called transaction fee mechanism design (TFM). Unlike the classical mechanism design literature, in the decentralized environment, even the auctioneer (i.e., the miner) can be a strategic player, and it can even collude with a subset of the users facilitated by binding side contracts. Chung and Shi showed two main impossibility results that rule out the existence of a dream TFM.
Besides today’s model that does not employ cryptography, we introduce a new MPC-assisted model where the TFM is implemented by a joint multi-party computation (MPC) protocol among the miners. While we show that cryptography allows us to overcome some impossibility results pertaining to the plain model, leading to non-trivial mechanisms with useful guarantees that are otherwise impossible in the plain model, it is not a panacea. We still have a zero-miner revenue limitation. To overcome this impossibility, we introduce a mildly stronger reasonable-world assumption, under which we can design mechanisms that achieve optimal miner revenue. We also systematically explore the mathematical landscape of transaction fee mechanism design under the new MPC-assisted model and demonstrate how the reasonable-world assumptions can alter the feasibility and infeasibility landscape.
Based on joint work with Elaine Shi and Hao Chung.
Bio
Ke Wu is a fourth year graduate student at CMU, advised by Elaine Shi.
MAR
08
2023
TALK A More Complete Analysis of the Signal Double Ratchet Algorithm
Speaker | ALEXANDER BIENSTOCK  NYU Location | Stata, G449 (Patil/Kiva) Time | Wed 4pm
Abstract
Seminal works by Cohn-Gordon, Cremers, Dowling, Garratt, and Stebila [EuroS&P 2017] and Alwen, Coretti and Dodis [EUROCRYPT 2019] provided the first formal frameworks for studying the widely-used Signal Double Ratchet (DR for short) algorithm.
In this work, we develop a new Universally Composable (UC) definition F_DR that we show is provably achieved by the DR protocol. Our definition captures not only the security and correctness guarantees of the DR already identified in the prior state-of-the-art analyses of Cohn-Gordon et al. and Alwen et al., but also more guarantees that are absent from one or both of these works. In particular, we construct six different modified versions of the DR protocol, all of which are insecure according to our definition F_DR, but remain secure according to one (or both) of their definitions. For example, our definition is the first to fully capture CCA-style attacks possible immediately after a compromise — attacks that, as we show, the DR protocol provably resists, but were not fully captured by prior definitions.
We additionally show that multiple compromises of a party in a short time interval, which the DR is expected to be able to withstand, as we understand from its whitepaper, nonetheless introduce a new non-trivial (albeit minor) weakness of the DR. Since the definitions in the literature (including our F_DR above) do not capture security against this more nuanced scenario, we define a new stronger definition F_TR that does.
Finally, we provide a minimalistic modification to the DR (that we call the Triple Ratchet, or TR for short) and show that the resulting protocol securely realizes the stronger functionality F_TR. Remarkably, the modification incurs no additional communication cost and virtually no additional computational cost. We also show that these techniques can be used to improve communication costs in other scenarios, e.g. practical Updatable Public Key Encryption schemes and the re-randomized TreeKEM protocol of Alwen et al. [CRYPTO 2020] for Secure Group Messaging.
Joint work with Jaiden Fairoze, Sanjam Garg, Pratyay Mukherjee, and Srinivasan Raghurama.
Bio
Alexander Bienstock is a fourth year PhD student at NYU advised by Yevgeniy Dodis.
MAR
01
2023
TALK Adaptive Risk-Limiting Audits
Speaker | ABIGAIL HARRISON  University of Connecticut Location | Stata, G882 Time | Wed 4pm
Abstract
Risk-limiting audits (RLAs) are rigorous statistical procedures meant to detect invalid election results. RLAs examine paper ballots cast during the election to statistically assess the possibility of a disagreement between the winner determined by the ballots and the winner reported by tabulation. The design of an RLA must balance risk against efficiency: “risk” refers to a bound on the chance that the audit fails to detect such a disagreement when one occurs; “efficiency” refers to the total effort to conduct the audit.
The most efficient approaches—when measured in terms of the number of ballots that must be inspected—proceed by “ballot comparison.” However, ballot comparison requires an (untrusted) declaration of the contents of each cast ballot, rather than a simple tabulation of vote totals. This “cast-vote record table” (CVR) is then spot-checked against ballots for consistency. In many practical settings, the cost of generating a suitable CVR dominates the cost of conducting the audit which has prevented widespread adoption of these sample-efficient techniques.
We introduce a new RLA procedure: an “adaptive ballot comparison” audit. In this audit, a global CVR is never produced; instead, a three-stage procedure is iterated: 1) a batch is selected, 2) a CVR is produced for that batch, and 3) a ballot within the batch is sampled, inspected by auditors, and compared with the CVR. We prove that such an audit can achieve risk commensurate with standard comparison audits while generating a fraction of the CVR. We present three main contributions: (1) a formal adversarial model for RLAs; (2) definition and analysis of an adaptive audit procedure with rigorous risk limits and an associated correctness analysis accounting for the incidental errors arising in typical audits; and (3) an analysis of efficiency.
Bio
Abigail is a graduate student at the University of Connecticut, getting her M.S. in Computer Science and Engineering. She started researching risk-limiting audits with the UConn VoTeR Center during her undergraduate years and graduated in 2022 with a B.A. in an individualized major titled "Cybersecurity, Law, & Ethics." Her interests lie in the intersection of security and law, and as such she focuses primarily on the public policy aspects of risk-limiting audits and election security.
FEB
08
2023
TALK A World Wide View of the World Wide Web
Speaker | KIMBERLY RUTH  Stanford University Location | Zoom Time | Wed 4pm
Abstract
Despite the pervasiveness of the modern web, we know surprisingly little about how people use it. In this talk, I’ll discuss two recent works aimed at understanding what web browsing looks like today, both appearing at IMC 2022. First, I’ll analyze lists of most popular websites, such as the Alexa Top Million, that are widely used in security and networking research but are not well vetted for accuracy. I’ll show that most top website lists capture web popularity poorly, with the exception of the Chrome User Experience Report dataset. Second, I’ll describe the first large-scale study of how people spend time on the web, using data from Chrome browser telemetry spanning hundreds of millions of users. I’ll explore how traffic is distributed among top websites, where people spend time on the web, and what differences we see in web browsing geographically. Finally, I’ll conclude with recommendations for how the research community can more accurately analyze the web in the future.
Bio
Kimberly Ruth is a third-year PhD student at Stanford University, advised by Zakir Durumeric.
DEC
15
2021
TALK Do You Feel a Chill? Using PIR Against Chilling Effects for Censorship-resistant Publishing
Speaker | MITI MAZMUDAR  U Waterloo Location | Zoom (contact for details) Time | Wed 4:00pm
Abstract
Peer-to-peer distributed hash tables (DHTs) rely on volunteers to contribute their computational resources, such as disk space and bandwidth. In order to incentivize these node operators of privacy-preserving DHTs, it is important to prevent exposing them to the data that is stored on the DHT and/or queried for. Vasserman et al.'s censorship-resistant publishing system, CROPS, aimed at providing plausible deniability to server nodes by encrypting stored content. However, node operators are still exposed to the contents of queries. In this talk, I will present our architecture that uses information-theoretic private information retrieval to efficiently render a server node incapable of determining what content was retrieved in a given request by a user. Our architecture can be integrated with censorship-resistant publishing systems such as CROPS. Finally, I will discuss the results of our system simulation, including the communication and performance overhead of our system over other systems without this privacy guarantee, as well as with respect to the closest related work. Our paper and code is available here: https://crysp.uwaterloo.ca/software/dhtpir/
Bio
Miti Mazmudar is a PhD student in Computer Science at the University of Waterloo, supervised by Prof. Ian Goldberg. She works at the CrySP (Cryptography, Security and Privacy) lab. Her Masters thesis research was focused on ensuring compliance of privacy policies with source code using trusted hardware platforms. Lately, she has been working on differential privacy as well as censorship-resistant publishing systems. Her PhD research topic is: integrating PETS with agile infrastructures, including purpose limitation and data minimization techniques. In general, she is interested in designing and implementing tools that help people protect their privacy.
DEC
08
2021
TALK Towards Proofs of Remote Software Execution and TOCTOU-Avoidance in Simple Embedded Systems.
Speaker | IVAN DE OLIVEIRA NUNES  RIT Location | Zoom (contact for details) Time | Wed 4:00pm
Abstract
Modern society is increasingly surrounded by, and is growing accustomed to, a wide range of Cyber-Physical Systems (CPS), Internet-of-Things (IoT), and smart devices. They often perform safety- critical functions, e.g., personal medical devices, automotive CPS as well as industrial and residential automation, e.g., sensor-alarm combinations. On the lower end of the scale, these devices are small, cheap, and specialized sensors and/or actuators. They tend to host small CPUs, have small amounts of memory, and run simple software. If such devices are left unprotected, consequences of forged sensor readings or ignored actuation commands can be catastrophic, particularly, in safety-critical settings. This prompts the following three questions: (1) How to trust data produced, or verify that commands were performed, by a simple remote embedded device?, (2) How to bind these actions/results to the execution of expected software? and, (3) Can (1) and (2) be efficiently attained even if all software on a device can be modified and/or compromised (e.g., by malware)? In this talk, I will overview two techniques that specifically target low-end microcontrollers, namely proofs of execution, and TOCTOU-avoidance. These techniques can be leveraged to assure the integrity of software and its execution, even on some of the most resource-constrained micro-controllers. In particular, I will discuss two formally verified architectures realizing the aforementioned techniques (APEX, and RATA) and how they have been securely implemented atop the TI MSP430 low-end micro-controller at a relatively low-cost.
Bio
Ivan De Oliveira Nunes is an Assistant Professor of Computing Security at the Rochester Institute of Technology (RIT). He received his Ph.D. from the University of California, Irvine (UCI) in 2021. Before UCI, he obtained a Computer Engineering degree at the Federal University of Espirito Santo (UFES), in Brazil, from 2009 to 2014. He also holds a Computer Science M.Sc. degree from the Federal University of Minas Gerais (UFMG) - Brazil (2016). In recent years, he has worked on several topics, including IoT Security, Content-Centric Networking Security, Secure Multi-Party Computation (MPC), Biometric-Based Authentication, and Opportunistic Mobile Networking. His research interests span the fields of security and privacy, embedded systems, computer networking, applied cryptography, and especially their intersection.
DEC
01
2021
TALK Swivel: Hardening WebAssembly against Spectre
Speaker | CRAIG DISSELKOEN  UCSD Location | Zoom (contact for details) Time | Wed 4:00pm
Abstract
Swivel is a new compiler framework for hardening WebAssembly (Wasm) against Spectre attacks. Wasm has become popular even outside the browser as a lightweight, in-process sandbox, used for example to isolate different clients on edge cloud platforms. Unfortunately, Spectre attacks can bypass Wasm’s isolation guarantees. Swivel hardens Wasm against these attacks, ensuring that potentially malicious code can neither break out of the Wasm sandbox nor coerce victim code to leak secret data. Swivel is joint work with 10 other authors led by Shravan Narayan.
Bio
Craig Disselkoen is a sixth-year PhD student at UC San Diego under Deian Stefan and Dean Tullsen. His research focuses on fighting memory safety vulnerabilities using techniques such as symbolic execution, secure sandboxing, and language- and compiler-based program transformations. Craig’s work has won two Distinguished Paper Awards (USENIX Security 2020 and POPL 2021), and his work on software Spectre defenses at PLDI 2020 was a finalist for the inaugural Intel Hardware Security Academic Award.
OCT
20
2021
TALK Software Update Systems: Attack and Defense
Speaker | MARINA MOORE  NYU Location | Zoom (contact for details) Time | Wed 4:00pm
Abstract
Software update systems form a critical link in the software supply chain as they provide a mechanism for software users to receive new features, security patches, and more. However, software updates themselves have been a vector of attack in many recent exploits. In this talk, Marina Moore will discuss attacks on software update systems and present The Update Framework (TUF), a framework for secure software updates designed to prevent these attacks. TUF has been used in practice by both tech companies and open source projects.
Bio
Marina Moore is a PhD candidate in the Secure Systems Lab at NYU.
OCT
06
2021
TALK Weaponizing Network Side Channels: From TCP Hijacking to DNS Cache Poisoning
Speaker | ZHIYUN QIAN  UC Riverside Location | Zoom (contact for details) Time | Wed 4:00pm
Abstract
Side channel attacks were never considered as part of the threat model when network protocols were designed. Even today, the impact of network side channels is vastly underestimated. Exploiting network side channels have been considered challenging, if not infeasible, due to its nature of being remote. In this talk, I will demonstrate a series of surprisingly powerful attacks where a blind off-path attacker can use side channels to hijack arbitrary remote TCP connections, as well as launch DNS cache poisoning attacks against popular DNS services. I will also give insights on how to systematically discover such problems.
Bio
Zhiyun Qian is the Everett and Imogene Ross associate professor in the CSE department at the University of California Riverside. His main research interests are in the area of system and network security, including vulnerability discovery, side channel analysis, applied program analysis, system building, and measurement and analysis of real-world security problems. He is a recipient of the ACM CCS distinguished paper award in 2020, Applied Networking Research Prize from IRTF in 2019, NSF CAREER Award in 2017, Facebook Internet Defense Prize Finalist in 2016, and the most creative idea award from Geekpwn 2016.
MAY
22
2019
TALK Who Watches the Watchers in Web PKI?
Speaker | KAT JOYCE  Google Location | Stata, 32-G882 (Hewlett) Time | Wed 2:00pm
Abstract
Since the dawn of time (well, Web PKI), certificates have been used to ensure that internet users are actually talking to the websites they think they are. Since the dawn of time (a.k.a. the mid-90s) Certificate Authorities have been trusted to Do The Right ThingTM when issuing these certificates, and watch out for baddies trying to get their hands on certificates for domains they don’t own. But what if a CA makes issuance mistakes? What if a CA is hacked? What if a CA is run by the baddies themselves?! Who watches the watchers?

Enter: Certificate Transparency.

Certificate Transparency is the latest internet security superhero. Power: detecting certificate misissuance and certificate authority misbehaviour (oooh yeah).

But seriously, capes and wearing-undies-over-skin-tight-lycra aside, what exactly is Certificate Transparency? How does it work? Why should you care? Is it even helping? Come along to this talk and find out!
Bio
Kat is a Software Engineer on the Trust Fabric team at Google, where she is currently focusing on building infrastructure to ensure actors within the Certificate Transparency ecosystem are operating in line with the Chrome Certificate Transparency Log Policy.

Prior to Google, Kat was a Research Engineer in the Networks and Systems research group at UCL. Kat has an MSc in Information Security from UCL, and a BSc (Hons) in Mathematics from Dalhousie University. In her spare time Kat loves to ski, swim, read, and play various musical instruments, with varying levels of success!
FEB
21
2019
TALK Microarchitectural Attacks and Beyond
Speaker | DANIEL GRUSS  Graz University of Technology Location | Stata, 32-G882 (Hewlett) Time | Thu 1:00pm
Abstract
Microarchitectural Attacks recently got a lot of attention with the publication of Meltdown and Spectre. In general, cache attacks have gained in popularity in the academic community over the past two decades. In this talk we will first discuss what architecture and microarchitecture means. We will then discuss cache attacks as a prime example of microarchitectural attacks, see how the work and how we can leak data from other processes. Then we will turn to another example on the software level where abstraction similarly enables a new form of cache attacks. The software cache that we target is a common concept implemented across various operating systems. By mounting a series of attacks we can see that this hardware-agnostic kind of cache attack can compete with state-of-the-art hardware cache attacks. Finally, we discuss mitigations for Linux and Windows.
Bio
Daniel Gruss (@lavados) is an Assistant Professor at Graz University of Technology. He finished his PhD with distinction in less than 3 years. He has been involved in teaching operating system undergraduate courses since 2010. Daniel's research focuses on software-based side-channel attacks that exploit timing differences in hardware and operating systems. He implemented the first remote fault attack running in a website, known as Rowhammer.js. He frequently speaks at top international venues, such as Black Hat, Usenix Security, IEEE S&P, ACM CCS, Chaos Communication Congress, and others. His research team was one of the teams that found the Meltdown and Spectre bugs published in early 2018.
FEB
20
2019
TALK Vault: Fast Bootstrapping for the Algorand Cryptocurrency
Speaker | DEREK LEUNG  Algorand Location | Stata, 32-G449 (Patil/Kiva) Time | Wed 2:00pm
Abstract
Decentralized cryptocurrencies rely on participants to keep track of the state of the system in order to verify new transactions. As the number of users and transactions grows, this requirement becomes a significant burden, requiring users to download, verify, and store a large amount of data to participate.
Vault is a new cryptocurrency design based on Algorand that minimizes these storage and bootstrapping costs for participants. Vault’s design is based on Algorand’s proof-of-stake consensus protocol and uses several techniques to achieve its goals. First, Vault decouples the storage of recent transactions from the storage of account balances, which enables Vault to delete old account state. Second, Vault allows sharding state across participants in a way that preserves strong security guarantees. Finally, Vault introduces the notion of stamping certificates, which allow a new client to catch up securely and efficiently in a proof- of-stake system without having to verify every single block.
Experiments with a prototype implementation of Vault’s data structures show that Vault’s design reduces the bandwidth cost of joining the network as a full client by 99.7% compared to Bitcoin and 90.5% compared to Ethereum when downloading a ledger containing 500 million transactions.
Paper URL: https://people.csail.mit.edu/nickolai/papers/leung-vault.pdf
Bio
Derek Leung is currently a software engineer at Algorand, a cryptocurrency startup. He received a M.S. in EECS from MIT in 2018 and was advised by Professor Nickolai Zeldovich. There he worked on Stadium, a scalable messaging system with strong metadata privacy guarantees. Previously he earned a B.A. in Computer Science and Mathematics from UC Berkeley in 2016. At Berkeley he worked with Professor David Wagner on usable security.
DEC
10
2018
TALK Safe passwords made easy to use
Speaker | NIKOLA K. BLANCHARD  IRIF Location | Stata, 32-G882 (Hewlett) Time | Mon 2:00pm
Abstract
How do we choose and remember our secure access codes? So far biometrics, password managers, and systems like Facebook connect have not been able to guarantee the security we need. Remembering dozens of different passwords becomes a usability nightmare. 25+ years into online experience, each of us have many hard-to-remember or easy-to-guess passwords, with all the risks and frustration they imply. We describe experiments showing how to make easy to remember codes and passwords and the system to make them, called Cue-Pin-Select. It can generate (and regenerate) passwords on the go using only the user's brain for computation. It has the advantage of creating memorable passwords, not requiring any external storage or computing device, and can be executed in less than a minute to create a new password. This talk will summarize recent usable security work done with Ted Selker. It will start with the Cue-Pin-Select algorithm, cover an improvement we found that applies to all passphrase-based security systems, and explain some of the work currently underway to have better tools to study password schemes and human computation.
Bio
Nikola K. Blanchard is a doctoral candidate at IRIF under the direction of Ted Selker and Nicolas Schabanel. After studying mathematics at ENS, he's currently pursuing research on usability of security and voting technologies, and he's been working and organizing votes with the random sample voting project for the past two years. His manuscript on the use of randomness in political institutions, "A chance for democracy", is currently being considered by publishers.
NOV
28
2018
TALK Blockchains and Trusted Execution Environments: Towards a New Security Paradigm
Speaker |  Fan Zhang Location | Stata, 32-G449 (Kiva/Patil) Time | Wed 2:00pm
Abstract
Through a decades-long endeavor of building secure, robust and performant systems, we’ve developed a rich and deep understanding of centralized computing models. However, with recent advances in the area of blockchain, a new decentralized model gives rise to even stronger security guarantees. Cryptocurrencies and smart contracts are just two examples showcasing the promises of the blockchain model of computation. Concurrently, another fundamentally different approach to achieve stronger security is trusted execution environment (TEE), which has also seen a great advance recently with the debut of Intel SGX, a CPU-based implementation of TEE.
However, despite the nice features offered by TEE and blockchain, neither is ideal. The current blockchain systems suffer from serious practical limitations, e.g. poor performance, high energy consumption and lack of confidentiality. On the other hand, TEE is imperfect in its specification and implementation, and in isolation does not offer satisfactory availability guarantees. Motivated by these practical concerns, my research focuses on understanding the principles of a hybrid model that has the best of both worlds. In this talk, I will talk about Town Crier and Ekiden, two systems we built that demonstrate the benefits of synthesizing TEE and blockchains, and the pitfalls arising from harmonizing them.
Bio
Fan Zhang is a PhD candidate in the Department of Computer Science at Cornell University. Advised by Prof. Ari Juels, Fan’s research interest is in blockchains, trusted hardware, applied cryptography. Fan is particularly interested in understanding and building hybrid systems that enjoy the best of both blockchains and trusted hardware. Fan is a member of the Initiative for Cryptocurrencies & Contracts (IC3). Before joining Cornell, Fan earned his bachelor's degree in Electronic Engineering from Tsinghua University in 2014.
OCT
17
2018
TALK Comprehensive Design Strategies for Efficient and Secure Memory
Speaker | TAMARA SILBERGLEIT  Duke University Location | Stata, 32-G882 (Hewlett) Time | Wed 2:00pm
Abstract
Distributed systems introduce a new set of security risks. When users compute on remote machines they become vulnerable to physical attacks. To protect against physical attacks, systems use secure memory, which provides confidentiality and integrity protection for data in memory. However, systems that run with secure memory, such as Intel SGX, suffer from significant delay, energy and space overheads. Our goal is to design an efficient approach to secure memory while maintaining the same security guarantees. To reduce delay overheads, we propose PoisonIvy, a safe speculation mechanism that hides the integrity verification latency while maintaining the security guarantees. To reduce energy overheads, we analyze the efficiency of a simple metadata cache and propose MCX, an improved cache design that increases the efficiency of the metadata cache by collaborating with the LLC. To improve the space overheads, we propose a dynamic allocation of secure memory metadata that makes the space overheads proportional to secure memory used. Our work effectively reduces all of these overheads making secure memory more accessible. Compared to a non-speculative secure memory design with a small metadata cache (i.e. Intel SGX), our work reduces delay overhead from 28% down to 8% and energy overhead from 55% down to 17% on average across three benchmark suites.
Bio
Tamara Silbergleit Lehman is a 6th year PhD candidate at Duke university advised by Andrew Hilton and Benjamin Lee. Her research interests lie on the intersection of computer architecture and security. She is also interested in memory systems, simulation methodologies and emerging technologies. Her thesis work focuses on reducing overheads of secure memory. Tamara has a Bachelor's degree from University of Florida in Industrial Engineering and a Masters degree in Computer Engineering from Duke University. Her latest publication on understanding metadata access patterns in secure memory at ISPASS 2018, MAPS, won the best paper award. Her earlier work on developing a safe speculation mechanism for secure memory, PoisonIvy, published in MICRO 2016 got an honorable mention in Micro Top Picks.
SEP
13
2018
TALK Foreshadow: Breaking the Virtual Memory Abstraction with Transient Out-of-Order Execution
Speaker | OFIR WEISSE  University of Michigan Location | Stata, 32-G449 (Patil/Kiva) Time | Thu 1:30pm
Abstract
Foreshadow is a speculative execution attack on Intel processors which allows an attacker to steal sensitive information stored inside personal computers or third party clouds. Foreshadow has two versions, the original attack designed to extract data from SGX enclaves and a Next-Generation version which affects Virtual Machines (VMs), hypervisors (VMM), operating system (OS) kernel memory, and System Management Mode (SMM) memory.

Foreshadow-SGX: At a high level, SGX is a new feature in modern Intel CPUs which allows computers to protect users’ data even if the entire system falls under the attacker’s control. While it was previously believed that SGX is resilient to speculative execution attacks (such as Meltdown and Spectre), Foreshadow demonstrates how speculative execution can be exploited for reading the contents of SGX-protected memory as well as extracting the machine’s private attestation key. Making things worse, due to SGX’s privacy features, an attestation report cannot be linked to the identity of its signer. Thus, it only takes a single compromised SGX machine to erode trust in the entire SGX ecosystem.

Foreshadow Next Generation: While investigating the vulnerability that causes Foreshadow, which Intel refers to as "L1 Terminal Fault", Intel identified two related attacks, which we call Foreshadow-NG. These attacks can potentially be used to read any information residing in the L1 cache, including information belonging to the System Management Mode (SMM), the Operating System's Kernel, or Hypervisor. Perhaps most devastating, Foreshadow-NG might also be used to read information stored in other virtual machines running on the same third-party cloud, presenting a risk to cloud infrastructure. Finally, in some cases, Foreshadow-NG might bypass previous mitigations against speculative execution attacks, including countermeasures to Meltdown and Spectre.

https://foreshadowattack.com
https://www.youtube.com/watch?v=ynB1inl4G3c&t=5s
https://www.youtube.com/watch?v=8ZF6kX6z7pM
Bio
Ofir is a Ph.D. candidate at the University of Michigan. His current research focuses on the feasibility of secure execution in the cloud. His recent publications include HotCalls (ISCA 2017) and WALNUT (EuroS&P 2017). Ofir worked for Intel in Haifa as a security researcher in the SGX group. He received his Master's in Computer Engineering from Tel-Aviv University and B.Sc from the Technion. His previous research focused on differential power analysis of cryptographic devices, which was published in CHES and HASP.
SEP
05
2018
TALK One File for the Price of Three: Catching Cheating Servers in Decentralized Storage Networks
Speaker | ETHAN CECCHETTI  Cornell University - Initiative for CryptoCurrencies & Contracts (IC3) Location | Stata, 32-G882 (Hewlett Room) Time | Wed 2:00pm
Abstract
Decentralized Storage Networks (DSNs) aim to store data on spare disk space owned by arbitrary strangers. These unknown computers may be unreliable or untrustworthy, so each file must be stored in redundant fashion. But how do you check that there are actually, say, three copies of the data, not three colluding servers with one copy total? This is particularly challenging when the file must be publicly readable and there is no single author (e.g., a Wikipedia article or the state of the Ethereum blockchain).

In this talk I will introduce the first provably secure, practical Public Incompressible Encoding (PIE). PIEs are a core building block needed to verify that potentially-cheating servers are redundantly storing public data.

A full copy of this work is available on the IACR ePrint Archive: https://eprint.iacr.org/2018/684.pdf
Bio
Ethan is a fourth year PhD student at Cornell University working with Ari Juels and Andrew Myers and is a member of the Initiative for CryptoCurrencies & Contracts (IC3). His work focuses on designing secure systems and building tools to ease their development. More information is available at his website.
MAY
16
2018
TALK Bringing Linux back to the BIOS with LinuxBoot
Speaker | TRAMMELL HUDSON  Two Sigma Investments Location | Stata, 32-G882 (Hewlett Room) Time | Wed 2:00pm
Abstract
The LinuxBoot projects bring Linux back to the cloud servers' boot ROMs by replacing nearly all of the vendor firmware with a reproducible built Linux runtime that acts as a fast, flexible, and measured boot loader. It has been years since any modern servers have supported Free Firmware options like LinuxBIOS or coreboot, and as a result server and cloud security has been dependent on unreviewable, closed source, proprietary vendor firmware of questionable quality. With LinuxBoot we are making it possible to take back control of our systems with Open Source Software from very early in the boot process, helping build a more trustworthy and secure cloud.
Bio
Trammell Hudson is a security researcher with Two Sigma Investments and has been focused on firmware security topics for the past few years. Previously he presented at CSAIL on Thunderstrike, the first firmware vulnerability for MacBooks, and has been collaborating with Google and Facebook, as well as the Mass Open Cloud project, to build slightly more secure cloud servers with the LinuxBoot project.
MAY
09
2018
TALK Preventing (Network) Time Travel with Chronos
Speaker | MICHAEL SCHAPIRA  Hebrew University of Jerusalem Location | Stata, 32-G882 (Hewlett Room) Time | Wed 2:00pm
Abstract
The Network Time Protocol (NTP) synchronizes time across computer systems over the Internet. Unfortunately, NTP is highly vulnerable to “time shifting attacks”, which has severe implications for time-sensitive applications and for security mechanisms. We present Chronos, a new NTP client whose design leverages ideas from distributed computing theory to achieve good synchronization even in the presence of powerful man-in-the-middle attackers. Chronos is backwards compatible with legacy NTP and involves no changes whatsoever to NTP servers. Our results indicate that to shift time at a Chronos client by over 100ms from the universal time (UTC), even powerful man-in-the-middle attackers require over 20 years of effort in expectation.

Joint work with Omer Deutsch, Neta Rozen Schiff, and Danny Dolev.
Bio
Michael Schapira is an associate professor and the co-leader of the Fraunhofer Cybersecurity Center at the Hebrew University. His research focuses on the design and analysis of (Inter)network architectures and protocols. Prior to joining Hebrew U, he worked at Google NYC's Infrastructure Networking Group and was a postdoctoral researcher at UC Berkeley, Yale University, and Princeton University. He is a recipient of the Microsoft Research Faculty Fellowship, 2 IETF/IRTF Applied Networking Research Prizes, a Google Faculty Research Award, and the ERC Starting Grant.
MAY
02
2018
TALK Sanctum: Minimal Hardware Extensions for Strong Software Isolation
Speaker | ILIA LEBEDEV  MIT CSAIL Location | Stata, 32-G882 (Hewlett Room) Time | Wed 2:00pm
Abstract
With the increasing prevalence of remote computation via cloud services and ubiquitous IoT devices, we must accept the security vulnerabilities inevitably found in these complex systems. Software systems built in practice are far too large for contemporary formal verification, as they must include all privileged software systems in the trusted computing base of any unprivileged workload. The staggering complexity of modern hardware further complicates matters, undermining simple guarantees such as process isolation.

TXT, SGX, TrustZone and similar work attempt to employ trusted hardware to construct an isolated software container and exclude some software from the TCB. While well-intentioned, these defy security analysis and present complex or vague threat models, all undermining their potential role as foundations for secure systems.

With our work (the Sanctum processor), we advocate for a transparent system with isolated containers. We offer integrity and confidentiality guarantees against a broad and straightforward threat model (a remote adversary capable of subverting arbitrary software on the system). While this work is certainly not the end-all to computer systems security, we propose a compelling threat model to inform future systems, and bootstrap one trusted platform on which secure systems may be built.
Bio
Ilia Lebedev is a PhD candidate at the Computer Science and Artificial Intelligence Lab at MIT. He works in the area of computer systems security, currently focused on bootstrapping trust for remotely attested computation. He deeply values accessible education and has received the 2016 Hazen Award for outstanding teaching. Outside of his academic career, he is a sailing ship captain, a bartender, and a generally questionable individual.
MAR
14
2018
TALK Privacy Tech in Interesting Times: Having fun with Plausibly Deniable Systems
Speaker | RADU SION  Stony Brook University Location | Stata, G449 (Patil/Kiva) Time | Wed 2:15pm
Abstract
Private or sensitive information is present on our disks, phones, watches and computers. Its protection is essential. Plausible deniability of stored data allows individuals to deny that their device contains a piece of sensitive information. This constitutes a key tool in the fight against oppressive governments and other sophisticated censorship tools. And recent developments in democratic, developed countries seems to have left plausible deniability as the last available tool in the fight for privacy and personal freedom.

In this talk we explore existing traditional plausible deniability and encryption solutions that can handle simple adversaries and then discuss emerging new research results that provide defenses against more powerful multi-snapshot state-level adversaries.

We'll also touch upon tamper-proof clouds, the future of computing, and sailing catamarans off the beaches of Stony Brook.
Bio
Radu Sion is an Associate Professor at Stony Brook University, the Director of the National Security Institute, and the CEO of Private Machines Inc.

Radu’s research is in Cyber Security and Large Scale Computing. He has published 100+ peer reviewed works in top venues, and has organized 65+ conferences. Dr. Sion has received the National Science Foundation CAREER award for his work on cloud computing security.

Radu has worked with and received funding from numerous industry and government partners, including the US Air Force, the Office of the Secretary of Defense, the Department of Homeland Security, the US Army, the Intelligence ARPA, the Office of Naval Research, Northrop Grumman, IBM, NOKIA, Motorola, Xerox Parc, Microsoft, SAP, CA Technologies, the National Science Foundation, and many others.

Radu is currently leading Private Machines Inc, a cyber security startup designing the next generation secure cloud computing technologies.
DEC
06
2017
TALK Building Secure Systems from Memory Enclaves
Speaker | SERGEY GORBUNOV  University of Waterloo Location | Stata, D463 (Star) Time | Wed 4pm
Abstract
Cloud computing has revolutionized modern IT environments, but also created a number of security challenges. For instance, a malicious infrastructure provider or a tenant can potentially see other tenants data in a public cloud.

Encrypted memory enclaves (Intel SGX) is an emerging architecture for building secure systems that can be used to protect data and programs from malicious co-tenants, operators, and even hypervisors. However, enclaves have a number of architectural limitations that make building secure systems challenging. For example, they have a small physical memory size, introduce large performance overheads, and remain vulnerable to side-channel attacks.

In this talk, I will discuss how to build secure systems from memory enclaves, addressing some of their limitations. I will present ZeroTrace an oblivious memory controller that can be used to protect applications against side-channel attacks. I will also present StealthDB an encrypted database system from Intel SGX. StealthDB has a very small trusted computing base, scales to large datasets, and provides strong security guarantees at steady state and during query execution. StealthDB is the first database that supports both analytical and transactional queries and runs on top of an unmodified DBMS engine.
Bio
Sergey is an Assistant Professor at the University of Waterloo. His interests range from cryptography to design of secure large scale systems, computer networks, protocols and blockchains. In his research he studies how to build secure systems in untrusted, distributed infrastructures. He received PhD from MIT, where he was a Microsoft PhD fellow. His academic advisor was Vinod Vaikuntanathan. His dissertation was on designing cryptographic tools for the cloud using lattice-based cryptography for which he received Sprowls Doctoral Thesis Prize for best PhD thesis in CS at MIT.
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 | Thurs 12pm
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